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