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 ($~ ∘ 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 ∘ SUC) (g ∘ 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 ($~ ∘ P) p

not_exists

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