1(* Title: HOL/HOLCF/Tr.thy 2 Author: Franz Regensburger 3*) 4 5section \<open>The type of lifted booleans\<close> 6 7theory Tr 8 imports Lift 9begin 10 11subsection \<open>Type definition and constructors\<close> 12 13type_synonym tr = "bool lift" 14 15translations 16 (type) "tr" \<leftharpoondown> (type) "bool lift" 17 18definition TT :: "tr" 19 where "TT = Def True" 20 21definition FF :: "tr" 22 where "FF = Def False" 23 24text \<open>Exhaustion and Elimination for type @{typ tr}\<close> 25 26lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF" 27 by (induct t) (auto simp: FF_def TT_def) 28 29lemma trE [case_names bottom TT FF, cases type: tr]: 30 "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 31 by (induct p) (auto simp: FF_def TT_def) 32 33lemma tr_induct [case_names bottom TT FF, induct type: tr]: 34 "P \<bottom> \<Longrightarrow> P TT \<Longrightarrow> P FF \<Longrightarrow> P x" 35 by (cases x) simp_all 36 37text \<open>distinctness for type @{typ tr}\<close> 38 39lemma dist_below_tr [simp]: 40 "TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT" 41 by (simp_all add: TT_def FF_def) 42 43lemma dist_eq_tr [simp]: "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT" 44 by (simp_all add: TT_def FF_def) 45 46lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT" 47 by (induct x) simp_all 48 49lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF" 50 by (induct x) simp_all 51 52lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF" 53 by (induct x) simp_all 54 55lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT" 56 by (induct x) simp_all 57 58 59subsection \<open>Case analysis\<close> 60 61default_sort pcpo 62 63definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a" 64 where "tr_case = (\<Lambda> t e (Def b). if b then t else e)" 65 66abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60) 67 where "If b then e1 else e2 \<equiv> tr_case\<cdot>e1\<cdot>e2\<cdot>b" 68 69translations 70 "\<Lambda> (XCONST TT). t" \<rightleftharpoons> "CONST tr_case\<cdot>t\<cdot>\<bottom>" 71 "\<Lambda> (XCONST FF). t" \<rightleftharpoons> "CONST tr_case\<cdot>\<bottom>\<cdot>t" 72 73lemma ifte_thms [simp]: 74 "If \<bottom> then e1 else e2 = \<bottom>" 75 "If FF then e1 else e2 = e2" 76 "If TT then e1 else e2 = e1" 77 by (simp_all add: tr_case_def TT_def FF_def) 78 79 80subsection \<open>Boolean connectives\<close> 81 82definition trand :: "tr \<rightarrow> tr \<rightarrow> tr" 83 where andalso_def: "trand = (\<Lambda> x y. If x then y else FF)" 84 85abbreviation andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) 86 where "x andalso y \<equiv> trand\<cdot>x\<cdot>y" 87 88definition tror :: "tr \<rightarrow> tr \<rightarrow> tr" 89 where orelse_def: "tror = (\<Lambda> x y. If x then TT else y)" 90 91abbreviation orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) 92 where "x orelse y \<equiv> tror\<cdot>x\<cdot>y" 93 94definition neg :: "tr \<rightarrow> tr" 95 where "neg = flift2 Not" 96 97definition If2 :: "tr \<Rightarrow> 'c \<Rightarrow> 'c \<Rightarrow> 'c" 98 where "If2 Q x y = (If Q then x else y)" 99 100text \<open>tactic for tr-thms with case split\<close> 101 102lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def 103 104text \<open>lemmas about andalso, orelse, neg and if\<close> 105 106lemma andalso_thms [simp]: 107 "(TT andalso y) = y" 108 "(FF andalso y) = FF" 109 "(\<bottom> andalso y) = \<bottom>" 110 "(y andalso TT) = y" 111 "(y andalso y) = y" 112 apply (unfold andalso_def, simp_all) 113 apply (cases y, simp_all) 114 apply (cases y, simp_all) 115 done 116 117lemma orelse_thms [simp]: 118 "(TT orelse y) = TT" 119 "(FF orelse y) = y" 120 "(\<bottom> orelse y) = \<bottom>" 121 "(y orelse FF) = y" 122 "(y orelse y) = y" 123 apply (unfold orelse_def, simp_all) 124 apply (cases y, simp_all) 125 apply (cases y, simp_all) 126 done 127 128lemma neg_thms [simp]: 129 "neg\<cdot>TT = FF" 130 "neg\<cdot>FF = TT" 131 "neg\<cdot>\<bottom> = \<bottom>" 132 by (simp_all add: neg_def TT_def FF_def) 133 134text \<open>split-tac for If via If2 because the constant has to be a constant\<close> 135 136lemma split_If2: "P (If2 Q x y) \<longleftrightarrow> ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))" 137 by (cases Q) (simp_all add: If2_def) 138 139(* FIXME unused!? *) 140ML \<open> 141fun split_If_tac ctxt = 142 simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym]) 143 THEN' (split_tac ctxt [@{thm split_If2}]) 144\<close> 145 146subsection "Rewriting of HOLCF operations to HOL functions" 147 148lemma andalso_or: "t \<noteq> \<bottom> \<Longrightarrow> (t andalso s) = FF \<longleftrightarrow> t = FF \<or> s = FF" 149 by (cases t) simp_all 150 151lemma andalso_and: "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) \<longleftrightarrow> t \<noteq> FF \<and> s \<noteq> FF" 152 by (cases t) simp_all 153 154lemma Def_bool1 [simp]: "Def x \<noteq> FF \<longleftrightarrow> x" 155 by (simp add: FF_def) 156 157lemma Def_bool2 [simp]: "Def x = FF \<longleftrightarrow> \<not> x" 158 by (simp add: FF_def) 159 160lemma Def_bool3 [simp]: "Def x = TT \<longleftrightarrow> x" 161 by (simp add: TT_def) 162 163lemma Def_bool4 [simp]: "Def x \<noteq> TT \<longleftrightarrow> \<not> x" 164 by (simp add: TT_def) 165 166lemma If_and_if: "(If Def P then A else B) = (if P then A else B)" 167 by (cases "Def P") (auto simp add: TT_def[symmetric] FF_def[symmetric]) 168 169 170subsection \<open>Compactness\<close> 171 172lemma compact_TT: "compact TT" 173 by (rule compact_chfin) 174 175lemma compact_FF: "compact FF" 176 by (rule compact_chfin) 177 178end 179