src/HOL/Datatype.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14274 0cb8a9a144d2
child 15131 c69542757a4d
permissions -rw-r--r--
Merged in license change from Isabelle2004
     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 = Datatype_Universe:
     9 
    10 subsection {* Representing primitive types *}
    11 
    12 rep_datatype bool
    13   distinct True_not_False False_not_True
    14   induction bool_induct
    15 
    16 declare case_split [cases type: bool]
    17   -- "prefer plain propositional version"
    18 
    19 rep_datatype unit
    20   induction unit_induct
    21 
    22 rep_datatype prod
    23   inject Pair_eq
    24   induction prod_induct
    25 
    26 rep_datatype sum
    27   distinct Inl_not_Inr Inr_not_Inl
    28   inject Inl_eq Inr_eq
    29   induction sum_induct
    30 
    31 ML {*
    32   val [sum_case_Inl, sum_case_Inr] = thms "sum.cases";
    33   bind_thm ("sum_case_Inl", sum_case_Inl);
    34   bind_thm ("sum_case_Inr", sum_case_Inr);
    35 *} -- {* compatibility *}
    36 
    37 lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
    38   apply (rule_tac s = s in sumE)
    39    apply (erule ssubst)
    40    apply (rule sum_case_Inl)
    41   apply (erule ssubst)
    42   apply (rule sum_case_Inr)
    43   done
    44 
    45 lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
    46   -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
    47   by (erule arg_cong)
    48 
    49 lemma sum_case_inject:
    50   "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
    51 proof -
    52   assume a: "sum_case f1 f2 = sum_case g1 g2"
    53   assume r: "f1 = g1 ==> f2 = g2 ==> P"
    54   show P
    55     apply (rule r)
    56      apply (rule ext)
    57      apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
    58     apply (rule ext)
    59     apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
    60     done
    61 qed
    62 
    63 constdefs
    64   Suml :: "('a => 'c) => 'a + 'b => 'c"
    65   "Suml == (%f. sum_case f arbitrary)"
    66 
    67   Sumr :: "('b => 'c) => 'a + 'b => 'c"
    68   "Sumr == sum_case arbitrary"
    69 
    70 lemma Suml_inject: "Suml f = Suml g ==> f = g"
    71   by (unfold Suml_def) (erule sum_case_inject)
    72 
    73 lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
    74   by (unfold Sumr_def) (erule sum_case_inject)
    75 
    76 
    77 subsection {* Finishing the datatype package setup *}
    78 
    79 text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
    80 hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
    81 hide type node item
    82 
    83 
    84 subsection {* Further cases/induct rules for tuples *}
    85 
    86 lemma prod_cases3 [case_names fields, cases type]:
    87     "(!!a b c. y = (a, b, c) ==> P) ==> P"
    88   apply (cases y)
    89   apply (case_tac b, blast)
    90   done
    91 
    92 lemma prod_induct3 [case_names fields, induct type]:
    93     "(!!a b c. P (a, b, c)) ==> P x"
    94   by (cases x) blast
    95 
    96 lemma prod_cases4 [case_names fields, cases type]:
    97     "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    98   apply (cases y)
    99   apply (case_tac c, blast)
   100   done
   101 
   102 lemma prod_induct4 [case_names fields, induct type]:
   103     "(!!a b c d. P (a, b, c, d)) ==> P x"
   104   by (cases x) blast
   105 
   106 lemma prod_cases5 [case_names fields, cases type]:
   107     "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
   108   apply (cases y)
   109   apply (case_tac d, blast)
   110   done
   111 
   112 lemma prod_induct5 [case_names fields, induct type]:
   113     "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
   114   by (cases x) blast
   115 
   116 lemma prod_cases6 [case_names fields, cases type]:
   117     "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
   118   apply (cases y)
   119   apply (case_tac e, blast)
   120   done
   121 
   122 lemma prod_induct6 [case_names fields, induct type]:
   123     "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
   124   by (cases x) blast
   125 
   126 lemma prod_cases7 [case_names fields, cases type]:
   127     "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
   128   apply (cases y)
   129   apply (case_tac f, blast)
   130   done
   131 
   132 lemma prod_induct7 [case_names fields, induct type]:
   133     "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   134   by (cases x) blast
   135 
   136 
   137 subsection {* The option type *}
   138 
   139 datatype 'a option = None | Some 'a
   140 
   141 lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
   142   by (induct x) auto
   143 
   144 lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
   145   by (induct x) auto
   146 
   147 lemma option_caseE:
   148   "(case x of None => P | Some y => Q y) ==>
   149     (x = None ==> P ==> R) ==>
   150     (!!y. x = Some y ==> Q y ==> R) ==> R"
   151   by (cases x) simp_all
   152 
   153 
   154 subsubsection {* Operations *}
   155 
   156 consts
   157   the :: "'a option => 'a"
   158 primrec
   159   "the (Some x) = x"
   160 
   161 consts
   162   o2s :: "'a option => 'a set"
   163 primrec
   164   "o2s None = {}"
   165   "o2s (Some x) = {x}"
   166 
   167 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   168   by simp
   169 
   170 ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *}
   171 
   172 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   173   by (cases xo) auto
   174 
   175 lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
   176   by (cases xo) auto
   177 
   178 
   179 constdefs
   180   option_map :: "('a => 'b) => ('a option => 'b option)"
   181   "option_map == %f y. case y of None => None | Some x => Some (f x)"
   182 
   183 lemma option_map_None [simp]: "option_map f None = None"
   184   by (simp add: option_map_def)
   185 
   186 lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
   187   by (simp add: option_map_def)
   188 
   189 lemma option_map_is_None[iff]:
   190  "(option_map f opt = None) = (opt = None)"
   191 by (simp add: option_map_def split add: option.split)
   192 
   193 lemma option_map_eq_Some [iff]:
   194     "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
   195 by (simp add: option_map_def split add: option.split)
   196 
   197 lemma option_map_comp:
   198  "option_map f (option_map g opt) = option_map (f o g) opt"
   199 by (simp add: option_map_def split add: option.split)
   200 
   201 lemma option_map_o_sum_case [simp]:
   202     "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
   203   apply (rule ext)
   204   apply (simp split add: sum.split)
   205   done
   206 
   207 end