src/HOLCF/Tr.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 36452 d37c6eed8117
child 40322 707eb30e8a53
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      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 types
    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   "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> 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]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
    57 by (induct x rule: tr_induct) simp_all
    58 
    59 lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> 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
    68   trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
    69   ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)"
    70 abbreviation
    71   cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(3If _/ (then _/ else _) fi)" 60)  where
    72   "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
    73 
    74 translations
    75   "\<Lambda> (XCONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
    76   "\<Lambda> (XCONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
    77 
    78 lemma ifte_thms [simp]:
    79   "If \<bottom> then e1 else e2 fi = \<bottom>"
    80   "If FF then e1 else e2 fi = e2"
    81   "If TT then e1 else e2 fi = e1"
    82 by (simp_all add: ifte_def TT_def FF_def)
    83 
    84 
    85 subsection {* Boolean connectives *}
    86 
    87 definition
    88   trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
    89   andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)"
    90 abbreviation
    91   andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)  where
    92   "x andalso y == trand\<cdot>x\<cdot>y"
    93 
    94 definition
    95   tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
    96   orelse_def: "tror = (\<Lambda> x y. If x then TT else y fi)"
    97 abbreviation
    98   orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)  where
    99   "x orelse y == tror\<cdot>x\<cdot>y"
   100 
   101 definition
   102   neg :: "tr \<rightarrow> tr" where
   103   "neg = flift2 Not"
   104 
   105 definition
   106   If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
   107   "If2 Q x y = (If Q then x else y fi)"
   108 
   109 text {* tactic for tr-thms with case split *}
   110 
   111 lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
   112 
   113 text {* lemmas about andalso, orelse, neg and if *}
   114 
   115 lemma andalso_thms [simp]:
   116   "(TT andalso y) = y"
   117   "(FF andalso y) = FF"
   118   "(\<bottom> andalso y) = \<bottom>"
   119   "(y andalso TT) = y"
   120   "(y andalso y) = y"
   121 apply (unfold andalso_def, simp_all)
   122 apply (cases y rule: trE, simp_all)
   123 apply (cases y rule: trE, simp_all)
   124 done
   125 
   126 lemma orelse_thms [simp]:
   127   "(TT orelse y) = TT"
   128   "(FF orelse y) = y"
   129   "(\<bottom> orelse y) = \<bottom>"
   130   "(y orelse FF) = y"
   131   "(y orelse y) = y"
   132 apply (unfold orelse_def, simp_all)
   133 apply (cases y rule: trE, simp_all)
   134 apply (cases y rule: trE, simp_all)
   135 done
   136 
   137 lemma neg_thms [simp]:
   138   "neg\<cdot>TT = FF"
   139   "neg\<cdot>FF = TT"
   140   "neg\<cdot>\<bottom> = \<bottom>"
   141 by (simp_all add: neg_def TT_def FF_def)
   142 
   143 text {* split-tac for If via If2 because the constant has to be a constant *}
   144 
   145 lemma split_If2:
   146   "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
   147 apply (unfold If2_def)
   148 apply (rule_tac p = "Q" in trE)
   149 apply (simp_all)
   150 done
   151 
   152 ML {*
   153 val split_If_tac =
   154   simp_tac (HOL_basic_ss addsimps [@{thm If2_def} RS sym])
   155     THEN' (split_tac [@{thm split_If2}])
   156 *}
   157 
   158 subsection "Rewriting of HOLCF operations to HOL functions"
   159 
   160 lemma andalso_or:
   161   "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
   162 apply (rule_tac p = "t" in trE)
   163 apply simp_all
   164 done
   165 
   166 lemma andalso_and:
   167   "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
   168 apply (rule_tac p = "t" in trE)
   169 apply simp_all
   170 done
   171 
   172 lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x"
   173 by (simp add: FF_def)
   174 
   175 lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)"
   176 by (simp add: FF_def)
   177 
   178 lemma Def_bool3 [simp]: "(Def x = TT) = x"
   179 by (simp add: TT_def)
   180 
   181 lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)"
   182 by (simp add: TT_def)
   183 
   184 lemma If_and_if:
   185   "(If Def P then A else B fi) = (if P then A else B)"
   186 apply (rule_tac p = "Def P" in trE)
   187 apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
   188 done
   189 
   190 subsection {* Compactness *}
   191 
   192 lemma compact_TT: "compact TT"
   193 by (rule compact_chfin)
   194 
   195 lemma compact_FF: "compact FF"
   196 by (rule compact_chfin)
   197 
   198 end