Structure itreeTauTheory
signature itreeTauTheory =
sig
type thm = Thm.thm
(* Definitions *)
val itree_TY_DEF : thm
val itree_bind_def : thm
val itree_el_case_def : thm
val itree_el_size_def : thm
val itree_iter_def : thm
val itree_loop_def : thm
val itree_next_case_def : thm
val itree_next_size_def : thm
val untau_def : thm
(* Theorems *)
val Ret_11 : thm
val Tau_11 : thm
val Vis_11 : thm
val datatype_itree : thm
val datatype_itree_el : thm
val datatype_itree_next : thm
val itree_11 : thm
val itree_CASE : thm
val itree_CASE_cong : thm
val itree_CASE_elim : thm
val itree_CASE_eq : thm
val itree_bind_assoc : thm
val itree_bind_resp_k_wbisim : thm
val itree_bind_resp_t_wbisim : thm
val itree_bind_resp_wbisim : thm
val itree_bind_right_identity : thm
val itree_bind_strip_tau_wbisim : thm
val itree_bind_thm : thm
val itree_bind_vis_strip_tau : thm
val itree_bisimulation : thm
val itree_cases : thm
val itree_distinct : thm
val itree_el_11 : thm
val itree_el_Axiom : thm
val itree_el_case_cong : thm
val itree_el_case_eq : thm
val itree_el_def : thm
val itree_el_distinct : thm
val itree_el_eqv : thm
val itree_el_ind : thm
val itree_el_induction : thm
val itree_el_nchotomy : thm
val itree_el_thm : thm
val itree_iter_resp_wbisim : thm
val itree_iter_thm : thm
val itree_next_11 : thm
val itree_next_Axiom : thm
val itree_next_case_cong : thm
val itree_next_case_eq : thm
val itree_next_distinct : thm
val itree_next_induction : thm
val itree_next_nchotomy : thm
val itree_strong_bisimulation : thm
val itree_unfold : thm
val itree_wbisim_cases : thm
val itree_wbisim_coind : thm
val itree_wbisim_coind_upto : thm
val itree_wbisim_refl : thm
val itree_wbisim_rules : thm
val itree_wbisim_strip_tau : thm
val itree_wbisim_strip_tau_Ret : thm
val itree_wbisim_strip_tau_Vis : thm
val itree_wbisim_strip_tau_sym : thm
val itree_wbisim_strong_coind : thm
val itree_wbisim_sym : thm
val itree_wbisim_tau : thm
val itree_wbisim_tau_eq : thm
val itree_wbisim_tau_eqn : thm
val itree_wbisim_trans : thm
val spin : thm
val spin_strip_tau : thm
val strip_tau_cases : thm
val strip_tau_ind : thm
val strip_tau_inj : thm
val strip_tau_rules : thm
val strip_tau_simps : thm
val strip_tau_simps2 : thm
val strip_tau_simps3 : thm
val strip_tau_spin : thm
val strip_tau_strongind : thm
val untau_IMP_wbisim : thm
val untau_spin : thm
val wbisim_IMP_untau : thm
val itreeTau_grammars : type_grammar.grammar * term_grammar.grammar
(*
[alist] Parent theory of "itreeTau"
[itree] Parent theory of "itreeTau"
[llist] Parent theory of "itreeTau"
[itree_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION itree_rep_ok rep
[itree_bind_def] Definition
⊢ ∀t k.
itree_bind t k =
itree_unfold
(λx.
case x of
INL (Ret r) =>
(case k r of
Ret s => Ret' s
| Tau t => Tau' (INR t)
| Vis e g => Vis' e (INR ∘ g))
| INL (Tau t) => Tau' (INL t)
| INL (Vis e g) => Vis' e (INL ∘ g)
| INR (Ret r') => Ret' r'
| INR (Tau t') => Tau' (INR t')
| INR (Vis e' g') => Vis' e' (INR ∘ g')) (INL t)
[itree_el_case_def] Definition
⊢ (∀a f f1 v. itree_el_CASE (Event a) f f1 v = f a) ∧
(∀a f f1 v. itree_el_CASE (Return a) f f1 v = f1 a) ∧
∀f f1 v. itree_el_CASE Silence f f1 v = v
[itree_el_size_def] Definition
⊢ (∀f f1 a. itree_el_size f f1 (Event a) = 1 + f a) ∧
(∀f f1 a. itree_el_size f f1 (Return a) = 1 + f1 a) ∧
∀f f1. itree_el_size f f1 Silence = 0
[itree_iter_def] Definition
⊢ ∀body seed.
itree_iter body seed =
itree_unfold
(λx.
case x of
Ret (INL seed') => Tau' (body seed')
| Ret (INR v) => Ret' v
| Tau u => Tau' u
| Vis e g => Vis' e g) (body seed)
[itree_loop_def] Definition
⊢ ∀body seed.
itree_loop body seed =
itree_iter
(λx.
itree_bind (body x)
(λcb.
case cb of
INL c => Ret (INL (INL c))
| INR b => Ret (INR b))) (INR seed)
[itree_next_case_def] Definition
⊢ (∀a f f1 f2. itree_next_CASE (Ret' a) f f1 f2 = f a) ∧
(∀a f f1 f2. itree_next_CASE (Tau' a) f f1 f2 = f1 a) ∧
∀a0 a1 f f1 f2. itree_next_CASE (Vis' a0 a1) f f1 f2 = f2 a0 a1
[itree_next_size_def] Definition
⊢ (∀f f1 f2 f3 a. itree_next_size f f1 f2 f3 (Ret' a) = 1 + f2 a) ∧
(∀f f1 f2 f3 a. itree_next_size f f1 f2 f3 (Tau' a) = 1 + f3 a) ∧
∀f f1 f2 f3 a0 a1.
itree_next_size f f1 f2 f3 (Vis' a0 a1) = 1 + f1 a0
[untau_def] Definition
⊢ untau =
itree_unfold
(λt.
case some t'. strip_tau t t' of
NONE => Div'
| SOME (Ret v) => Ret' v
| SOME (Tau t') => Div'
| SOME (Vis e k) => Vis' e k)
[Ret_11] Theorem
⊢ ∀x y. Ret x = Ret y ⇔ x = y
[Tau_11] Theorem
⊢ ∀x y. Tau x = Tau y ⇔ x = y
[Vis_11] Theorem
⊢ ∀x f y g. Vis x f = Vis y g ⇔ x = y ∧ f = g
[datatype_itree] Theorem
⊢ DATATYPE (itree Ret Tau Vis)
[datatype_itree_el] Theorem
⊢ DATATYPE (itree_el Event Return Silence)
[datatype_itree_next] Theorem
⊢ DATATYPE (itree_next Ret' Tau' Vis')
[itree_11] Theorem
⊢ (∀x y. Ret x = Ret y ⇔ x = y) ∧ (∀x y. Tau x = Tau y ⇔ x = y) ∧
∀x f y g. Vis x f = Vis y g ⇔ x = y ∧ f = g
[itree_CASE] Theorem
⊢ itree_CASE (Ret r) ret tau vis = ret r ∧
itree_CASE (Tau t) ret tau vis = tau t ∧
itree_CASE (Vis a g) ret tau vis = vis a g
[itree_CASE_cong] Theorem
⊢ ∀M M' ret tau vis ret' tau' vis'.
M = M' ∧ (∀x. M' = Ret x ⇒ ret x = ret' x) ∧
(∀t. M' = Tau t ⇒ tau t = tau' t) ∧
(∀a g. M' = Vis a g ⇒ vis a g = vis' a g) ⇒
itree_CASE M ret tau vis = itree_CASE M' ret' tau' vis'
[itree_CASE_elim] Theorem
⊢ ∀f. f (itree_CASE t ret tau vis) ⇔
(∃r. t = Ret r ∧ f (ret r)) ∨ (∃u. t = Tau u ∧ f (tau u)) ∨
∃a g. t = Vis a g ∧ f (vis a g)
[itree_CASE_eq] Theorem
⊢ itree_CASE t ret tau vis = v ⇔
(∃r. t = Ret r ∧ ret r = v) ∨ (∃u. t = Tau u ∧ tau u = v) ∨
∃a g. t = Vis a g ∧ vis a g = v
[itree_bind_assoc] Theorem
⊢ itree_bind (itree_bind t k) k' =
itree_bind t (λx. itree_bind (k x) k')
[itree_bind_resp_k_wbisim] Theorem
⊢ ∀t k1 k2.
(∀r. itree_wbisim (k1 r) (k2 r)) ⇒
itree_wbisim (itree_bind t k1) (itree_bind t k2)
[itree_bind_resp_t_wbisim] Theorem
⊢ ∀a b k.
itree_wbisim a b ⇒ itree_wbisim (itree_bind a k) (itree_bind b k)
[itree_bind_resp_wbisim] Theorem
⊢ ∀a b k1 k2.
itree_wbisim a b ∧ (∀r. itree_wbisim (k1 r) (k2 r)) ⇒
itree_wbisim (itree_bind a k1) (itree_bind b k2)
[itree_bind_right_identity] Theorem
⊢ itree_bind t Ret = t
[itree_bind_strip_tau_wbisim] Theorem
⊢ ∀u u' k.
strip_tau u u' ⇒ itree_wbisim (itree_bind u k) (itree_bind u' k)
[itree_bind_thm] Theorem
⊢ itree_bind (Ret r) k = k r ∧
itree_bind (Tau t) k = Tau (itree_bind t k) ∧
itree_bind (Vis e k') k = Vis e (λx. itree_bind (k' x) k)
[itree_bind_vis_strip_tau] Theorem
⊢ ∀u k k' e.
strip_tau u (Vis e k') ⇒
strip_tau (itree_bind u k) (Vis e (λx. itree_bind (k' x) k))
[itree_bisimulation] Theorem
⊢ ∀t1 t2.
t1 = t2 ⇔
∃R. R t1 t2 ∧ (∀x t. R (Ret x) t ⇒ t = Ret x) ∧
(∀u t. R (Tau u) t ⇒ ∃v. t = Tau v ∧ R u v) ∧
∀a f t. R (Vis a f) t ⇒ ∃g. t = Vis a g ∧ ∀s. R (f s) (g s)
[itree_cases] Theorem
⊢ ∀t. (∃x. t = Ret x) ∨ (∃u. t = Tau u) ∨ ∃a g. t = Vis a g
[itree_distinct] Theorem
⊢ Ret x ≠ Tau t ∧ Ret x ≠ Vis e g ∧ Tau t ≠ Vis e g
[itree_el_11] Theorem
⊢ (∀a a'. Event a = Event a' ⇔ a = a') ∧
∀a a'. Return a = Return a' ⇔ a = a'
[itree_el_Axiom] Theorem
⊢ ∀f0 f1 f2. ∃fn.
(∀a. fn (Event a) = f0 a) ∧ (∀a. fn (Return a) = f1 a) ∧
fn Silence = f2
[itree_el_case_cong] Theorem
⊢ ∀M M' f f1 v.
M = M' ∧ (∀a. M' = Event a ⇒ f a = f' a) ∧
(∀a. M' = Return a ⇒ f1 a = f1' a) ∧ (M' = Silence ⇒ v = v') ⇒
itree_el_CASE M f f1 v = itree_el_CASE M' f' f1' v'
[itree_el_case_eq] Theorem
⊢ itree_el_CASE x f f1 v = v' ⇔
(∃e. x = Event e ∧ f e = v') ∨ (∃r. x = Return r ∧ f1 r = v') ∨
x = Silence ∧ v = v'
[itree_el_def] Theorem
⊢ (∀t. itree_el t [] =
case t of
Ret r => Return r
| Tau t => Silence
| Vis e g => Event e) ∧
(∀t ns.
itree_el t (NONE::ns) =
case t of
Ret r => Silence
| Tau t' => itree_el t' ns
| Vis e g => Silence) ∧
∀t ns a.
itree_el t (SOME a::ns) =
case t of
Ret r => Silence
| Tau t => Silence
| Vis e g => itree_el (g a) ns
[itree_el_distinct] Theorem
⊢ (∀a' a. Event a ≠ Return a') ∧ (∀a. Event a ≠ Silence) ∧
∀a. Return a ≠ Silence
[itree_el_eqv] Theorem
⊢ ∀t1 t2. t1 = t2 ⇔ ∀path. itree_el t1 path = itree_el t2 path
[itree_el_ind] Theorem
⊢ ∀P. (∀t. P t []) ∧ (∀t ns. (∀t'. P t' ns) ⇒ P t (NONE::ns)) ∧
(∀t a ns. (∀g. P (g a) ns) ⇒ P t (SOME a::ns)) ⇒
∀v v1. P v v1
[itree_el_induction] Theorem
⊢ ∀P. (∀e. P (Event e)) ∧ (∀r. P (Return r)) ∧ P Silence ⇒ ∀i. P i
[itree_el_nchotomy] Theorem
⊢ ∀ii. (∃e. ii = Event e) ∨ (∃r. ii = Return r) ∨ ii = Silence
[itree_el_thm] Theorem
⊢ itree_el (Ret r) [] = Return r ∧ itree_el (Tau t) [] = Silence ∧
itree_el (Vis e g) [] = Event e ∧
itree_el (Ret r) (NONE::ns) = Silence ∧
itree_el (Tau t) (NONE::ns) = itree_el t ns ∧
itree_el (Vis e g) (NONE::ns) = Silence ∧
itree_el (Ret r) (SOME a::ns) = Silence ∧
itree_el (Tau t) (SOME a::ns) = Silence ∧
itree_el (Vis e g) (SOME a::ns) = itree_el (g a) ns
[itree_iter_resp_wbisim] Theorem
⊢ ∀t k1 k2.
(∀r. itree_wbisim (k1 r) (k2 r)) ⇒
itree_wbisim (itree_iter k1 t) (itree_iter k2 t)
[itree_iter_thm] Theorem
⊢ itree_iter body seed =
itree_bind (body seed)
(λx. case x of INL a => Tau (itree_iter body a) | INR b => Ret b)
[itree_next_11] Theorem
⊢ (∀a a'. Ret' a = Ret' a' ⇔ a = a') ∧
(∀a a'. Tau' a = Tau' a' ⇔ a = a') ∧
∀a0 a1 a0' a1'. Vis' a0 a1 = Vis' a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
[itree_next_Axiom] Theorem
⊢ ∀f0 f1 f2. ∃fn.
(∀a. fn (Ret' a) = f0 a) ∧ (∀a. fn (Tau' a) = f1 a) ∧
∀a0 a1. fn (Vis' a0 a1) = f2 a0 a1
[itree_next_case_cong] Theorem
⊢ ∀M M' f f1 f2.
M = M' ∧ (∀a. M' = Ret' a ⇒ f a = f' a) ∧
(∀a. M' = Tau' a ⇒ f1 a = f1' a) ∧
(∀a0 a1. M' = Vis' a0 a1 ⇒ f2 a0 a1 = f2' a0 a1) ⇒
itree_next_CASE M f f1 f2 = itree_next_CASE M' f' f1' f2'
[itree_next_case_eq] Theorem
⊢ itree_next_CASE x f f1 f2 = v ⇔
(∃r. x = Ret' r ∧ f r = v) ∨ (∃s. x = Tau' s ∧ f1 s = v) ∨
∃e f'. x = Vis' e f' ∧ f2 e f' = v
[itree_next_distinct] Theorem
⊢ (∀a' a. Ret' a ≠ Tau' a') ∧ (∀a1 a0 a. Ret' a ≠ Vis' a0 a1) ∧
∀a1 a0 a. Tau' a ≠ Vis' a0 a1
[itree_next_induction] Theorem
⊢ ∀P. (∀r. P (Ret' r)) ∧ (∀s. P (Tau' s)) ∧ (∀e f. P (Vis' e f)) ⇒
∀i. P i
[itree_next_nchotomy] Theorem
⊢ ∀ii. (∃r. ii = Ret' r) ∨ (∃s. ii = Tau' s) ∨ ∃e f. ii = Vis' e f
[itree_strong_bisimulation] Theorem
⊢ ∀t1 t2.
t1 = t2 ⇔
∃R. R t1 t2 ∧ (∀x t. R (Ret x) t ⇒ t = Ret x) ∧
(∀u t. R (Tau u) t ⇒ ∃v. t = Tau v ∧ (R u v ∨ u = v)) ∧
∀a f t.
R (Vis a f) t ⇒
∃g. t = Vis a g ∧ ∀s. R (f s) (g s) ∨ f s = g s
[itree_unfold] Theorem
⊢ itree_unfold f seed =
case f seed of
Ret' r => Ret r
| Tau' s => Tau (itree_unfold f s)
| Vis' e g => Vis e (itree_unfold f ∘ g)
[itree_wbisim_cases] Theorem
⊢ ∀a0 a1.
itree_wbisim a0 a1 ⇔
(∃t t'. a0 = Tau t ∧ a1 = Tau t' ∧ itree_wbisim t t') ∨
(∃e k k'.
strip_tau a0 (Vis e k) ∧ strip_tau a1 (Vis e k') ∧
∀r. itree_wbisim (k r) (k' r)) ∨
∃r. strip_tau a0 (Ret r) ∧ strip_tau a1 (Ret r)
[itree_wbisim_coind] Theorem
⊢ ∀itree_wbisim'.
(∀a0 a1.
itree_wbisim' a0 a1 ⇒
(∃t t'. a0 = Tau t ∧ a1 = Tau t' ∧ itree_wbisim' t t') ∨
(∃e k k'.
strip_tau a0 (Vis e k) ∧ strip_tau a1 (Vis e k') ∧
∀r. itree_wbisim' (k r) (k' r)) ∨
∃r. strip_tau a0 (Ret r) ∧ strip_tau a1 (Ret r)) ⇒
∀a0 a1. itree_wbisim' a0 a1 ⇒ itree_wbisim a0 a1
[itree_wbisim_coind_upto] Theorem
⊢ ∀R. (∀t t'.
R t t' ⇒
(∃t2 t3.
t = Tau t2 ∧ t' = Tau t3 ∧ (R t2 t3 ∨ itree_wbisim t2 t3)) ∨
(∃e k k'.
strip_tau t (Vis e k) ∧ strip_tau t' (Vis e k') ∧
∀r. R (k r) (k' r) ∨ itree_wbisim (k r) (k' r)) ∨
(∃r. strip_tau t (Ret r) ∧ strip_tau t' (Ret r)) ∨
itree_wbisim t t') ⇒
∀t t'. R t t' ⇒ itree_wbisim t t'
[itree_wbisim_refl] Theorem
⊢ itree_wbisim t t
[itree_wbisim_rules] Theorem
⊢ (∀t t'. itree_wbisim t t' ⇒ itree_wbisim (Tau t) (Tau t')) ∧
(∀e k k' t t'.
strip_tau t (Vis e k) ∧ strip_tau t' (Vis e k') ∧
(∀r. itree_wbisim (k r) (k' r)) ⇒
itree_wbisim t t') ∧
∀r t t'.
strip_tau t (Ret r) ∧ strip_tau t' (Ret r) ⇒ itree_wbisim t t'
[itree_wbisim_strip_tau] Theorem
⊢ ∀t t' t''.
itree_wbisim t t' ∧ strip_tau t t'' ⇒ itree_wbisim t'' t'
[itree_wbisim_strip_tau_Ret] Theorem
⊢ ∀t t' v.
itree_wbisim t t' ∧ strip_tau t (Ret v) ⇒ strip_tau t' (Ret v)
[itree_wbisim_strip_tau_Vis] Theorem
⊢ ∀t t' e k.
itree_wbisim t t' ∧ strip_tau t (Vis e k) ⇒
∃k'. strip_tau t' (Vis e k') ∧ ∀r. itree_wbisim (k r) (k' r)
[itree_wbisim_strip_tau_sym] Theorem
⊢ ∀t t' t''.
itree_wbisim t t' ∧ strip_tau t' t'' ⇒ itree_wbisim t t''
[itree_wbisim_strong_coind] Theorem
⊢ ∀R. (∀t t'.
R t t' ⇒
(∃t2 t3.
t = Tau t2 ∧ t' = Tau t3 ∧ (R t2 t3 ∨ itree_wbisim t2 t3)) ∨
(∃e k k'.
strip_tau t (Vis e k) ∧ strip_tau t' (Vis e k') ∧
∀r. R (k r) (k' r) ∨ itree_wbisim (k r) (k' r)) ∨
∃r. strip_tau t (Ret r) ∧ strip_tau t' (Ret r)) ⇒
∀t t'. R t t' ⇒ itree_wbisim t t'
[itree_wbisim_sym] Theorem
⊢ ∀t t'. itree_wbisim t t' ⇒ itree_wbisim t' t
[itree_wbisim_tau] Theorem
⊢ ∀t t'. itree_wbisim (Tau t) t' ⇒ itree_wbisim t t'
[itree_wbisim_tau_eq] Theorem
⊢ itree_wbisim (Tau t) t
[itree_wbisim_tau_eqn] Theorem
⊢ (itree_wbisim (Tau t1) t2 ⇔ itree_wbisim t1 t2) ∧
(itree_wbisim t1 (Tau t2) ⇔ itree_wbisim t1 t2)
[itree_wbisim_trans] Theorem
⊢ ∀t t' t''.
itree_wbisim t t' ∧ itree_wbisim t' t'' ⇒ itree_wbisim t t''
[spin] Theorem
⊢ spin = Tau spin
[spin_strip_tau] Theorem
⊢ ∀t. strip_tau spin t ⇒ F
[strip_tau_cases] Theorem
⊢ ∀a0 a1.
strip_tau a0 a1 ⇔
(∃t. a0 = Tau t ∧ strip_tau t a1) ∨
(∃e k. a0 = Vis e k ∧ a1 = Vis e k) ∨ ∃v. a0 = Ret v ∧ a1 = Ret v
[strip_tau_ind] Theorem
⊢ ∀strip_tau'.
(∀t t'. strip_tau' t t' ⇒ strip_tau' (Tau t) t') ∧
(∀e k. strip_tau' (Vis e k) (Vis e k)) ∧
(∀v. strip_tau' (Ret v) (Ret v)) ⇒
∀a0 a1. strip_tau a0 a1 ⇒ strip_tau' a0 a1
[strip_tau_inj] Theorem
⊢ ∀t t' t''. strip_tau t t' ∧ strip_tau t t'' ⇒ t' = t''
[strip_tau_rules] Theorem
⊢ (∀t t'. strip_tau t t' ⇒ strip_tau (Tau t) t') ∧
(∀e k. strip_tau (Vis e k) (Vis e k)) ∧
∀v. strip_tau (Ret v) (Ret v)
[strip_tau_simps] Theorem
⊢ (strip_tau t' (Tau t) ⇔ F) ∧ (strip_tau (Ret v) (Vis e k) ⇔ F) ∧
(strip_tau (Vis e k) (Ret v) ⇔ F) ∧
(strip_tau (Tau t) t' ⇔ strip_tau t t')
[strip_tau_simps2] Theorem
⊢ strip_tau (Ret v) (Ret v') ⇔ v = v'
[strip_tau_simps3] Theorem
⊢ strip_tau (Vis e k) (Vis e' k') ⇔ e = e' ∧ k = k'
[strip_tau_spin] Theorem
⊢ (∀t'. ¬strip_tau t t') ⇒ t = spin
[strip_tau_strongind] Theorem
⊢ ∀strip_tau'.
(∀t t'. strip_tau t t' ∧ strip_tau' t t' ⇒ strip_tau' (Tau t) t') ∧
(∀e k. strip_tau' (Vis e k) (Vis e k)) ∧
(∀v. strip_tau' (Ret v) (Ret v)) ⇒
∀a0 a1. strip_tau a0 a1 ⇒ strip_tau' a0 a1
[untau_IMP_wbisim] Theorem
⊢ ∀t t'. untau t = untau t' ⇒ itree_wbisim t t'
[untau_spin] Theorem
⊢ untau spin = Div
[wbisim_IMP_untau] Theorem
⊢ ∀t t'. itree_wbisim t t' ⇒ untau t = untau t'
*)
end
HOL 4, Trindemossen-1