(* Title: HOL/HOLCF/Tr.thy
Author: Franz Regensburger
*)
section \<open>The type of lifted booleans\<close>
theory Tr
imports Lift
begin
subsection \<open>Type definition and constructors\<close>
type_synonym tr = "bool lift"
translations
(type) "tr" \<leftharpoondown> (type) "bool lift"
definition TT :: "tr"
where "TT = Def True"
definition FF :: "tr"
where "FF = Def False"
text \<open>Exhaustion and Elimination for type \<^typ>\<open>tr\<close>\<close>
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 \<open>distinctness for type \<^typ>\<open>tr\<close>\<close>
lemma dist_below_tr [simp]:
"TT \ \" "FF \ \" "TT \ FF" "FF \ TT"
by (simp_all add: TT_def FF_def)
lemma dist_eq_tr [simp]: "TT \ \" "FF \ \" "TT \ FF" "\ \ TT" "\ \ FF" "FF \ TT"
by (simp_all add: TT_def FF_def)
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 \ TT \ x = FF"
by (induct x) simp_all
lemma not_below_FF_iff [simp]: "x \ FF \ x = TT"
by (induct x) simp_all
subsection \<open>Case analysis\<close>
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 \<open>Boolean connectives\<close>
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 \<open>tactic for tr-thms with case split\<close>
lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def
text \<open>lemmas about andalso, orelse, neg and if\<close>
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 \<open>split-tac for If via If2 because the constant has to be a constant\<close>
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 \<open>
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}])
\<close>
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"
by (simp add: FF_def)
lemma Def_bool2 [simp]: "Def x = FF \ \ x"
by (simp add: FF_def)
lemma Def_bool3 [simp]: "Def x = TT \ x"
by (simp add: TT_def)
lemma Def_bool4 [simp]: "Def x \ TT \ \ x"
by (simp add: TT_def)
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 \<open>Compactness\<close>
lemma compact_TT: "compact TT"
by (rule compact_chfin)
lemma compact_FF: "compact FF"
by (rule compact_chfin)
end
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
