# Theory Tr

theory Tr
imports Lift
```(*  Title:      HOL/HOLCF/Tr.thy
Author:     Franz Regensburger
*)

section ‹The type of lifted booleans›

theory Tr
imports Lift
begin

subsection ‹Type definition and constructors›

type_synonym tr = "bool lift"

translations
(type) "tr" ↽ (type) "bool lift"

definition TT :: "tr"
where "TT = Def True"

definition FF :: "tr"
where "FF = Def False"

text ‹Exhaustion and Elimination for type @{typ tr}›

lemma Exh_tr: "t = ⊥ ∨ t = TT ∨ t = FF"
by (induct t) (auto simp: FF_def TT_def)

lemma trE [case_names bottom TT FF, cases type: tr]:
"⟦p = ⊥ ⟹ Q; p = TT ⟹ Q; p = FF ⟹ Q⟧ ⟹ Q"
by (induct p) (auto simp: FF_def TT_def)

lemma tr_induct [case_names bottom TT FF, induct type: tr]:
"P ⊥ ⟹ P TT ⟹ P FF ⟹ P x"
by (cases x) simp_all

text ‹distinctness for type @{typ tr}›

lemma dist_below_tr [simp]:
"TT \<notsqsubseteq> ⊥" "FF \<notsqsubseteq> ⊥" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT"

lemma dist_eq_tr [simp]: "TT ≠ ⊥" "FF ≠ ⊥" "TT ≠ FF" "⊥ ≠ TT" "⊥ ≠ FF" "FF ≠ TT"

lemma TT_below_iff [simp]: "TT ⊑ x ⟷ x = TT"
by (induct x) simp_all

lemma FF_below_iff [simp]: "FF ⊑ x ⟷ x = FF"
by (induct x) simp_all

lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT ⟷ x = FF"
by (induct x) simp_all

lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF ⟷ x = TT"
by (induct x) simp_all

subsection ‹Case analysis›

default_sort pcpo

definition tr_case :: "'a → 'a → tr → 'a"
where "tr_case = (Λ t e (Def b). if b then t else e)"

abbreviation cifte_syn :: "[tr, 'c, 'c] ⇒ 'c"  ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60)
where "If b then e1 else e2 ≡ tr_case⋅e1⋅e2⋅b"

translations
"Λ (XCONST TT). t" ⇌ "CONST tr_case⋅t⋅⊥"
"Λ (XCONST FF). t" ⇌ "CONST tr_case⋅⊥⋅t"

lemma ifte_thms [simp]:
"If ⊥ then e1 else e2 = ⊥"
"If FF then e1 else e2 = e2"
"If TT then e1 else e2 = e1"
by (simp_all add: tr_case_def TT_def FF_def)

subsection ‹Boolean connectives›

definition trand :: "tr → tr → tr"
where andalso_def: "trand = (Λ x y. If x then y else FF)"

abbreviation andalso_syn :: "tr ⇒ tr ⇒ tr"  ("_ andalso _" [36,35] 35)
where "x andalso y ≡ trand⋅x⋅y"

definition tror :: "tr → tr → tr"
where orelse_def: "tror = (Λ x y. If x then TT else y)"

abbreviation orelse_syn :: "tr ⇒ tr ⇒ tr"  ("_ orelse _"  [31,30] 30)
where "x orelse y ≡ tror⋅x⋅y"

definition neg :: "tr → tr"
where "neg = flift2 Not"

definition If2 :: "tr ⇒ 'c ⇒ 'c ⇒ 'c"
where "If2 Q x y = (If Q then x else y)"

text ‹tactic for tr-thms with case split›

lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def

text ‹lemmas about andalso, orelse, neg and if›

lemma andalso_thms [simp]:
"(TT andalso y) = y"
"(FF andalso y) = FF"
"(⊥ andalso y) = ⊥"
"(y andalso TT) = y"
"(y andalso y) = y"
apply (unfold andalso_def, simp_all)
apply (cases y, simp_all)
apply (cases y, simp_all)
done

lemma orelse_thms [simp]:
"(TT orelse y) = TT"
"(FF orelse y) = y"
"(⊥ orelse y) = ⊥"
"(y orelse FF) = y"
"(y orelse y) = y"
apply (unfold orelse_def, simp_all)
apply (cases y, simp_all)
apply (cases y, simp_all)
done

lemma neg_thms [simp]:
"neg⋅TT = FF"
"neg⋅FF = TT"
"neg⋅⊥ = ⊥"
by (simp_all add: neg_def TT_def FF_def)

text ‹split-tac for If via If2 because the constant has to be a constant›

lemma split_If2: "P (If2 Q x y) ⟷ ((Q = ⊥ ⟶ P ⊥) ∧ (Q = TT ⟶ P x) ∧ (Q = FF ⟶ P y))"
by (cases Q) (simp_all add: If2_def)

(* FIXME unused!? *)
ML ‹
fun split_If_tac ctxt =
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym])
THEN' (split_tac ctxt [@{thm split_If2}])
›

subsection "Rewriting of HOLCF operations to HOL functions"

lemma andalso_or: "t ≠ ⊥ ⟹ (t andalso s) = FF ⟷ t = FF ∨ s = FF"
by (cases t) simp_all

lemma andalso_and: "t ≠ ⊥ ⟹ ((t andalso s) ≠ FF) ⟷ t ≠ FF ∧ s ≠ FF"
by (cases t) simp_all

lemma Def_bool1 [simp]: "Def x ≠ FF ⟷ x"

lemma Def_bool2 [simp]: "Def x = FF ⟷ ¬ x"

lemma Def_bool3 [simp]: "Def x = TT ⟷ x"

lemma Def_bool4 [simp]: "Def x ≠ TT ⟷ ¬ x"

lemma If_and_if: "(If Def P then A else B) = (if P then A else B)"
by (cases "Def P") (auto simp add: TT_def[symmetric] FF_def[symmetric])

subsection ‹Compactness›

lemma compact_TT: "compact TT"
by (rule compact_chfin)

lemma compact_FF: "compact FF"
by (rule compact_chfin)

end
```