Theory PhiSem_Generic_Boolean

chapter ‹Generic Boolean›

theory PhiSem_Generic_Boolean
  imports PhiSem_Base
  abbrevs "<bool>" = "𝖻𝗈𝗈𝗅"
begin

section ‹Semantics›

debt_axiomatization 𝖻𝗈𝗈𝗅          :: TY
                and sem_mk_bool   :: ‹bool ⇒ VAL›
                and sem_dest_bool :: ‹VAL ⇒ bool›
  where sem_mk_dest_bool[simp]: ‹sem_dest_bool (sem_mk_bool b) = b›
    and 𝖻𝗈𝗈𝗅_neq_𝗉𝗈𝗂𝗌𝗈𝗇[simp]: ‹𝖻𝗈𝗈𝗅 ≠ 𝗉𝗈𝗂𝗌𝗈𝗇›
    and can_eq_bool: ‹Can_EqCompare res (sem_mk_bool x1) (sem_mk_bool x2)›
    and eq_bool:     ‹EqCompare (sem_mk_bool x1) (sem_mk_bool x2) = (x1 = x2)›
    and zero_bool[simp]: ‹Zero 𝖻𝗈𝗈𝗅 = Some (sem_mk_bool False)›
    and WT_bool[simp]:   ‹Well_Type 𝖻𝗈𝗈𝗅 = { sem_mk_bool x |x. True }›  

lemma sem_mk_bool_inj[simp]:
  ‹sem_mk_bool x = sem_mk_bool y ≡ x = y›
  by (smt (verit, del_insts) sem_mk_dest_bool)

lemma 𝗉𝗈𝗂𝗌𝗈𝗇_neq_𝖻𝗈𝗈𝗅[simp]:
  ‹𝗉𝗈𝗂𝗌𝗈𝗇 ≠ 𝖻𝗈𝗈𝗅›
  using 𝖻𝗈𝗈𝗅_neq_𝗉𝗈𝗂𝗌𝗈𝗇 by fastforce

lemma [φreason add]:
  ‹ Is_Type_Literal 𝖻𝗈𝗈𝗅 ›
  unfolding Is_Type_Literal_def ..

section ‹Instructions›

definition op_const_bool :: "bool ⇒ VAL proc"
  where "op_const_bool b = Return (φarg (sem_mk_bool b))"

definition op_not :: "(VAL, VAL) proc'"
  where "op_not v =
    φM_getV 𝖻𝗈𝗈𝗅 sem_dest_bool v (λv.
    Return (φarg (sem_mk_bool (¬ v)))
  )"

definition op_and :: "(VAL × VAL, VAL) proc'"
  where "op_and =
    φM_caseV (λva vb.
    φM_getV 𝖻𝗈𝗈𝗅 sem_dest_bool va (λv.
    φM_getV 𝖻𝗈𝗈𝗅 sem_dest_bool vb (λu.
    Return (φarg (sem_mk_bool (v ∧ u)))
  )))"

definition op_or :: "(VAL × VAL, VAL) proc'"
  where "op_or =
    φM_caseV (λva vb.
    φM_getV 𝖻𝗈𝗈𝗅 sem_dest_bool va (λv.
    φM_getV 𝖻𝗈𝗈𝗅 sem_dest_bool vb (λu.
    Return (φarg (sem_mk_bool (v ∨ u)))
  )))"

definition op_xor :: "(VAL × VAL, VAL) proc'"
  where "op_xor =
    φM_caseV (λva vb.
    φM_getV 𝖻𝗈𝗈𝗅 sem_dest_bool va (λv.
    φM_getV 𝖻𝗈𝗈𝗅 sem_dest_bool vb (λu.
    Return (φarg (sem_mk_bool (v ∧ ¬ u ∨ ¬ v ∧ u)))
  )))"

definition op_equal :: "TY ⇒ (VAL × VAL, VAL) proc'"
  where "op_equal TY =
    φM_caseV (λva vb.
    φM_getV TY id va (λv.
    φM_getV TY id vb (λu.
    (λres. φM_assert (Can_EqCompare res v u) res) ⪢
    Return (φarg (sem_mk_bool (EqCompare v u)))
)))"


section ‹φ-Type›
 
φtype_def φBool :: "(VAL, bool) φ" ("𝔹")
  where ‹x ⦂ 𝔹 ≡ sem_mk_bool x ⦂ Itself›
  deriving Basic
       and Abstract_Domain⇩L
       and Functionality
       and ‹Semantic_Zero_Val 𝖻𝗈𝗈𝗅 𝔹 False›
       and Inhabited
       and ‹𝗍𝗒𝗉𝖾𝗈𝖿 𝔹 = 𝖻𝗈𝗈𝗅›
       and Equiv_Class

lemma φBool_eqcmp[φreason 2000]:
  "φEqual 𝔹 (λx y. True) (=)" (*TODO: auto derive!*)
  unfolding φEqual_def
  by (simp add: can_eq_bool eq_bool)


section ‹Abstractions of Boolean Arithmetic›
 
declare_φlang_operator
  infix 50 "="
  infix 35 "∧"
  infix 30 "∨"
  infix 30 ⊕ ― ‹Xor›
  prefix 40 "¬"


subsection ‹Constant›

lemma op_const_bool_φapp[φsynthesis for ‹λv. True ⦂ ?T v› (1200) and ‹λv. False ⦂ ?T v› (1200)]:
  ‹ Is_Literal b
⟹ 𝗉𝗋𝗈𝖼 op_const_bool b ⦃ Void ⟼ 𝗏𝖺𝗅 b ⦂ 𝔹 ⦄›
  unfolding op_const_bool_def
  by (rule, simp)

lemma True_φapp:
  ‹𝗉𝗋𝗈𝖼 op_const_bool True ⦃ Void ⟼ 𝗏𝖺𝗅 True ⦂ 𝔹 ⦄›
  ❴ ‹True› ❵.

lemma False_φapp:
  ‹𝗉𝗋𝗈𝖼 op_const_bool False ⦃ Void ⟼ 𝗏𝖺𝗅 False ⦂ 𝔹 ⦄›
  ❴ ‹False› ❵.


subsection ‹Not›

lemma op_not[φoverload ¬, φsynthesis 100]:
  ‹𝗉𝗋𝗈𝖼 op_not raw ⦃ x ⦂ 𝗏𝖺𝗅[raw] 𝔹 ⟼ 𝗏𝖺𝗅 ¬ x ⦂ 𝔹 ⦄›
  unfolding op_not_def
  by (cases raw, simp, rule, simp, rule,  simp)

subsection ‹And›

lemma op_and[φoverload ∧, φsynthesis add]:
  ‹𝗉𝗋𝗈𝖼 op_and (va❙, vb) ⦃ a ⦂ 𝗏𝖺𝗅[va] 𝔹❟ b ⦂ 𝗏𝖺𝗅[vb] 𝔹 ⟼ 𝗏𝖺𝗅 (a ∧ b) ⦂ 𝔹 ⦄›
  unfolding op_and_def
  by (cases va; cases vb; simp, rule, rule, simp, rule, simp, rule, simp)


subsection ‹Or›

lemma op_or[φoverload ∨, φsynthesis 100]:
  ‹𝗉𝗋𝗈𝖼 op_or (va❙, vb) ⦃ a ⦂ 𝗏𝖺𝗅[va] 𝔹❟ b ⦂ 𝗏𝖺𝗅[vb] 𝔹 ⟼ 𝗏𝖺𝗅 (a ∨ b) ⦂ 𝔹 ⦄›
  unfolding op_or_def
  by (cases va; cases vb, simp, rule, rule, simp, rule, simp, rule, simp)

subsection ‹Xor›

lemma op_xor[φoverload ⊕, φsynthesis 100]:
  ‹𝗉𝗋𝗈𝖼 op_xor (va❙, vb) ⦃ a ⦂ 𝗏𝖺𝗅[va] 𝔹❟ b ⦂ 𝗏𝖺𝗅[vb] 𝔹 ⟼ 𝗏𝖺𝗅 (a ∧ ¬ b ∨ ¬ a ∧ b) ⦂ 𝔹 ⦄›
  unfolding op_xor_def
  by (cases va; cases vb, simp, rule, rule, simp, rule, simp, rule, simp)

subsection ‹Equal›

declare [[
    overloaded_operator_in_synthesis ‹λv. x ⦂ T v› ‹λv. y ⦂ U v› ⇒ ‹λv. x = y ⦂ 𝗏𝖺𝗅[v] 𝔹›,
    overloaded_operator_in_synthesis
        ‹λv. x mod N ⦂ T v› ‹λv. y mod N ⦂ U v› ⇒ ‹λv. x mod N = y mod N ⦂ 𝗏𝖺𝗅[v] 𝔹›
]]

lemma op_equal_φapp[φoverload =]:
  ‹ φEqual T can_eq eq
⟹ Semantic_Type' (a ⦂ T) TY
⟹ Semantic_Type' (b ⦂ T) TY
⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 can_eq a b
⟹ 𝗉𝗋𝗈𝖼 op_equal TY (φV_pair rawa rawb) ⦃ a ⦂ 𝗏𝖺𝗅[rawa] T❟ b ⦂ 𝗏𝖺𝗅[rawb] T ⟼ eq a b ⦂ 𝗏𝖺𝗅 𝔹 ⦄›
  unfolding op_equal_def
  by ((cases rawa; cases rawb; simp, rule, rule),
      simp add: Semantic_Type'_def subset_iff Premise_def,
      simp add: Semantic_Type'_def subset_iff Premise_def, rule,
      unfold φEqual_def Premise_def, simp, simp,
      rule, simp)

declare op_equal_φapp[where eq=‹(=)›, φsynthesis 100]
declare op_equal_φapp[where eq=‹(λx y. x mod N = y mod N)› for N, φsynthesis 100]



end