Structure itreeTheory
signature itreeTheory =
sig
type thm = Thm.thm
(* Definitions *)
val ibind_def : thm
val iflat_def : thm
val imap_def : thm
val itree_TY_DEF : thm
val itree_el_case_def : thm
val itree_el_size_def : thm
val itree_next_case_def : thm
val itree_next_size_def : thm
(* Theorems *)
val Ret_11 : thm
val Vis_11 : thm
val at_path_cases : thm
val at_path_implies_iset : thm
val at_path_ind : thm
val at_path_ret : thm
val at_path_rules : thm
val at_path_strongind : thm
val at_path_thm : thm
val at_path_vis : thm
val datatype_itree : thm
val datatype_itree_el : thm
val datatype_itree_next : thm
val ibind_assoc : thm
val ibind_eq_div : thm
val ibind_eq_ret : thm
val ibind_eq_vis : thm
val ibind_left_id : thm
val ibind_right_id : thm
val ievery_cases : thm
val ievery_coind : thm
val ievery_div : thm
val ievery_ret : thm
val ievery_rules : thm
val ievery_set : thm
val ievery_thm : thm
val ievery_vis : thm
val iexists_cases : thm
val iexists_ind : thm
val iexists_ret : thm
val iexists_rules : thm
val iexists_set : thm
val iexists_strongind : thm
val iexists_thm : thm
val iexists_vis : thm
val ifinite_cases : thm
val ifinite_div : thm
val ifinite_ind : thm
val ifinite_ret : thm
val ifinite_rules : thm
val ifinite_strongind : thm
val ifinite_vis : thm
val iflat_div : thm
val iflat_eq_div : thm
val iflat_eq_ret : thm
val iflat_eq_vis : thm
val iflat_ret : thm
val iflat_vis : thm
val imap_composition : thm
val imap_div : thm
val imap_eq_div : thm
val imap_eq_ret : thm
val imap_eq_vis : thm
val imap_id : thm
val imap_ret : thm
val imap_vis : thm
val iset_cases : thm
val iset_flat : thm
val iset_flat_1 : thm
val iset_flat_2 : thm
val iset_iff_exists_path : thm
val iset_ind : thm
val iset_map : thm
val iset_map_1 : thm
val iset_map_2 : thm
val iset_ret : thm
val iset_rules : thm
val iset_strongind : thm
val iset_thm : thm
val iset_truncate : thm
val iset_vis : 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_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_induction : thm
val itree_el_nchotomy : 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_unfold : thm
val itree_unfold_err : thm
val itruncate_compute : thm
val itruncate_def : thm
val itruncate_implies_ifinite : thm
val itruncate_ind : thm
val itruncate_ret : thm
val not_ievery_exists : thm
val itree_grammars : type_grammar.grammar * term_grammar.grammar
(*
[indexedLists] Parent theory of "itree"
[patternMatches] Parent theory of "itree"
[ibind_def] Definition
⊢ ∀itr f. ibind itr f = iflat (imap f itr)
[iflat_def] Definition
⊢ ∀itr.
iflat itr =
itree_unfold
(λx.
case x of
INL (ireturn (ireturn r0)) => Ret' r0
| INL (ireturn Div) => Div'
| INL (ireturn (Vis e f)) => Vis' e (λi. INR (f i))
| INL Div => Div'
| INL (Vis e f) => Vis' e (λi. INL (f i))
| INR (ireturn r) => Ret' r
| INR Div => Div'
| INR (Vis e' f') => Vis' e' (λi. INR (f' i))) (INL itr)
[imap_def] Definition
⊢ ∀g itr.
imap g itr =
itree_unfold
(λx. itree_CASE x (λr. Ret' (g r)) Div' (λe f. Vis' e f)) itr
[itree_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION itree_rep_ok rep
[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 Stuck 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 Stuck = 0
[itree_next_case_def] Definition
⊢ (∀a f v f1. itree_next_CASE (Ret' a) f v f1 = f a) ∧
(∀f v f1. itree_next_CASE Div' f v f1 = v) ∧
∀a0 a1 f v f1. itree_next_CASE (Vis' a0 a1) f v f1 = f1 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. itree_next_size f f1 f2 f3 Div' = 0) ∧
∀f f1 f2 f3 a0 a1.
itree_next_size f f1 f2 f3 (Vis' a0 a1) = 1 + f1 a0
[Ret_11] Theorem
⊢ ∀x y. ireturn x = ireturn y ⇔ x = y
[Vis_11] Theorem
⊢ ∀x f y g. Vis x f = Vis y g ⇔ x = y ∧ f = g
[at_path_cases] Theorem
⊢ ∀a0 a1 a2.
at_path a0 a1 a2 ⇔
a0 = ireturn a2 ∧ a1 = [] ∨
∃f i ov p. a0 = Vis ov f ∧ a1 = (ov,i)::p ∧ at_path (f i) p a2
[at_path_implies_iset] Theorem
⊢ at_path itree p e ⇒ iset itree e
[at_path_ind] Theorem
⊢ ∀at_path'.
(∀e. at_path' (ireturn e) [] e) ∧
(∀e f i ov p.
at_path' (f i) p e ⇒ at_path' (Vis ov f) ((ov,i)::p) e) ⇒
∀a0 a1 a2. at_path a0 a1 a2 ⇒ at_path' a0 a1 a2
[at_path_ret] Theorem
⊢ ∀e. at_path (ireturn e) [] e
[at_path_rules] Theorem
⊢ (∀e. at_path (ireturn e) [] e) ∧
∀e f i ov p. at_path (f i) p e ⇒ at_path (Vis ov f) ((ov,i)::p) e
[at_path_strongind] Theorem
⊢ ∀at_path'.
(∀e. at_path' (ireturn e) [] e) ∧
(∀e f i ov p.
at_path (f i) p e ∧ at_path' (f i) p e ⇒
at_path' (Vis ov f) ((ov,i)::p) e) ⇒
∀a0 a1 a2. at_path a0 a1 a2 ⇒ at_path' a0 a1 a2
[at_path_thm] Theorem
⊢ (at_path Div p e ⇔ F) ∧
(at_path (ireturn e) p a ⇔ p = [] ∧ a = e) ∧
(at_path (Vis ov f) p e ⇔ ∃i l. p = (ov,i)::l ∧ at_path (f i) l e)
[at_path_vis] Theorem
⊢ ∀e f i ov p. at_path (f i) p e ⇒ at_path (Vis ov f) ((ov,i)::p) e
[datatype_itree] Theorem
⊢ DATATYPE (itree ireturn Div Vis)
[datatype_itree_el] Theorem
⊢ DATATYPE (itree_el Event Return Stuck)
[datatype_itree_next] Theorem
⊢ DATATYPE (itree_next Ret' Div' Vis')
[ibind_assoc] Theorem
⊢ ibind itr (λx. ibind (f x) g) = ibind (ibind itr f) g
[ibind_eq_div] Theorem
⊢ ibind itr f = Div ⇔ itr = Div ∨ ∃x. itr = ireturn x ∧ f x = Div
[ibind_eq_ret] Theorem
⊢ ibind itr f = ireturn v ⇔ ∃v'. itr = ireturn v' ∧ f v' = ireturn v
[ibind_eq_vis] Theorem
⊢ ibind itr f = Vis rv g ⇔
(∃h. itr = Vis rv h ∧ iflat ∘ imap f ∘ h = g) ∨
∃x. itr = ireturn x ∧ f x = Vis rv g
[ibind_left_id] Theorem
⊢ ibind (ireturn itr) f = f itr
[ibind_right_id] Theorem
⊢ ibind itr ireturn = itr
[ievery_cases] Theorem
⊢ ∀P a0.
ievery P a0 ⇔
a0 = Div ∨ (∃e. a0 = ireturn e ∧ P e) ∨
∃f ov. a0 = Vis ov f ∧ ∀iv. ievery P (f iv)
[ievery_coind] Theorem
⊢ ∀P ievery'.
(∀a0.
ievery' a0 ⇒
a0 = Div ∨ (∃e. a0 = ireturn e ∧ P e) ∨
∃f ov. a0 = Vis ov f ∧ ∀iv. ievery' (f iv)) ⇒
∀a0. ievery' a0 ⇒ ievery P a0
[ievery_div] Theorem
⊢ ∀P. ievery P Div
[ievery_ret] Theorem
⊢ ∀P e. P e ⇒ ievery P (ireturn e)
[ievery_rules] Theorem
⊢ ∀P. ievery P Div ∧ (∀e. P e ⇒ ievery P (ireturn e)) ∧
∀f ov. (∀iv. ievery P (f iv)) ⇒ ievery P (Vis ov f)
[ievery_set] Theorem
⊢ ∀itr. ievery P itr ⇔ ∀rv. iset itr rv ⇒ P rv
[ievery_thm] Theorem
⊢ (ievery P Div ⇔ T) ∧ (ievery P (ireturn e) ⇔ P e) ∧
(ievery P (Vis ov f) ⇔ ∀iv. ievery P (f iv))
[ievery_vis] Theorem
⊢ ∀P f ov. (∀iv. ievery P (f iv)) ⇒ ievery P (Vis ov f)
[iexists_cases] Theorem
⊢ ∀P a0.
iexists P a0 ⇔
(∃e. a0 = ireturn e ∧ P e) ∨
∃f ov. a0 = Vis ov f ∧ ∃iv. iexists P (f iv)
[iexists_ind] Theorem
⊢ ∀P iexists'.
(∀e. P e ⇒ iexists' (ireturn e)) ∧
(∀f ov. (∃iv. iexists' (f iv)) ⇒ iexists' (Vis ov f)) ⇒
∀a0. iexists P a0 ⇒ iexists' a0
[iexists_ret] Theorem
⊢ ∀P e. P e ⇒ iexists P (ireturn e)
[iexists_rules] Theorem
⊢ ∀P. (∀e. P e ⇒ iexists P (ireturn e)) ∧
∀f ov. (∃iv. iexists P (f iv)) ⇒ iexists P (Vis ov f)
[iexists_set] Theorem
⊢ iexists P itr ⇔ ∃x. iset itr x ∧ P x
[iexists_strongind] Theorem
⊢ ∀P iexists'.
(∀e. P e ⇒ iexists' (ireturn e)) ∧
(∀f ov.
(∃iv. iexists P (f iv) ∧ iexists' (f iv)) ⇒
iexists' (Vis ov f)) ⇒
∀a0. iexists P a0 ⇒ iexists' a0
[iexists_thm] Theorem
⊢ (iexists P Div ⇔ F) ∧ (iexists P (ireturn e) ⇔ P e) ∧
(iexists P (Vis ov f) ⇔ ∃iv. iexists P (f iv))
[iexists_vis] Theorem
⊢ ∀P f ov. (∃iv. iexists P (f iv)) ⇒ iexists P (Vis ov f)
[ifinite_cases] Theorem
⊢ ∀a0.
ifinite a0 ⇔
(∃e. a0 = ireturn e) ∨ a0 = Div ∨
∃f ov. a0 = Vis ov f ∧ ∀iv. ifinite (f iv)
[ifinite_div] Theorem
⊢ ifinite Div
[ifinite_ind] Theorem
⊢ ∀ifinite'.
(∀e. ifinite' (ireturn e)) ∧ ifinite' Div ∧
(∀f ov. (∀iv. ifinite' (f iv)) ⇒ ifinite' (Vis ov f)) ⇒
∀a0. ifinite a0 ⇒ ifinite' a0
[ifinite_ret] Theorem
⊢ ∀e. ifinite (ireturn e)
[ifinite_rules] Theorem
⊢ (∀e. ifinite (ireturn e)) ∧ ifinite Div ∧
∀f ov. (∀iv. ifinite (f iv)) ⇒ ifinite (Vis ov f)
[ifinite_strongind] Theorem
⊢ ∀ifinite'.
(∀e. ifinite' (ireturn e)) ∧ ifinite' Div ∧
(∀f ov.
(∀iv. ifinite (f iv) ∧ ifinite' (f iv)) ⇒ ifinite' (Vis ov f)) ⇒
∀a0. ifinite a0 ⇒ ifinite' a0
[ifinite_vis] Theorem
⊢ ∀f ov. (∀iv. ifinite (f iv)) ⇒ ifinite (Vis ov f)
[iflat_div] Theorem
⊢ iflat Div = Div
[iflat_eq_div] Theorem
⊢ iflat itr = Div ⇔ itr = Div ∨ itr = ireturn Div
[iflat_eq_ret] Theorem
⊢ (iflat itr = ireturn rv ⇔ itr = ireturn (ireturn rv)) ∧
(ireturn rv = iflat itr ⇔ itr = ireturn (ireturn rv))
[iflat_eq_vis] Theorem
⊢ iflat itr = Vis ov f ⇔
(∃g. itr = Vis ov g ∧ iflat ∘ g = f) ∨ itr = ireturn (Vis ov f)
[iflat_ret] Theorem
⊢ iflat (ireturn r) = r
[iflat_vis] Theorem
⊢ iflat (Vis ov f) = Vis ov (iflat ∘ f)
[imap_composition] Theorem
⊢ imap (f ∘ g) itr = imap f (imap g itr)
[imap_div] Theorem
⊢ imap g Div = Div
[imap_eq_div] Theorem
⊢ (imap g itr = Div ⇔ itr = Div) ∧ (Div = imap g itr ⇔ itr = Div)
[imap_eq_ret] Theorem
⊢ ireturn r = imap g itr ⇔ ∃x. itr = ireturn x ∧ g x = r
[imap_eq_vis] Theorem
⊢ Vis rv f = imap g itr ⇔ ∃h. itr = Vis rv h ∧ imap g ∘ h = f
[imap_id] Theorem
⊢ imap (λx. x) itr = itr
[imap_ret] Theorem
⊢ imap g (ireturn rv) = ireturn (g rv)
[imap_vis] Theorem
⊢ imap f (Vis ov g) = Vis ov (imap f ∘ g)
[iset_cases] Theorem
⊢ ∀a0 a1.
iset a0 a1 ⇔
a0 = ireturn a1 ∨ ∃f i ov. a0 = Vis ov f ∧ iset (f i) a1
[iset_flat] Theorem
⊢ ∀itr e. iset (iflat itr) e ⇔ ∃t0. iset itr t0 ∧ iset t0 e
[iset_flat_1] Theorem
⊢ ∀itr e. iset (iflat itr) e ⇒ ∃t0. iset itr t0 ∧ iset t0 e
[iset_flat_2] Theorem
⊢ ∀itr t0 e. iset itr t0 ∧ iset t0 e ⇒ iset (iflat itr) e
[iset_iff_exists_path] Theorem
⊢ iset itree e ⇔ ∃p. at_path itree p e
[iset_ind] Theorem
⊢ ∀iset'.
(∀e. iset' (ireturn e) e) ∧
(∀e f i ov. iset' (f i) e ⇒ iset' (Vis ov f) e) ⇒
∀a0 a1. iset a0 a1 ⇒ iset' a0 a1
[iset_map] Theorem
⊢ iset (imap f itr) = IMAGE f (iset itr)
[iset_map_1] Theorem
⊢ ∀itr x. iset (imap f itr) x ⇒ ∃y. x = f y ∧ iset itr y
[iset_map_2] Theorem
⊢ ∀itr. iset itr y ⇒ iset (imap f itr) (f y)
[iset_ret] Theorem
⊢ ∀e. iset (ireturn e) e
[iset_rules] Theorem
⊢ (∀e. iset (ireturn e) e) ∧
∀e f i ov. iset (f i) e ⇒ iset (Vis ov f) e
[iset_strongind] Theorem
⊢ ∀iset'.
(∀e. iset' (ireturn e) e) ∧
(∀e f i ov. iset (f i) e ∧ iset' (f i) e ⇒ iset' (Vis ov f) e) ⇒
∀a0 a1. iset a0 a1 ⇒ iset' a0 a1
[iset_thm] Theorem
⊢ (iset (ireturn e) e' ⇔ e = e') ∧ (iset Div e ⇔ F) ∧
(iset (Vis ov f) e ⇔ ∃i. iset (f i) e)
[iset_truncate] Theorem
⊢ iset itr elem ⇒ ∃n. iset (itruncate n itr) elem
[iset_vis] Theorem
⊢ ∀e f i ov. iset (f i) e ⇒ iset (Vis ov f) e
[itree_11] Theorem
⊢ (∀x y. ireturn x = ireturn y ⇔ x = y) ∧
∀x f y g. Vis x f = Vis y g ⇔ x = y ∧ f = g
[itree_CASE] Theorem
⊢ itree_CASE (ireturn r) ret div vis = ret r ∧
itree_CASE Div ret div vis = div ∧
itree_CASE (Vis a g) ret div vis = vis a g
[itree_CASE_cong] Theorem
⊢ ∀M M' ret div vis ret' div' vis'.
M = M' ∧ (∀x. M' = ireturn x ⇒ ret x = ret' x) ∧
(M' = Div ⇒ div = div') ∧
(∀a g. M' = Vis a g ⇒ vis a g = vis' a g) ⇒
itree_CASE M ret div vis = itree_CASE M' ret' div' vis'
[itree_CASE_elim] Theorem
⊢ ∀f. f (itree_CASE t ret div vis) ⇔
(∃r. t = ireturn r ∧ f (ret r)) ∨ t = Div ∧ f div ∨
∃a g. t = Vis a g ∧ f (vis a g)
[itree_CASE_eq] Theorem
⊢ itree_CASE t ret div vis = v ⇔
(∃r. t = ireturn r ∧ ret r = v) ∨ t = Div ∧ div = v ∨
∃a g. t = Vis a g ∧ vis a g = v
[itree_bisimulation] Theorem
⊢ ∀t1 t2.
t1 = t2 ⇔
∃R. R t1 t2 ∧ (∀x t. R (ireturn x) t ⇒ t = ireturn x) ∧
(∀t. R Div t ⇒ t = Div) ∧
∀a f t. R (Vis a f) t ⇒ ∃b g. t = Vis a g ∧ ∀s. R (f s) (g s)
[itree_cases] Theorem
⊢ ∀t. (∃x. t = ireturn x) ∨ t = Div ∨ ∃a g. t = Vis a g
[itree_distinct] Theorem
⊢ (∀x. ireturn x ≠ Div) ∧ (∀x g e. ireturn x ≠ Vis e g) ∧
∀g e. Div ≠ 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 Stuck = 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' = Stuck ⇒ 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 = Stuck ∧ v = v'
[itree_el_def] Theorem
⊢ itree_el (ireturn r) [] = Return r ∧ itree_el Div [] = Stuck ∧
itree_el (Vis e g) [] = Event e ∧
itree_el (ireturn r) (a::ns) = Return ARB ∧
itree_el Div (a::ns) = Return ARB ∧
itree_el (Vis e g) (a::ns) = itree_el (g a) ns
[itree_el_distinct] Theorem
⊢ (∀a' a. Event a ≠ Return a') ∧ (∀a. Event a ≠ Stuck) ∧
∀a. Return a ≠ Stuck
[itree_el_eqv] Theorem
⊢ ∀t1 t2. t1 = t2 ⇔ ∀path. itree_el t1 path = itree_el t2 path
[itree_el_induction] Theorem
⊢ ∀P. (∀e. P (Event e)) ∧ (∀r. P (Return r)) ∧ P Stuck ⇒ ∀i. P i
[itree_el_nchotomy] Theorem
⊢ ∀ii. (∃e. ii = Event e) ∨ (∃r. ii = Return r) ∨ ii = Stuck
[itree_next_11] Theorem
⊢ (∀a a'. Ret' a = Ret' 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) ∧ fn Div' = f1 ∧
∀a0 a1. fn (Vis' a0 a1) = f2 a0 a1
[itree_next_case_cong] Theorem
⊢ ∀M M' f v f1.
M = M' ∧ (∀a. M' = Ret' a ⇒ f a = f' a) ∧ (M' = Div' ⇒ v = v') ∧
(∀a0 a1. M' = Vis' a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ⇒
itree_next_CASE M f v f1 = itree_next_CASE M' f' v' f1'
[itree_next_case_eq] Theorem
⊢ itree_next_CASE x f v f1 = v' ⇔
(∃r. x = Ret' r ∧ f r = v') ∨ x = Div' ∧ v = v' ∨
∃e f'. x = Vis' e f' ∧ f1 e f' = v'
[itree_next_distinct] Theorem
⊢ (∀a. Ret' a ≠ Div') ∧ (∀a1 a0 a. Ret' a ≠ Vis' a0 a1) ∧
∀a1 a0. Div' ≠ Vis' a0 a1
[itree_next_induction] Theorem
⊢ ∀P. (∀r. P (Ret' r)) ∧ P Div' ∧ (∀e f. P (Vis' e f)) ⇒ ∀i. P i
[itree_next_nchotomy] Theorem
⊢ ∀ii. (∃r. ii = Ret' r) ∨ ii = Div' ∨ ∃e f. ii = Vis' e f
[itree_unfold] Theorem
⊢ itree_unfold f seed =
case f seed of
Ret' r => ireturn r
| Div' => Div
| Vis' e g => Vis e (itree_unfold f ∘ g)
[itree_unfold_err] Theorem
⊢ itree_unfold_err f (rel,err_f,err) seed =
case f seed of
Ret' r => ireturn r
| Div' => Div
| Vis' e g =>
Vis e
(λa.
case a of
INL x => ireturn (err_f e x)
| INR y =>
if rel e y then itree_unfold_err f (rel,err_f,err) (g y)
else ireturn (err e))
[itruncate_compute] Theorem
⊢ (∀itr. itruncate 0 itr = Div) ∧
(∀v2. itruncate (NUMERAL (BIT1 v2)) Div = Div) ∧
(∀v2. itruncate (NUMERAL (BIT2 v2)) Div = Div) ∧
(∀v3 rv. itruncate (NUMERAL (BIT1 v3)) (ireturn rv) = ireturn rv) ∧
(∀v3 rv. itruncate (NUMERAL (BIT2 v3)) (ireturn rv) = ireturn rv) ∧
(∀v4 ov f.
itruncate (NUMERAL (BIT1 v4)) (Vis ov f) =
Vis ov (λx. itruncate (NUMERAL (BIT1 v4) − 1) (f x))) ∧
∀v4 ov f.
itruncate (NUMERAL (BIT2 v4)) (Vis ov f) =
Vis ov (λx. itruncate (NUMERAL (BIT2 v4) − 1) (f x))
[itruncate_def] Theorem
⊢ (∀itr. itruncate 0 itr = Div) ∧
(∀v2. itruncate (SUC v2) Div = Div) ∧
(∀v3 rv. itruncate (SUC v3) (ireturn rv) = ireturn rv) ∧
∀v4 ov f.
itruncate (SUC v4) (Vis ov f) =
Vis ov (λx. itruncate (SUC v4 − 1) (f x))
[itruncate_implies_ifinite] Theorem
⊢ ∀itr. itruncate n itr = itr ⇒ ifinite itr
[itruncate_ind] Theorem
⊢ ∀P. (∀itr. P 0 itr) ∧ (∀v2. P (SUC v2) Div) ∧
(∀v3 rv. P (SUC v3) (ireturn rv)) ∧
(∀v4 ov f. (∀x. P (SUC v4 − 1) (f x)) ⇒ P (SUC v4) (Vis ov f)) ⇒
∀v v1. P v v1
[itruncate_ret] Theorem
⊢ ∀n. itruncate n itr = ireturn r ⇔ itr = ireturn r ∧ n ≠ 0
[not_ievery_exists] Theorem
⊢ ¬ievery P itr ⇔ iexists (λx. ¬P x) itr
*)
end
HOL 4, Trindemossen-1