src/HOL/Datatype.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 20105 454f4be984b7
child 20453 855f07fabd76
permissions -rw-r--r--
simplified code generator setup
     1 (*  Title:      HOL/Datatype.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {* Datatypes *}
     7 
     8 theory Datatype
     9 imports Datatype_Universe
    10 begin
    11 
    12 subsection {* Representing primitive types *}
    13 
    14 rep_datatype bool
    15   distinct True_not_False False_not_True
    16   induction bool_induct
    17 
    18 declare case_split [cases type: bool]
    19   -- "prefer plain propositional version"
    20 
    21 rep_datatype unit
    22   induction unit_induct
    23 
    24 rep_datatype prod
    25   inject Pair_eq
    26   induction prod_induct
    27 
    28 rep_datatype sum
    29   distinct Inl_not_Inr Inr_not_Inl
    30   inject Inl_eq Inr_eq
    31   induction sum_induct
    32 
    33 ML {*
    34   val [sum_case_Inl, sum_case_Inr] = thms "sum.cases";
    35   bind_thm ("sum_case_Inl", sum_case_Inl);
    36   bind_thm ("sum_case_Inr", sum_case_Inr);
    37 *} -- {* compatibility *}
    38 
    39 lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
    40   apply (rule_tac s = s in sumE)
    41    apply (erule ssubst)
    42    apply (rule sum_case_Inl)
    43   apply (erule ssubst)
    44   apply (rule sum_case_Inr)
    45   done
    46 
    47 lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
    48   -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
    49   by (erule arg_cong)
    50 
    51 lemma sum_case_inject:
    52   "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
    53 proof -
    54   assume a: "sum_case f1 f2 = sum_case g1 g2"
    55   assume r: "f1 = g1 ==> f2 = g2 ==> P"
    56   show P
    57     apply (rule r)
    58      apply (rule ext)
    59      apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
    60     apply (rule ext)
    61     apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
    62     done
    63 qed
    64 
    65 constdefs
    66   Suml :: "('a => 'c) => 'a + 'b => 'c"
    67   "Suml == (%f. sum_case f arbitrary)"
    68 
    69   Sumr :: "('b => 'c) => 'a + 'b => 'c"
    70   "Sumr == sum_case arbitrary"
    71 
    72 lemma Suml_inject: "Suml f = Suml g ==> f = g"
    73   by (unfold Suml_def) (erule sum_case_inject)
    74 
    75 lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
    76   by (unfold Sumr_def) (erule sum_case_inject)
    77 
    78 
    79 subsection {* Finishing the datatype package setup *}
    80 
    81 text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
    82 hide (open) const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
    83 hide (open) type node item
    84 
    85 
    86 subsection {* Further cases/induct rules for tuples *}
    87 
    88 lemma prod_cases3 [case_names fields, cases type]:
    89     "(!!a b c. y = (a, b, c) ==> P) ==> P"
    90   apply (cases y)
    91   apply (case_tac b, blast)
    92   done
    93 
    94 lemma prod_induct3 [case_names fields, induct type]:
    95     "(!!a b c. P (a, b, c)) ==> P x"
    96   by (cases x) blast
    97 
    98 lemma prod_cases4 [case_names fields, cases type]:
    99     "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
   100   apply (cases y)
   101   apply (case_tac c, blast)
   102   done
   103 
   104 lemma prod_induct4 [case_names fields, induct type]:
   105     "(!!a b c d. P (a, b, c, d)) ==> P x"
   106   by (cases x) blast
   107 
   108 lemma prod_cases5 [case_names fields, cases type]:
   109     "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
   110   apply (cases y)
   111   apply (case_tac d, blast)
   112   done
   113 
   114 lemma prod_induct5 [case_names fields, induct type]:
   115     "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
   116   by (cases x) blast
   117 
   118 lemma prod_cases6 [case_names fields, cases type]:
   119     "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
   120   apply (cases y)
   121   apply (case_tac e, blast)
   122   done
   123 
   124 lemma prod_induct6 [case_names fields, induct type]:
   125     "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
   126   by (cases x) blast
   127 
   128 lemma prod_cases7 [case_names fields, cases type]:
   129     "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
   130   apply (cases y)
   131   apply (case_tac f, blast)
   132   done
   133 
   134 lemma prod_induct7 [case_names fields, induct type]:
   135     "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   136   by (cases x) blast
   137 
   138 
   139 subsection {* The option type *}
   140 
   141 datatype 'a option = None | Some 'a
   142 
   143 lemma not_None_eq[iff]: "(x ~= None) = (EX y. x = Some y)"
   144   by (induct x) auto
   145 
   146 lemma not_Some_eq[iff]: "(ALL y. x ~= Some y) = (x = None)"
   147   by (induct x) auto
   148 
   149 text{*Although it may appear that both of these equalities are helpful
   150 only when applied to assumptions, in practice it seems better to give
   151 them the uniform iff attribute. *}
   152 
   153 (*
   154 lemmas not_None_eq_D = not_None_eq [THEN iffD1]
   155 declare not_None_eq_D [dest!]
   156 
   157 lemmas not_Some_eq_D = not_Some_eq [THEN iffD1]
   158 declare not_Some_eq_D [dest!]
   159 *)
   160 
   161 lemma option_caseE:
   162   "(case x of None => P | Some y => Q y) ==>
   163     (x = None ==> P ==> R) ==>
   164     (!!y. x = Some y ==> Q y ==> R) ==> R"
   165   by (cases x) simp_all
   166 
   167 
   168 subsubsection {* Operations *}
   169 
   170 consts
   171   the :: "'a option => 'a"
   172 primrec
   173   "the (Some x) = x"
   174 
   175 consts
   176   o2s :: "'a option => 'a set"
   177 primrec
   178   "o2s None = {}"
   179   "o2s (Some x) = {x}"
   180 
   181 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   182   by simp
   183 
   184 ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
   185 
   186 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   187   by (cases xo) auto
   188 
   189 lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
   190   by (cases xo) auto
   191 
   192 
   193 constdefs
   194   option_map :: "('a => 'b) => ('a option => 'b option)"
   195   "option_map == %f y. case y of None => None | Some x => Some (f x)"
   196 
   197 lemma option_map_None [simp]: "option_map f None = None"
   198   by (simp add: option_map_def)
   199 
   200 lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
   201   by (simp add: option_map_def)
   202 
   203 lemma option_map_is_None[iff]:
   204  "(option_map f opt = None) = (opt = None)"
   205 by (simp add: option_map_def split add: option.split)
   206 
   207 lemma option_map_eq_Some [iff]:
   208     "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
   209 by (simp add: option_map_def split add: option.split)
   210 
   211 lemma option_map_comp:
   212  "option_map f (option_map g opt) = option_map (f o g) opt"
   213 by (simp add: option_map_def split add: option.split)
   214 
   215 lemma option_map_o_sum_case [simp]:
   216     "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
   217   apply (rule ext)
   218   apply (simp split add: sum.split)
   219   done
   220 
   221 
   222 subsubsection {* Codegenerator setup *}
   223 
   224 consts
   225   is_none :: "'a option \<Rightarrow> bool"
   226 primrec
   227   "is_none None = True"
   228   "is_none (Some x) = False"
   229 
   230 lemma is_none_none [code inline]:
   231   "(x = None) = (is_none x)" 
   232 by (cases x) simp_all
   233 
   234 lemmas [code] = imp_conv_disj
   235 
   236 lemma [code fun]:
   237   "(\<not> True) = False" by (rule HOL.simp_thms)
   238 
   239 lemma [code fun]:
   240   "(\<not> False) = True" by (rule HOL.simp_thms)
   241 
   242 lemma [code fun]:
   243   shows "(False \<and> x) = False"
   244   and   "(True \<and> x) = x"
   245   and   "(x \<and> False) = False"
   246   and   "(x \<and> True) = x" by simp_all
   247 
   248 lemma [code fun]:
   249   shows "(False \<or> x) = x"
   250   and   "(True \<or> x) = True"
   251   and   "(x \<or> False) = x"
   252   and   "(x \<or> True) = True" by simp_all
   253 
   254 declare
   255   if_True [code fun]
   256   if_False [code fun]
   257   fst_conv [code]
   258   snd_conv [code]
   259 
   260 lemma split_is_prod_case [code inline]:
   261   "split = prod_case"
   262 by (simp add: expand_fun_eq split_def prod.cases)
   263 
   264 code_typapp bool
   265   ml (target_atom "bool")
   266   haskell (target_atom "Bool")
   267 
   268 code_constapp
   269   True
   270     ml (target_atom "true")
   271     haskell (target_atom "True")
   272   False
   273     ml (target_atom "false")
   274     haskell (target_atom "False")
   275   Not
   276     ml (target_atom "not")
   277     haskell (target_atom "not")
   278   "op &"
   279     ml (infixl 1 "andalso")
   280     haskell (infixl 3 "&&")
   281   "op |"
   282     ml (infixl 0 "orelse")
   283     haskell (infixl 2 "||")
   284   If
   285     ml (target_atom "(if __/ then __/ else __)")
   286     haskell (target_atom "(if __/ then __/ else __)")
   287 
   288 code_typapp
   289   *
   290     ml (infix 2 "*")
   291     haskell (target_atom "(__,/ __)")
   292 
   293 code_constapp
   294   Pair
   295     ml (target_atom "(__,/ __)")
   296     haskell (target_atom "(__,/ __)")
   297 
   298 code_typapp
   299   unit
   300     ml (target_atom "unit")
   301     haskell (target_atom "()")
   302 
   303 code_constapp
   304   Unity
   305     ml (target_atom "()")
   306     haskell (target_atom "()")
   307 
   308 code_typapp
   309   option
   310     ml ("_ option")
   311     haskell ("Maybe _")
   312 
   313 code_constapp
   314   None
   315     ml (target_atom "NONE")
   316     haskell (target_atom "Nothing")
   317   Some
   318     ml (target_atom "SOME")
   319     haskell (target_atom "Just")
   320 
   321 end