removed obsolete sum_case_Inl/Inr;
authorwenzelm
Sat Sep 30 21:39:20 2006 +0200 (2006-09-30)
changeset 207983275b03e2fff
parent 20797 c1f0bc7e7d80
child 20799 46694b230cfb
removed obsolete sum_case_Inl/Inr;
moved 'hide' to Datatype_Universe;
tuned proofs;
src/HOL/Datatype.thy
     1.1 --- a/src/HOL/Datatype.thy	Sat Sep 30 21:39:17 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Sat Sep 30 21:39:20 2006 +0200
     1.3 @@ -32,23 +32,17 @@
     1.4    inject Inl_eq Inr_eq
     1.5    induction sum_induct
     1.6  
     1.7 -ML {*
     1.8 -  val [sum_case_Inl, sum_case_Inr] = thms "sum.cases";
     1.9 -  bind_thm ("sum_case_Inl", sum_case_Inl);
    1.10 -  bind_thm ("sum_case_Inr", sum_case_Inr);
    1.11 -*} -- {* compatibility *}
    1.12 -
    1.13  lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
    1.14    apply (rule_tac s = s in sumE)
    1.15     apply (erule ssubst)
    1.16 -   apply (rule sum_case_Inl)
    1.17 +   apply (rule sum.cases(1))
    1.18    apply (erule ssubst)
    1.19 -  apply (rule sum_case_Inr)
    1.20 +  apply (rule sum.cases(2))
    1.21    done
    1.22  
    1.23  lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
    1.24    -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
    1.25 -  by (erule arg_cong)
    1.26 +  by simp
    1.27  
    1.28  lemma sum_case_inject:
    1.29    "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
    1.30 @@ -77,61 +71,46 @@
    1.31  lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
    1.32    by (unfold Sumr_def) (erule sum_case_inject)
    1.33  
    1.34 -
    1.35 -subsection {* Finishing the datatype package setup *}
    1.36 -
    1.37 -text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
    1.38 -hide (open) const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
    1.39 -hide (open) type node item
    1.40 +hide (open) const Suml Sumr
    1.41  
    1.42  
    1.43  subsection {* Further cases/induct rules for tuples *}
    1.44  
    1.45 -lemma prod_cases3 [case_names fields, cases type]:
    1.46 -    "(!!a b c. y = (a, b, c) ==> P) ==> P"
    1.47 -  apply (cases y)
    1.48 -  apply (case_tac b, blast)
    1.49 -  done
    1.50 +lemma prod_cases3 [cases type]:
    1.51 +  obtains (fields) a b c where "y = (a, b, c)"
    1.52 +  by (cases y, case_tac b) blast
    1.53  
    1.54  lemma prod_induct3 [case_names fields, induct type]:
    1.55      "(!!a b c. P (a, b, c)) ==> P x"
    1.56    by (cases x) blast
    1.57  
    1.58 -lemma prod_cases4 [case_names fields, cases type]:
    1.59 -    "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    1.60 -  apply (cases y)
    1.61 -  apply (case_tac c, blast)
    1.62 -  done
    1.63 +lemma prod_cases4 [cases type]:
    1.64 +  obtains (fields) a b c d where "y = (a, b, c, d)"
    1.65 +  by (cases y, case_tac c) blast
    1.66  
    1.67  lemma prod_induct4 [case_names fields, induct type]:
    1.68      "(!!a b c d. P (a, b, c, d)) ==> P x"
    1.69    by (cases x) blast
    1.70  
    1.71 -lemma prod_cases5 [case_names fields, cases type]:
    1.72 -    "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
    1.73 -  apply (cases y)
    1.74 -  apply (case_tac d, blast)
    1.75 -  done
    1.76 +lemma prod_cases5 [cases type]:
    1.77 +  obtains (fields) a b c d e where "y = (a, b, c, d, e)"
    1.78 +  by (cases y, case_tac d) blast
    1.79  
    1.80  lemma prod_induct5 [case_names fields, induct type]:
    1.81      "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
    1.82    by (cases x) blast
    1.83  
    1.84 -lemma prod_cases6 [case_names fields, cases type]:
    1.85 -    "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
    1.86 -  apply (cases y)
    1.87 -  apply (case_tac e, blast)
    1.88 -  done
    1.89 +lemma prod_cases6 [cases type]:
    1.90 +  obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
    1.91 +  by (cases y, case_tac e) blast
    1.92  
    1.93  lemma prod_induct6 [case_names fields, induct type]:
    1.94      "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
    1.95    by (cases x) blast
    1.96  
    1.97 -lemma prod_cases7 [case_names fields, cases type]:
    1.98 -    "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
    1.99 -  apply (cases y)
   1.100 -  apply (case_tac f, blast)
   1.101 -  done
   1.102 +lemma prod_cases7 [cases type]:
   1.103 +  obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
   1.104 +  by (cases y, case_tac f) blast
   1.105  
   1.106  lemma prod_induct7 [case_names fields, induct type]:
   1.107      "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   1.108 @@ -142,29 +121,22 @@
   1.109  
   1.110  datatype 'a option = None | Some 'a
   1.111  
   1.112 -lemma not_None_eq[iff]: "(x ~= None) = (EX y. x = Some y)"
   1.113 +lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
   1.114    by (induct x) auto
   1.115  
   1.116 -lemma not_Some_eq[iff]: "(ALL y. x ~= Some y) = (x = None)"
   1.117 +lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
   1.118    by (induct x) auto
   1.119  
   1.120  text{*Although it may appear that both of these equalities are helpful
   1.121  only when applied to assumptions, in practice it seems better to give
   1.122  them the uniform iff attribute. *}
   1.123  
   1.124 -(*
   1.125 -lemmas not_None_eq_D = not_None_eq [THEN iffD1]
   1.126 -declare not_None_eq_D [dest!]
   1.127 -
   1.128 -lemmas not_Some_eq_D = not_Some_eq [THEN iffD1]
   1.129 -declare not_Some_eq_D [dest!]
   1.130 -*)
   1.131 -
   1.132  lemma option_caseE:
   1.133 -  "(case x of None => P | Some y => Q y) ==>
   1.134 -    (x = None ==> P ==> R) ==>
   1.135 -    (!!y. x = Some y ==> Q y ==> R) ==> R"
   1.136 -  by (cases x) simp_all
   1.137 +  assumes c: "(case x of None => P | Some y => Q y)"
   1.138 +  obtains
   1.139 +    (None) "x = None" and P
   1.140 +  | (Some) y where "x = Some y" and "Q y"
   1.141 +  using c by (cases x) simp_all
   1.142  
   1.143  
   1.144  subsubsection {* Operations *}
   1.145 @@ -202,23 +174,21 @@
   1.146  lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
   1.147    by (simp add: option_map_def)
   1.148  
   1.149 -lemma option_map_is_None[iff]:
   1.150 - "(option_map f opt = None) = (opt = None)"
   1.151 -by (simp add: option_map_def split add: option.split)
   1.152 +lemma option_map_is_None [iff]:
   1.153 +    "(option_map f opt = None) = (opt = None)"
   1.154 +  by (simp add: option_map_def split add: option.split)
   1.155  
   1.156  lemma option_map_eq_Some [iff]:
   1.157      "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
   1.158 -by (simp add: option_map_def split add: option.split)
   1.159 +  by (simp add: option_map_def split add: option.split)
   1.160  
   1.161  lemma option_map_comp:
   1.162 - "option_map f (option_map g opt) = option_map (f o g) opt"
   1.163 -by (simp add: option_map_def split add: option.split)
   1.164 +    "option_map f (option_map g opt) = option_map (f o g) opt"
   1.165 +  by (simp add: option_map_def split add: option.split)
   1.166  
   1.167  lemma option_map_o_sum_case [simp]:
   1.168      "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"
   1.169 -  apply (rule ext)
   1.170 -  apply (simp split add: sum.split)
   1.171 -  done
   1.172 +  by (rule ext) (simp split: sum.split)
   1.173  
   1.174  
   1.175  subsubsection {* Codegenerator setup *}
   1.176 @@ -230,8 +200,8 @@
   1.177    "is_none (Some x) = False"
   1.178  
   1.179  lemma is_none_none [code inline]:
   1.180 -  "(x = None) = (is_none x)" 
   1.181 -by (cases x) simp_all
   1.182 +    "(x = None) = (is_none x)" 
   1.183 +  by (cases x) simp_all
   1.184  
   1.185  lemmas [code] = imp_conv_disj
   1.186  
   1.187 @@ -243,15 +213,15 @@
   1.188  
   1.189  lemma [code func]:
   1.190    shows "(False \<and> x) = False"
   1.191 -  and   "(True \<and> x) = x"
   1.192 -  and   "(x \<and> False) = False"
   1.193 -  and   "(x \<and> True) = x" by simp_all
   1.194 +    and "(True \<and> x) = x"
   1.195 +    and "(x \<and> False) = False"
   1.196 +    and "(x \<and> True) = x" by simp_all
   1.197  
   1.198  lemma [code func]:
   1.199    shows "(False \<or> x) = x"
   1.200 -  and   "(True \<or> x) = True"
   1.201 -  and   "(x \<or> False) = x"
   1.202 -  and   "(x \<or> True) = True" by simp_all
   1.203 +    and "(True \<or> x) = True"
   1.204 +    and "(x \<or> False) = x"
   1.205 +    and "(x \<or> True) = True" by simp_all
   1.206  
   1.207  declare
   1.208    if_True [code func]
   1.209 @@ -260,8 +230,8 @@
   1.210    snd_conv [code]
   1.211  
   1.212  lemma split_is_prod_case [code inline]:
   1.213 -  "split = prod_case"
   1.214 -by (simp add: expand_fun_eq split_def prod.cases)
   1.215 +    "split = prod_case"
   1.216 +  by (simp add: expand_fun_eq split_def prod.cases)
   1.217  
   1.218  code_type bool
   1.219    (SML target_atom "bool")