Theory Data_Bool

section ‹Data: Bool›

theory Data_Bool
  imports Type_Classes
begin

subsection ‹Class instances›

text ‹Eq›

lemma eq_eqI[case_names bottomLTR bottomRTL LTR RTL]:
  "(x = ⊥ ⟹ y = ⊥) ⟹ (y = ⊥ ⟹ x = ⊥) ⟹ (x = TT ⟹ y = TT) ⟹ (y = TT ⟹ x = TT) ⟹ x = y"
by (metis Exh_tr)

lemma eq_tr_simps [simp]:
  shows "eq⋅TT⋅TT = TT" and "eq⋅TT⋅FF = FF"
    and "eq⋅FF⋅TT = FF" and "eq⋅FF⋅FF = TT"
  unfolding TT_def FF_def eq_lift_def by simp_all

text ‹Ord›

lemma compare_tr_simps [simp]:
  "compare⋅FF⋅FF = EQ"
  "compare⋅FF⋅TT = LT"
  "compare⋅TT⋅FF = GT"
  "compare⋅TT⋅TT = EQ"
  unfolding TT_def FF_def compare_lift_def
  by simp_all

subsection ‹Lemmas›

lemma andalso_eq_TT_iff [simp]:
  "(x andalso y) = TT ⟷ x = TT ∧ y = TT"
  by (cases x, simp_all)

lemma andalso_eq_FF_iff [simp]:
  "(x andalso y) = FF ⟷ x = FF ∨ (x = TT ∧ y = FF)"
  by (cases x, simp_all)

lemma andalso_eq_bottom_iff [simp]:
  "(x andalso y) = ⊥ ⟷ x = ⊥ ∨ (x = TT ∧ y = ⊥)"
  by (cases x, simp_all)

lemma orelse_eq_FF_iff [simp]:
  "(x orelse y) = FF ⟷ x = FF ∧ y = FF"
  by (cases x, simp_all)

lemma orelse_assoc [simp]:
  "((x orelse y) orelse z) = (x orelse y orelse z)"
  by (cases x) auto

lemma andalso_assoc [simp]:
  "((x andalso y) andalso z) = (x andalso y andalso z)"
  by (cases x) auto

lemma neg_orelse [simp]:
  "neg⋅(x orelse y) = (neg⋅x andalso neg⋅y)"
  by (cases x) auto

lemma neg_andalso [simp]:
  "neg⋅(x andalso y) = (neg⋅x orelse neg⋅y)"
  by (cases x) auto

text ‹Not suitable as default simp rules, because they cause the
  simplifier to loop:›
lemma neg_eq_simps:
  "neg⋅x = TT ⟹ x = FF"
  "neg⋅x = FF ⟹ x = TT"
  "neg⋅x = ⊥ ⟹ x = ⊥"
  by (cases x, simp_all)+

lemma neg_eq_TT_iff [simp]: "neg⋅x = TT ⟷ x = FF"
  by (cases x, simp_all)+

lemma neg_eq_FF_iff [simp]: "neg⋅x = FF ⟷ x = TT"
  by (cases x, simp_all)+

lemma neg_eq_bottom_iff [simp]: "neg⋅x = ⊥ ⟷ x = ⊥"
  by (cases x, simp_all)+

(* TODO: set up reorient_proc for TT and FF *)

lemma neg_eq [simp]:
  "neg⋅x = neg⋅y ⟷ x = y"
  by (cases y, simp_all)

lemma neg_neg [simp]:
  "neg⋅(neg⋅x) = x"
  by (cases x, auto)

lemma neg_comp_neg [simp]:
  "neg oo neg = ID"
  by (metis cfun_eqI cfcomp2 neg_neg ID1)

end