src/HOL/Datatype.thy
author nipkow
Sun Sep 14 17:53:27 2003 +0200 (2003-09-14)
changeset 14187 26dfcd0ac436
parent 13635 c41e88151b54
child 14208 144f45277d5a
permissions -rw-r--r--
Added new theorems
     1 (*  Title:      HOL/Datatype.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Datatypes *}
     8 
     9 theory Datatype = Datatype_Universe:
    10 
    11 subsection {* Representing primitive types *}
    12 
    13 rep_datatype bool
    14   distinct True_not_False False_not_True
    15   induction bool_induct
    16 
    17 declare case_split [cases type: bool]
    18   -- "prefer plain propositional version"
    19 
    20 rep_datatype unit
    21   induction unit_induct
    22 
    23 rep_datatype prod
    24   inject Pair_eq
    25   induction prod_induct
    26 
    27 rep_datatype sum
    28   distinct Inl_not_Inr Inr_not_Inl
    29   inject Inl_eq Inr_eq
    30   induction sum_induct
    31 
    32 ML {*
    33   val [sum_case_Inl, sum_case_Inr] = thms "sum.cases";
    34   bind_thm ("sum_case_Inl", sum_case_Inl);
    35   bind_thm ("sum_case_Inr", sum_case_Inr);
    36 *} -- {* compatibility *}
    37 
    38 lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
    39   apply (rule_tac s = s in sumE)
    40    apply (erule ssubst)
    41    apply (rule sum_case_Inl)
    42   apply (erule ssubst)
    43   apply (rule sum_case_Inr)
    44   done
    45 
    46 lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
    47   -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
    48   by (erule arg_cong)
    49 
    50 lemma sum_case_inject:
    51   "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
    52 proof -
    53   assume a: "sum_case f1 f2 = sum_case g1 g2"
    54   assume r: "f1 = g1 ==> f2 = g2 ==> P"
    55   show P
    56     apply (rule r)
    57      apply (rule ext)
    58      apply (cut_tac x = "Inl x" in a [THEN fun_cong])
    59      apply simp
    60     apply (rule ext)
    61     apply (cut_tac x = "Inr x" in a [THEN fun_cong])
    62     apply 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 const Node Atom Leaf Numb Lim Split Case Suml Sumr
    84 hide 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)
    93   apply 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)
   104   apply blast
   105   done
   106 
   107 lemma prod_induct4 [case_names fields, induct type]:
   108     "(!!a b c d. P (a, b, c, d)) ==> P x"
   109   by (cases x) blast
   110 
   111 lemma prod_cases5 [case_names fields, cases type]:
   112     "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
   113   apply (cases y)
   114   apply (case_tac d)
   115   apply blast
   116   done
   117 
   118 lemma prod_induct5 [case_names fields, induct type]:
   119     "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
   120   by (cases x) blast
   121 
   122 lemma prod_cases6 [case_names fields, cases type]:
   123     "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
   124   apply (cases y)
   125   apply (case_tac e)
   126   apply blast
   127   done
   128 
   129 lemma prod_induct6 [case_names fields, induct type]:
   130     "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
   131   by (cases x) blast
   132 
   133 lemma prod_cases7 [case_names fields, cases type]:
   134     "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
   135   apply (cases y)
   136   apply (case_tac f)
   137   apply blast
   138   done
   139 
   140 lemma prod_induct7 [case_names fields, induct type]:
   141     "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   142   by (cases x) blast
   143 
   144 
   145 subsection {* The option type *}
   146 
   147 datatype 'a option = None | Some 'a
   148 
   149 lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
   150   by (induct x) auto
   151 
   152 lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
   153   by (induct x) auto
   154 
   155 lemma option_caseE:
   156   "(case x of None => P | Some y => Q y) ==>
   157     (x = None ==> P ==> R) ==>
   158     (!!y. x = Some y ==> Q y ==> R) ==> R"
   159   by (cases x) simp_all
   160 
   161 
   162 subsubsection {* Operations *}
   163 
   164 consts
   165   the :: "'a option => 'a"
   166 primrec
   167   "the (Some x) = x"
   168 
   169 consts
   170   o2s :: "'a option => 'a set"
   171 primrec
   172   "o2s None = {}"
   173   "o2s (Some x) = {x}"
   174 
   175 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   176   by simp
   177 
   178 ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *}
   179 
   180 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   181   by (cases xo) auto
   182 
   183 lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
   184   by (cases xo) auto
   185 
   186 
   187 constdefs
   188   option_map :: "('a => 'b) => ('a option => 'b option)"
   189   "option_map == %f y. case y of None => None | Some x => Some (f x)"
   190 
   191 lemma option_map_None [simp]: "option_map f None = None"
   192   by (simp add: option_map_def)
   193 
   194 lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
   195   by (simp add: option_map_def)
   196 
   197 lemma option_map_is_None[iff]:
   198  "(option_map f opt = None) = (opt = None)"
   199 by (simp add: option_map_def split add: option.split)
   200 
   201 lemma option_map_eq_Some [iff]:
   202     "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
   203 by (simp add: option_map_def split add: option.split)
   204 
   205 lemma option_map_comp:
   206  "option_map f (option_map g opt) = option_map (f o g) opt"
   207 by (simp add: option_map_def split add: option.split)
   208 
   209 lemma option_map_o_sum_case [simp]:
   210     "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
   211   apply (rule ext)
   212   apply (simp split add: sum.split)
   213   done
   214 
   215 end