# Theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra

section ‹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 + order_top + order_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]: "⊤ * x = ⊤"
and inf_comp: "(x ⊓ y) * z = (x * z) ⊓ (y * z)"
and le_comp: "x ≤ y ⟹ z * x ≤ z * y"
and dual_neg: "(x * ⊤) ⊓ (x ^ o * ⊥) = ⊥"
and omega_fix: "x ^ ω = (x * (x ^ ω)) ⊓ 1"
and omega_least: "(x * z) ⊓ y ≤ z ⟹ (x ^ ω) * y ≤ z"
and star_fix: "x ^ * = (x * (x ^ *)) ⊓ 1"
and star_greatest: "z ≤ (x * z) ⊓ 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 ⊓ (y * z) ≤ y * z")
apply simp
by (rule inf_le2)

subclass bounded_lattice
proof qed

end

instantiation MonoTran :: (complete_boolean_algebra) mbt_algebra
begin

lift_definition dual_MonoTran :: "'a MonoTran ⇒ 'a MonoTran"
is dual_fun
by (fact mono_dual_fun)

lift_definition omega_MonoTran :: "'a MonoTran ⇒ 'a MonoTran"
is omega_fun
by (fact mono_omega_fun)

lift_definition star_MonoTran :: "'a MonoTran ⇒ 'a MonoTran"
is star_fun
by (fact mono_star_fun)

definition dual_star_MonoTran :: "'a MonoTran ⇒ 'a MonoTran"
where
"(x::('a MonoTran)) ^ ⊗ = ((x ^ o) ^ *) ^ o"

instance proof
fix x y :: "'a MonoTran" show "(x ≤ y) = (y ^ o ≤ x ^ o)"
apply transfer
apply (auto simp add: fun_eq_iff le_fun_def)
apply (drule_tac x = "-xa" in spec)
apply simp
done
next
fix x :: "'a MonoTran" show "(x ^ o) ^ o = x"
apply transfer
apply (simp add: fun_eq_iff)
done
next
fix x y :: "'a MonoTran" show "(x * y) ^ o = x ^ o * y ^ o"
apply transfer
apply (simp add: fun_eq_iff)
done
next
show "(1::'a MonoTran) ^ o = 1"
apply transfer
apply (simp add: fun_eq_iff)
done
next
fix x :: "'a MonoTran" show "⊤ * x = ⊤"
apply transfer
apply (simp add: fun_eq_iff)
done
next
fix x y z :: "'a MonoTran" show "(x ⊓ y) * z = (x * z) ⊓ (y * z)"
apply transfer
apply (simp add: fun_eq_iff)
done
next
fix x y z :: "'a MonoTran" assume A: "x ≤ y" from A show " z * x ≤ z * y"
apply transfer
apply (auto simp add: le_fun_def elim: monoE)
done
next
fix x :: "'a MonoTran" show "x * ⊤ ⊓ (x ^ o * ⊥) = ⊥"
apply transfer
apply (simp add: fun_eq_iff)
done
next
fix x :: "'a MonoTran" show "x ^ ω = x * x ^ ω ⊓ 1"
apply transfer
apply (simp add: fun_eq_iff)
apply (simp add: omega_fun_def Omega_fun_def)
apply (subst lfp_unfold, simp_all add: ac_simps)
apply (auto intro!: mono_comp mono_comp_fun)
done
next
fix x y z :: "'a MonoTran" assume A: "x * z ⊓ y ≤ z" from A show "x ^ ω * y ≤ z"
apply transfer
apply (auto simp add: lfp_omega lfp_def)
apply (rule Inf_lower)
apply (auto simp add: Omega_fun_def ac_simps)
done
next
fix x :: "'a MonoTran" show "x ^ * = x * x ^ * ⊓ 1"
apply transfer
apply (auto simp add: star_fun_def Omega_fun_def)
apply (subst gfp_unfold, simp_all add: ac_simps)
apply (auto intro!: mono_comp mono_comp_fun)
done
next
fix x y z :: "'a MonoTran" assume A: "z ≤ x * z ⊓ y" from A show "z ≤ x ^ * * y"
apply transfer
apply (auto simp add: gfp_star gfp_def)
apply (rule Sup_upper)
apply (auto simp add: Omega_fun_def)
done
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]: "⊤ ^ o = ⊥"
apply (rule order.antisym, simp_all)
by (subst dual_le, simp)

lemma dual_bot [simp]: "⊥ ^ o = ⊤"
apply (rule order.antisym, simp_all)
by (subst dual_le, simp)

lemma dual_inf: "(x ⊓ y) ^ o = (x ^ o) ⊔ (y ^ o)"
apply (rule order.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 ⊔ y) ^ o = (x ^ o) ⊓ (y ^ o)"
apply (rule order.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 ⊔ y) * z = (x * z) ⊔ (y * z)"
apply (subgoal_tac "((x ^ o ⊓ y ^ o) * z ^ o) ^ o = ((x ^ o * z ^ o) ⊓ (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 * ⊥) ⊔ (x * ⊤) = ⊤"
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 * ⊤) * y = x * ⊤"
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) ⊓ y"
apply (subst omega_fix)
by (simp add: inf_comp)

theorem dual_star_fix: "x^⊗ = (x * (x^⊗)) ⊔ 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) ⊓ y"
apply (subst star_fix)
by (simp add: inf_comp)

theorem dual_star_comp_fix: "x^⊗ * y = (x * (x^⊗) * y) ⊔ y"
apply (subst dual_star_fix)
by (simp add: sup_comp)

theorem dual_star_least: "(x * z) ⊔ 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 order.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 order.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 * ⊤) ⊓ (x ^ o) = x}"

lemma assertion_prop: "x ∈ assertion ⟹ (x * ⊤) ⊓ 1 = x"
apply (simp add: assertion_def)
apply safe
apply (rule order.antisym)
apply simp_all
proof -
assume [simp]: "x ≤ 1"
assume A: "x * ⊤ ⊓ x ^ o = x"
have "x * ⊤ ⊓ 1 ≤ x * ⊤ ⊓ 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 * ⊤ ⊓ 1 ≤ x" .
next
assume A: "x * ⊤ ⊓ x ^ o = x"
have "x = x * ⊤ ⊓ x ^ o" by (simp add: A)
also have "… ≤ x * ⊤" by simp
finally show "x ≤ x * ⊤" .
qed

lemma dual_assertion_prop: "x ∈ assertion ⟹ ((x ^ o) * ⊥) ⊔ 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 * ⊤ ⊓ 1 = x"
fix y z::"'a"
have "x * (y ⊔ z) = (x * ⊤ ⊓ 1) * (y ⊔ z)" by (cut_tac  A, simp)
also have "… = (x * ⊤) ⊓ (y ⊔ z)" by (simp add: inf_comp)
also have "… = ((x * ⊤) ⊓ y) ⊔ ((x * ⊤) ⊓ z)" by (simp add: inf_sup_distrib)
also have "… = (((x * ⊤) ⊓ 1) * y) ⊔ (((x * ⊤) ⊓ 1) * z)" by (simp add: inf_comp)
also have "… = x * y ⊔ x * z" by (cut_tac  A, simp)
finally show "x * (y ⊔ z) = x * y ⊔ x * z" .
qed

lemma Abs_MonoTran_injective: "mono x ⟹ mono y ⟹ 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 (simp add: disjunctive_def Apply.disjunctive_def)
apply transfer
apply auto
proof -
fix f :: "'a ⇒ 'a" and a b
assume prem: "∀y. mono y ⟶ (∀z. mono z ⟶ f ∘ y ⊔ z = (f ∘ y) ⊔ (f ∘ z))"
{ fix g h :: "'b ⇒ 'a"
assume "mono g" and "mono h"
then have "f ∘ g ⊔ h = (f ∘ g) ⊔ (f ∘ h)"
using prem by blast
} note * = this
assume "mono f"
show "f (a ⊔ b) = f a ⊔ f b" (is "?P = ?Q")
proof (rule order_antisym)
show "?P ≤ ?Q"
using * [of "λ_. a" "λ_. b"] by (simp add: comp_def fun_eq_iff)
next
from ‹mono f› show "?Q ≤ ?P"
using Fun.semilattice_sup_class.mono_sup by blast
qed
next
fix f :: "'a ⇒ 'a"
assume "∀y z. f (y ⊔ z) = f y ⊔ f z"
then have *: "⋀y z. f (y ⊔ z) = f y ⊔ f z" by blast
show "mono f"
proof
fix a b :: 'a
assume "a ≤ b"
then show "f a ≤ f b"
unfolding sup.order_iff * [symmetric] by simp
qed
qed

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 * ⊤ ⊓ 1 = x"
fix y z::"'a"
have "x * (y ⊓ z) = (x * ⊤ ⊓ 1) * (y ⊓ z)" by (cut_tac  A, simp)
also have "… = (x * ⊤) ⊓ (y ⊓ z)" by (simp add: inf_comp)
also have "… = ((x * ⊤) ⊓ y) ⊓ ((x * ⊤) ⊓ z)"
apply (rule order.antisym, simp_all, safe)
apply (rule_tac y = "y ⊓ z" in order_trans)
apply (rule inf_le2)
apply simp
apply (rule_tac y = "y ⊓ z" in order_trans)
apply (rule inf_le2)
apply simp_all
apply (simp add: inf_assoc)
apply (rule_tac y = " x * ⊤ ⊓ y" in order_trans)
apply (rule inf_le1)
apply simp
apply (rule_tac y = " x * ⊤ ⊓ z" in order_trans)
apply (rule inf_le2)
by simp
also have "… = (((x * ⊤) ⊓ 1) * y) ⊓ (((x * ⊤) ⊓ 1) * z)" by (simp add: inf_comp)
also have "… = (x * y) ⊓ (x * z)" by (cut_tac  A, simp)
finally show "x * (y ⊓ z) = (x * y) ⊓ (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 ⊓ y ≤ x * y"
apply (simp add: assertion_def, safe)
proof -
assume A: "x ≤ 1"
assume B: "x * ⊤ ⊓ x ^ o = x"
assume C: "y ≤ 1"
assume D: "y * ⊤ ⊓ y ^ o = y"
have "x ⊓ y = (x * ⊤ ⊓ x ^ o) ⊓ (y * ⊤ ⊓ y ^ o)" by (cut_tac B D, simp)
also have "… ≤ (x * ⊤) ⊓ (((x^o) * (y * ⊤)) ⊓ ((x^o) * (y^o)))"
apply (simp, safe)
apply (rule_tac y = "x * ⊤ ⊓ x ^ o" in order_trans)
apply (rule inf_le1)
apply simp
apply (rule_tac y = "y * ⊤" in order_trans)
apply (rule_tac y = "y * ⊤ ⊓ 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 * ⊤ ⊓ 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 * ⊤) ⊓ (x ^ o)) * ((y * ⊤) ⊓ (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 ⊓ 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 * ⊤) ⊓ (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 ⊓ y = x * y"
by (rule order.antisym, simp_all)

lemma one_right_assertion [simp]: "x ∈ assertion ⟹ x * 1 = x"
apply (drule assertion_prop)
proof -
assume A: "x * ⊤ ⊓ 1 = x"
have "x * 1 = (x * ⊤ ⊓ 1) * 1" by (simp add: A)
also have "… = x * ⊤ ⊓ 1" by (simp add: inf_comp)
also have "… = x" by (simp add: A)
finally show ?thesis .
qed

lemma [simp]: "x ∈ assertion ⟹ x ⊔ 1 = 1"
by (rule order.antisym, simp_all add: assertion_def)

lemma [simp]: "x ∈ assertion ⟹ 1 ⊔ x = 1"
by (rule order.antisym, simp_all add: assertion_def)

lemma [simp]: "x ∈ assertion ⟹ x ⊓ 1 = x"
by (rule order.antisym, simp_all add: assertion_def)

lemma [simp]: "x ∈ assertion ⟹ 1 ⊓ x = x"
by (rule order.antisym, simp_all add: assertion_def)

lemma [simp]:  "x ∈ assertion ⟹ x ≤ x * ⊤"
by (cut_tac x = 1 and y = ⊤ 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 * ⊥) ⊓ 1"

lemma sup_uminus[simp]: "x ∈ assertion ⟹ x ⊔ neg_assert x = 1"
apply (simp add: neg_assert_def)
apply (simp add: sup_inf_distrib)
apply (rule order.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 ⊓ neg_assert x = ⊥"
apply (simp add: neg_assert_def)
apply (rule order.antisym, simp_all)
apply (rule_tac y = "x ⊓ (x ^ o * ⊥)" in order_trans)
apply simp
apply (rule_tac y = "x ^ o * ⊥ ⊓ 1" in order_trans)
apply (rule inf_le2)
apply simp
apply (rule_tac y = "(x * ⊤)  ⊓ (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 ⊔ (neg_assert x) * ⊤ = x ^ o * y"
apply (simp add: neg_assert_def inf_comp)
apply (rule order.antisym, simp_all)
by (rule le_comp, simp)

lemma [simp]: "(neg_assert x) ^ o * y ⊔ x * ⊤ = (neg_assert x) ^ o * y"
apply (simp add: neg_assert_def inf_comp dual_inf dual_comp sup_comp)
by (rule order.antisym, simp_all)

lemma [simp]: " x * ⊤ ⊔ (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 ⊓ 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 * ⊤) ⊓ (x ^ o) = x"
by (cut_tac A, unfold assertion_def, simp)
have D: "(y * ⊤) ⊓ (y ^ o) = y"
by (cut_tac B, unfold assertion_def, simp)
have "x * y = ((x * ⊤) ⊓ (x ^ o)) * ((y * ⊤) ⊓ (y ^ o))" by (simp add: C D)
also have "… = x * ⊤ ⊓ ((x ^ o) * ((y * ⊤) ⊓ (y ^ o)))" by (simp add: inf_comp)
also have "… =  x * ⊤ ⊓ ((x ^ o) * (y * ⊤)) ⊓ ((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 * ⊤) ⊓ (x ^ o)) * (y * ⊤)) ⊓ ((x ^ o) *(y ^ o))"
by (simp add: inf_comp)
also have "… = (x * y * ⊤)  ⊓ ((x * y) ^ o)" by (simp add: C mult.assoc dual_comp)
finally show "(x * y * ⊤)  ⊓ ((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 ⊔ 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 * ⊤ ⊓ x ^ o = x"
assume B: "y * ⊤ ⊓ y ^ o = y"
have "(y * ⊤) ⊓ (x ^ o) ⊓ (y ^ o) = (x ^ o) ⊓ (y * ⊤) ⊓ (y ^ o)" by (simp add: inf_commute)
also have "… = (x ^ o) ⊓ ((y * ⊤) ⊓ (y ^ o))" by (simp add: inf_assoc)
also have "… = (x ^ o) ⊓ y" by (simp add: B)
also have "… = y"
apply (rule order.antisym, simp_all)
apply (rule_tac y = 1 in order_trans)
apply simp
by (subst dual_le, simp)
finally have [simp]: "(y * ⊤) ⊓ (x ^ o) ⊓ (y ^ o) = y" .
have "x * ⊤ ⊓ (x ^ o) ⊓ (y ^ o) = x ⊓ (y ^ o)"  by (simp add: A)
also have "… = x"
apply (rule order.antisym, simp_all)
apply (rule_tac y = 1 in order_trans)
apply simp
by (subst dual_le, simp)
finally have [simp]: "x * ⊤ ⊓ (x ^ o) ⊓ (y ^ o) = x" .
have "(x ⊔ y) * ⊤ ⊓ (x ⊔ y) ^ o = (x * ⊤ ⊔ y * ⊤) ⊓ ((x ^ o) ⊓ (y ^ o))" by (simp add: sup_comp dual_sup)
also have "… = x ⊔ y" by (simp add: inf_sup_distrib inf_assoc [THEN sym])
finally show "(x ⊔ y) * ⊤ ⊓ (x ⊔ y) ^ o = x ⊔ 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 * ⊤ ⊓ (x ^ o) = x" by (cut_tac A, unfold assertion_def, simp)
have "x * x ^ o = (x * ⊤ ⊓ (x ^ o)) * x ^ o" by (simp add: B)
also have "… = x * ⊤ ⊓ (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 * ⊤) ⊓ 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 order.antisym)
by (simp_all add: dual_neg)

lemma wpt_comp: "(wpt x) * x = x"
apply (simp add: wpt_def inf_comp)
apply (rule order.antisym, simp_all)
by (cut_tac x = 1 and y = ⊤ 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 * ⊤ ⊓ 1 = x * (y * ⊤) ⊓ 1" by (simp add: B mult.assoc [THEN sym])
also have "… ≤ x * ⊤ ⊓ 1"
apply simp
apply (rule_tac y = "x * (y * ⊤)" 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 * ⊤ ⊓ 1 ≤ x" .
qed

lemma wpt_choice: "wpt (x ⊓ y) = wpt x ⊓ wpt y"
apply (simp add: wpt_def inf_comp)
proof -
have "x * ⊤ ⊓ 1 ⊓ (y * ⊤ ⊓ 1) = x * ⊤ ⊓ ((y * ⊤ ⊓ 1) ⊓ 1)" apply (subst inf_assoc) by (simp add: inf_commute)
also have "... = x * ⊤ ⊓ (y * ⊤ ⊓ 1)" by (subst inf_assoc, simp)
also have "... = (x * ⊤) ⊓ (y * ⊤) ⊓ 1" by (subst inf_assoc, simp)
finally show "x * ⊤ ⊓ (y * ⊤) ⊓ 1 = x * ⊤ ⊓ 1 ⊓ (y * ⊤ ⊓ 1)" by simp
qed
end

context lattice begin
lemma [simp]: "x ≤ y ⟹ x ⊓ 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) ⊔ y"
apply (simp add: wpt_def neg_assert_def)
proof -
assume A: "x ∈ assertion"
assume B: "y ∈ assertion"
have C: "((x ^ o) * ⊥) ⊔ 1 = x ^ o"
by (rule dual_assertion_prop, rule A)
have "x ^ o * y * ⊤ ⊓ 1 = (((x ^ o) * ⊥) ⊔ 1) * y * ⊤ ⊓ 1" by (simp add: C)
also have "… = ((x ^ o) * ⊥ ⊔ (y * ⊤)) ⊓ 1" by (simp add: sup_comp)
also have "… = (((x ^ o) * ⊥) ⊓ 1) ⊔ ((y * ⊤) ⊓ 1)" by (simp add: inf_sup_distrib2)
also have "… = (((x ^ o) * ⊥) ⊓ 1) ⊔ y" by (cut_tac B, drule assertion_prop, simp)
finally show "x ^ o * y * ⊤ ⊓ 1 = (((x ^ o) * ⊥) ⊓ 1) ⊔ 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 order.antisym)
apply simp_all
apply (cut_tac x = 1 and y = "x ^ o" and u = 1 and v = ⊤ 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 * ⊤" 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 * ⊤" 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 ^ ω ⊓ 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 * ⊤"
by (cut_tac x = 1 and y = ⊤ 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 (⊤::'b::{order_bot,order_top}) else ⊥)"

lemma mono_post_fun [simp]: "mono (post_fun (p::_::{order_bot,order_top}))"
apply (simp add: post_fun_def mono_def, safe)
apply (subgoal_tac "p ≤ y", simp)
apply (rule_tac y = x in order_trans)
apply simp_all
done

lemma post_top [simp]: "post_fun p p = ⊤"
by (simp add: post_fun_def)

lemma post_refin [simp]: "mono S ⟹ ((S p)::'a::bounded_lattice) ⊓ (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 * ⊤ = ⊤"
and post_2: "y * x * ⊤ ⊓ (post x) ≤ y"

instantiation MonoTran :: (complete_boolean_algebra) post_mbt_algebra
begin

lift_definition post_MonoTran :: "'a::complete_boolean_algebra MonoTran ⇒ 'a::complete_boolean_algebra MonoTran"
is "λx. post_fun (x ⊤)"
by (rule mono_post_fun)

instance proof
fix x :: "'a MonoTran" show "post x * x * ⊤ = ⊤"
apply transfer
apply (simp add: fun_eq_iff)
done
fix x y :: "'a MonoTran" show "y * x * ⊤ ⊓ post x ≤ y"
apply transfer
apply (simp add: le_fun_def)
done
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))"

instance MonoTran :: (complete_boolean_algebra) complete_mbt_algebra
apply intro_classes
apply transfer
apply (simp add: Inf_comp_fun)
done

context complete_mbt_algebra begin
lemma dual_Inf: "(Inf X) ^ o = (SUP x∈ X . x ^ o)"
apply (rule order.antisym)
apply (subst dual_le, simp)
apply (rule Inf_greatest)
apply (subst dual_le, simp)
apply (rule SUP_upper, simp)
apply (rule SUP_least)
apply (subst dual_le, simp)
by (rule Inf_lower, simp)

lemma dual_Sup: "(Sup X) ^ o = (INF x∈ X . x ^ o)"
apply (rule order.antisym)
apply (rule INF_greatest)
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 INF_comp: "(⨅(f  A)) * z = (INF a ∈ A . (f a) * z)"
unfolding Inf_comp
apply (subgoal_tac "((λx::'a. x * z)  f  A) = ((λa::'b. f a * z)  A)")
by auto

lemma dual_INF: "(⨅(f  A)) ^ o = (SUP a ∈ A . (f a) ^ o)"
unfolding Inf_comp dual_Inf
apply (subgoal_tac "(dual  f  A) = ((λa::'b. f a ^ o)  A)")
by auto

lemma dual_SUP: "(⨆(f  A)) ^ o = (INF a ∈ A . (f a) ^ o)"
unfolding dual_Sup
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_SUP INF_comp image_comp)

lemma SUP_comp: "(⨆(f  A)) * z = (SUP a ∈ A . (f a) * z)"
unfolding 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_inf)
apply (subgoal_tac "((λy . y ⊓ ⨅(dual  X))  (λx . x * ⊤)  X) = X")
apply simp
proof -
assume A: "X ⊆ {x. x ≤ 1 ∧ x * ⊤ ⊓ x ^ o = x}"
have B [simp]: "!! x . x ∈ X ⟹  x * ⊤ ⊓ (⨅(dual  X)) = x"
proof -
fix x
assume C: "x ∈ X"
have "x * ⊤ ⊓ ⨅(dual  X) = x * ⊤ ⊓ (x ^ o ⊓ ⨅(dual  X))"
apply (subgoal_tac "⨅(dual  X) = (x ^ o ⊓ ⨅(dual  X))", simp)
apply (rule order.antisym, simp_all)
apply (rule Inf_lower, cut_tac C, simp)
done
also have "… = x ⊓ ⨅(dual  X)" by (unfold  inf_assoc [THEN sym], cut_tac A, cut_tac C, auto)
also have "… = x"
apply (rule order.antisym, simp_all)
apply (rule INF_greatest)
apply (cut_tac A C)
apply (rule_tac y = 1 in order_trans)
apply auto[1]
apply (subst dual_le, auto)
done
finally show "x * ⊤ ⊓ ⨅(dual  X) = x" .
qed
show "(λy. y ⊓ ⨅(dual  X))  (λx . x * ⊤)  X = X"
by (simp add: image_comp)
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) ⊓ y)"
apply (rule order.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 ⊓ 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 ⊓ y ⊓ z ≤ u * (t ⊓ z) ⊓ v)
⟹ (x ^ ω) * y ⊓ z ≤ (u ^ ω) * v "

lemma
"class.mbt_algebra_fusion (1::'a::complete_mbt_algebra) ((*)) (⊓) (≤) (<) (⊔) dual dual_star omega star ⊥ ⊤"
apply unfold_locales
apply (cut_tac h = "λ t . t ⊓ z" and f = "λ t . x * t ⊓ y" and g = "λ t . u * t ⊓ 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 order.antisym)
apply (cut_tac x = x and y = 1 and z = "x ^ ω * ⊤ ⊓ 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 = ⊤ 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
`