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