<commit_before>(*  Title:      HOLCF/Tr.thy
    Author:     <NAME>
*)

header {* The type of lifted booleans *}

theory Tr
imports Lift
begin

subsection {* Type definition and constructors *}

types
  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 = \<bottom> \<or> t = TT \<or> t = FF"
unfolding FF_def TT_def by (induct t) auto

lemma trE [case_names bottom TT FF]:
  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
unfolding FF_def TT_def by (induct p) auto

lemma tr_induct [case_names bottom TT FF]:
  "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
by (cases x rule: trE) simp_all

text {* distinctness for type @{typ tr} *}

lemma dist_below_tr [simp]:
  "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
unfolding TT_def FF_def by simp_all

lemma dist_eq_tr [simp]:
  "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
unfolding TT_def FF_def by simp_all

lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
by (induct x rule: tr_induct) simp_all

lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
by (induct x rule: tr_induct) simp_all

lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
by (induct x rule: tr_induct) simp_all

lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
by (induct x rule: tr_induct) simp_all


subsection {* Case analysis *}

default_sort pcpo

definition
  trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
  ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)"

abbreviation
  cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60)
where
  "If b then e1 else e2 == trifte\<cdot>e1\<cdot>e2\<cdot>b"

translations
  "\<Lambda> (XCONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
  "\<Lambda> (XCONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"

lemma ifte_thms [simp]:
  "If \<bottom> then e1 else e2 = \<bottom>"
  "If FF then e1 else e2 = e2"
  "If TT then e1 else e2 = e1"
by (simp_all add: ifte_def TT_def FF_def)


subsection {* Boolean connectives *}

definition
  trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
  andalso_def: "trand = (\<Lambda> x y. If x then y else FF)"
abbreviation
  andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)  where
  "x andalso y == trand\<cdot>x\<cdot>y"

definition
  tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
  orelse_def: "tror = (\<Lambda> x y. If x then TT else y)"
abbreviation
  orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)  where
  "x orelse y == tror\<cdot>x\<cdot>y"

definition
  neg :: "tr \<rightarrow> tr" where
  "neg = flift2 Not"

definition
  If2 :: "[tr, 'c, 'c] \<Rightarrow> '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 ifte_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"
  "(\<bottom> andalso y) = \<bottom>"
  "(y andalso TT) = y"
  "(y andalso y) = y"<commit_msg>rename constant trifte to tr_case<commit_after>(*  Title:      HOLCF/Tr.thy
    Author:     <NAME>
*)

header {* The type of lifted booleans *}

theory Tr
imports Lift
begin

subsection {* Type definition and constructors *}

types
  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 = \<bottom> \<or> t = TT \<or> t = FF"
unfolding FF_def TT_def by (induct t) auto

lemma trE [case_names bottom TT FF]:
  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
unfolding FF_def TT_def by (induct p) auto

lemma tr_induct [case_names bottom TT FF]:
  "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
by (cases x rule: trE) simp_all

text {* distinctness for type @{typ tr} *}

lemma dist_below_tr [simp]:
  "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
unfolding TT_def FF_def by simp_all

lemma dist_eq_tr [simp]:
  "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
unfolding TT_def FF_def by simp_all

lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
by (induct x rule: tr_induct) simp_all

lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
by (induct x rule: tr_induct) simp_all

lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
by (induct x rule: tr_induct) simp_all

lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
by (induct x rule: tr_induct) simp_all


subsection {* Case analysis *}

default_sort pcpo

definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a" where
  "tr_case = (\<Lambda> t e (Def b). if b then t else e)"

abbreviation
  cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60)
where
  "If b then e1 else e2 == tr_case\<cdot>e1\<cdot>e2\<cdot>b"

translations
  "\<Lambda> (XCONST TT). t" == "CONST tr_case\<cdot>t\<cdot>\<bottom>"
  "\<Lambda> (XCONST FF). t" == "CONST tr_case\<cdot>\<bottom>\<cdot>t"

lemma ifte_thms [simp]:
  "If \<bottom> then e1 else e2 = \<bottom>"
  "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 \<rightarrow> tr \<rightarrow> tr" where
  andalso_def: "trand = (\<Lambda> x y. If x then y else FF)"
abbreviation
  andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)  where
  "x andalso y == trand\<cdot>x\<cdot>y"

definition
  tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
  orelse_def: "tror = (\<Lambda> x y. If x then TT else y)"
abbreviation
  orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)  where
  "x orelse y == tror\<cdot>x\<cdot>y"

definition
  neg :: "tr \<rightarrow> tr" where
  "neg = flift2 Not"

definition
  If2 :: "[tr, 'c, 'c] \<Rightarrow> '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"
  "(\<bottom> andalso y) = \<bottom>"
  "(y andalso TT) = y"
  "(y andalso y) = y"
{'fraction_non_alphanumeric': 0.16616064035329836, 'fraction_numerical': 0.009108473640629312, 'mean_word_length': 3.7834983498349835, 'pattern_counts': {'":': 0, '<': 167, '<?xml version=': 0, '>': 165, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4578489', 'n_tokens_mistral': 3165, 'n_tokens_neox': 2833, 'n_words': 948}