Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Tr.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.