Theory: path

Definitions

PL_def

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

SN_def

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

drop_def

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

el_def

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

every_def

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

exists_def

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

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

finite_def

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

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_def

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

first_label_def

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

is_stopped_def

⊢ ∀p. is_stopped p ⇔ ∃x. p = stopped_at x

labels_def

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

last_thm

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

length_def

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

mem_def

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

nth_label_def

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

okpath_def

⊢ ∀R. okpath R = gfp (okpath_f R)

okpath_f_def

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

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'

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

pconcat_def

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

pcons_def

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

pgenerate_def

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

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)

pmap_def

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

seg_def

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

stopped_at_def

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

tail_def

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

trace_machine_def

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

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)

Theorems

EXISTS_path

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

FORALL_path

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

IN_PL_drop

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

LTAKE_labels

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

PL_0

⊢ ∀p. 0 ∈ PL p

PL_downward_closed

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

PL_drop

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

PL_pcons

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

PL_pmap

⊢ PL (pmap f g p) = PL p

PL_seg

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

PL_stopped_at

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

PL_take

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

PL_thm

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

SN_finite_paths

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

SN_finite_paths_EQ

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

alt_length_thm

⊢ (∀x. length (stopped_at x) = SOME 1) ∧
  ∀x r p. length (pcons x r p) = OPTION_MAP SUC (length 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)

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)

drop_eq_pcons

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

drop_not_stopped

⊢ ∀i p. SUC i ∈ PL p ⇒ ∃v r q. drop i p = pcons v r q

drop_tail_commute

⊢ ∀i p. SUC i ∈ PL p ⇒ drop i (tail p) = tail (drop i 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)

el_drop

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

el_pgenerate

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

el_pmap

⊢ ∀i p. i ∈ PL p ⇒ el i (pmap f g p) = f (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

every_el

⊢ ∀P p. every 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

exists_el

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

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

⊢ ∀P p. exists P p ⇒ every P (filter P p)

finite_drop

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

finite_labels

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

finite_last_el

⊢ ∀p. finite p ⇒ last p = el (PRE (THE (length p))) p

finite_length

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

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_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_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_paths_SN

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

finite_pconcat

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

finite_plink

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

finite_pmap

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

finite_seg

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

finite_take

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

finite_take_all

⊢ ∀p. finite p ⇒ take (PRE (THE (length p))) p = p

finite_thm

⊢ (∀x. finite (stopped_at x) ⇔ T) ∧ ∀x r p. finite (pcons x r p) ⇔ finite 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_unique

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

firstP_at_zero

⊢ ∀P p. firstP_at P p 0 ⇔ P (first 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

first_plink

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

first_pmap

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

first_seg

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

first_take

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

first_thm

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

fromPath_11

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

fromPath_onto

⊢ ∀r. ∃a. r = fromPath a

infinite_PL

⊢ ∀p. infinite p ⇒ ∀i. i ∈ PL p

infinite_path_cases

⊢ ∀p. infinite p ⇒ ∃x r q. p = pcons x r q ∧ infinite q

is_stopped_thm

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

labels_LMAP

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

labels_plink

⊢ ∀p1 p2. labels (plink p1 p2) = labels p1 ++ₗ labels p2

labels_unfold

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

last_plink

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

last_pmap

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

last_seg

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

last_take

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

length_cases

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

length_drop

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

length_never_zero

⊢ ∀p. length p ≠ SOME 0

length_pmap

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

length_take

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

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

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

not_every

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

not_exists

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

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 = l❲i❳

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)

nth_label_drop

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

nth_label_pgenerate

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

nth_label_pmap

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

nth_label_take

⊢ ∀n p i. i < n ∧ n ∈ PL p ⇒ nth_label i (take n p) = nth_label i 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)

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_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_drop

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

okpath_monotone

⊢ ∀R. monotone (okpath_f R)

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_plink

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

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_seg

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

okpath_take

⊢ ∀R p i. i ∈ PL p ∧ okpath R p ⇒ okpath R (take i 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

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)

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)

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_cases

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

path_rep_bijections_thm

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

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)

pconcat_eq_stopped

⊢ ∀p1 lab p2 x.
    pconcat p1 lab p2 ≠ stopped_at x ∧ stopped_at x ≠ pconcat p1 lab p2

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)

pcons_11

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

pgenerate_11

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

pgenerate_infinite

⊢ ∀f g. infinite (pgenerate f g)

pgenerate_not_stopped

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

pgenerate_onto

⊢ ∀p. infinite p ⇒ ∃f g. p = pgenerate f g

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)

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)

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

singleton_seg

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

stopped_at_11

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

stopped_at_not_pcons

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

tail_drop

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

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

toPath_11

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

toPath_onto

⊢ ∀a. ∃r. a = toPath r

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)

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

Theory path

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems