src/coalgebras/pathScript.sml

54 val first_def = Define`first (p:('a,'b) path) = FST (fromPath p)`;
58                       toPath (x, LCONS (r, first p) (SND (fromPath p)))`;
105   ``(!x. first (stopped_at x : ('a,'b) path) = x) /\
106     (!x r p. first (pcons x r p : ('a,'b) path) = x)``,
126                             if SND (fromPath p) = LNIL then first p
154                                   (first p = first q)` THEN
183          ?r q1' q2'. (ll3 = LCONS (r, first q1') (SND (fromPath q1'))) /\
184                      (ll4 = LCONS (r, first q2') (SND (fromPath q2'))) /\
233   ``!p. first (pmap f g p) = f (first p)``,
361   (el 0 p = first p) /\ (el (SUC n) p = el n (tail p))
420              toPath (first p1, LAPPEND (SND (fromPath p1))
421                                        (LCONS (lab,first p2)
577   ``!P p. firstP_at P p 0 = P (first p)``,
732   ``!i p. i IN PL p ==> (first (drop i p) = el i p)``,
785   (take 0 p = stopped_at (first p)) /\
786   (take (SUC n) p = pcons (first p) (first_label p) (take n (tail p)))
792   ``!p i. first (take i p) = first p``,
904   ``!i j p. i <= j /\ j IN PL p ==> (first (seg i j p) = el i p)``,
976                                (first r,
1101               { pcons x r p | R x r (first p) /\ p IN X }`;
1142       (!x r p. okpath R (pcons x r p) <=> R x r (first p) /\ okpath R p)
1154         (!x r p. okpath R p /\ finite p /\ R x r (first p) /\ P p ==>
1181         (Q.ISPEC `\pair. let pullapart g p = (first p,
1234   ``!p1 p2. (last p1 = first p2) ==> (first (plink p1 p2) = first p1)``,
1241   ``!p1 p2. finite p1 /\ finite p2 /\ (last p1 = first p2) ==>
1244                        !p2. finite p2 /\ (last p1 = first p2) ==>
1252   !R p1 p2. finite p1 /\ (last p1 = first p2) ==>
1258               !p2. (last p1 = first p2) ==>
1297   Q_TAC SUFF_TAC `!x p. (x = first p) /\ okpath R p ==> finite p`
1424   (!x r p. P (pcons x r p) ==> R x r (first p) /\ P p) /\ P p ==> okpath R p`,
1482     ?p. (tr = labels p) /\ okpath (trace_machine P) p /\ (first p = [])`,
1530     P (first p)
1532     ((LTAKE n (labels p) = SOME l) ==> P (first p ++ l))`,
1617            Cases_on `first t` THEN
1639            Cases_on `first t` THEN
1656            Cases_on `first p'` THEN
1677        (first p = (first p1, first p2))`,
1679  Q.EXISTS_TAC `unfold (��(p1,p2). (first p1, first p2))
1774    R (first p) t_init
1776    ?q. okpath M2 q /\ (labels p = labels q) /\ (first q = t_init)`,
1786                                        next_t (first p)
1788                                               (first (tail p)) t),
1793      Q.EXISTS_TAC `��(p',t_init'). okpath M1 p' /\ R (first p') t_init'` THEN