src/HOLCF/Tr.thy
author huffman
Mon May 11 08:28:09 2009 -0700 (2009-05-11)
changeset 31095 b79d140f6d0b
parent 31076 99fe356cbbc2
child 35431 8758fe1fc9f8
permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
     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   "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: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    33 unfolding FF_def TT_def by (induct p) auto
    34 
    35 lemma tr_induct: "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
    36 by (cases x rule: trE) simp_all
    37 
    38 text {* distinctness for type @{typ tr} *}
    39 
    40 lemma dist_below_tr [simp]:
    41   "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
    42 unfolding TT_def FF_def by simp_all
    43 
    44 lemma dist_eq_tr [simp]:
    45   "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
    46 unfolding TT_def FF_def by simp_all
    47 
    48 lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
    49 by (induct x rule: tr_induct) simp_all
    50 
    51 lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
    52 by (induct x rule: tr_induct) simp_all
    53 
    54 lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
    55 by (induct x rule: tr_induct) simp_all
    56 
    57 lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
    58 by (induct x rule: tr_induct) simp_all
    59 
    60 
    61 subsection {* Case analysis *}
    62 
    63 defaultsort pcpo
    64 
    65 definition
    66   trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
    67   ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)"
    68 abbreviation
    69   cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(3If _/ (then _/ else _) fi)" 60)  where
    70   "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
    71 
    72 translations
    73   "\<Lambda> (XCONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
    74   "\<Lambda> (XCONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
    75 
    76 lemma ifte_thms [simp]:
    77   "If \<bottom> then e1 else e2 fi = \<bottom>"
    78   "If FF then e1 else e2 fi = e2"
    79   "If TT then e1 else e2 fi = e1"
    80 by (simp_all add: ifte_def TT_def FF_def)
    81 
    82 
    83 subsection {* Boolean connectives *}
    84 
    85 definition
    86   trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
    87   andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)"
    88 abbreviation
    89   andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)  where
    90   "x andalso y == trand\<cdot>x\<cdot>y"
    91 
    92 definition
    93   tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
    94   orelse_def: "tror = (\<Lambda> x y. If x then TT else y fi)"
    95 abbreviation
    96   orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)  where
    97   "x orelse y == tror\<cdot>x\<cdot>y"
    98 
    99 definition
   100   neg :: "tr \<rightarrow> tr" where
   101   "neg = flift2 Not"
   102 
   103 definition
   104   If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
   105   "If2 Q x y = (If Q then x else y fi)"
   106 
   107 text {* tactic for tr-thms with case split *}
   108 
   109 lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
   110 
   111 text {* lemmas about andalso, orelse, neg and if *}
   112 
   113 lemma andalso_thms [simp]:
   114   "(TT andalso y) = y"
   115   "(FF andalso y) = FF"
   116   "(\<bottom> andalso y) = \<bottom>"
   117   "(y andalso TT) = y"
   118   "(y andalso y) = y"
   119 apply (unfold andalso_def, simp_all)
   120 apply (cases y rule: trE, simp_all)
   121 apply (cases y rule: trE, simp_all)
   122 done
   123 
   124 lemma orelse_thms [simp]:
   125   "(TT orelse y) = TT"
   126   "(FF orelse y) = y"
   127   "(\<bottom> orelse y) = \<bottom>"
   128   "(y orelse FF) = y"
   129   "(y orelse y) = y"
   130 apply (unfold orelse_def, simp_all)
   131 apply (cases y rule: trE, simp_all)
   132 apply (cases y rule: trE, simp_all)
   133 done
   134 
   135 lemma neg_thms [simp]:
   136   "neg\<cdot>TT = FF"
   137   "neg\<cdot>FF = TT"
   138   "neg\<cdot>\<bottom> = \<bottom>"
   139 by (simp_all add: neg_def TT_def FF_def)
   140 
   141 text {* split-tac for If via If2 because the constant has to be a constant *}
   142 
   143 lemma split_If2:
   144   "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
   145 apply (unfold If2_def)
   146 apply (rule_tac p = "Q" in trE)
   147 apply (simp_all)
   148 done
   149 
   150 ML {*
   151 val split_If_tac =
   152   simp_tac (HOL_basic_ss addsimps [@{thm If2_def} RS sym])
   153     THEN' (split_tac [@{thm split_If2}])
   154 *}
   155 
   156 subsection "Rewriting of HOLCF operations to HOL functions"
   157 
   158 lemma andalso_or:
   159   "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
   160 apply (rule_tac p = "t" in trE)
   161 apply simp_all
   162 done
   163 
   164 lemma andalso_and:
   165   "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
   166 apply (rule_tac p = "t" in trE)
   167 apply simp_all
   168 done
   169 
   170 lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x"
   171 by (simp add: FF_def)
   172 
   173 lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)"
   174 by (simp add: FF_def)
   175 
   176 lemma Def_bool3 [simp]: "(Def x = TT) = x"
   177 by (simp add: TT_def)
   178 
   179 lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)"
   180 by (simp add: TT_def)
   181 
   182 lemma If_and_if:
   183   "(If Def P then A else B fi) = (if P then A else B)"
   184 apply (rule_tac p = "Def P" in trE)
   185 apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
   186 done
   187 
   188 subsection {* Compactness *}
   189 
   190 lemma compact_TT: "compact TT"
   191 by (rule compact_chfin)
   192 
   193 lemma compact_FF: "compact FF"
   194 by (rule compact_chfin)
   195 
   196 end