src/HOLCF/Tr.thy
changeset 18070 b653e18f0a41
parent 16756 e05c8039873a
child 18081 fe15796b257d
equal deleted inserted replaced
18069:f2c8f68a45e6 18070:b653e18f0a41
    18 
    18 
    19 translations
    19 translations
    20   "tr" <= (type) "bool lift" 
    20   "tr" <= (type) "bool lift" 
    21 
    21 
    22 consts
    22 consts
    23 	TT              :: "tr"
    23   TT     :: "tr"
    24 	FF              :: "tr"
    24   FF     :: "tr"
    25         Icifte          :: "tr -> 'c -> 'c -> 'c"
    25   Icifte :: "tr \<rightarrow> 'c \<rightarrow> 'c \<rightarrow> 'c"
    26         trand           :: "tr -> tr -> tr"
    26   trand  :: "tr \<rightarrow> tr \<rightarrow> tr"
    27         tror            :: "tr -> tr -> tr"
    27   tror   :: "tr \<rightarrow> tr \<rightarrow> tr"
    28         neg             :: "tr -> tr"
    28   neg    :: "tr \<rightarrow> tr"
    29         If2             :: "tr=>'c=>'c=>'c"
    29   If2    :: "[tr, 'c, 'c] \<Rightarrow> 'c"
    30 
    30 
    31 syntax  "@cifte"        :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
    31 syntax
    32         "@andalso"      :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
    32   "@cifte"   :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60)
    33         "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
    33   "@andalso" :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ andalso _" [36,35] 35)
       
    34   "@orelse"  :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ orelse _"  [31,30] 30)
    34  
    35  
    35 translations 
    36 translations
    36 	     "x andalso y" == "trand$x$y"
    37   "x andalso y" == "trand\<cdot>x\<cdot>y"
    37              "x orelse y"  == "tror$x$y"
    38   "x orelse y"  == "tror\<cdot>x\<cdot>y"
    38              "If b then e1 else e2 fi" == "Icifte$b$e1$e2"
    39   "If b then e1 else e2 fi" == "Icifte\<cdot>b\<cdot>e1\<cdot>e2"
       
    40 
    39 defs
    41 defs
    40   TT_def:      "TT==Def True"
    42   TT_def:      "TT==Def True"
    41   FF_def:      "FF==Def False"
    43   FF_def:      "FF==Def False"
    42   neg_def:     "neg == flift2 Not"
    44   neg_def:     "neg == flift2 Not"
    43   ifte_def:    "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
    45   ifte_def:    "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
    45   orelse_def:  "tror == (LAM x y. If x then TT else y fi)"
    47   orelse_def:  "tror == (LAM x y. If x then TT else y fi)"
    46   If2_def:     "If2 Q x y == If Q then x else y fi"
    48   If2_def:     "If2 Q x y == If Q then x else y fi"
    47 
    49 
    48 text {* Exhaustion and Elimination for type @{typ tr} *}
    50 text {* Exhaustion and Elimination for type @{typ tr} *}
    49 
    51 
    50 lemma Exh_tr: "t=UU | t = TT | t = FF"
    52 lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
    51 apply (unfold FF_def TT_def)
    53 apply (unfold FF_def TT_def)
    52 apply (induct_tac "t")
    54 apply (induct_tac "t")
    53 apply fast
    55 apply fast
    54 apply fast
    56 apply fast
    55 done
    57 done
    56 
    58 
    57 lemma trE: "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
    59 lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    58 apply (rule Exh_tr [THEN disjE])
    60 apply (rule Exh_tr [THEN disjE])
    59 apply fast
    61 apply fast
    60 apply (erule disjE)
    62 apply (erule disjE)
    61 apply fast
    63 apply fast
    62 apply fast
    64 apply fast
    74 		[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
    76 		[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
    75 	])
    77 	])
    76 *)
    78 *)
    77 text {* distinctness for type @{typ tr} *}
    79 text {* distinctness for type @{typ tr} *}
    78 
    80 
    79 lemma dist_less_tr [simp]: "~TT << UU" "~FF << UU" "~TT << FF" "~FF << TT"
    81 lemma dist_less_tr [simp]:
       
    82   "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
    80 by (simp_all add: tr_defs)
    83 by (simp_all add: tr_defs)
    81 
    84 
    82 lemma dist_eq_tr [simp]: "TT~=UU" "FF~=UU" "TT~=FF" "UU~=TT" "UU~=FF" "FF~=TT"
    85 lemma dist_eq_tr [simp]:
       
    86   "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
    83 by (simp_all add: tr_defs)
    87 by (simp_all add: tr_defs)
    84 
    88 
    85 text {* lemmas about andalso, orelse, neg and if *}
    89 text {* lemmas about andalso, orelse, neg and if *}
    86 
    90 
    87 lemma ifte_thms [simp]:
    91 lemma ifte_thms [simp]:
    88   "If UU then e1 else e2 fi = UU"
    92   "If \<bottom> then e1 else e2 fi = \<bottom>"
    89   "If FF then e1 else e2 fi = e2"
    93   "If FF then e1 else e2 fi = e2"
    90   "If TT then e1 else e2 fi = e1"
    94   "If TT then e1 else e2 fi = e1"
    91 by (simp_all add: ifte_def TT_def FF_def)
    95 by (simp_all add: ifte_def TT_def FF_def)
    92 
    96 
    93 lemma andalso_thms [simp]:
    97 lemma andalso_thms [simp]:
    94   "(TT andalso y) = y"
    98   "(TT andalso y) = y"
    95   "(FF andalso y) = FF"
    99   "(FF andalso y) = FF"
    96   "(UU andalso y) = UU"
   100   "(\<bottom> andalso y) = \<bottom>"
    97   "(y andalso TT) = y"
   101   "(y andalso TT) = y"
    98   "(y andalso y) = y"
   102   "(y andalso y) = y"
    99 apply (unfold andalso_def, simp_all)
   103 apply (unfold andalso_def, simp_all)
   100 apply (rule_tac p=y in trE, simp_all)
   104 apply (rule_tac p=y in trE, simp_all)
   101 apply (rule_tac p=y in trE, simp_all)
   105 apply (rule_tac p=y in trE, simp_all)
   102 done
   106 done
   103 
   107 
   104 lemma orelse_thms [simp]:
   108 lemma orelse_thms [simp]:
   105   "(TT orelse y) = TT"
   109   "(TT orelse y) = TT"
   106   "(FF orelse y) = y"
   110   "(FF orelse y) = y"
   107   "(UU orelse y) = UU"
   111   "(\<bottom> orelse y) = \<bottom>"
   108   "(y orelse FF) = y"
   112   "(y orelse FF) = y"
   109   "(y orelse y) = y"
   113   "(y orelse y) = y"
   110 apply (unfold orelse_def, simp_all)
   114 apply (unfold orelse_def, simp_all)
   111 apply (rule_tac p=y in trE, simp_all)
   115 apply (rule_tac p=y in trE, simp_all)
   112 apply (rule_tac p=y in trE, simp_all)
   116 apply (rule_tac p=y in trE, simp_all)
   113 done
   117 done
   114 
   118 
   115 lemma neg_thms [simp]:
   119 lemma neg_thms [simp]:
   116   "neg$TT = FF"
   120   "neg\<cdot>TT = FF"
   117   "neg$FF = TT"
   121   "neg\<cdot>FF = TT"
   118   "neg$UU = UU"
   122   "neg\<cdot>\<bottom> = \<bottom>"
   119 by (simp_all add: neg_def TT_def FF_def)
   123 by (simp_all add: neg_def TT_def FF_def)
   120 
   124 
   121 text {* split-tac for If via If2 because the constant has to be a constant *}
   125 text {* split-tac for If via If2 because the constant has to be a constant *}
   122   
   126   
   123 lemma split_If2: 
   127 lemma split_If2: 
   124   "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))"  
   128   "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
   125 apply (unfold If2_def)
   129 apply (unfold If2_def)
   126 apply (rule_tac p = "Q" in trE)
   130 apply (rule_tac p = "Q" in trE)
   127 apply (simp_all)
   131 apply (simp_all)
   128 done
   132 done
   129 
   133 
   134 *}
   138 *}
   135 
   139 
   136 subsection "Rewriting of HOLCF operations to HOL functions"
   140 subsection "Rewriting of HOLCF operations to HOL functions"
   137 
   141 
   138 lemma andalso_or: 
   142 lemma andalso_or: 
   139 "!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)"
   143   "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
   140 apply (rule_tac p = "t" in trE)
   144 apply (rule_tac p = "t" in trE)
   141 apply simp_all
   145 apply simp_all
   142 done
   146 done
   143 
   147 
   144 lemma andalso_and: "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)"
   148 lemma andalso_and:
       
   149   "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
   145 apply (rule_tac p = "t" in trE)
   150 apply (rule_tac p = "t" in trE)
   146 apply simp_all
   151 apply simp_all
   147 done
   152 done
   148 
   153 
   149 lemma Def_bool1 [simp]: "(Def x ~= FF) = x"
   154 lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x"
   150 by (simp add: FF_def)
   155 by (simp add: FF_def)
   151 
   156 
   152 lemma Def_bool2 [simp]: "(Def x = FF) = (~x)"
   157 lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)"
   153 by (simp add: FF_def)
   158 by (simp add: FF_def)
   154 
   159 
   155 lemma Def_bool3 [simp]: "(Def x = TT) = x"
   160 lemma Def_bool3 [simp]: "(Def x = TT) = x"
   156 by (simp add: TT_def)
   161 by (simp add: TT_def)
   157 
   162 
   158 lemma Def_bool4 [simp]: "(Def x ~= TT) = (~x)"
   163 lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)"
   159 by (simp add: TT_def)
   164 by (simp add: TT_def)
   160 
   165 
   161 lemma If_and_if: 
   166 lemma If_and_if: 
   162   "(If Def P then A else B fi)= (if P then A else B)"
   167   "(If Def P then A else B fi) = (if P then A else B)"
   163 apply (rule_tac p = "Def P" in trE)
   168 apply (rule_tac p = "Def P" in trE)
   164 apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
   169 apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
   165 done
   170 done
   166 
   171 
   167 subsection "admissibility"
   172 subsection {* Compactness *}
   168 
   173 
   169 text {*
   174 lemma compact_TT [simp]: "compact TT"
   170    The following rewrite rules for admissibility should in the future be 
   175 by (rule compact_chfin)
   171    replaced by a more general admissibility test that also checks 
       
   172    chain-finiteness, of which these lemmata are specific examples
       
   173 *}
       
   174 
   176 
   175 lemma adm_trick_1: "(x~=FF) = (x=TT|x=UU)"
   177 lemma compact_FF [simp]: "compact FF"
   176 apply (rule_tac p = "x" in trE)
   178 by (rule compact_chfin)
   177 apply (simp_all)
       
   178 done
       
   179 
       
   180 lemma adm_trick_2: "(x~=TT) = (x=FF|x=UU)"
       
   181 apply (rule_tac p = "x" in trE)
       
   182 apply (simp_all)
       
   183 done
       
   184 
       
   185 lemmas adm_tricks = adm_trick_1 adm_trick_2
       
   186 
       
   187 lemma adm_nTT [simp]: "cont(f) ==> adm (%x. (f x)~=TT)"
       
   188 by (simp add: adm_tricks)
       
   189 
       
   190 lemma adm_nFF [simp]: "cont(f) ==> adm (%x. (f x)~=FF)"
       
   191 by (simp add: adm_tricks)
       
   192 
   179 
   193 end
   180 end