Theory "path"

Signature

Definitions

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

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

tail_def

⊢ ∀x r p. tail (pcons x r p) = p

stopped_at_def

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

SN_def

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

seg_def

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

pmap_def

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

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)

PL_def

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

pgenerate_def

⊢ ∀f g. pgenerate f g = pcons (f 0) (g 0) (pgenerate (f ∘ SUC) (g ∘ SUC))

pcons_def

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

pconcat_def

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

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)

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'

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)

nth_label_def

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

mem_def

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

length_def

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

last_thm

⊢ (∀x. last (stopped_at x) = x) ∧ ∀x r p. last (pcons x r p) = last 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

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)

first_label_def

⊢ ∀x r p. first_label (pcons x r p) = r

first_def

⊢ ∀p. first p = FST (fromPath p)

finite_def

⊢ ∀sigma. finite sigma ⇔ LFINITE (SND (fromPath sigma))

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

exists_def

⊢ ∀P p. exists P p ⇔ ∃i. firstP_at P p i

every_def

⊢ ∀P p. every P p ⇔ ¬exists ($~ ∘ P) p

el_def

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

drop_def

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

Theorems

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

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

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)

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 = [])

toPath_onto

⊢ ∀a. ∃r. a = toPath r

toPath_11

⊢ ∀r r'. (toPath r = toPath r') ⇔ (r = r')

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

tail_drop

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

stopped_at_not_pcons

⊢ ∀x y r p. stopped_at x ≠ pcons y r p ∧ pcons y r p ≠ stopped_at x

stopped_at_11

⊢ ∀x y. (stopped_at x = stopped_at y) ⇔ (x = y)

SN_finite_paths_EQ

⊢ ∀R. SN R ⇔ ∀p. okpath R p ⇒ finite p

SN_finite_paths

⊢ ∀R p. SN R ∧ okpath R p ⇒ finite p

singleton_seg

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

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)

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

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)

PL_thm

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

PL_take

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

PL_stopped_at

⊢ ∀x. PL (stopped_at x) = {0}

PL_seg

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

PL_pmap

⊢ PL (pmap f g p) = PL p

PL_pcons

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

PL_drop

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

PL_downward_closed

⊢ ∀i p. i ∈ PL p ⇒ ∀j. j < i ⇒ j ∈ PL p

PL_0

⊢ ∀p. 0 ∈ PL p

pgenerate_onto

⊢ ∀p. ¬finite p ⇒ ∃f g. p = pgenerate f g

pgenerate_not_stopped

⊢ ∀f g x. stopped_at x ≠ pgenerate f g

pgenerate_infinite

⊢ ∀f g. ¬finite (pgenerate f g)

pgenerate_11

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

pcons_11

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

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

path_rep_bijections_thm

⊢ (∀a. toPath (fromPath a) = a) ∧ ∀r. fromPath (toPath r) = r

path_cases

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

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'

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)

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)

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

okpath_take

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

okpath_seg

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

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)

okpath_plink

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

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)

okpath_monotone

⊢ ∀R. monotone (okpath_f R)

okpath_drop

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

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

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)

nth_label_take

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

nth_label_pmap

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

nth_label_pgenerate

⊢ ∀n f g. nth_label n (pgenerate f g) = g n

nth_label_LTAKE

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

nth_label_LNTH

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

nth_label_drop

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

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

not_exists

⊢ ∀P p. ¬exists P p ⇔ every ($~ ∘ P) p

not_every

⊢ ∀P p. ¬every P p ⇔ exists ($~ ∘ 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

LTAKE_labels

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

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

length_take

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

length_pmap

⊢ ∀f g p. length (pmap f g p) = length p

length_never_zero

⊢ ∀p. length p ≠ SOME 0

length_drop

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

last_take

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

last_seg

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

last_pmap

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

last_plink

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

labels_unfold

⊢ ∀proj f s. labels (unfold proj f s) = LUNFOLD f s

labels_plink

⊢ ∀p1 p2. labels (plink p1 p2) = LAPPEND (labels p1) (labels p2)

labels_LMAP

⊢ ∀p. labels p = LMAP FST (SND (fromPath p))

is_stopped_thm

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

infinite_PL

⊢ ∀p. ¬finite p ⇒ ∀i. i ∈ PL p

IN_PL_drop

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

fromPath_onto

⊢ ∀r. ∃a. r = fromPath a

fromPath_11

⊢ ∀a a'. (fromPath a = fromPath a') ⇔ (a = a')

FORALL_path

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

firstP_at_zero

⊢ ∀P p. firstP_at P p 0 ⇔ P (first p)

firstP_at_unique

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

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)

first_thm

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

first_take

⊢ ∀p i. first (take i p) = first p

first_seg

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

first_pmap

⊢ ∀p. first (pmap f g p) = f (first p)

first_plink

⊢ ∀p1 p2. (last p1 = first p2) ⇒ (first (plink p1 p2) = first p1)

first_label_drop

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

first_drop

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

finite_thm

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

finite_take

⊢ ∀p i. i ∈ PL p ⇒ finite (take i p)

finite_seg

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

finite_pmap

⊢ ∀f g p. finite (pmap f g p) ⇔ finite p

finite_plink

⊢ ∀p1 p2. finite (plink p1 p2) ⇔ finite p1 ∧ finite p2

finite_pconcat

⊢ ∀p1 lab p2. finite (pconcat p1 lab p2) ⇔ finite p1 ∧ finite p2

finite_paths_SN

⊢ ∀R. (∀p. okpath R p ⇒ finite p) ⇒ SN R

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

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

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

finite_length

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

finite_labels

⊢ ∀p. LFINITE (labels p) ⇔ finite p

finite_drop

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

filter_every

⊢ ∀P p. exists P p ⇒ every P (filter P 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

EXISTS_path

⊢ ∀P. (∃p. P p) ⇔ (∃x. P (stopped_at x)) ∨ ∃x r p. P (pcons x r 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

exists_el

⊢ ∀P p. exists P p ⇔ ∃i. i ∈ PL p ∧ P (el i 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

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

el_pmap

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

el_pgenerate

⊢ ∀n f g. el n (pgenerate f g) = f n

el_drop

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

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

drop_eq_pcons

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

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

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

alt_length_thm

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