signature pathTheory = sig type thm = Thm.thm (* Definitions *) val PL_def : thm val SN_def : thm val drop_def : thm val el_def : thm val every_def : thm val exists_def : thm val filter_def : thm val finite_def : thm val firstP_at_def : thm val first_def : thm val first_label_def : thm val is_stopped_def : thm val labels_def : thm val last_thm : thm val length_def : thm val mem_def : thm val nth_label_def : thm val okpath_def : thm val okpath_f_def : thm val path_TY_DEF : thm val path_absrep_bijections : thm val pconcat_def : thm val pcons_def : thm val pgenerate_def : thm val plink_def : thm val pmap_def : thm val seg_def : thm val stopped_at_def : thm val tail_def : thm val take_def : thm (* Theorems *) val FORALL_path : thm val IN_PL_drop : thm val PL_0 : thm val PL_downward_closed : thm val PL_drop : thm val PL_pcons : thm val PL_pmap : thm val PL_seg : thm val PL_stopped_at : thm val PL_take : thm val PL_thm : thm val SN_finite_paths : thm val SN_finite_paths_EQ : thm val alt_length_thm : thm val el_drop : thm val el_pgenerate : thm val el_pmap : thm val every_coinduction : thm val every_el : thm val every_thm : thm val exists_el : thm val exists_induction : thm val exists_thm : thm val filter_every : thm val finite_drop : thm val finite_length : thm val finite_okpath_ind : thm val finite_path_ind : thm val finite_paths_SN : thm val finite_pconcat : thm val finite_plink : thm val finite_pmap : thm val finite_seg : thm val finite_take : thm val finite_thm : thm val firstP_at_thm : thm val firstP_at_unique : thm val firstP_at_zero : thm val first_drop : thm val first_label_drop : thm val first_plink : thm val first_pmap : thm val first_seg : thm val first_take : thm val first_thm : thm val fromPath_11 : thm val fromPath_onto : thm val infinite_PL : thm val is_stopped_thm : thm val last_plink : thm val last_pmap : thm val last_seg : thm val last_take : thm val length_drop : thm val length_never_zero : thm val length_pmap : thm val length_take : thm val length_thm : thm val mem_thm : thm val not_every : thm val not_exists : thm val nth_label_drop : thm val nth_label_pgenerate : thm val nth_label_pmap : thm val numeral_drop : thm val okpath_cases : thm val okpath_co_ind : thm val okpath_drop : thm val okpath_monotone : thm val okpath_plink : thm val okpath_pmap : thm val okpath_seg : thm val okpath_take : thm val okpath_thm : thm val path_Axiom : thm val path_bisimulation : thm val path_cases : thm val path_rep_bijections_thm : thm val pconcat_eq_pcons : thm val pconcat_eq_stopped : thm val pconcat_thm : thm val pcons_11 : thm val pgenerate_11 : thm val pgenerate_infinite : thm val pgenerate_not_stopped : thm val pgenerate_onto : thm val pmap_thm : thm val recursive_seg : thm val singleton_seg : thm val stopped_at_11 : thm val stopped_at_not_pcons : thm val tail_drop : thm val toPath_11 : thm val toPath_onto : thm val path_grammars : type_grammar.grammar * term_grammar.grammar val path_rwts : simpLib.ssdata (* [fixedPoint] Parent theory of "path" [llist] Parent theory of "path" [PL_def] Definition |- ∀p. PL p = {i | finite p ⇒ i < THE (length p)} [SN_def] Definition |- ∀R. SN R = WF (\x y. ∃l. R y l x) [drop_def] Definition |- (∀p. drop 0 p = p) ∧ ∀n p. drop (SUC n) p = drop n (tail p) [el_def] Definition |- (∀p. el 0 p = first p) ∧ ∀n p. el (SUC n) p = el n (tail p) [every_def] Definition |- ∀P p. every P p = ¬exists ($~ o P) p [exists_def] Definition |- ∀P p. exists P p = ∃i. firstP_at P p i [filter_def] Definition |- ∀P. (∀x. P x ⇒ (filter P (stopped_at x) = stopped_at x)) ∧ ∀x r p. filter P (pcons x r p) = (if P x then (if exists P p then pcons x r (filter P p) else stopped_at x) else filter P p) [finite_def] Definition |- ∀sigma. finite sigma = LFINITE (SND (fromPath sigma)) [firstP_at_def] Definition |- ∀P p i. firstP_at P p i = i ∈ PL p ∧ P (el i p) ∧ ∀j. j < i ⇒ ¬P (el j p) [first_def] Definition |- ∀p. first p = FST (fromPath p) [first_label_def] Definition |- ∀x r p. first_label (pcons x r p) = r [is_stopped_def] Definition |- ∀p. is_stopped p = ∃x. p = stopped_at x [labels_def] Definition |- (∀x. labels (stopped_at x) = LNIL) ∧ ∀x r p. labels (pcons x r p) = LCONS r (labels p) [last_thm] Definition |- (∀x. last (stopped_at x) = x) ∧ ∀x r p. last (pcons x r p) = last p [length_def] Definition |- ∀p. length p = (if finite p then SOME (LENGTH (THE (toList (SND (fromPath p)))) + 1) else NONE) [mem_def] Definition |- ∀s p. mem s p = ∃i. i ∈ PL p ∧ (s = el i p) [nth_label_def] Definition |- (∀p. nth_label 0 p = first_label p) ∧ ∀n p. nth_label (SUC n) p = nth_label n (tail p) [okpath_def] Definition |- ∀R. okpath R = gfp (okpath_f R) [okpath_f_def] Definition |- ∀R X. okpath_f R X = {stopped_at x | x ∈ UNIV} ∪ {pcons x r p | R x r (first p) ∧ p ∈ X} [path_TY_DEF] Definition |- ∃rep. TYPE_DEFINITION (\x. T) rep [path_absrep_bijections] Definition |- (∀a. toPath (fromPath a) = a) ∧ ∀r. (\x. T) r = (fromPath (toPath r) = r) [pconcat_def] Definition |- ∀p1 lab p2. pconcat p1 lab p2 = toPath (first p1, LAPPEND (SND (fromPath p1)) (LCONS (lab,first p2) (SND (fromPath p2)))) [pcons_def] Definition |- ∀x r p. pcons x r p = toPath (x,LCONS (r,first p) (SND (fromPath p))) [pgenerate_def] Definition |- ∀f g. pgenerate f g = pcons (f 0) (g 0) (pgenerate (f o SUC) (g o SUC)) [plink_def] Definition |- (∀x p. plink (stopped_at x) p = p) ∧ ∀x r p1 p2. plink (pcons x r p1) p2 = pcons x r (plink p1 p2) [pmap_def] Definition |- ∀f g p. pmap f g p = toPath ((f ## LMAP (g ## f)) (fromPath p)) [seg_def] Definition |- ∀i j p. seg i j p = take (j - i) (drop i p) [stopped_at_def] Definition |- ∀x. stopped_at x = toPath (x,LNIL) [tail_def] Definition |- ∀x r p. tail (pcons x r p) = p [take_def] Definition |- (∀p. take 0 p = stopped_at (first p)) ∧ ∀n p. take (SUC n) p = pcons (first p) (first_label p) (take n (tail p)) [FORALL_path] Theorem |- ∀P. (∀p. P p) = (∀x. P (stopped_at x)) ∧ ∀x r p. P (pcons x r p) [IN_PL_drop] Theorem |- ∀i j p. i ∈ PL p ⇒ (j ∈ PL (drop i p) = i + j ∈ PL p) [PL_0] Theorem |- ∀p. 0 ∈ PL p [PL_downward_closed] Theorem |- ∀i p. i ∈ PL p ⇒ ∀j. j < i ⇒ j ∈ PL p [PL_drop] Theorem |- ∀p i. i ∈ PL p ⇒ (PL (drop i p) = IMAGE (\n. n - i) (PL p)) [PL_pcons] Theorem |- ∀x r q. PL (pcons x r q) = 0 INSERT IMAGE SUC (PL q) [PL_pmap] Theorem |- PL (pmap f g p) = PL p [PL_seg] Theorem |- ∀i j p. i ≤ j ∧ j ∈ PL p ⇒ (PL (seg i j p) = {n | n ≤ j - i}) [PL_stopped_at] Theorem |- ∀x. PL (stopped_at x) = {0} [PL_take] Theorem |- ∀p i. i ∈ PL p ⇒ (PL (take i p) = {n | n ≤ i}) [PL_thm] Theorem |- (∀x. PL (stopped_at x) = {0}) ∧ ∀x r q. PL (pcons x r q) = 0 INSERT IMAGE SUC (PL q) [SN_finite_paths] Theorem |- ∀R p. SN R ∧ okpath R p ⇒ finite p [SN_finite_paths_EQ] Theorem |- ∀R. SN R = ∀p. okpath R p ⇒ finite p [alt_length_thm] Theorem |- (∀x. length (stopped_at x) = SOME 1) ∧ ∀x r p. length (pcons x r p) = OPTION_MAP SUC (length p) [el_drop] Theorem |- ∀i j p. i + j ∈ PL p ⇒ (el i (drop j p) = el (i + j) p) [el_pgenerate] Theorem |- ∀n f g. el n (pgenerate f g) = f n [el_pmap] Theorem |- ∀i p. i ∈ PL p ⇒ (el i (pmap f g p) = f (el i p)) [every_coinduction] Theorem |- ∀P Q. (∀x. P (stopped_at x) ⇒ Q x) ∧ (∀x r p. P (pcons x r p) ⇒ Q x ∧ P p) ⇒ ∀p. P p ⇒ every Q p [every_el] Theorem |- ∀P p. every P p = ∀i. i ∈ PL p ⇒ P (el i p) [every_thm] Theorem |- ∀P. (∀x. every P (stopped_at x) = P x) ∧ ∀x r p. every P (pcons x r p) = P x ∧ every P p [exists_el] Theorem |- ∀P p. exists P p = ∃i. i ∈ PL p ∧ P (el i p) [exists_induction] Theorem |- (∀x. Q x ⇒ P (stopped_at x)) ∧ (∀x r p. Q x ⇒ P (pcons x r p)) ∧ (∀x r p. P p ⇒ P (pcons x r p)) ⇒ ∀p. exists Q p ⇒ P p [exists_thm] Theorem |- ∀P. (∀x. exists P (stopped_at x) = P x) ∧ ∀x r p. exists P (pcons x r p) = P x ∨ exists P p [filter_every] Theorem |- ∀P p. exists P p ⇒ every P (filter P p) [finite_drop] Theorem |- ∀p n. n ∈ PL p ⇒ (finite (drop n p) = finite p) [finite_length] Theorem |- ∀p. (finite p = ∃n. length p = SOME n) ∧ (¬finite p = (length p = NONE)) [finite_okpath_ind] Theorem |- ∀R. (∀x. P (stopped_at x)) ∧ (∀x r p. okpath R p ∧ finite p ∧ R x r (first p) ∧ P p ⇒ P (pcons x r p)) ⇒ ∀sigma. okpath R sigma ∧ finite sigma ⇒ P sigma [finite_path_ind] Theorem |- ∀P. (∀x. P (stopped_at x)) ∧ (∀x r p. finite p ∧ P p ⇒ P (pcons x r p)) ⇒ ∀q. finite q ⇒ P q [finite_paths_SN] Theorem |- ∀R. (∀p. okpath R p ⇒ finite p) ⇒ SN R [finite_pconcat] Theorem |- ∀p1 lab p2. finite (pconcat p1 lab p2) = finite p1 ∧ finite p2 [finite_plink] Theorem |- ∀p1 p2. finite (plink p1 p2) = finite p1 ∧ finite p2 [finite_pmap] Theorem |- ∀f g p. finite (pmap f g p) = finite p [finite_seg] Theorem |- ∀p i j. i ≤ j ∧ j ∈ PL p ⇒ finite (seg i j p) [finite_take] Theorem |- ∀p i. i ∈ PL p ⇒ finite (take i p) [finite_thm] Theorem |- (∀x. finite (stopped_at x) = T) ∧ ∀x r p. finite (pcons x r p) = finite p [firstP_at_thm] Theorem |- (∀P x n. firstP_at P (stopped_at x) n = (n = 0) ∧ P x) ∧ ∀P n x r p. firstP_at P (pcons x r p) n = (n = 0) ∧ P x ∨ 0 < n ∧ ¬P x ∧ firstP_at P p (n - 1) [firstP_at_unique] Theorem |- ∀P p n. firstP_at P p n ⇒ ∀m. firstP_at P p m = (m = n) [firstP_at_zero] Theorem |- ∀P p. firstP_at P p 0 = P (first p) [first_drop] Theorem |- ∀i p. i ∈ PL p ⇒ (first (drop i p) = el i p) [first_label_drop] Theorem |- ∀i p. i ∈ PL p ⇒ (first_label (drop i p) = nth_label i p) [first_plink] Theorem |- ∀p1 p2. (last p1 = first p2) ⇒ (first (plink p1 p2) = first p1) [first_pmap] Theorem |- ∀p. first (pmap f g p) = f (first p) [first_seg] Theorem |- ∀i j p. i ≤ j ∧ j ∈ PL p ⇒ (first (seg i j p) = el i p) [first_take] Theorem |- ∀p i. first (take i p) = first p [first_thm] Theorem |- (∀x. first (stopped_at x) = x) ∧ ∀x r p. first (pcons x r p) = x [fromPath_11] Theorem |- ∀a a'. (fromPath a = fromPath a') = (a = a') [fromPath_onto] Theorem |- ∀r. ∃a. r = fromPath a [infinite_PL] Theorem |- ∀p. ¬finite p ⇒ ∀i. i ∈ PL p [is_stopped_thm] Theorem |- (∀x. is_stopped (stopped_at x) = T) ∧ ∀x r p. is_stopped (pcons x r p) = F [last_plink] Theorem |- ∀p1 p2. finite p1 ∧ finite p2 ∧ (last p1 = first p2) ⇒ (last (plink p1 p2) = last p2) [last_pmap] Theorem |- ∀p. finite p ⇒ (last (pmap f g p) = f (last p)) [last_seg] Theorem |- ∀i j p. i ≤ j ∧ j ∈ PL p ⇒ (last (seg i j p) = el j p) [last_take] Theorem |- ∀i p. i ∈ PL p ⇒ (last (take i p) = el i p) [length_drop] Theorem |- ∀p n. n ∈ PL p ⇒ (length (drop n p) = case length p of NONE -> NONE || SOME v -> SOME (v - n)) [length_never_zero] Theorem |- ∀p. ¬(length p = SOME 0) [length_pmap] Theorem |- ∀f g p. length (pmap f g p) = length p [length_take] Theorem |- ∀p i. i ∈ PL p ⇒ (length (take i p) = SOME (i + 1)) [length_thm] Theorem |- (∀x. length (stopped_at x) = SOME 1) ∧ ∀x r p. length (pcons x r p) = (if finite p then SOME (THE (length p) + 1) else NONE) [mem_thm] Theorem |- (∀x s. mem s (stopped_at x) = (s = x)) ∧ ∀x r p s. mem s (pcons x r p) = (s = x) ∨ mem s p [not_every] Theorem |- ∀P p. ¬every P p = exists ($~ o P) p [not_exists] Theorem |- ∀P p. ¬exists P p = every ($~ o P) p [nth_label_drop] Theorem |- ∀i j p. SUC (i + j) ∈ PL p ⇒ (nth_label i (drop j p) = nth_label (i + j) p) [nth_label_pgenerate] Theorem |- ∀n f g. nth_label n (pgenerate f g) = g n [nth_label_pmap] Theorem |- ∀i p. SUC i ∈ PL p ⇒ (nth_label i (pmap f g p) = g (nth_label i p)) [numeral_drop] Theorem |- (∀n p. drop (NUMERAL (BIT1 n)) p = drop (NUMERAL (BIT1 n) - 1) (tail p)) ∧ ∀n p. drop (NUMERAL (BIT2 n)) p = drop (NUMERAL (BIT1 n)) (tail p) [okpath_cases] Theorem |- ∀R x. okpath R x = (∃x'. x = stopped_at x') ∨ ∃x' r p. (x = pcons x' r p) ∧ R x' r (first p) ∧ okpath R p [okpath_co_ind] Theorem |- ∀R P. (∀x. P x ⇒ (∃x'. x = stopped_at x') ∨ ∃x' r p. (x = pcons x' r p) ∧ R x' r (first p) ∧ P p) ⇒ ∀x. P x ⇒ okpath R x [okpath_drop] Theorem |- ∀R p i. i ∈ PL p ∧ okpath R p ⇒ okpath R (drop i p) [okpath_monotone] Theorem |- ∀R. monotone (okpath_f R) [okpath_plink] Theorem |- ∀R p1 p2. finite p1 ∧ (last p1 = first p2) ⇒ (okpath R (plink p1 p2) = okpath R p1 ∧ okpath R p2) [okpath_pmap] Theorem |- ∀R f g p. okpath R p ∧ (∀x r y. R x r y ⇒ R (f x) (g r) (f y)) ⇒ okpath R (pmap f g p) [okpath_seg] Theorem |- ∀R p i j. i ≤ j ∧ j ∈ PL p ∧ okpath R p ⇒ okpath R (seg i j p) [okpath_take] Theorem |- ∀R p i. i ∈ PL p ∧ okpath R p ⇒ okpath R (take i p) [okpath_thm] Theorem |- ∀R. (∀x. okpath R (stopped_at x)) ∧ ∀x r p. okpath R (pcons x r p) = R x r (first p) ∧ okpath R p [path_Axiom] Theorem |- ∀f. ∃g. ∀x. g x = case f x of (v1,v2) -> case v2 of NONE -> stopped_at v1 || SOME v3 -> case v3 of (v4,v5) -> pcons v1 v4 (g v5) [path_bisimulation] Theorem |- ∀p1 p2. (p1 = p2) = ∃R. R p1 p2 ∧ ∀q1 q2. R q1 q2 ⇒ (∃x. (q1 = stopped_at x) ∧ (q2 = stopped_at x)) ∨ ∃x r q1' q2'. (q1 = pcons x r q1') ∧ (q2 = pcons x r q2') ∧ R q1' q2' [path_cases] Theorem |- ∀p. (∃x. p = stopped_at x) ∨ ∃x r q. p = pcons x r q [path_rep_bijections_thm] Theorem |- (∀a. toPath (fromPath a) = a) ∧ ∀r. fromPath (toPath r) = r [pconcat_eq_pcons] Theorem |- ∀x r p p1 lab p2. ((pconcat p1 lab p2 = pcons x r p) = (lab = r) ∧ (p1 = stopped_at x) ∧ (p = p2) ∨ ∃p1'. (p1 = pcons x r p1') ∧ (p = pconcat p1' lab p2)) ∧ ((pcons x r p = pconcat p1 lab p2) = (lab = r) ∧ (p1 = stopped_at x) ∧ (p = p2) ∨ ∃p1'. (p1 = pcons x r p1') ∧ (p = pconcat p1' lab p2)) [pconcat_eq_stopped] Theorem |- ∀p1 lab p2 x. ¬(pconcat p1 lab p2 = stopped_at x) ∧ ¬(stopped_at x = pconcat p1 lab p2) [pconcat_thm] Theorem |- (∀x lab p2. pconcat (stopped_at x) lab p2 = pcons x lab p2) ∧ ∀x r p lab p2. pconcat (pcons x r p) lab p2 = pcons x r (pconcat p lab p2) [pcons_11] Theorem |- ∀x r p y s q. (pcons x r p = pcons y s q) = (x = y) ∧ (r = s) ∧ (p = q) [pgenerate_11] Theorem |- ∀f1 g1 f2 g2. (pgenerate f1 g1 = pgenerate f2 g2) = (f1 = f2) ∧ (g1 = g2) [pgenerate_infinite] Theorem |- ∀f g. ¬finite (pgenerate f g) [pgenerate_not_stopped] Theorem |- ∀f g x. ¬(stopped_at x = pgenerate f g) [pgenerate_onto] Theorem |- ∀p. ¬finite p ⇒ ∃f g. p = pgenerate f g [pmap_thm] Theorem |- (∀x. pmap f g (stopped_at x) = stopped_at (f x)) ∧ ∀x r p. pmap f g (pcons x r p) = pcons (f x) (g r) (pmap f g p) [recursive_seg] Theorem |- ∀i j p. i < j ∧ j ∈ PL p ⇒ (seg i j p = pcons (el i p) (nth_label i p) (seg (i + 1) j p)) [singleton_seg] Theorem |- ∀i p. i ∈ PL p ⇒ (seg i i p = stopped_at (el i p)) [stopped_at_11] Theorem |- ∀x y. (stopped_at x = stopped_at y) = (x = y) [stopped_at_not_pcons] Theorem |- ∀x y r p. ¬(stopped_at x = pcons y r p) ∧ ¬(pcons y r p = stopped_at x) [tail_drop] Theorem |- ∀i p. i + 1 ∈ PL p ⇒ (tail (drop i p) = drop (i + 1) p) [toPath_11] Theorem |- ∀r r'. (toPath r = toPath r') = (r = r') [toPath_onto] Theorem |- ∀a. ∃r. a = toPath r *) end