Theory Assertion_Algebra

section ‹Boolean Algebra of Assertions›

theory  Assertion_Algebra
imports Mono_Bool_Tran_Algebra
begin

text‹
This section introduces the boolean algebra of assertions. The 
type $\mathsf{Assertion}$ and the boolean operation are instroduced 
based on the set $\mathsf{assertion}$ and the operations on the monotonic 
boolean transformers algebra. The type $\mathsf{Assertion}$ over
a complete monotonic boolean transformers algebra is a complete boolean 
algebra.
›

typedef (overloaded) ('a::mbt_algebra) Assertion = "assertion::'a set"
  apply (rule_tac x = "" in exI)
  by (unfold assertion_def, simp)

definition
  assert :: "'a::mbt_algebra Assertion  'a"  ("{⋅ _ }" [0] 1000) where
  "{⋅p} =  Rep_Assertion p"

definition 
  "abs_wpt x = Abs_Assertion (wpt x)"

lemma [simp]: "{⋅p}  assertion"
  by (unfold assert_def, cut_tac x = p in Rep_Assertion, simp)

lemma [simp]: "abs_wpt ({⋅p}) = p"
  apply (simp add: abs_wpt_def)
  by (simp add: assert_def Rep_Assertion_inverse)


lemma [simp]: "x  assertion  {⋅Abs_Assertion x} = x"
  apply (simp add: assert_def)
  by (rule Abs_Assertion_inverse, simp)

  
lemma [simp]: "x  assertion  {⋅abs_wpt x} = x"
  apply (simp add: abs_wpt_def assert_def)
  by (rule Abs_Assertion_inverse, simp)

lemma assert_injective: "{⋅p} = {⋅q}  p = q"
  proof -
    assume A: "{⋅ p } = {⋅ q } "
    have "p = abs_wpt ({⋅p})" by simp
    also have "... = q" by (subst A, simp)
    finally show ?thesis .
  qed

instantiation Assertion :: (mbt_algebra) boolean_algebra
begin
  definition
    uminus_Assertion_def: "- p = abs_wpt(neg_assert {⋅p})"

  definition
    bot_Assertion_def: " = abs_wpt "

  definition
    top_Assertion_def: " = abs_wpt 1"

  definition
    inf_Assertion_def: "p  q = abs_wpt ({⋅p}  {⋅q})"
  
  definition
    sup_Assertion_def: "p  q = abs_wpt ({⋅p}  {⋅q})"

  definition 
    less_eq_Assertion_def: "(p  q) = ({⋅p}   {⋅q})"

  definition 
    less_Assertion_def: "(p < q) = ({⋅p} < {⋅q})"

  definition 
    minus_Assertion_def: "(p::'a Assertion) - q = p  - q"

instance
  proof
    fix x y :: "'a Assertion" show "(x < y) = (x  y  ¬ y  x)"
      by (simp add: less_Assertion_def less_eq_Assertion_def less_le_not_le)
  next
    fix x ::"'a Assertion" show "x  x" by (simp add: less_eq_Assertion_def)
  next
    fix x y z :: "'a Assertion" assume A: "x  y" assume B: "y  z" from A and B show "x  z"
      by (simp add: less_eq_Assertion_def)
  next
    fix x y :: "'a Assertion" assume A: "x  y" assume B: "y  x" from A and B show "x = y"
      apply (cut_tac p = x and q = y in assert_injective)
      by (rule antisym, simp_all add: less_eq_Assertion_def)
  next
    fix x y :: "'a Assertion" show "x  y  x"
      by (simp add: less_eq_Assertion_def inf_Assertion_def)
    fix x y :: "'a Assertion" show "x  y  y"
      by (simp add: less_eq_Assertion_def inf_Assertion_def)
  next
    fix x y z :: "'a Assertion" assume A: "x  y" assume B: "x  z" from A and B show "x  y  z"
      by (simp add: less_eq_Assertion_def inf_Assertion_def)
  next
    fix x y :: "'a Assertion" show "x  x  y"
      by (simp add: less_eq_Assertion_def sup_Assertion_def)
    fix x y :: "'a Assertion" show "y  x  y"
      by (simp add: less_eq_Assertion_def sup_Assertion_def)
  next
    fix x y z :: "'a Assertion" assume A: "y  x" assume B: "z  x" from A and B show "y  z  x"
      by (simp add: less_eq_Assertion_def sup_Assertion_def)
  next
    fix x :: "'a Assertion" show "  x"
      by (simp add: less_eq_Assertion_def bot_Assertion_def)
  next
    fix x :: "'a Assertion" show "x  "
      by (simp add: less_eq_Assertion_def top_Assertion_def)
  next
    fix x y z :: "'a Assertion" show "x  y  z = (x  y)  (x  z)"
      by (simp add: less_eq_Assertion_def sup_Assertion_def inf_Assertion_def sup_inf_distrib)
  next
    fix x :: "'a Assertion" show "x  - x = "
      by (simp add: inf_Assertion_def uminus_Assertion_def bot_Assertion_def)
  next
    fix x :: "'a Assertion" show "x  - x = "
      by (simp add: sup_Assertion_def uminus_Assertion_def top_Assertion_def)
  next
    fix x y :: "'a Assertion" show "x - y = x  - y"
      by (simp add: minus_Assertion_def)
  qed

end


lemma assert_image [simp]: "assert ` A  assertion"
  by auto

instantiation Assertion :: (complete_mbt_algebra) complete_lattice
begin
  definition
    Sup_Assertion_def: "Sup A = abs_wpt (Sup (assert ` A))"

  definition
    Inf_Assertion_def: "Inf (A::('a Assertion) set) = - (Sup (uminus ` A))"

lemma Sup1: "(x::'a Assertion)  A  x  Sup A"
    apply (simp add: Sup_Assertion_def less_eq_Assertion_def Abs_Assertion_inverse)
    by (rule Sup_upper, simp)

lemma Sup2: "(x::'a Assertion . x  A  x  z)  Sup A  z"
    apply (simp add: Sup_Assertion_def less_eq_Assertion_def Abs_Assertion_inverse)
    apply (rule Sup_least)
    by blast

instance
proof
  fix x :: "'a Assertion" fix A assume A: "x  A" from A show "Inf A  x"
    apply (simp add: Inf_Assertion_def)
    apply (subst compl_le_compl_iff [THEN sym], simp)
    by (rule Sup1, simp)
next
  fix z :: "'a Assertion" fix A assume A: "x . x  A  z  x" from A show "z  Inf A"
    apply (simp add: Inf_Assertion_def)
    apply (subst compl_le_compl_iff [THEN sym], simp)
    apply (rule Sup2)
    apply safe
    by simp
next
  fix x :: "'a Assertion" fix A assume A: "x  A" from A show "x  Sup A"
    by (rule Sup1)
next
  fix z :: "'a Assertion" fix A assume A: "x . x  A  x  z" from A show "Sup A  z"
    by (rule Sup2)
next
  show "Inf {} = (::'a Assertion)"
    by (auto simp: Inf_Assertion_def Sup_Assertion_def compl_bot_eq [symmetric] bot_Assertion_def)
next
  show "Sup {} = (::'a Assertion)"
    by (auto simp: Sup_Assertion_def bot_Assertion_def)
qed
end

lemma assert_top [simp]: "{⋅} = 1"
  by (simp add: top_Assertion_def)

lemma assert_Sup: "{⋅Sup A} = Sup (assert ` A)"
  by (simp add: Sup_Assertion_def Abs_Assertion_inverse)

 
lemma assert_Inf: "{⋅Inf A} = (Inf (assert ` A))  1"
proof (cases "A = {}")
  case True then show ?thesis by simp
next
  note image_cong_simp [cong del]
  case False then show ?thesis
  apply (simp add: Inf_Assertion_def uminus_Assertion_def)
  apply (simp add: neg_assert_def assert_Sup dual_Sup Inf_comp inf_commute inf_Inf comp_def)
  apply (rule_tac f = Inf in arg_cong)
  apply safe
  apply simp
  apply (subst inf_commute)
  apply (simp add: image_def uminus_Assertion_def)
  apply (simp add: neg_assert_def dual_comp dual_inf sup_comp assertion_prop)
  apply auto [1]
  apply (simp)
  apply (subst image_def, simp)
  apply (simp add: uminus_Assertion_def)
  apply (subst inf_commute)
  apply (simp add: neg_assert_def dual_comp dual_inf sup_comp assertion_prop)
  apply auto
  done
qed

lemma assert_Inf_ne: "A  {}  {⋅Inf A} = Inf (assert ` A)"
  apply (unfold assert_Inf)
  apply (rule antisym)
  apply simp_all
  apply safe
  apply (erule notE)
  apply (rule_tac y = "{⋅x}" in order_trans)
  by (simp_all add: INF_lower)
 
  
lemma assert_Sup_range: "{⋅Sup (range p)} = Sup (range (assert o p))"
  apply (subst assert_Sup)
  by (rule_tac f = "Sup" in arg_cong, auto)

lemma assert_Sup_less: "{⋅ Sup_less p w } = Sup_less (assert o p) w"
  apply (simp add: Sup_less_def)
  apply (subst assert_Sup)
  by (rule_tac f = "Sup" in arg_cong, auto)

end