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