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