src/HOLCF/Tr.thy
author haftmann
Tue Jul 10 17:30:50 2007 +0200 (2007-07-10)
changeset 23709 fd31da8f752a
parent 18081 fe15796b257d
child 25131 2c8caac48ade
permissions -rw-r--r--
moved lfp_induct2 here
     1 (*  Title:      HOLCF/Tr.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 
     5 Introduce infix if_then_else_fi and boolean connectives andalso, orelse.
     6 *)
     7 
     8 header {* The type of lifted booleans *}
     9 
    10 theory Tr
    11 imports Lift
    12 begin
    13 
    14 defaultsort pcpo
    15 
    16 types
    17   tr = "bool lift"
    18 
    19 translations
    20   "tr" <= (type) "bool lift" 
    21 
    22 consts
    23   TT     :: "tr"
    24   FF     :: "tr"
    25   trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c"
    26   trand  :: "tr \<rightarrow> tr \<rightarrow> tr"
    27   tror   :: "tr \<rightarrow> tr \<rightarrow> tr"
    28   neg    :: "tr \<rightarrow> tr"
    29   If2    :: "[tr, 'c, 'c] \<Rightarrow> 'c"
    30 
    31 syntax
    32   "@cifte"   :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60)
    33   "@andalso" :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ andalso _" [36,35] 35)
    34   "@orelse"  :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ orelse _"  [31,30] 30)
    35  
    36 translations
    37   "x andalso y" == "trand\<cdot>x\<cdot>y"
    38   "x orelse y"  == "tror\<cdot>x\<cdot>y"
    39   "If b then e1 else e2 fi" == "trifte\<cdot>e1\<cdot>e2\<cdot>b"
    40 
    41 translations
    42   "\<Lambda> TT. t" == "trifte\<cdot>t\<cdot>\<bottom>"
    43   "\<Lambda> FF. t" == "trifte\<cdot>\<bottom>\<cdot>t"
    44 
    45 defs
    46   TT_def:      "TT \<equiv> Def True"
    47   FF_def:      "FF \<equiv> Def False"
    48   neg_def:     "neg \<equiv> flift2 Not"
    49   ifte_def:    "trifte \<equiv> \<Lambda> t e. FLIFT b. if b then t else e"
    50   andalso_def: "trand \<equiv> \<Lambda> x y. If x then y else FF fi"
    51   orelse_def:  "tror \<equiv> \<Lambda> x y. If x then TT else y fi"
    52   If2_def:     "If2 Q x y \<equiv> If Q then x else y fi"
    53 
    54 text {* Exhaustion and Elimination for type @{typ tr} *}
    55 
    56 lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
    57 apply (unfold FF_def TT_def)
    58 apply (induct_tac "t")
    59 apply fast
    60 apply fast
    61 done
    62 
    63 lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    64 apply (rule Exh_tr [THEN disjE])
    65 apply fast
    66 apply (erule disjE)
    67 apply fast
    68 apply fast
    69 done
    70 
    71 text {* tactic for tr-thms with case split *}
    72 
    73 lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
    74 (*
    75 fun prover t =  prove_goal thy t
    76  (fn prems =>
    77         [
    78         (res_inst_tac [("p","y")] trE 1),
    79 	(REPEAT(asm_simp_tac (simpset() addsimps 
    80 		[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
    81 	])
    82 *)
    83 text {* distinctness for type @{typ tr} *}
    84 
    85 lemma dist_less_tr [simp]:
    86   "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
    87 by (simp_all add: tr_defs)
    88 
    89 lemma dist_eq_tr [simp]:
    90   "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
    91 by (simp_all add: tr_defs)
    92 
    93 text {* lemmas about andalso, orelse, neg and if *}
    94 
    95 lemma ifte_thms [simp]:
    96   "If \<bottom> then e1 else e2 fi = \<bottom>"
    97   "If FF then e1 else e2 fi = e2"
    98   "If TT then e1 else e2 fi = e1"
    99 by (simp_all add: ifte_def TT_def FF_def)
   100 
   101 lemma andalso_thms [simp]:
   102   "(TT andalso y) = y"
   103   "(FF andalso y) = FF"
   104   "(\<bottom> andalso y) = \<bottom>"
   105   "(y andalso TT) = y"
   106   "(y andalso y) = y"
   107 apply (unfold andalso_def, simp_all)
   108 apply (rule_tac p=y in trE, simp_all)
   109 apply (rule_tac p=y in trE, simp_all)
   110 done
   111 
   112 lemma orelse_thms [simp]:
   113   "(TT orelse y) = TT"
   114   "(FF orelse y) = y"
   115   "(\<bottom> orelse y) = \<bottom>"
   116   "(y orelse FF) = y"
   117   "(y orelse y) = y"
   118 apply (unfold orelse_def, simp_all)
   119 apply (rule_tac p=y in trE, simp_all)
   120 apply (rule_tac p=y in trE, simp_all)
   121 done
   122 
   123 lemma neg_thms [simp]:
   124   "neg\<cdot>TT = FF"
   125   "neg\<cdot>FF = TT"
   126   "neg\<cdot>\<bottom> = \<bottom>"
   127 by (simp_all add: neg_def TT_def FF_def)
   128 
   129 text {* split-tac for If via If2 because the constant has to be a constant *}
   130   
   131 lemma split_If2: 
   132   "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
   133 apply (unfold If2_def)
   134 apply (rule_tac p = "Q" in trE)
   135 apply (simp_all)
   136 done
   137 
   138 ML {*
   139 val split_If_tac =
   140   simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")])
   141     THEN' (split_tac [thm "split_If2"])
   142 *}
   143 
   144 subsection "Rewriting of HOLCF operations to HOL functions"
   145 
   146 lemma andalso_or: 
   147   "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
   148 apply (rule_tac p = "t" in trE)
   149 apply simp_all
   150 done
   151 
   152 lemma andalso_and:
   153   "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
   154 apply (rule_tac p = "t" in trE)
   155 apply simp_all
   156 done
   157 
   158 lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x"
   159 by (simp add: FF_def)
   160 
   161 lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)"
   162 by (simp add: FF_def)
   163 
   164 lemma Def_bool3 [simp]: "(Def x = TT) = x"
   165 by (simp add: TT_def)
   166 
   167 lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)"
   168 by (simp add: TT_def)
   169 
   170 lemma If_and_if: 
   171   "(If Def P then A else B fi) = (if P then A else B)"
   172 apply (rule_tac p = "Def P" in trE)
   173 apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
   174 done
   175 
   176 subsection {* Compactness *}
   177 
   178 lemma compact_TT [simp]: "compact TT"
   179 by (rule compact_chfin)
   180 
   181 lemma compact_FF [simp]: "compact FF"
   182 by (rule compact_chfin)
   183 
   184 end