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