Structure pathTheory


Source File Identifier index Theory binding index

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 parallel_comp_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
    val trace_machine_def : thm
    val unfold_def : thm
  
  (*  Theorems  *)
    val EXISTS_path : thm
    val FORALL_path : thm
    val IN_PL_drop : thm
    val LTAKE_labels : 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 build_pcomp_trace : thm
    val drop_compute : thm
    val drop_eq_pcons : thm
    val el_compute : 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_labels : thm
    val finite_length : thm
    val finite_okpath_ind : thm
    val finite_path_end_cases : 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 labels_LMAP : thm
    val labels_plink : thm
    val labels_unfold : 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_LNTH : thm
    val nth_label_LTAKE : thm
    val nth_label_compute : thm
    val nth_label_drop : thm
    val nth_label_pgenerate : thm
    val nth_label_pmap : thm
    val nth_label_take : thm
    val numeral_drop : thm
    val okpath_cases : thm
    val okpath_co_ind : thm
    val okpath_drop : thm
    val okpath_monotone : thm
    val okpath_parallel_comp : thm
    val okpath_plink : thm
    val okpath_pmap : thm
    val okpath_seg : thm
    val okpath_take : thm
    val okpath_thm : thm
    val okpath_unfold : 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 simulation_trace_inclusion : thm
    val singleton_seg : thm
    val stopped_at_11 : thm
    val stopped_at_not_pcons : thm
    val tail_drop : thm
    val take_compute : thm
    val toPath_11 : thm
    val toPath_onto : thm
    val trace_machine_thm : thm
    val trace_machine_thm2 : thm
    val unfold_thm : thm
    val unfold_thm2 : thm
  
  val path_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [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 ($~ ∘ 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) = [||]) ∧
        ∀x r p. labels (pcons x r p) = 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 ∈ 𝕌(:α)} ∪
            {pcons x r p | R x r (first p) ∧ p ∈ X}
   
   [parallel_comp_def]  Definition
      
      ⊢ ∀m1 m2 s1 s2 l s1' s2'.
            parallel_comp m1 m2 (s1,s2) l (s1',s2') ⇔
            m1 s1 l s1' ∧ m2 s2 l s2'
   
   [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))
                 ((lab,first p2):::SND (fromPath p2)))
   
   [pcons_def]  Definition
      
      ⊢ ∀x r p. pcons x r p = toPath (x,(r,first p):::SND (fromPath p))
   
   [pgenerate_def]  Definition
      
      ⊢ ∀f g.
            pgenerate f g =
            pcons (f 0) (g 0) (pgenerate (f ∘ SUC) (g ∘ 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,[||])
   
   [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))
   
   [trace_machine_def]  Definition
      
      ⊢ ∀P s l s'. trace_machine P s l s' ⇔ P (s ++ [l]) ∧ s' = s ++ [l]
   
   [unfold_def]  Definition
      
      ⊢ ∀proj f s.
            unfold proj f s =
            toPath
              (proj s,
               LUNFOLD
                 (λs.
                      OPTION_MAP (λ(next_s,lbl). (next_s,lbl,proj next_s))
                        (f s)) s)
   
   [EXISTS_path]  Theorem
      
      ⊢ ∀P. (∃p. P p) ⇔ (∃x. P (stopped_at x)) ∨ ∃x r p. P (pcons x r 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)
   
   [LTAKE_labels]  Theorem
      
      ⊢ ∀n p l.
            LTAKE n (labels p) = SOME l ⇔
            n ∈ PL p ∧ toList (labels (take n p)) = SOME l
   
   [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)
   
   [build_pcomp_trace]  Theorem
      
      ⊢ ∀m1 p1 m2 p2.
            okpath m1 p1 ∧ okpath m2 p2 ∧ labels p1 = labels p2 ⇒
            ∃p.
                okpath (parallel_comp m1 m2) p ∧ labels p = labels p1 ∧
                first p = (first p1,first p2)
   
   [drop_compute]  Theorem
      
      ⊢ (∀p. drop 0 p = p) ∧
        (∀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)
   
   [drop_eq_pcons]  Theorem
      
      ⊢ ∀n p h l t. n ∈ PL p ∧ drop n p = pcons h l t ⇒ n + 1 ∈ PL p
   
   [el_compute]  Theorem
      
      ⊢ (∀p. el 0 p = first p) ∧
        (∀n p. el (NUMERAL (BIT1 n)) p = el (NUMERAL (BIT1 n) − 1) (tail p)) ∧
        ∀n p. el (NUMERAL (BIT2 n)) p = el (NUMERAL (BIT1 n)) (tail 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_labels]  Theorem
      
      ⊢ ∀p. LFINITE (labels 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_end_cases]  Theorem
      
      ⊢ ∀p.
            finite p ⇒
            (∃x. p = stopped_at x) ∨
            ∃p' l s. p = plink p' (pcons (last p') l (stopped_at s))
   
   [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
   
   [labels_LMAP]  Theorem
      
      ⊢ ∀p. labels p = LMAP FST (SND (fromPath p))
   
   [labels_plink]  Theorem
      
      ⊢ ∀p1 p2. labels (plink p1 p2) = LAPPEND (labels p1) (labels p2)
   
   [labels_unfold]  Theorem
      
      ⊢ ∀proj f s. labels (unfold proj f s) = LUNFOLD f s
   
   [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 m => SOME (m − 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 ($~ ∘ P) p
   
   [not_exists]  Theorem
      
      ⊢ ∀P p. ¬exists P p ⇔ every ($~ ∘ P) p
   
   [nth_label_LNTH]  Theorem
      
      ⊢ ∀n p x.
            LNTH n (labels p) = SOME x ⇔ n + 1 ∈ PL p ∧ nth_label n p = x
   
   [nth_label_LTAKE]  Theorem
      
      ⊢ ∀n p l i v.
            LTAKE n (labels p) = SOME l ∧ i < LENGTH l ⇒
            nth_label i p = EL i l
   
   [nth_label_compute]  Theorem
      
      ⊢ (∀p. nth_label 0 p = first_label p) ∧
        (∀n p.
             nth_label (NUMERAL (BIT1 n)) p =
             nth_label (NUMERAL (BIT1 n) − 1) (tail p)) ∧
        ∀n p.
            nth_label (NUMERAL (BIT2 n)) p =
            nth_label (NUMERAL (BIT1 n)) (tail 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)
   
   [nth_label_take]  Theorem
      
      ⊢ ∀n p i. i < n ∧ n ∈ PL p ⇒ nth_label i (take n p) = 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
      
      ⊢ ∀P.
            (∀x r p. P (pcons x r p) ⇒ R x r (first p) ∧ P p) ⇒
            ∀p. P p ⇒ okpath R p
   
   [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_parallel_comp]  Theorem
      
      ⊢ ∀p m1 m2.
            okpath (parallel_comp m1 m2) p ⇔
            okpath m1 (pmap FST (λx. x) p) ∧ okpath m2 (pmap SND (λx. x) p)
   
   [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
   
   [okpath_unfold]  Theorem
      
      ⊢ ∀P m proj f s.
            P s ∧ (∀s s' l. P s ∧ f s = SOME (s',l) ⇒ P s') ∧
            (∀s s' l. P s ∧ f s = SOME (s',l) ⇒ m (proj s) l (proj s')) ⇒
            okpath m (unfold proj f s)
   
   [path_Axiom]  Theorem
      
      ⊢ ∀f.
            ∃g.
                ∀x.
                    g x =
                    case f x of
                      (y,NONE) => stopped_at y
                    | (y,SOME (l,v)) => pcons y l (g v)
   
   [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)
   
   [simulation_trace_inclusion]  Theorem
      
      ⊢ ∀R M1 M2 p t_init.
            (∀s1 l s2 t1. R s1 t1 ∧ M1 s1 l s2 ⇒ ∃t2. R s2 t2 ∧ M2 t1 l t2) ∧
            okpath M1 p ∧ R (first p) t_init ⇒
            ∃q. okpath M2 q ∧ labels p = labels q ∧ first q = t_init
   
   [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
   
   [take_compute]  Theorem
      
      ⊢ (∀p. take 0 p = stopped_at (first p)) ∧
        (∀n p.
             take (NUMERAL (BIT1 n)) p =
             pcons (first p) (first_label p)
               (take (NUMERAL (BIT1 n) − 1) (tail p))) ∧
        ∀n p.
            take (NUMERAL (BIT2 n)) p =
            pcons (first p) (first_label p)
              (take (NUMERAL (BIT1 n)) (tail p))
   
   [toPath_11]  Theorem
      
      ⊢ ∀r r'. toPath r = toPath r' ⇔ r = r'
   
   [toPath_onto]  Theorem
      
      ⊢ ∀a. ∃r. a = toPath r
   
   [trace_machine_thm]  Theorem
      
      ⊢ ∀P tr.
            (∀n l. LTAKE n tr = SOME l ⇒ P l) ⇒
            ∃p. tr = labels p ∧ okpath (trace_machine P) p ∧ first p = []
   
   [trace_machine_thm2]  Theorem
      
      ⊢ ∀n l P p init.
            okpath (trace_machine P) p ∧ P (first p) ⇒
            LTAKE n (labels p) = SOME l ⇒
            P (first p ++ l)
   
   [unfold_thm]  Theorem
      
      ⊢ ∀proj f s.
            unfold proj f s =
            case f s of
              NONE => stopped_at (proj s)
            | SOME (s',l) => pcons (proj s) l (unfold proj f s')
   
   [unfold_thm2]  Theorem
      
      ⊢ ∀proj f x v1 v2.
            (f x = NONE ⇒ unfold proj f x = stopped_at (proj x)) ∧
            (f x = SOME (v1,v2) ⇒
             unfold proj f x = pcons (proj x) v2 (unfold proj f v1))
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13