# Theory Mono_Bool_Tran_Algebra

Up to index of Isabelle/HOL/LatticeProperties/MonoBoolTranAlgebra

theory Mono_Bool_Tran_Algebra
imports Mono_Bool_Tran
header {* Algebra of Monotonic Boolean Transformers *}theory  Mono_Bool_Tran_Algebraimports Mono_Bool_Tranbegintext{*In this section we introduce the {\em algebra of monotonic boolean transformers}.This is a bounded distributive lattice with a monoid operation, adual operator and an iteration operator. The standard model for thisalgebra is the set of monotonic boolean transformers introducedin the previous section. *}class dual =   fixes dual::"'a => 'a" ("_ ^ o" [81] 80)class omega =   fixes omega::"'a => 'a" ("_ ^ ω" [81] 80)class star =   fixes star::"'a => 'a" ("(_ ^ *)" [81] 80)class dual_star =   fixes dual_star::"'a => 'a" ("(_ ^ ⊗)" [81] 80)class mbt_algebra = monoid_mult + dual + omega + distrib_lattice + top + bot + star + dual_star +  assumes      dual_le: "(x ≤ y) = (y ^ o ≤ x ^ o)"  and dual_dual [simp]: "(x ^ o) ^ o = x"  and dual_comp: "(x * y) ^ o = x ^ o * y ^ o"  and dual_one [simp]: "1 ^ o = 1"  and top_comp [simp]: "\<top> * x = \<top>"  and inf_comp: "(x \<sqinter> y) * z = (x * z) \<sqinter> (y * z)"  and le_comp: "x ≤ y ==> z * x ≤ z * y"  and dual_neg: "(x * \<top>) \<sqinter> (x ^ o * ⊥) = ⊥"  and omega_fix: "x ^ ω = (x * (x ^ ω)) \<sqinter> 1"  and omega_least: "(x * z) \<sqinter> y ≤ z ==> (x ^ ω) * y ≤ z"  and star_fix: "x ^ * = (x * (x ^ *)) \<sqinter> 1"  and star_greatest: "z ≤ (x * z) \<sqinter> y ==> z ≤ (x ^ *) * y"  and dual_star_def: "(x ^ ⊗) = (((x ^ o) ^ *) ^ o)"beginlemma le_comp_right: "x ≤ y ==> x * z ≤ y * z"  apply (cut_tac x = x and y = y and z = z in inf_comp)  apply (simp add: inf_absorb1)  apply (subgoal_tac "x * z \<sqinter> (y * z) ≤ y * z")  apply simp  by (rule inf_le2)subclass bounded_lattice  proof qedendinstantiation MonoTran :: (complete_boolean_algebra) mbt_algebrabegindefinition   dual_MonoTran_def: "x ^ o = Abs_MonoTran (dual_fun (Rep_MonoTran x))"definition  omega_MonoTran_def: "x ^ ω = Abs_MonoTran (omega_fun (Rep_MonoTran x))"definition   star_MonoTran_def: "x ^ * = Abs_MonoTran (star_fun (Rep_MonoTran x))"definition  dual_star_MonoTran_def: "(x::('a MonoTran)) ^ ⊗ = ((x ^ o) ^ *) ^ o"  instance proof  fix x y :: "'a MonoTran" show "(x ≤ y) = (y ^ o ≤ x ^ o)"    apply (simp add: dual_MonoTran_def less_eq_MonoTran_def Abs_MonoTran_inverse)    apply (simp add: dual_fun_def le_fun_def)    apply safe    apply simp    apply (drule_tac x = "-xa" in spec)     by simpnext  fix x :: "'a MonoTran" show "(x ^ o) ^ o = x"    apply (simp add: dual_MonoTran_def Abs_MonoTran_inverse)    by (simp add: dual_fun_def Rep_MonoTran_inverse)next  fix x y :: "'a MonoTran" show "(x * y) ^ o = x ^ o * y ^ o"    apply (simp add: dual_MonoTran_def times_MonoTran_def Abs_MonoTran_inverse)    apply (simp add: dual_fun_def)    apply (subgoal_tac "(λp . - Rep_MonoTran x (Rep_MonoTran y (- p))) = ((λp . - Rep_MonoTran x (- p)) o (λp . - Rep_MonoTran y (- p)))")    apply simp_all    by (simp add: fun_eq_iff)next  show "(1::'a MonoTran) ^ o = 1"    apply (simp add: dual_MonoTran_def one_MonoTran_def Abs_MonoTran_inverse)    by (simp add: dual_fun_def id_def)next  fix x :: "'a MonoTran" show "\<top> * x = \<top>"    apply (simp add: top_MonoTran_def times_MonoTran_def Abs_MonoTran_inverse)    by (simp add: top_fun_def o_def)next  fix x y z :: "'a MonoTran" show "(x \<sqinter> y) * z = (x * z) \<sqinter> (y * z)"    apply (simp add: inf_MonoTran_def times_MonoTran_def Abs_MonoTran_inverse)    by (simp add: inf_fun_def o_def)next  fix x y z :: "'a MonoTran" assume A: "x ≤ y" from A show " z * x ≤ z * y"    apply (simp add: less_eq_MonoTran_def times_MonoTran_def Abs_MonoTran_inverse)    apply (cut_tac x = z in Rep_MonoTran)    by (simp add: le_fun_def MonoTran_def mono_def o_def)next  fix x :: "'a MonoTran" show "x * \<top> \<sqinter> (x ^ o * ⊥) = ⊥"    apply (simp add: inf_MonoTran_def times_MonoTran_def top_MonoTran_def bot_MonoTran_def dual_MonoTran_def Abs_MonoTran_inverse)    by (simp add: inf_fun_def bot_fun_def dual_fun_def o_def top_fun_def inf_compl_bot)  fix x :: "'a MonoTran" show "x ^ ω = x * x ^ ω \<sqinter> 1"    apply (simp add: omega_MonoTran_def times_MonoTran_def inf_MonoTran_def one_MonoTran_def Abs_MonoTran_inverse)    apply (simp add: omega_fun_def Omega_fun_def)    apply (subst lfp_unfold, simp_all)    apply (cut_tac x = x in Rep_MonoTran)    by (unfold Omega_fun_def [THEN sym], simp)next  fix x y z :: "'a MonoTran" assume A: "x * z \<sqinter> y ≤ z" from A show "x ^ ω * y ≤ z"    apply (simp add: omega_MonoTran_def times_MonoTran_def less_eq_MonoTran_def inf_MonoTran_def one_MonoTran_def Abs_MonoTran_inverse)    apply (cut_tac f = "Rep_MonoTran x" and g = "Rep_MonoTran y" in lfp_omega)    apply (cut_tac x = x in Rep_MonoTran)    apply simp_all    apply (simp add: lfp_def)    apply (rule Inf_lower)    by (simp add: Omega_fun_def)next  fix x :: "'a MonoTran" show "x ^ * = x * x ^ * \<sqinter> 1"    apply (simp add: star_MonoTran_def times_MonoTran_def inf_MonoTran_def one_MonoTran_def Abs_MonoTran_inverse)    apply (simp add: star_fun_def Omega_fun_def)    apply (subst gfp_unfold, simp_all)    apply (cut_tac x = x in Rep_MonoTran)    by (unfold Omega_fun_def [THEN sym], simp)next  fix x y z :: "'a MonoTran" assume A: "z ≤ x * z \<sqinter> y" from A show "z ≤ x ^ * * y"    apply (simp add: star_MonoTran_def times_MonoTran_def less_eq_MonoTran_def inf_MonoTran_def one_MonoTran_def Abs_MonoTran_inverse)    apply (cut_tac f = "Rep_MonoTran x" and g = "Rep_MonoTran y" in gfp_star)    apply (cut_tac x = x in Rep_MonoTran)    apply simp_all    apply (simp add: gfp_def)    apply (rule Sup_upper)    by (simp add: Omega_fun_def)next  fix x :: "'a MonoTran" show "x ^ ⊗ = ((x ^ o) ^ *) ^ o"    by (simp add: dual_star_MonoTran_def) qedendcontext mbt_algebra beginlemma dual_top [simp]: "\<top> ^ o = ⊥"  apply (rule antisym, simp_all)  by (subst dual_le, simp)lemma dual_bot [simp]: "⊥ ^ o = \<top>"  apply (rule antisym, simp_all)  by (subst dual_le, simp)lemma dual_inf: "(x \<sqinter> y) ^ o = (x ^ o) \<squnion> (y ^ o)"  apply (rule antisym, simp_all, safe)  apply (subst dual_le, simp, safe)  apply (subst dual_le, simp)  apply (subst dual_le, simp)  apply (subst dual_le, simp)  by (subst dual_le, simp)lemma dual_sup: "(x \<squnion> y) ^ o = (x ^ o) \<sqinter> (y ^ o)"  apply (rule antisym, simp_all, safe)  apply (subst dual_le, simp)  apply (subst dual_le, simp)  apply (subst dual_le, simp, safe)  apply (subst dual_le, simp)  by (subst dual_le, simp)lemma sup_comp: "(x \<squnion> y) * z = (x * z) \<squnion> (y * z)"  apply (subgoal_tac "((x ^ o \<sqinter> y ^ o) * z ^ o) ^ o = ((x ^ o * z ^ o) \<sqinter> (y ^ o * z ^ o)) ^ o")  apply (simp add: dual_inf dual_comp)  by (simp add: inf_comp)lemma dual_eq: "x ^ o = y ^ o ==> x = y"  apply (subgoal_tac "(x ^ o) ^ o = (y ^ o) ^ o")  apply (subst (asm) dual_dual)  apply (subst (asm) dual_dual)  by simp_alllemma dual_neg_top [simp]: "(x ^ o * ⊥) \<squnion> (x * \<top>) = \<top>"  apply (rule dual_eq)  by(simp add: dual_sup dual_comp dual_neg) lemma bot_comp [simp]: "⊥ * x = ⊥"   by (rule dual_eq, simp add: dual_comp)lemma [simp]: "(x * \<top>) * y = x * \<top>"   by (simp add: mult_assoc)lemma [simp]: "(x * ⊥) * y = x * ⊥"   by (simp add: mult_assoc)lemma gt_one_comp: "1 ≤ x ==> y ≤ x * y"  by (cut_tac x = 1 and y = x and z = y in le_comp_right, simp_all)  theorem omega_comp_fix: "x ^ ω * y = (x * (x ^ ω) * y) \<sqinter> y"  apply (subst omega_fix)  by (simp add: inf_comp)  theorem dual_star_fix: "x^⊗ = (x * (x^⊗)) \<squnion> 1"    by (metis dual_comp dual_dual dual_inf dual_one dual_star_def star_fix)  theorem star_comp_fix: "x ^ * * y = (x * (x ^ *) * y) \<sqinter> y"  apply (subst star_fix)  by (simp add: inf_comp)  theorem dual_star_comp_fix: "x^⊗ * y = (x * (x^⊗) * y) \<squnion> y"  apply (subst dual_star_fix)  by (simp add: sup_comp)  theorem dual_star_least: "(x * z) \<squnion> y ≤ z ==> (x^⊗) * y ≤ z"    apply (subst dual_le)    apply (simp add: dual_star_def dual_comp)    apply (rule star_greatest)    apply (subst dual_le)    by (simp add: dual_inf dual_comp)  lemma omega_one [simp]: "1 ^ ω = ⊥"    apply (rule antisym, simp_all)    by (cut_tac x = "1::'a" and y = 1 and z = ⊥ in omega_least, simp_all)  lemma omega_mono: "x ≤ y ==> x ^ ω ≤ y ^ ω"    apply (cut_tac x = x and y = 1 and z = "y ^ ω" in omega_least, simp_all)    apply (subst (2) omega_fix, simp_all)    apply (rule_tac y = "x * y ^ ω" in order_trans, simp)    by (rule le_comp_right, simp)endsublocale mbt_algebra < conjunctive "inf" "inf" "times"donesublocale mbt_algebra < disjunctive "sup" "sup" "times"donecontext mbt_algebra beginlemma dual_conjunctive: "x ∈ conjunctive ==> x ^ o ∈ disjunctive"  apply (simp add: conjunctive_def disjunctive_def)  apply safe  apply (rule dual_eq)  by (simp add: dual_comp dual_sup)lemma dual_disjunctive: "x ∈ disjunctive ==> x ^ o ∈ conjunctive"  apply (simp add: conjunctive_def disjunctive_def)  apply safe  apply (rule dual_eq)  by (simp add: dual_comp dual_inf)lemma comp_pres_conj: "x ∈ conjunctive ==> y ∈ conjunctive ==> x * y ∈ conjunctive"  apply (subst conjunctive_def, safe)  by (simp add: mult_assoc conjunctiveD)lemma comp_pres_disj: "x ∈ disjunctive ==> y ∈ disjunctive ==> x * y ∈ disjunctive"  apply (subst disjunctive_def, safe)  by (simp add: mult_assoc disjunctiveD)lemma start_pres_conj: "x ∈ conjunctive ==> (x ^ *) ∈ conjunctive"  apply (subst conjunctive_def, safe)  apply (rule antisym, simp_all)  apply (metis inf_le1 inf_le2 le_comp)  apply (rule star_greatest)  apply (subst conjunctiveD, simp)  apply (subst star_comp_fix)  apply (subst star_comp_fix)  by (metis inf.assoc inf_left_commute mult.assoc order_refl)lemma dual_star_pres_disj: "x ∈ disjunctive ==> x^⊗ ∈ disjunctive"  apply (simp add: dual_star_def)  apply (rule dual_conjunctive)  apply (rule start_pres_conj)  by (rule dual_disjunctive, simp)subsection{*Assertions*}text{*Usually, in Kleene algebra with tests or in other progrm algebras, tests or assertionsor assumptions are defined using an existential quantifier. An element of the algebrais a test if it has a complement with respect to $\bot$ and $1$. In this formalizationassertions can be defined much simpler using the dual operator.*}definition   "assertion = {x . x ≤ 1 ∧ (x * \<top>) \<sqinter> (x ^ o) = x}"lemma assertion_prop: "x ∈ assertion ==> (x * \<top>) \<sqinter> 1 = x"  apply (simp add: assertion_def)  apply safe  apply (rule antisym)  apply simp_all  proof -    assume [simp]: "x ≤ 1"    assume A: "x * \<top> \<sqinter> x ^ o = x"    have "x * \<top> \<sqinter> 1 ≤ x * \<top> \<sqinter> x ^ o"      apply simp      apply (rule_tac y = 1 in order_trans)      apply simp      apply (subst dual_le)      by simp    also have "… = x" by (cut_tac A, simp)    finally show "x * \<top> \<sqinter> 1 ≤ x" .  next    assume A: "x * \<top> \<sqinter> x ^ o = x"    have "x = x * \<top> \<sqinter> x ^ o" by (simp add: A)    also have "… ≤ x * \<top>" by simp    finally show "x ≤ x * \<top>" .  qedlemma dual_assertion_prop: "x ∈ assertion ==> ((x ^ o) * ⊥) \<squnion> 1 = x ^ o"  apply (rule dual_eq)  by (simp add: dual_sup dual_comp assertion_prop)lemma assertion_disjunctive: "x ∈ assertion ==> x ∈ disjunctive"  apply (simp add: disjunctive_def, safe)  apply (drule assertion_prop)  proof -    assume A: "x * \<top> \<sqinter> 1 = x"    fix y z::"'a"    have "x * (y \<squnion> z) = (x * \<top> \<sqinter> 1) * (y \<squnion> z)" by (cut_tac  A, simp)    also have "… = (x * \<top>) \<sqinter> (y \<squnion> z)" by (simp add: inf_comp)    also have "… = ((x * \<top>) \<sqinter> y) \<squnion> ((x * \<top>) \<sqinter> z)" by (simp add: inf_sup_distrib)    also have "… = (((x * \<top>) \<sqinter> 1) * y) \<squnion> (((x * \<top>) \<sqinter> 1) * z)" by (simp add: inf_comp)    also have "… = x * y \<squnion> x * z" by (cut_tac  A, simp)    finally show "x * (y \<squnion> z) = x * y \<squnion> x * z" .  qedlemma Abs_MonoTran_injective: "x ∈ MonoTran ==> y ∈ MonoTran ==> Abs_MonoTran x = Abs_MonoTran y ==> x = y"  apply (subgoal_tac "Rep_MonoTran (Abs_MonoTran x) = Rep_MonoTran (Abs_MonoTran y)")  apply (subst (asm) Abs_MonoTran_inverse, simp)  by (subst (asm) Abs_MonoTran_inverse, simp_all)endlemma mbta_MonoTran_disjunctive: "Rep_MonoTran  disjunctive = Apply.disjunctive"  apply safe  apply (simp add: disjunctive_def Apply.disjunctive_def, safe)  apply (simp add: sup_MonoTran_def times_MonoTran_def Abs_MonoTran_inverse Rep_MonoTran_inverse)    apply (drule_tac x = "Abs_MonoTran (λ u . y)" in spec)    apply (drule_tac x = "Abs_MonoTran (λ u . z)" in spec)    apply (simp add: Abs_MonoTran_inverse Rep_MonoTran_inverse)    apply (cut_tac x = "Rep_MonoTran xa o (λu::'a. y) \<squnion> (λu::'a. z)"       and y = "((Rep_MonoTran xa o (λu::'a. y)) \<squnion> (Rep_MonoTran xa o (λu::'a. z)))" in Abs_MonoTran_injective)    apply simp_all    apply (simp add: fun_eq_iff sup_fun_def o_def)    apply (simp add: image_def)    apply (subgoal_tac "x ∈ MonoTran")    apply (rule_tac x = "Abs_MonoTran x" in bexI)    apply (simp add: Abs_MonoTran_inverse)    apply (simp add: disjunctive_def sup_MonoTran_def times_MonoTran_def Abs_MonoTran_inverse Rep_MonoTran_inverse)    apply safe    apply (rule_tac f = "Abs_MonoTran" in fun_eq)    apply (simp add: Apply.disjunctive_def fun_eq_iff o_def sup_fun_def)    by (subst MonoTran_def, simp)lemma assertion_MonoTran: "assertion = Abs_MonoTran  assertion_fun"    apply (safe)    apply (subst assertion_fun_disj_less_one)    apply (simp add: image_def)    apply (rule_tac x = "Rep_MonoTran x" in bexI)    apply (simp add: Rep_MonoTran_inverse)    apply safe    apply (drule assertion_disjunctive)    apply (unfold mbta_MonoTran_disjunctive [THEN sym], simp)    apply (simp add: assertion_def less_eq_MonoTran_def one_MonoTran_def Abs_MonoTran_inverse)    apply (simp add: assertion_def)    by (simp_all add: inf_MonoTran_def less_eq_MonoTran_def       times_MonoTran_def dual_MonoTran_def top_MonoTran_def Abs_MonoTran_inverse one_MonoTran_def assertion_fun_dual)context mbt_algebra beginlemma assertion_conjunctive: "x ∈ assertion ==> x ∈ conjunctive"  apply (simp add: conjunctive_def, safe)  apply (drule assertion_prop)  proof -    assume A: "x * \<top> \<sqinter> 1 = x"    fix y z::"'a"    have "x * (y \<sqinter> z) = (x * \<top> \<sqinter> 1) * (y \<sqinter> z)" by (cut_tac  A, simp)    also have "… = (x * \<top>) \<sqinter> (y \<sqinter> z)" by (simp add: inf_comp)    also have "… = ((x * \<top>) \<sqinter> y) \<sqinter> ((x * \<top>) \<sqinter> z)"      apply (rule antisym, simp_all, safe)      apply (rule_tac y = "y \<sqinter> z" in order_trans)      apply (rule inf_le2)      apply simp      apply (rule_tac y = "y \<sqinter> z" in order_trans)      apply (rule inf_le2)      apply simp_all      apply (simp add: inf_assoc)      apply (rule_tac y = " x * \<top> \<sqinter> y" in order_trans)      apply (rule inf_le1)      apply simp      apply (rule_tac y = " x * \<top> \<sqinter> z" in order_trans)      apply (rule inf_le2)      by simp    also have "… = (((x * \<top>) \<sqinter> 1) * y) \<sqinter> (((x * \<top>) \<sqinter> 1) * z)" by (simp add: inf_comp)    also have "… = (x * y) \<sqinter> (x * z)" by (cut_tac  A, simp)    finally show "x * (y \<sqinter> z) = (x * y) \<sqinter> (x * z)" .  qedlemma dual_assertion_conjunctive: "x ∈ assertion ==> x ^ o ∈ conjunctive"  apply (drule assertion_disjunctive)  by (rule dual_disjunctive, simp)lemma dual_assertion_disjunct: "x ∈ assertion ==> x ^ o ∈ disjunctive"  apply (drule assertion_conjunctive)  by (rule dual_conjunctive, simp)lemma [simp]: "x ∈ assertion ==> y ∈ assertion ==> x \<sqinter> y ≤ x * y"  apply (simp add: assertion_def, safe)  proof -  assume A: "x ≤ 1"  assume B: "x * \<top> \<sqinter> x ^ o = x"  assume C: "y ≤ 1"  assume D: "y * \<top> \<sqinter> y ^ o = y"  have "x \<sqinter> y = (x * \<top> \<sqinter> x ^ o) \<sqinter> (y * \<top> \<sqinter> y ^ o)" by (cut_tac B D, simp)  also have "… ≤ (x * \<top>) \<sqinter> (((x^o) * (y * \<top>)) \<sqinter> ((x^o) * (y^o)))"    apply (simp, safe)      apply (rule_tac y = "x * \<top> \<sqinter> x ^ o" in order_trans)      apply (rule inf_le1)      apply simp      apply (rule_tac y = "y * \<top>" in order_trans)      apply (rule_tac y = "y * \<top> \<sqinter> y ^ o" in order_trans)      apply (rule inf_le2)      apply simp      apply (rule gt_one_comp)      apply (subst dual_le, simp add: A)      apply (rule_tac y = "y ^ o" in order_trans)      apply (rule_tac y = "y * \<top> \<sqinter> y ^ o" in order_trans)      apply (rule inf_le2)      apply simp      apply (rule gt_one_comp)      by (subst dual_le, simp add: A)    also have "... = ((x * \<top>) \<sqinter> (x ^ o)) * ((y * \<top>) \<sqinter> (y ^ o))"      apply (cut_tac x = x in dual_assertion_conjunctive)      apply (cut_tac A, cut_tac B, simp add: assertion_def)      by (simp add: inf_comp conjunctiveD)    also have "... = x * y"      by (cut_tac B, cut_tac D, simp)    finally show "x \<sqinter> y ≤ x * y" .  qed    lemma [simp]: "x ∈ assertion ==> x * y ≤ y"  by (unfold assertion_def, cut_tac x = x and y = 1 and z = y in le_comp_right, simp_all)lemma [simp]: "x ∈ assertion ==> y ∈ assertion ==> x * y ≤ x"  apply (subgoal_tac "x * y ≤ (x * \<top>) \<sqinter> (x ^ o)")  apply (simp add: assertion_def)   apply (simp, safe)  apply (rule le_comp, simp)  apply (rule_tac y = 1 in order_trans)  apply (rule_tac y = y in order_trans)  apply simp  apply (simp add: assertion_def)  by (subst dual_le, simp add: assertion_def)lemma assertion_inf_comp_eq: "x ∈ assertion ==> y ∈ assertion ==> x \<sqinter> y = x * y"  by (rule antisym, simp_all)lemma one_right_assertion [simp]: "x ∈ assertion ==> x * 1 = x"  apply (drule assertion_prop)  proof -    assume A: "x * \<top> \<sqinter> 1 = x"    have "x * 1 = (x * \<top> \<sqinter> 1) * 1" by (simp add: A)    also have "… = x * \<top> \<sqinter> 1" by (simp add: inf_comp)    also have "… = x" by (simp add: A)    finally show ?thesis .  qedlemma [simp]: "x ∈ assertion ==> x \<squnion> 1 = 1"  by (rule antisym, simp_all add: assertion_def)  lemma [simp]: "x ∈ assertion ==> 1 \<squnion> x = 1"  by (rule antisym, simp_all add: assertion_def)  lemma [simp]: "x ∈ assertion ==> x \<sqinter> 1 = x"  by (rule antisym, simp_all add: assertion_def)  lemma [simp]: "x ∈ assertion ==> 1 \<sqinter> x = x"  by (rule antisym, simp_all add: assertion_def)lemma [simp]:  "x ∈ assertion ==> x ≤ x * \<top>"  by (cut_tac x = 1 and y = \<top> and z = x in le_comp, simp_all)lemma [simp]: "x ∈ assertion ==> x ≤ 1"  by (simp add: assertion_def)definition  "neg_assert (x::'a) = (x ^ o * ⊥) \<sqinter> 1"  lemma sup_uminus[simp]: "x ∈ assertion ==> x \<squnion> neg_assert x = 1"  apply (simp add: neg_assert_def)  apply (simp add: sup_inf_distrib)  apply (rule antisym, simp_all)  apply (unfold assertion_def)  apply safe  apply (subst dual_le)  apply (simp add: dual_sup dual_comp)  apply (subst inf_commute)  by simplemma inf_uminus[simp]: "x ∈ assertion ==> x \<sqinter> neg_assert x = ⊥"  apply (simp add: neg_assert_def)  apply (rule antisym, simp_all)  apply (rule_tac y = "x \<sqinter> (x ^ o * ⊥)" in order_trans)  apply simp  apply (rule_tac y = "x ^ o * ⊥ \<sqinter> 1" in order_trans)  apply (rule inf_le2)  apply simp  apply (rule_tac y = "(x * \<top>)  \<sqinter> (x ^ o * ⊥)" in order_trans)  apply simp  apply (rule_tac y = x in order_trans)  apply simp_all  by (simp add: dual_neg)lemma uminus_assertion[simp]: "x ∈ assertion ==> neg_assert x ∈ assertion"  apply (subst assertion_def)  apply (simp add: neg_assert_def)  apply (simp add: inf_comp dual_inf dual_comp inf_sup_distrib)  apply (subst inf_commute)  by (simp add: dual_neg)lemma uminus_uminus [simp]: "x ∈ assertion ==> neg_assert (neg_assert x) = x"  apply (simp add: neg_assert_def)  by (simp add: dual_inf dual_comp sup_comp assertion_prop)lemma dual_comp_neg [simp]: "x ^ o * y \<squnion> (neg_assert x) * \<top> = x ^ o * y"  apply (simp add: neg_assert_def inf_comp)  apply (rule antisym, simp_all)  by (rule le_comp, simp)lemma [simp]: "(neg_assert x) ^ o * y \<squnion> x * \<top> = (neg_assert x) ^ o * y"  apply (simp add: neg_assert_def inf_comp dual_inf dual_comp sup_comp)  by (rule antisym, simp_all)lemma [simp]: " x * \<top> \<squnion> (neg_assert x) ^ o * y= (neg_assert x) ^ o * y"  by (simp add: neg_assert_def inf_comp dual_inf dual_comp sup_comp)lemma inf_assertion [simp]: "x ∈ assertion ==> y ∈ assertion ==> x \<sqinter> y ∈ assertion"  apply (subst assertion_def)  apply safe  apply (rule_tac y = x in order_trans)  apply simp_all  apply (simp add: assertion_inf_comp_eq)  proof -    assume A: "x ∈ assertion"    assume B: "y ∈ assertion"    have C: "(x * \<top>) \<sqinter> (x ^ o) = x"      by (cut_tac A, unfold assertion_def, simp)     have D: "(y * \<top>) \<sqinter> (y ^ o) = y"      by (cut_tac B, unfold assertion_def, simp)    have "x * y = ((x * \<top>) \<sqinter> (x ^ o)) * ((y * \<top>) \<sqinter> (y ^ o))" by (simp add: C D)    also have "… = x * \<top> \<sqinter> ((x ^ o) * ((y * \<top>) \<sqinter> (y ^ o)))" by (simp add: inf_comp)    also have "… =  x * \<top> \<sqinter> ((x ^ o) * (y * \<top>)) \<sqinter> ((x ^ o) *(y ^ o))"       by (cut_tac A, cut_tac x = x in dual_assertion_conjunctive, simp_all add: conjunctiveD inf_assoc)    also have "… = (((x * \<top>) \<sqinter> (x ^ o)) * (y * \<top>)) \<sqinter> ((x ^ o) *(y ^ o))"      by (simp add: inf_comp)    also have "… = (x * y * \<top>)  \<sqinter> ((x * y) ^ o)" by (simp add: C mult_assoc dual_comp)    finally show "(x * y * \<top>)  \<sqinter> ((x * y) ^ o) = x * y" by simp  qedlemma comp_assertion [simp]: "x ∈ assertion ==> y ∈ assertion ==> x * y ∈ assertion"  by (subst assertion_inf_comp_eq [THEN sym], simp_all)lemma sup_assertion [simp]: "x ∈ assertion ==> y ∈ assertion ==> x \<squnion> y ∈ assertion"  apply (subst assertion_def)  apply safe  apply (unfold assertion_def)  apply simp  apply safe  proof -    assume [simp]: "x ≤ 1"    assume [simp]: "y ≤ 1"    assume A: "x * \<top> \<sqinter> x ^ o = x"    assume B: "y * \<top> \<sqinter> y ^ o = y"    have "(y * \<top>) \<sqinter> (x ^ o) \<sqinter> (y ^ o) = (x ^ o) \<sqinter> (y * \<top>) \<sqinter> (y ^ o)" by (simp add: inf_commute)    also have "… = (x ^ o) \<sqinter> ((y * \<top>) \<sqinter> (y ^ o))" by (simp add: inf_assoc)    also have "… = (x ^ o) \<sqinter> y" by (simp add: B)    also have "… = y"      apply (rule antisym, simp_all)      apply (rule_tac y = 1 in order_trans)      apply simp      by (subst dual_le, simp)    finally have [simp]: "(y * \<top>) \<sqinter> (x ^ o) \<sqinter> (y ^ o) = y" .    have "x * \<top> \<sqinter> (x ^ o) \<sqinter> (y ^ o) = x \<sqinter> (y ^ o)"  by (simp add: A)    also have "… = x"      apply (rule antisym, simp_all)      apply (rule_tac y = 1 in order_trans)      apply simp      by (subst dual_le, simp)    finally have [simp]: "x * \<top> \<sqinter> (x ^ o) \<sqinter> (y ^ o) = x" .    have "(x \<squnion> y) * \<top> \<sqinter> (x \<squnion> y) ^ o = (x * \<top> \<squnion> y * \<top>) \<sqinter> ((x ^ o) \<sqinter> (y ^ o))" by (simp add: sup_comp dual_sup)    also have "… = x \<squnion> y" by (simp add: inf_sup_distrib inf_assoc [THEN sym])    finally show "(x \<squnion> y) * \<top> \<sqinter> (x \<squnion> y) ^ o = x \<squnion> y" .  qedlemma [simp]: "x ∈ assertion ==> x * x = x"  by (simp add: assertion_inf_comp_eq [THEN sym])lemma [simp]: "x ∈ assertion ==> (x ^ o) * (x ^ o) = x ^ o"  apply (rule dual_eq)  by (simp add: dual_comp assertion_inf_comp_eq [THEN sym])lemma [simp]: "x ∈ assertion ==> x * (x ^ o) = x"  proof -    assume A: "x ∈ assertion"    have B: "x * \<top> \<sqinter> (x ^ o) = x" by (cut_tac A, unfold assertion_def, simp)    have "x * x ^ o = (x * \<top> \<sqinter> (x ^ o)) * x ^ o" by (simp add: B)    also have "… = x * \<top> \<sqinter> (x ^ o)" by (cut_tac A, simp add: inf_comp)    also have "… = x" by (simp add: B)    finally show ?thesis .  qedlemma [simp]: "x ∈ assertion ==> (x ^ o) * x = x ^ o"  apply (rule dual_eq)  by (simp add: dual_comp)lemma [simp]: "⊥ ∈ assertion"  by (unfold assertion_def, simp)lemma [simp]: "1 ∈ assertion"  by (unfold assertion_def, simp)subsection {*Weakest precondition of true*}definition  "wpt x = (x * \<top>) \<sqinter> 1"lemma wpt_is_assertion [simp]: "wpt x ∈ assertion"  apply (unfold wpt_def assertion_def, safe)  apply simp  apply (simp add: inf_comp dual_inf dual_comp inf_sup_distrib)  apply (rule antisym)  by (simp_all add: dual_neg)lemma wpt_comp: "(wpt x) * x = x"  apply (simp add: wpt_def inf_comp)  apply (rule antisym, simp_all)  by (cut_tac x = 1 and y = \<top> and z = x in le_comp, simp_all)lemma wpt_comp_2: "wpt (x * y) = wpt (x * (wpt y))"  by (simp add: wpt_def inf_comp mult_assoc)lemma wpt_assertion [simp]: "x ∈ assertion ==> wpt x = x"  by (simp add: wpt_def assertion_prop)lemma wpt_le_assertion: "x ∈ assertion ==> x * y = y ==> wpt y ≤ x"  apply (simp add: wpt_def)  proof -    assume A: "x ∈ assertion"    assume B: "x * y = y"    have "y * \<top> \<sqinter> 1 = x * (y * \<top>) \<sqinter> 1" by (simp add: B mult_assoc [THEN sym])    also have "… ≤ x * \<top> \<sqinter> 1"       apply simp      apply (rule_tac y = "x * (y * \<top>)" in order_trans)      apply simp_all      by (rule le_comp, simp)    also have "… = x" by (cut_tac A, simp add: assertion_prop)    finally show "y * \<top> \<sqinter> 1 ≤ x" .  qedlemma wpt_choice: "wpt (x \<sqinter> y) = wpt x \<sqinter> wpt y"  apply (simp add: wpt_def inf_comp)  proof -    have "x * \<top> \<sqinter> 1 \<sqinter> (y * \<top> \<sqinter> 1) = x * \<top> \<sqinter> ((y * \<top> \<sqinter> 1) \<sqinter> 1)" apply (subst inf_assoc) by (simp add: inf_commute)    also have "... = x * \<top> \<sqinter> (y * \<top> \<sqinter> 1)" by (subst inf_assoc, simp)    also have "... = (x * \<top>) \<sqinter> (y * \<top>) \<sqinter> 1" by (subst inf_assoc, simp)    finally show "x * \<top> \<sqinter> (y * \<top>) \<sqinter> 1 = x * \<top> \<sqinter> 1 \<sqinter> (y * \<top> \<sqinter> 1)" by simp  qedend context lattice beginlemma [simp]: "x ≤ y ==> x \<sqinter> y = x"  by (simp add: inf_absorb1)endcontext mbt_algebra beginlemma wpt_dual_assertion_comp: "x ∈ assertion ==> y ∈ assertion ==> wpt ((x ^ o) * y) = (neg_assert x) \<squnion> y"  apply (simp add: wpt_def neg_assert_def)  proof -    assume A: "x ∈ assertion"    assume B: "y ∈ assertion"    have C: "((x ^ o) * ⊥) \<squnion> 1 = x ^ o"      by (rule dual_assertion_prop, rule A)    have "x ^ o * y * \<top> \<sqinter> 1 = (((x ^ o) * ⊥) \<squnion> 1) * y * \<top> \<sqinter> 1" by (simp add: C)    also have "… = ((x ^ o) * ⊥ \<squnion> (y * \<top>)) \<sqinter> 1" by (simp add: sup_comp)    also have "… = (((x ^ o) * ⊥) \<sqinter> 1) \<squnion> ((y * \<top>) \<sqinter> 1)" by (simp add: inf_sup_distrib2)    also have "… = (((x ^ o) * ⊥) \<sqinter> 1) \<squnion> y" by (cut_tac B, drule assertion_prop, simp)    finally show "x ^ o * y * \<top> \<sqinter> 1 = (((x ^ o) * ⊥) \<sqinter> 1) \<squnion> y" .  qedlemma le_comp_left_right: "x ≤ y ==> u ≤ v ==> x * u ≤ y * v"  apply (rule_tac y = "x * v" in order_trans)  apply (rule le_comp, simp)  by (rule le_comp_right, simp)lemma wpt_dual_assertion: "x ∈ assertion ==> wpt (x ^ o) = 1"  apply (simp add: wpt_def)  apply (rule antisym)  apply simp_all  apply (cut_tac x = 1 and y = "x ^ o" and u = 1 and v = \<top> in le_comp_left_right)  apply simp_all  apply (subst dual_le)  by simplemma assertion_commute: "x ∈ assertion ==> y ∈ conjunctive ==> y * x = wpt(y * x) * y"  apply (simp add: wpt_def)  apply (simp add: inf_comp)  apply (drule_tac x = y and y = "x * \<top>" and z = 1 in conjunctiveD)  by (simp add: mult_assoc [THEN sym] assertion_prop)lemma wpt_mono: "x ≤ y ==> wpt x ≤ wpt y"  apply (simp add: wpt_def)  apply (rule_tac y = "x * \<top>" in order_trans, simp_all)  by (rule le_comp_right, simp)lemma "a ∈ conjunctive ==> x * a ≤ a * y ==> (x ^ ω) * a ≤ a * (y ^ ω)"  apply (rule omega_least)  apply (simp add: mult_assoc [THEN sym])  apply (rule_tac y = "a * y * y ^ ω \<sqinter> a" in order_trans)  apply (simp)  apply (rule_tac y = "x * a * y ^ ω" in order_trans, simp_all)  apply (rule le_comp_right, simp)  apply (simp add: mult_assoc)  apply (subst (2) omega_fix)  by (simp add: conjunctiveD)lemma [simp]: "x ≤ 1 ==> y * x ≤ y"  by (cut_tac x = x and y = 1 and z = y in le_comp, simp_all)lemma [simp]: "x ≤ x * \<top>"  by (cut_tac x = 1 and y = \<top> and z = x in le_comp, simp_all)lemma [simp]: "x * ⊥ ≤ x"  by (cut_tac x = ⊥ and y = 1 and z = x in le_comp, simp_all)endsubsection{*Monotonic Boolean trasformers algebra with post condition statement*}definition  "post_fun (p::'a::order) q = (if p ≤ q then \<top> else ⊥)"lemma post_mono [simp]: "(post_fun p) ∈ MonoTran"   apply (simp add: post_fun_def MonoTran_def mono_def, safe)   apply (subgoal_tac "p ≤ y", simp)   by (rule_tac y = x in order_trans, simp_all)lemma post_top [simp]: "post_fun p p = \<top>"  by (simp add: post_fun_def)lemma post_refin [simp]: "mono S ==> ((S p)::'a::bounded_lattice) \<sqinter> (post_fun p) x ≤ S x"  apply (simp add: le_fun_def assert_fun_def post_fun_def, safe)  by (rule_tac f = S in monoD, simp_all)class post_mbt_algebra = mbt_algebra +  fixes post :: "'a => 'a"  assumes post_1: "(post x) * x * \<top> = \<top>"  and post_2: "y * x * \<top> \<sqinter> (post x) ≤ y"instantiation MonoTran :: (complete_boolean_algebra) post_mbt_algebrabegindefinition  post_MonoTran_def: "post x = Abs_MonoTran (post_fun ((Rep_MonoTran x) \<top>))"instance proofhave op_p_MonoTran [simp]: "!!p::'a . op \<sqinter> p ∈ MonoTran"   apply (simp add: MonoTran_def mono_def, safe)   by (rule_tac y = x in order_trans, simp_all)  fix x :: "'a MonoTran" show "post x * x * \<top> = \<top>"    apply (simp add: post_MonoTran_def times_MonoTran_def top_MonoTran_def       Abs_MonoTran_inverse Rep_MonoTran_inverse)   by (simp add:  top_fun_def o_def)  fix x y :: "'a MonoTran" show "y * x * \<top> \<sqinter> post x ≤ y"    apply (simp add: post_MonoTran_def times_MonoTran_def top_MonoTran_def Abs_MonoTran_inverse       Rep_MonoTran_inverse inf_MonoTran_def less_eq_MonoTran_def)    by (simp add: le_fun_def bot_fun_def inf_fun_def top_fun_def o_def)qed   endsubsection{*Complete monotonic Boolean transformers algebra*}class complete_mbt_algebra = post_mbt_algebra + complete_distrib_lattice +  assumes Inf_comp: "(Inf X) * z = (INF x : X . (x * z))"instantiation MonoTran :: (complete_boolean_algebra) complete_mbt_algebrabegininstance proof  fix z :: "'a MonoTran" fix X show "Inf X * z = (INF x:X. x * z)"    apply (simp add: INF_def Inf_MonoTran_def times_MonoTran_def Inf_comp_fun Abs_MonoTran_inverse sup_Inf)    apply (subgoal_tac "{g::'a => 'a. ∃m::'a MonoTran∈X. g = Rep_MonoTran m o Rep_MonoTran z} =         Rep_MonoTran  (λx::'a MonoTran. Abs_MonoTran (Rep_MonoTran x o Rep_MonoTran z))  X")    apply simp    apply (simp add: image_def, safe)    apply (rule_tac x = "Abs_MonoTran (Rep_MonoTran m o Rep_MonoTran z)" in exI)    apply (simp_all add: Abs_MonoTran_inverse)    by autoqedendcontext complete_mbt_algebra beginlemma dual_Inf: "(Inf X) ^ o = (SUP x: X . x ^ o)"  apply (rule antisym)  apply (simp_all add: SUP_def)  apply (subst dual_le, simp)  apply (rule Inf_greatest)  apply (subst dual_le, simp)  apply (rule Sup_upper, simp)  apply (rule Sup_least, safe)  apply (subst dual_le, simp)  by (rule Inf_lower, simp)lemma dual_Sup: "(Sup X) ^ o = (INF x: X . x ^ o)"  apply (rule antisym)  apply (simp_all add: INF_def)  apply (rule Inf_greatest, safe)  apply (subst dual_le, simp)  apply (rule Sup_upper, simp)  apply (subst dual_le, simp)  apply (rule Sup_least)  apply (subst dual_le, simp)  by (rule Inf_lower, simp)lemma INFI_comp: "(INFI A f) * z = (INF a : A . (f a) * z)"  apply (simp add: INF_def Inf_comp)  apply (subgoal_tac "((λx::'a. x * z)  f  A) = ((λa::'b. f a * z)  A)")  by autolemma dual_INFI: "(INFI A f) ^ o = (SUP a : A . (f a) ^ o)"  apply (simp add: INF_def dual_Inf SUP_def)  apply (subgoal_tac "(dual  f  A) = ((λa::'b. f a ^ o)  A)")  by autolemma dual_SUPR: "(SUPR A f) ^ o = (INF a : A . (f a) ^ o)"  apply (simp add: INF_def dual_Sup SUP_def)  apply (subgoal_tac "(dual  f  A) = ((λa::'b. f a ^ o)  A)")  by autolemma Sup_comp: "(Sup X) * z = (SUP x : X . (x * z))"  apply (rule dual_eq)  by (simp add: dual_comp dual_Sup dual_SUPR INFI_comp)lemma SUPR_comp: "(SUPR A f) * z = (SUP a : A . (f a) * z)"  apply (simp add: SUP_def Sup_comp)  apply (subgoal_tac "((λx::'a. x * z)  f  A) = ((λa::'b. f a * z)  A)")  by autolemma Sup_assertion [simp]: "X ⊆ assertion ==> Sup X ∈ assertion"  apply (unfold assertion_def)  apply safe  apply (rule Sup_least)  apply blast  apply (simp add: Sup_comp dual_Sup SUP_def Sup_inf)  apply (subgoal_tac "((λy . y \<sqinter> INFI X dual)  (λx . x * \<top>)  X) = X")  apply simp  proof -    assume A: "X ⊆ {x. x ≤ 1 ∧ x * \<top> \<sqinter> x ^ o = x}"    have B [simp]: "!! x . x ∈ X ==>  x * \<top> \<sqinter> (INFI X dual) = x"      proof -        fix x        assume C: "x ∈ X"        have "x * \<top> \<sqinter> INFI X dual = x * \<top> \<sqinter> (x ^ o \<sqinter> INFI X dual)"          apply (subgoal_tac "INFI X dual = (x ^ o \<sqinter> INFI X dual)", simp)          apply (rule antisym, simp_all)          by (unfold INF_def, rule Inf_lower, cut_tac C, simp)        also have "… = x \<sqinter> INFI X dual" by (unfold  inf_assoc [THEN sym], cut_tac A, cut_tac C, auto)        also have "… = x"          apply (rule antisym, simp_all)          apply (simp add: INF_def)          apply (rule Inf_greatest, safe)          apply (cut_tac A C)          apply (rule_tac y = 1 in order_trans)          apply auto[1]          by (subst dual_le, auto)        finally show "x * \<top> \<sqinter> INFI X dual = x" .      qed      show "(λy. y \<sqinter> INFI X dual)  (λx . x * \<top>)  X = X"        by (unfold image_def, auto)    qedlemma Sup_range_assertion [simp]: "(!!w . p w ∈ assertion) ==> Sup (range p) ∈ assertion"  by (rule Sup_assertion, auto)lemma Sup_less_assertion [simp]: "(!!w . p w ∈ assertion) ==> Sup_less p w ∈ assertion"  by (unfold Sup_less_def, rule Sup_assertion, auto)theorem omega_lfp:   "x ^ ω * y = lfp (λ z . (x * z) \<sqinter> y)"  apply (rule antisym)  apply (rule lfp_greatest)  apply (drule omega_least, simp)  apply (rule lfp_lowerbound)  apply (subst (2) omega_fix)  by (simp add: inf_comp mult_assoc)endlemma [simp]: "mono (λ (t::'a::mbt_algebra) . x * t \<sqinter> y)"  apply (simp add: mono_def, safe)  apply (rule_tac y = "x * xa" in order_trans, simp)  by (rule le_comp, simp)class mbt_algebra_fusion = mbt_algebra +  assumes fusion: "(∀ t . x * t \<sqinter> y \<sqinter> z ≤ u * (t \<sqinter> z) \<sqinter> v)          ==> (x ^ ω) * y \<sqinter> z ≤ (u ^ ω) * v "lemma     "class.mbt_algebra_fusion (1::'a::complete_mbt_algebra) (op *) (op \<sqinter>) (op ≤) (op <) (op \<squnion>) dual dual_star omega star ⊥ \<top>"    apply unfold_locales    apply (cut_tac h = "λ t . t \<sqinter> z" and f = "λ t . x * t \<sqinter> y" and g = "λ t . u * t \<sqinter> v" in weak_fusion)    apply (rule inf_Disj)    apply simp_all    apply (simp add: le_fun_def)    by  (simp add: omega_lfp)context mbt_algebra_fusionbeginlemma omega_star: "x ∈ conjunctive ==> x ^ ω = wpt (x ^ ω) * (x ^ *)"  apply (simp add: wpt_def inf_comp)  apply (rule antisym)  apply (cut_tac x = x and y = 1 and z = "x ^ ω * \<top> \<sqinter> x ^ *" in omega_least)  apply (simp_all add: conjunctiveD,safe)  apply  (subst (2) omega_fix)  apply (simp add: inf_comp inf_assoc mult_assoc)  apply (metis inf.commute inf_assoc inf_le1 star_fix)  apply (cut_tac x = x and y = \<top> and z = "x ^ *" and u = x and v = 1 in fusion)  apply (simp add: conjunctiveD)  apply (metis inf_commute inf_le1 le_infE star_fix)  by (metis mult.right_neutral)lemma omega_pres_conj: "x ∈ conjunctive ==> x ^ ω ∈ conjunctive"  apply (subst omega_star, simp)  apply (rule comp_pres_conj)  apply (rule assertion_conjunctive, simp)  by (rule start_pres_conj, simp)endend