Theory "path"

Signature

Definitions

path_TY_DEF

|- ∃rep. TYPE_DEFINITION (λx. T) rep

path_absrep_bijections

|- (∀a. toPath (fromPath a) = a) ∧ ∀r. (λx. T) r ⇔ (fromPath (toPath r) = r)

first_def

|- ∀p. first p = FST (fromPath p)

stopped_at_def

|- ∀x. stopped_at x = toPath (x,[||])

pcons_def

|- ∀x r p. pcons x r p = toPath (x,(r,first p):::SND (fromPath p))

finite_def

|- ∀sigma. finite sigma ⇔ LFINITE (SND (fromPath sigma))

last_thm

|- (∀x. last (stopped_at x) = x) ∧ ∀x r p. last (pcons x r p) = last p

pmap_def

|- ∀f g p. pmap f g p = toPath ((f ## LMAP (g ## f)) (fromPath p))

tail_def

|- ∀x r p. tail (pcons x r p) = p

first_label_def

|- ∀x r p. first_label (pcons x r p) = r

length_def

|- ∀p.
     length p =
     if finite p then SOME (LENGTH (THE (toList (SND (fromPath p)))) + 1)
     else NONE

el_def

|- (∀p. el 0 p = first p) ∧ ∀n p. el (SUC n) p = el n (tail p)

nth_label_def

|- (∀p. nth_label 0 p = first_label p) ∧
   ∀n p. nth_label (SUC n) p = nth_label n (tail p)

pconcat_def

|- ∀p1 lab p2.
     pconcat p1 lab p2 =
     toPath
       (first p1,
        LAPPEND (SND (fromPath p1)) ((lab,first p2):::SND (fromPath p2)))

PL_def

|- ∀p. PL p = {i | finite p ⇒ i < THE (length p)}

firstP_at_def

|- ∀P p i. firstP_at P p i ⇔ i ∈ PL p ∧ P (el i p) ∧ ∀j. j < i ⇒ ¬P (el j p)

exists_def

|- ∀P p. exists P p ⇔ ∃i. firstP_at P p i

every_def

|- ∀P p. every P p ⇔ ¬exists ($~ o P) p

mem_def

|- ∀s p. mem s p ⇔ ∃i. i ∈ PL p ∧ (s = el i p)

drop_def

|- (∀p. drop 0 p = p) ∧ ∀n p. drop (SUC n) p = drop n (tail p)

take_def

|- (∀p. take 0 p = stopped_at (first p)) ∧
   ∀n p. take (SUC n) p = pcons (first p) (first_label p) (take n (tail p))

seg_def

|- ∀i j p. seg i j p = take (j − i) (drop i p)

labels_def

|- (∀x. labels (stopped_at x) = [||]) ∧
   ∀x r p. labels (pcons x r p) = r:::labels p

is_stopped_def

|- ∀p. is_stopped p ⇔ ∃x. p = stopped_at x

filter_def

|- ∀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

pgenerate_def

|- ∀f g. pgenerate f g = pcons (f 0) (g 0) (pgenerate (f o SUC) (g o SUC))

okpath_f_def

|- ∀R X.
     okpath_f R X =
     {stopped_at x | x ∈ 𝕌(:α)} ∪ {pcons x r p | R x r (first p) ∧ p ∈ X}

okpath_def

|- ∀R. okpath R = gfp (okpath_f R)

plink_def

|- (∀x p. plink (stopped_at x) p = p) ∧
   ∀x r p1 p2. plink (pcons x r p1) p2 = pcons x r (plink p1 p2)

SN_def

|- ∀R. SN R ⇔ WF (λx y. ∃l. R y l x)

unfold_def

|- ∀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)

trace_machine_def

|- ∀P s l s'. trace_machine P s l s' ⇔ P (s ++ [l]) ∧ (s' = s ++ [l])

parallel_comp_def

|- ∀m1 m2 s1 s2 l s1' s2'.
     parallel_comp m1 m2 (s1,s2) l (s1',s2') ⇔ m1 s1 l s1' ∧ m2 s2 l s2'

Theorems

path_rep_bijections_thm

|- (∀a. toPath (fromPath a) = a) ∧ ∀r. fromPath (toPath r) = r

toPath_11

|- ∀r r'. (toPath r = toPath r') ⇔ (r = r')

fromPath_11

|- ∀a a'. (fromPath a = fromPath a') ⇔ (a = a')

fromPath_onto

|- ∀r. ∃a. r = fromPath a

toPath_onto

|- ∀a. ∃r. a = toPath r

stopped_at_11

|- ∀x y. (stopped_at x = stopped_at y) ⇔ (x = y)

pcons_11

|- ∀x r p y s q. (pcons x r p = pcons y s q) ⇔ (x = y) ∧ (r = s) ∧ (p = q)

stopped_at_not_pcons

|- ∀x y r p. stopped_at x ≠ pcons y r p ∧ pcons y r p ≠ stopped_at x

path_cases

|- ∀p. (∃x. p = stopped_at x) ∨ ∃x r q. p = pcons x r q

FORALL_path

|- ∀P. (∀p. P p) ⇔ (∀x. P (stopped_at x)) ∧ ∀x r p. P (pcons x r p)

EXISTS_path

|- ∀P. (∃p. P p) ⇔ (∃x. P (stopped_at x)) ∨ ∃x r p. P (pcons x r p)

first_thm

|- (∀x. first (stopped_at x) = x) ∧ ∀x r p. first (pcons x r p) = x

finite_thm

|- (∀x. finite (stopped_at x) ⇔ T) ∧ ∀x r p. finite (pcons x r p) ⇔ finite p

path_bisimulation

|- ∀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'

finite_path_ind

|- ∀P.
     (∀x. P (stopped_at x)) ∧ (∀x r p. finite p ∧ P p ⇒ P (pcons x r p)) ⇒
     ∀q. finite q ⇒ P q

pmap_thm

|- (∀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)

first_pmap

|- ∀p. first (pmap f g p) = f (first p)

last_pmap

|- ∀p. finite p ⇒ (last (pmap f g p) = f (last p))

finite_pmap

|- ∀f g p. finite (pmap f g p) ⇔ finite p

length_thm

|- (∀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

alt_length_thm

|- (∀x. length (stopped_at x) = SOME 1) ∧
   ∀x r p. length (pcons x r p) = OPTION_MAP SUC (length p)

length_never_zero

|- ∀p. length p ≠ SOME 0

finite_length

|- ∀p. (finite p ⇔ ∃n. length p = SOME n) ∧ (¬finite p ⇔ (length p = NONE))

length_pmap

|- ∀f g p. length (pmap f g p) = length p

el_def_compute

|- (∀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)

nth_label_def_compute

|- (∀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)

path_Axiom

|- ∀f.
     ∃g.
       ∀x.
         g x =
         case f x of
           (y,NONE) => stopped_at y
         | (y,SOME (l,v)) => pcons y l (g v)

pconcat_thm

|- (∀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)

pconcat_eq_stopped

|- ∀p1 lab p2 x.
     pconcat p1 lab p2 ≠ stopped_at x ∧ stopped_at x ≠ pconcat p1 lab p2

pconcat_eq_pcons

|- ∀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))

finite_pconcat

|- ∀p1 lab p2. finite (pconcat p1 lab p2) ⇔ finite p1 ∧ finite p2

infinite_PL

|- ∀p. ¬finite p ⇒ ∀i. i ∈ PL p

PL_pcons

|- ∀x r q. PL (pcons x r q) = 0 INSERT IMAGE SUC (PL q)

PL_stopped_at

|- ∀x. PL (stopped_at x) = {0}

PL_thm

|- (∀x. PL (stopped_at x) = {0}) ∧
   ∀x r q. PL (pcons x r q) = 0 INSERT IMAGE SUC (PL q)

PL_0

|- ∀p. 0 ∈ PL p

PL_downward_closed

|- ∀i p. i ∈ PL p ⇒ ∀j. j < i ⇒ j ∈ PL p

PL_pmap

|- PL (pmap f g p) = PL p

el_pmap

|- ∀i p. i ∈ PL p ⇒ (el i (pmap f g p) = f (el i p))

nth_label_pmap

|- ∀i p. SUC i ∈ PL p ⇒ (nth_label i (pmap f g p) = g (nth_label i p))

firstP_at_thm

|- (∀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_zero

|- ∀P p. firstP_at P p 0 ⇔ P (first p)

exists_thm

|- ∀P.
     (∀x. exists P (stopped_at x) ⇔ P x) ∧
     ∀x r p. exists P (pcons x r p) ⇔ P x ∨ exists P p

every_thm

|- ∀P.
     (∀x. every P (stopped_at x) ⇔ P x) ∧
     ∀x r p. every P (pcons x r p) ⇔ P x ∧ every P p

not_every

|- ∀P p. ¬every P p ⇔ exists ($~ o P) p

not_exists

|- ∀P p. ¬exists P p ⇔ every ($~ o P) p

exists_el

|- ∀P p. exists P p ⇔ ∃i. i ∈ PL p ∧ P (el i p)

every_el

|- ∀P p. every P p ⇔ ∀i. i ∈ PL p ⇒ P (el i p)

every_coinduction

|- ∀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

exists_induction

|- (∀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

mem_thm

|- (∀x s. mem s (stopped_at x) ⇔ (s = x)) ∧
   ∀x r p s. mem s (pcons x r p) ⇔ (s = x) ∨ mem s p

drop_def_compute

|- (∀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)

numeral_drop

|- (∀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)

finite_drop

|- ∀p n. n ∈ PL p ⇒ (finite (drop n p) ⇔ finite p)

length_drop

|- ∀p n.
     n ∈ PL p ⇒
     (length (drop n p) =
      case length p of NONE => NONE | SOME m => SOME (m − n))

PL_drop

|- ∀p i. i ∈ PL p ⇒ (PL (drop i p) = IMAGE (λn. n − i) (PL p))

IN_PL_drop

|- ∀i j p. i ∈ PL p ⇒ (j ∈ PL (drop i p) ⇔ i + j ∈ PL p)

first_drop

|- ∀i p. i ∈ PL p ⇒ (first (drop i p) = el i p)

first_label_drop

|- ∀i p. i ∈ PL p ⇒ (first_label (drop i p) = nth_label i p)

tail_drop

|- ∀i p. i + 1 ∈ PL p ⇒ (tail (drop i p) = drop (i + 1) p)

el_drop

|- ∀i j p. i + j ∈ PL p ⇒ (el i (drop j p) = el (i + j) p)

nth_label_drop

|- ∀i j p. SUC (i + j) ∈ PL p ⇒ (nth_label i (drop j p) = nth_label (i + j) p)

take_def_compute

|- (∀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))

first_take

|- ∀p i. first (take i p) = first p

finite_take

|- ∀p i. i ∈ PL p ⇒ finite (take i p)

length_take

|- ∀p i. i ∈ PL p ⇒ (length (take i p) = SOME (i + 1))

PL_take

|- ∀p i. i ∈ PL p ⇒ (PL (take i p) = {n | n ≤ i})

last_take

|- ∀i p. i ∈ PL p ⇒ (last (take i p) = el i p)

nth_label_take

|- ∀n p i. i < n ∧ n ∈ PL p ⇒ (nth_label i (take n p) = nth_label i p)

singleton_seg

|- ∀i p. i ∈ PL p ⇒ (seg i i p = stopped_at (el i p))

recursive_seg

|- ∀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))

PL_seg

|- ∀i j p. i ≤ j ∧ j ∈ PL p ⇒ (PL (seg i j p) = {n | n ≤ j − i})

finite_seg

|- ∀p i j. i ≤ j ∧ j ∈ PL p ⇒ finite (seg i j p)

first_seg

|- ∀i j p. i ≤ j ∧ j ∈ PL p ⇒ (first (seg i j p) = el i p)

last_seg

|- ∀i j p. i ≤ j ∧ j ∈ PL p ⇒ (last (seg i j p) = el j p)

firstP_at_unique

|- ∀P p n. firstP_at P p n ⇒ ∀m. firstP_at P p m ⇔ (m = n)

is_stopped_thm

|- (∀x. is_stopped (stopped_at x) ⇔ T) ∧ ∀x r p. is_stopped (pcons x r p) ⇔ F

filter_every

|- ∀P p. exists P p ⇒ every P (filter P p)

pgenerate_infinite

|- ∀f g. ¬finite (pgenerate f g)

pgenerate_not_stopped

|- ∀f g x. stopped_at x ≠ pgenerate f g

el_pgenerate

|- ∀n f g. el n (pgenerate f g) = f n

nth_label_pgenerate

|- ∀n f g. nth_label n (pgenerate f g) = g n

pgenerate_11

|- ∀f1 g1 f2 g2. (pgenerate f1 g1 = pgenerate f2 g2) ⇔ (f1 = f2) ∧ (g1 = g2)

pgenerate_onto

|- ∀p. ¬finite p ⇒ ∃f g. p = pgenerate f g

okpath_monotone

|- ∀R. monotone (okpath_f R)

okpath_co_ind

|- ∀P.
     (∀x r p. P (pcons x r p) ⇒ R x r (first p) ∧ P p) ⇒ ∀p. P p ⇒ okpath R p

okpath_cases

|- ∀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_thm

|- ∀R.
     (∀x. okpath R (stopped_at x)) ∧
     ∀x r p. okpath R (pcons x r p) ⇔ R x r (first p) ∧ okpath R p

finite_okpath_ind

|- ∀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

okpath_pmap

|- ∀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)

finite_plink

|- ∀p1 p2. finite (plink p1 p2) ⇔ finite p1 ∧ finite p2

first_plink

|- ∀p1 p2. (last p1 = first p2) ⇒ (first (plink p1 p2) = first p1)

last_plink

|- ∀p1 p2.
     finite p1 ∧ finite p2 ∧ (last p1 = first p2) ⇒
     (last (plink p1 p2) = last p2)

okpath_plink

|- ∀R p1 p2.
     finite p1 ∧ (last p1 = first p2) ⇒
     (okpath R (plink p1 p2) ⇔ okpath R p1 ∧ okpath R p2)

okpath_take

|- ∀R p i. i ∈ PL p ∧ okpath R p ⇒ okpath R (take i p)

okpath_drop

|- ∀R p i. i ∈ PL p ∧ okpath R p ⇒ okpath R (drop i p)

okpath_seg

|- ∀R p i j. i ≤ j ∧ j ∈ PL p ∧ okpath R p ⇒ okpath R (seg i j p)

SN_finite_paths

|- ∀R p. SN R ∧ okpath R p ⇒ finite p

finite_paths_SN

|- ∀R. (∀p. okpath R p ⇒ finite p) ⇒ SN R

SN_finite_paths_EQ

|- ∀R. SN R ⇔ ∀p. okpath R p ⇒ finite p

labels_LMAP

|- ∀p. labels p = LMAP FST (SND (fromPath p))

labels_plink

|- ∀p1 p2. labels (plink p1 p2) = LAPPEND (labels p1) (labels p2)

finite_labels

|- ∀p. LFINITE (labels p) ⇔ finite p

unfold_thm

|- ∀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

|- ∀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)))

labels_unfold

|- ∀proj f s. labels (unfold proj f s) = LUNFOLD f s

okpath_unfold

|- ∀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)

trace_machine_thm

|- ∀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

|- ∀n l P p init.
     okpath (trace_machine P) p ∧ P (first p) ⇒
     (LTAKE n (labels p) = SOME l) ⇒
     P (first p ++ l)

LTAKE_labels

|- ∀n p l.
     (LTAKE n (labels p) = SOME l) ⇔
     n ∈ PL p ∧ (toList (labels (take n p)) = SOME l)

drop_eq_pcons

|- ∀n p h l t. n ∈ PL p ∧ (drop n p = pcons h l t) ⇒ n + 1 ∈ PL p

okpath_parallel_comp

|- ∀p m1 m2.
     okpath (parallel_comp m1 m2) p ⇔
     okpath m1 (pmap FST (λx. x) p) ∧ okpath m2 (pmap SND (λx. x) p)

build_pcomp_trace

|- ∀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))

nth_label_LNTH

|- ∀n p x. (LNTH n (labels p) = SOME x) ⇔ n + 1 ∈ PL p ∧ (nth_label n p = x)

nth_label_LTAKE

|- ∀n p l i v.
     (LTAKE n (labels p) = SOME l) ∧ i < LENGTH l ⇒ (nth_label i p = EL i l)

finite_path_end_cases

|- ∀p.
     finite p ⇒
     (∃x. p = stopped_at x) ∨
     ∃p' l s. p = plink p' (pcons (last p') l (stopped_at s))

simulation_trace_inclusion

|- ∀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)