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