Theory "path"

Parents fixedPoint llist

Signature

Type	Arity
path	2
Constant	Type
toPath	:'a # ('b # 'a) llist -> ('a, 'b) path
take	:num -> ('a, 'b) path -> ('a, 'b) path
tail	:('a, 'b) path -> ('a, 'b) path
stopped_at	:'a -> ('a, 'b) path
seg	:num -> num -> ('a, 'b) path -> ('a, 'b) path
pmap	:('a -> 'c) -> ('b -> 'd) -> ('a, 'b) path -> ('c, 'd) path
plink	:('a, 'b) path -> ('a, 'b) path -> ('a, 'b) path
pgenerate	:(num -> 'a) -> (num -> 'b) -> ('a, 'b) path
pcons	:'a -> 'b -> ('a, 'b) path -> ('a, 'b) path
pconcat	:('a, 'b) path -> 'b -> ('a, 'b) path -> ('a, 'b) path
okpath_f	:('a -> 'b -> 'a -> bool) -> (('a, 'b) path -> bool) -> ('a, 'b) path -> bool
okpath	:('a -> 'b -> 'a -> bool) -> ('a, 'b) path -> bool
nth_label	:num -> ('b, 'a) path -> 'a
mem	:'a -> ('a, 'b) path -> bool
length	:('a, 'b) path -> num option
last	:('a, 'b) path -> 'a
labels	:('a, 'b) path -> 'b llist
is_stopped	:('a, 'b) path -> bool
fromPath	:('a, 'b) path -> 'a # ('b # 'a) llist
first_label	:('a, 'b) path -> 'b
firstP_at	:('a -> bool) -> ('a, 'b) path -> num -> bool
first	:('a, 'b) path -> 'a
finite	:('a, 'b) path -> bool
filter	:('a -> bool) -> ('a, 'b) path -> ('a, 'b) path
exists	:('a -> bool) -> ('a, 'b) path -> bool
every	:('a -> bool) -> ('a, 'b) path -> bool
el	:num -> ('a, 'b) path -> 'a
drop	:num -> ('a, 'b) path -> ('a, 'b) path
SN	:('a -> 'b -> 'a -> bool) -> bool
PL	:('a, 'b) path -> num -> bool

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 IN 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 IN 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 IN UNIV} UNION
     {pcons x r p | R x r (first p) /\ p IN 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)

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)

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

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 IN 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 IN PL p

PL_downward_closed

|- !i p. i IN PL p ==> !j. j < i ==> j IN PL p

PL_pmap

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

el_pmap

|- !i p. i IN PL p ==> (el i (pmap f g p) = f (el i p))

nth_label_pmap

|- !i p. SUC i IN 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 IN PL p /\ P (el i p)

every_el

|- !P p. every P p = !i. i IN 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

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 IN PL p ==> (finite (drop n p) = finite p)

length_drop

|- !p n.
     n IN PL p ==>
     (length (drop n p) =
      case length p of NONE -> NONE || SOME m -> SOME (m - n))

PL_drop

|- !p i. i IN PL p ==> (PL (drop i p) = IMAGE (\n. n - i) (PL p))

IN_PL_drop

|- !i j p. i IN PL p ==> (j IN PL (drop i p) = i + j IN PL p)

first_drop

|- !i p. i IN PL p ==> (first (drop i p) = el i p)

first_label_drop

|- !i p. i IN PL p ==> (first_label (drop i p) = nth_label i p)

tail_drop

|- !i p. i + 1 IN PL p ==> (tail (drop i p) = drop (i + 1) p)

el_drop

|- !i j p. i + j IN PL p ==> (el i (drop j p) = el (i + j) p)

nth_label_drop

|- !i j p.
     SUC (i + j) IN PL p ==> (nth_label i (drop j p) = nth_label (i + j) p)

first_take

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

finite_take

|- !p i. i IN PL p ==> finite (take i p)

length_take

|- !p i. i IN PL p ==> (length (take i p) = SOME (i + 1))

PL_take

|- !p i. i IN PL p ==> (PL (take i p) = {n | n <= i})

last_take

|- !i p. i IN PL p ==> (last (take i p) = el i p)

singleton_seg

|- !i p. i IN PL p ==> (seg i i p = stopped_at (el i p))

recursive_seg

|- !i j p.
     i < j /\ j IN 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 IN PL p ==> (PL (seg i j p) = {n | n <= j - i})

finite_seg

|- !p i j. i <= j /\ j IN PL p ==> finite (seg i j p)

first_seg

|- !i j p. i <= j /\ j IN PL p ==> (first (seg i j p) = el i p)

last_seg

|- !i j p. i <= j /\ j IN 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

|- !R P.
     (!x.
        P x ==>
        (?x'. x = stopped_at x') \/
        ?x' r p. (x = pcons x' r p) /\ R x' r (first p) /\ P p) ==>
     !x. P x ==> okpath R x

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 IN PL p /\ okpath R p ==> okpath R (take i p)

okpath_drop

|- !R p i. i IN PL p /\ okpath R p ==> okpath R (drop i p)

okpath_seg

|- !R p i j. i <= j /\ j IN 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