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