Up to index of Isabelle/HOL/LatticeProperties/MonoBoolTranAlgebra
theory Mono_Bool_Tran_Algebraheader {* Algebra of Monotonic Boolean Transformers *}
theory Mono_Bool_Tran_Algebra
imports Mono_Bool_Tran
begin
text{*
In this section we introduce the {\em algebra of monotonic boolean transformers}.
This is a bounded distributive lattice with a monoid operation, a
dual operator and an iteration operator. The standard model for this
algebra is the set of monotonic boolean transformers introduced
in 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)"
begin
lemma 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 qed
end
instantiation MonoTran :: (complete_boolean_algebra) mbt_algebra
begin
definition
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 simp
next
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)
qed
end
context mbt_algebra begin
lemma 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_all
lemma 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)
end
sublocale mbt_algebra < conjunctive "inf" "inf" "times"
done
sublocale mbt_algebra < disjunctive "sup" "sup" "times"
done
context mbt_algebra begin
lemma 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 assertions
or assumptions are defined using an existential quantifier. An element of the algebra
is a test if it has a complement with respect to $\bot$ and $1$. In this formalization
assertions 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>" .
qed
lemma 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" .
qed
lemma 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)
end
lemma 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 begin
lemma 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)" .
qed
lemma 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 .
qed
lemma [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 simp
lemma 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
qed
lemma 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" .
qed
lemma [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 .
qed
lemma [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" .
qed
lemma 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
qed
end
context lattice begin
lemma [simp]: "x ≤ y ==> x \<sqinter> y = x"
by (simp add: inf_absorb1)
end
context mbt_algebra begin
lemma 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" .
qed
lemma 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 simp
lemma 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)
end
subsection{*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_algebra
begin
definition
post_MonoTran_def: "post x = Abs_MonoTran (post_fun ((Rep_MonoTran x) \<top>))"
instance proof
have 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
end
subsection{*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_algebra
begin
instance 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 auto
qed
end
context complete_mbt_algebra begin
lemma 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 auto
lemma 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 auto
lemma 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 auto
lemma 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 auto
lemma 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)
qed
lemma 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)
end
lemma [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_fusion
begin
lemma 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)
end
end