adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
authorblanchet
Fri Feb 21 00:09:56 2014 +0100 (2014-02-21)
changeset 5564263beb38e9258
parent 55641 5b466efedd2c
child 55643 18fe288f6801
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
src/HOL/BNF_Def.thy
src/HOL/BNF_FP_Base.thy
src/HOL/Code_Evaluation.thy
src/HOL/Code_Numeral.thy
src/HOL/Datatype.thy
src/HOL/Extraction.thy
src/HOL/HOLCF/Lift.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Nitpick.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Product_Type.thy
src/HOL/String.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/sum_tree.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/set_comprehension_pointfree.ML
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/BNF_Def.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/BNF_Def.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4  
     1.5  lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)"
     1.6  unfolding fstOp_def mem_Collect_eq
     1.7 -by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct1])
     1.8 +by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1])
     1.9  
    1.10  lemma fst_fstOp: "fst bc = (fst \<circ> fstOp P Q) bc"
    1.11  unfolding comp_def fstOp_def by simp
    1.12 @@ -91,7 +91,7 @@
    1.13  
    1.14  lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)"
    1.15  unfolding sndOp_def mem_Collect_eq
    1.16 -by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct2])
    1.17 +by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
    1.18  
    1.19  lemma csquare_fstOp_sndOp:
    1.20  "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
     2.1 --- a/src/HOL/BNF_FP_Base.thy	Fri Feb 21 00:09:55 2014 +0100
     2.2 +++ b/src/HOL/BNF_FP_Base.thy	Fri Feb 21 00:09:56 2014 +0100
     2.3 @@ -20,7 +20,7 @@
     2.4  by blast
     2.5  
     2.6  lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
     2.7 -by (cases u) (hypsubst, rule unit.cases)
     2.8 +by (cases u) (hypsubst, rule unit.case)
     2.9  
    2.10  lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
    2.11  by simp
     3.1 --- a/src/HOL/Code_Evaluation.thy	Fri Feb 21 00:09:55 2014 +0100
     3.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Feb 21 00:09:56 2014 +0100
     3.3 @@ -107,7 +107,7 @@
     3.4  
     3.5  subsubsection {* Code generator setup *}
     3.6  
     3.7 -lemmas [code del] = term.recs term.cases term.size
     3.8 +lemmas [code del] = term.rec term.case term.size
     3.9  lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
    3.10  
    3.11  lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
     4.1 --- a/src/HOL/Code_Numeral.thy	Fri Feb 21 00:09:55 2014 +0100
     4.2 +++ b/src/HOL/Code_Numeral.thy	Fri Feb 21 00:09:56 2014 +0100
     4.3 @@ -888,7 +888,7 @@
     4.4    "case_natural f g n = (if n = 0 then f else g (n - 1))"
     4.5    by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
     4.6  
     4.7 -declare natural.recs [code del]
     4.8 +declare natural.rec [code del]
     4.9  
    4.10  lemma [code abstract]:
    4.11    "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"
     5.1 --- a/src/HOL/Datatype.thy	Fri Feb 21 00:09:55 2014 +0100
     5.2 +++ b/src/HOL/Datatype.thy	Fri Feb 21 00:09:56 2014 +0100
     5.3 @@ -133,7 +133,7 @@
     5.4  
     5.5  lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
     5.6  apply (simp add: Node_def Push_def) 
     5.7 -apply (fast intro!: apfst_conv nat.cases(2)[THEN trans])
     5.8 +apply (fast intro!: apfst_conv nat.case(2)[THEN trans])
     5.9  done
    5.10  
    5.11  
     6.1 --- a/src/HOL/Extraction.thy	Fri Feb 21 00:09:55 2014 +0100
     6.2 +++ b/src/HOL/Extraction.thy	Fri Feb 21 00:09:56 2014 +0100
     6.3 @@ -280,28 +280,28 @@
     6.4    conjunct2: "Null" "conjunct2"
     6.5  
     6.6    disjI1 (P, Q): "Inl"
     6.7 -    "\<^bold>\<lambda>(c: _) (d: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
     6.8 +    "\<^bold>\<lambda>(c: _) (d: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.case_1 \<cdot> P \<cdot> _ \<cdot> p \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
     6.9  
    6.10    disjI1 (P): "Some"
    6.11 -    "\<^bold>\<lambda>(c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)"
    6.12 +    "\<^bold>\<lambda>(c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)"
    6.13  
    6.14    disjI1 (Q): "None"
    6.15 -    "\<^bold>\<lambda>(c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
    6.16 +    "\<^bold>\<lambda>(c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
    6.17  
    6.18    disjI1: "Left"
    6.19 -    "\<^bold>\<lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
    6.20 +    "\<^bold>\<lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
    6.21  
    6.22    disjI2 (P, Q): "Inr"
    6.23 -    "\<^bold>\<lambda>(d: _) (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
    6.24 +    "\<^bold>\<lambda>(d: _) (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.case_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c \<bullet> d)"
    6.25  
    6.26    disjI2 (P): "None"
    6.27 -    "\<^bold>\<lambda>(c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
    6.28 +    "\<^bold>\<lambda>(c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
    6.29  
    6.30    disjI2 (Q): "Some"
    6.31 -    "\<^bold>\<lambda>(c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)"
    6.32 +    "\<^bold>\<lambda>(c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)"
    6.33  
    6.34    disjI2: "Right"
    6.35 -    "\<^bold>\<lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
    6.36 +    "\<^bold>\<lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.case_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
    6.37  
    6.38    disjE (P, Q, R): "\<lambda>pq pr qr.
    6.39       (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)"
     7.1 --- a/src/HOL/HOLCF/Lift.thy	Fri Feb 21 00:09:55 2014 +0100
     7.2 +++ b/src/HOL/HOLCF/Lift.thy	Fri Feb 21 00:09:56 2014 +0100
     7.3 @@ -74,7 +74,7 @@
     7.4  subsection {* Continuity of @{const case_lift} *}
     7.5  
     7.6  lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
     7.7 -apply (induct x, unfold lift.cases)
     7.8 +apply (induct x, unfold lift.case)
     7.9  apply (simp add: Rep_lift_strict)
    7.10  apply (simp add: Def_def Abs_lift_inverse)
    7.11  done
     8.1 --- a/src/HOL/Lazy_Sequence.thy	Fri Feb 21 00:09:55 2014 +0100
     8.2 +++ b/src/HOL/Lazy_Sequence.thy	Fri Feb 21 00:09:56 2014 +0100
     8.3 @@ -52,8 +52,8 @@
     8.4  code_datatype Lazy_Sequence
     8.5  
     8.6  declare list_of_lazy_sequence.simps [code del]
     8.7 -declare lazy_sequence.cases [code del]
     8.8 -declare lazy_sequence.recs [code del]
     8.9 +declare lazy_sequence.case [code del]
    8.10 +declare lazy_sequence.rec [code del]
    8.11  
    8.12  lemma list_of_Lazy_Sequence [simp]:
    8.13    "list_of_lazy_sequence (Lazy_Sequence f) = (case f () of
     9.1 --- a/src/HOL/Library/Polynomial.thy	Fri Feb 21 00:09:55 2014 +0100
     9.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Feb 21 00:09:56 2014 +0100
     9.3 @@ -406,7 +406,7 @@
     9.4    { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
     9.5      assume "\<forall>m\<in>set ms. m > 0"
     9.6      then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
     9.7 -      by (induct ms) (auto, metis Suc_pred' nat.cases(2)) }
     9.8 +      by (induct ms) (auto, metis Suc_pred' nat.case(2)) }
     9.9    note * = this
    9.10    show ?thesis
    9.11      by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
    9.12 @@ -452,7 +452,7 @@
    9.13  lemma coeff_Poly_eq:
    9.14    "coeff (Poly xs) n = nth_default 0 xs n"
    9.15    apply (induct xs arbitrary: n) apply simp_all
    9.16 -  by (metis nat.cases not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
    9.17 +  by (metis nat.case not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
    9.18  
    9.19  lemma nth_default_coeffs_eq:
    9.20    "nth_default 0 (coeffs p) = coeff p"
    10.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Feb 21 00:09:55 2014 +0100
    10.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Feb 21 00:09:56 2014 +0100
    10.3 @@ -1753,8 +1753,8 @@
    10.4  hide_fact (open)
    10.5    Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
    10.6    Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
    10.7 -  compare.simps compare.exhaust compare.induct compare.recs compare.simps
    10.8 -  compare.size compare.case_cong compare.weak_case_cong compare.cases 
    10.9 +  compare.simps compare.exhaust compare.induct compare.rec compare.simps
   10.10 +  compare.size compare.case_cong compare.weak_case_cong compare.case
   10.11    compare.nchotomy compare.split compare.split_asm rec_compare_def
   10.12    compare.eq.refl compare.eq.simps
   10.13    compare.EQ_def compare.GT_def compare.LT_def
    11.1 --- a/src/HOL/List.thy	Fri Feb 21 00:09:55 2014 +0100
    11.2 +++ b/src/HOL/List.thy	Fri Feb 21 00:09:56 2014 +0100
    11.3 @@ -1645,10 +1645,10 @@
    11.4  lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
    11.5  apply (induct xs, simp, simp)
    11.6  apply safe
    11.7 -apply (metis nat.cases(1) nth.simps zero_less_Suc)
    11.8 +apply (metis nat.case(1) nth.simps zero_less_Suc)
    11.9  apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
   11.10  apply (case_tac i, simp)
   11.11 -apply (metis diff_Suc_Suc nat.cases(2) nth.simps zero_less_diff)
   11.12 +apply (metis diff_Suc_Suc nat.case(2) nth.simps zero_less_diff)
   11.13  done
   11.14  
   11.15  lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
    12.1 --- a/src/HOL/Nat.thy	Fri Feb 21 00:09:55 2014 +0100
    12.2 +++ b/src/HOL/Nat.thy	Fri Feb 21 00:09:56 2014 +0100
    12.3 @@ -112,9 +112,8 @@
    12.4  
    12.5  lemmas induct = old.nat.induct
    12.6  lemmas inducts = old.nat.inducts
    12.7 -lemmas recs = old.nat.recs
    12.8 -lemmas cases = nat.case
    12.9 -lemmas simps = nat.inject nat.distinct nat.case old.nat.recs
   12.10 +lemmas rec = old.nat.rec
   12.11 +lemmas simps = nat.inject nat.distinct nat.case nat.rec
   12.12  
   12.13  setup {* Sign.parent_path *}
   12.14  
    13.1 --- a/src/HOL/Nitpick.thy	Fri Feb 21 00:09:55 2014 +0100
    13.2 +++ b/src/HOL/Nitpick.thy	Fri Feb 21 00:09:56 2014 +0100
    13.3 @@ -101,17 +101,17 @@
    13.4  lemma case_unit_unfold [nitpick_unfold]:
    13.5  "case_unit x u \<equiv> x"
    13.6  apply (subgoal_tac "u = ()")
    13.7 - apply (simp only: unit.cases)
    13.8 + apply (simp only: unit.case)
    13.9  by simp
   13.10  
   13.11 -declare unit.cases [nitpick_simp del]
   13.12 +declare unit.case [nitpick_simp del]
   13.13  
   13.14  lemma case_nat_unfold [nitpick_unfold]:
   13.15  "case_nat x f n \<equiv> if n = 0 then x else f (n - 1)"
   13.16  apply (rule eq_reflection)
   13.17  by (cases n) auto
   13.18  
   13.19 -declare nat.cases [nitpick_simp del]
   13.20 +declare nat.case [nitpick_simp del]
   13.21  
   13.22  lemma list_size_simp [nitpick_simp]:
   13.23  "list_size f xs = (if xs = [] then 0
    14.1 --- a/src/HOL/Probability/Caratheodory.thy	Fri Feb 21 00:09:55 2014 +0100
    14.2 +++ b/src/HOL/Probability/Caratheodory.thy	Fri Feb 21 00:09:56 2014 +0100
    14.3 @@ -528,7 +528,7 @@
    14.4        with sbBB [of i] obtain j where "x \<in> BB i j"
    14.5          by blast
    14.6        thus "\<exists>i. x \<in> split BB (prod_decode i)"
    14.7 -        by (metis prod_encode_inverse prod.cases)
    14.8 +        by (metis prod_encode_inverse prod.case)
    14.9      qed
   14.10      have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
   14.11        by (rule ext)  (auto simp add: C_def)
    15.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Feb 21 00:09:55 2014 +0100
    15.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Feb 21 00:09:56 2014 +0100
    15.3 @@ -196,7 +196,7 @@
    15.4            (\<forall>n. ?a / 2 ^ (k + 1) \<le> ?q k n (w k)) \<and> (k \<noteq> 0 \<longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1))"
    15.5          proof (induct k)
    15.6            case 0 with w0 show ?case
    15.7 -            unfolding w_def nat.recs(1) by auto
    15.8 +            unfolding w_def nat.rec(1) by auto
    15.9          next
   15.10            case (Suc k)
   15.11            then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
   15.12 @@ -241,7 +241,7 @@
   15.13                   (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
   15.14            qed
   15.15            then have "?P k (w k) (w (Suc k))"
   15.16 -            unfolding w_def nat.recs(2) unfolding w_def[symmetric]
   15.17 +            unfolding w_def nat.rec(2) unfolding w_def[symmetric]
   15.18              by (rule someI_ex)
   15.19            then show ?case by auto
   15.20          qed
    16.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Feb 21 00:09:55 2014 +0100
    16.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Feb 21 00:09:56 2014 +0100
    16.3 @@ -250,7 +250,7 @@
    16.4    { fix i have "A i \<in> sets M" unfolding A_def
    16.5      proof (induct i)
    16.6        case (Suc i)
    16.7 -      from Ex_P[OF this, of i] show ?case unfolding nat.recs(2)
    16.8 +      from Ex_P[OF this, of i] show ?case unfolding nat.rec(2)
    16.9          by (rule someI2_ex) simp
   16.10      qed simp }
   16.11    note A_in_sets = this
   16.12 @@ -281,7 +281,7 @@
   16.13        from ex_inverse_of_nat_Suc_less[OF this]
   16.14        obtain n where *: "?d B < - 1 / real (Suc n)"
   16.15          by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
   16.16 -      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.recs(2))
   16.17 +      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.rec(2))
   16.18        from epsilon[OF B(1) this] *
   16.19        show False by auto
   16.20      qed
    17.1 --- a/src/HOL/Product_Type.thy	Fri Feb 21 00:09:55 2014 +0100
    17.2 +++ b/src/HOL/Product_Type.thy	Fri Feb 21 00:09:56 2014 +0100
    17.3 @@ -29,9 +29,8 @@
    17.4  
    17.5  lemmas induct = old.bool.induct
    17.6  lemmas inducts = old.bool.inducts
    17.7 -lemmas recs = old.bool.recs
    17.8 -lemmas cases = bool.case
    17.9 -lemmas simps = bool.distinct bool.case old.bool.recs
   17.10 +lemmas rec = old.bool.rec
   17.11 +lemmas simps = bool.distinct bool.case bool.rec
   17.12  
   17.13  setup {* Sign.parent_path *}
   17.14  
   17.15 @@ -99,9 +98,8 @@
   17.16  
   17.17  lemmas induct = old.unit.induct
   17.18  lemmas inducts = old.unit.inducts
   17.19 -lemmas recs = old.unit.recs
   17.20 -lemmas cases = unit.case
   17.21 -lemmas simps = unit.case old.unit.recs
   17.22 +lemmas rec = old.unit.rec
   17.23 +lemmas simps = unit.case unit.rec
   17.24  
   17.25  setup {* Sign.parent_path *}
   17.26  
   17.27 @@ -217,9 +215,8 @@
   17.28  
   17.29  lemmas induct = old.prod.induct
   17.30  lemmas inducts = old.prod.inducts
   17.31 -lemmas recs = old.prod.recs
   17.32 -lemmas cases = prod.case
   17.33 -lemmas simps = prod.inject prod.case old.prod.recs
   17.34 +lemmas rec = old.prod.rec
   17.35 +lemmas simps = prod.inject prod.case prod.rec
   17.36  
   17.37  setup {* Sign.parent_path *}
   17.38  
   17.39 @@ -403,7 +400,7 @@
   17.40    by (simp add: prod_eq_iff)
   17.41  
   17.42  lemma split_conv [simp, code]: "split f (a, b) = f a b"
   17.43 -  by (fact prod.cases)
   17.44 +  by (fact prod.case)
   17.45  
   17.46  lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
   17.47    by (rule split_conv [THEN iffD2])
   17.48 @@ -684,7 +681,7 @@
   17.49    Setup of internal @{text split_rule}.
   17.50  *}
   17.51  
   17.52 -lemmas case_prodI = prod.cases [THEN iffD2]
   17.53 +lemmas case_prodI = prod.case [THEN iffD2]
   17.54  
   17.55  lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
   17.56    by (fact splitI2)
    18.1 --- a/src/HOL/String.thy	Fri Feb 21 00:09:55 2014 +0100
    18.2 +++ b/src/HOL/String.thy	Fri Feb 21 00:09:56 2014 +0100
    18.3 @@ -289,7 +289,7 @@
    18.4  lemma case_char_code [code]:
    18.5    "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
    18.6    by (cases c)
    18.7 -    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
    18.8 +    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
    18.9  
   18.10  lemma [code]:
   18.11    "rec_char = case_char"
    19.1 --- a/src/HOL/Sum_Type.thy	Fri Feb 21 00:09:55 2014 +0100
    19.2 +++ b/src/HOL/Sum_Type.thy	Fri Feb 21 00:09:56 2014 +0100
    19.3 @@ -114,9 +114,8 @@
    19.4  
    19.5  lemmas induct = old.sum.induct
    19.6  lemmas inducts = old.sum.inducts
    19.7 -lemmas recs = old.sum.recs
    19.8 -lemmas cases = sum.case
    19.9 -lemmas simps = sum.inject sum.distinct sum.case old.sum.recs
   19.10 +lemmas rec = old.sum.rec
   19.11 +lemmas simps = sum.inject sum.distinct sum.case sum.rec
   19.12  
   19.13  setup {* Sign.parent_path *}
   19.14  
    20.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Feb 21 00:09:55 2014 +0100
    20.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Fri Feb 21 00:09:56 2014 +0100
    20.3 @@ -257,7 +257,7 @@
    20.4             ((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
    20.5               map_comp RS sym, map_id]) RSN (2, trans))),
    20.6          REPEAT_DETERM_N (2 * live) o atac,
    20.7 -        REPEAT_DETERM_N live o rtac (@{thm prod.cases} RS trans),
    20.8 +        REPEAT_DETERM_N live o rtac (@{thm prod.case} RS trans),
    20.9          rtac refl,
   20.10          rtac @{thm surj_imp_ordLeq}, rtac subsetI, rtac (Drule.rotate_prems 1 @{thm image_eqI}),
   20.11          REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
    21.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Feb 21 00:09:55 2014 +0100
    21.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Feb 21 00:09:56 2014 +0100
    21.3 @@ -35,7 +35,7 @@
    21.4  val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
    21.5  val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
    21.6  
    21.7 -val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.cases sum.cases sum_map.simps};
    21.8 +val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps};
    21.9  val sum_prod_thms_set0 =
   21.10    @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
   21.11        Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
    22.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Feb 21 00:09:55 2014 +0100
    22.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Feb 21 00:09:56 2014 +0100
    22.3 @@ -468,8 +468,8 @@
    22.4  
    22.5  fun mk_sum_caseN_balanced 1 1 = refl
    22.6    | mk_sum_caseN_balanced n k =
    22.7 -    Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm case_sum_step(1)},
    22.8 -      right = mk_sum_step @{thm sum.cases(2)} @{thm case_sum_step(2)}, init = refl} n k;
    22.9 +    Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)},
   22.10 +      right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k;
   22.11  
   22.12  fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
   22.13    let
    23.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Feb 21 00:09:55 2014 +0100
    23.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Feb 21 00:09:56 2014 +0100
    23.3 @@ -1129,7 +1129,7 @@
    23.4      val phi = Proof_Context.export_morphism lthy_old lthy;
    23.5  
    23.6      val strT_defs = map (fn def =>
    23.7 -        trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.cases}])
    23.8 +        trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.case}])
    23.9        strT_def_frees;
   23.10      val strTs = map (fst o Term.dest_Const o Morphism.term phi) strT_frees;
   23.11  
    24.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Feb 21 00:09:55 2014 +0100
    24.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Feb 21 00:09:56 2014 +0100
    24.3 @@ -138,7 +138,7 @@
    24.4      eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    24.5      etac notE THEN' atac ORELSE'
    24.6      (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
    24.7 -       sum.cases} @ mapsx @ map_comps @ map_idents))) ORELSE'
    24.8 +       sum.case} @ mapsx @ map_comps @ map_idents))) ORELSE'
    24.9      fo_rtac @{thm cong} ctxt ORELSE'
   24.10      rtac ext));
   24.11  
    25.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Feb 21 00:09:55 2014 +0100
    25.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Feb 21 00:09:56 2014 +0100
    25.3 @@ -751,7 +751,7 @@
    25.4  
    25.5  fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
    25.6    unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
    25.7 -    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
    25.8 +    rtac trans, rtac unfold, fo_rtac (@{thm sum.case(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
    25.9      REPEAT_DETERM_N m o rtac refl,
   25.10      EVERY' (map (fn thm => rtac @{thm case_sum_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
   25.11  
   25.12 @@ -1033,8 +1033,8 @@
   25.13            rtac (map_comp0 RS trans), rtac (map_cong RS trans),
   25.14            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_comp]},
   25.15            REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
   25.16 -          etac (@{thm prod.cases} RS map_arg_cong RS trans),
   25.17 -          SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}), 
   25.18 +          etac (@{thm prod.case} RS map_arg_cong RS trans),
   25.19 +          SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case}), 
   25.20            CONJ_WRAP' (fn set_map0 =>
   25.21              EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
   25.22                dtac (set_map0 RS equalityD1 RS set_mp),
   25.23 @@ -1046,7 +1046,7 @@
   25.24        ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps)] 1
   25.25    end;
   25.26  
   25.27 -val split_id_unfolds = @{thms prod.cases image_id id_apply};
   25.28 +val split_id_unfolds = @{thms prod.case image_id id_apply};
   25.29  
   25.30  fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
   25.31    let val n = length ks;
    26.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Feb 21 00:09:55 2014 +0100
    26.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Feb 21 00:09:56 2014 +0100
    26.3 @@ -44,7 +44,7 @@
    26.4  fun meta thm = thm RS eq_reflection
    26.5  
    26.6  fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
    26.7 -  (map meta (@{thm split_conv} :: @{thms sum.cases}))
    26.8 +  (map meta (@{thm split_conv} :: @{thms sum.case}))
    26.9  
   26.10  fun term_conv thy cv t =
   26.11    cv (cterm_of thy t)
   26.12 @@ -315,7 +315,7 @@
   26.13          val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
   26.14            |> Goal.init
   26.15            |> (Simplifier.rewrite_goals_tac ctxt
   26.16 -                (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
   26.17 +                (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.case}))
   26.18                THEN CONVERSION (ind_rulify ctxt) 1)
   26.19            |> Seq.hd
   26.20            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
    27.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Feb 21 00:09:55 2014 +0100
    27.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Feb 21 00:09:56 2014 +0100
    27.3 @@ -129,7 +129,7 @@
    27.4    THEN rtac @{thm CollectI} 1
    27.5    THEN etac @{thm conjE} 1
    27.6    THEN etac @{thm ssubst} 1
    27.7 -  THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.cases}
    27.8 +  THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.case}
    27.9  
   27.10  (* Sets *)
   27.11  
    28.1 --- a/src/HOL/Tools/Function/sum_tree.ML	Fri Feb 21 00:09:55 2014 +0100
    28.2 +++ b/src/HOL/Tools/Function/sum_tree.ML	Fri Feb 21 00:09:56 2014 +0100
    28.3 @@ -22,7 +22,7 @@
    28.4  (* Theory dependencies *)
    28.5  val sumcase_split_ss =
    28.6    simpset_of (put_simpset HOL_basic_ss @{context}
    28.7 -    addsimps (@{thm Product_Type.split} :: @{thms sum.cases}))
    28.8 +    addsimps (@{thm Product_Type.split} :: @{thms sum.case}))
    28.9  
   28.10  (* top-down access in balanced tree *)
   28.11  fun access_top_down {left, right, init} len i =
    29.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Feb 21 00:09:55 2014 +0100
    29.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Feb 21 00:09:56 2014 +0100
    29.3 @@ -145,7 +145,7 @@
    29.4            fold (union Thm.eq_thm) (case_thms :: map get_case_rewrite (snd (strip_comb t))) []
    29.5          end
    29.6        else []
    29.7 -    val simprules = insert Thm.eq_thm @{thm "unit.cases"} (insert Thm.eq_thm @{thm "prod.cases"}
    29.8 +    val simprules = insert Thm.eq_thm @{thm "unit.case"} (insert Thm.eq_thm @{thm "prod.case"}
    29.9        (fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
   29.10    (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   29.11    in
    30.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 21 00:09:55 2014 +0100
    30.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 21 00:09:56 2014 +0100
    30.3 @@ -774,7 +774,7 @@
    30.4    |> map nickname_of_thm
    30.5  
    30.6  fun is_size_def [dep] th =
    30.7 -    (case first_field ".recs" dep of
    30.8 +    (case first_field ".rec" dep of
    30.9         SOME (pref, _) =>
   30.10         (case first_field ".size" (nickname_of_thm th) of
   30.11            SOME (pref', _) => pref = pref'
    31.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Feb 21 00:09:55 2014 +0100
    31.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Feb 21 00:09:56 2014 +0100
    31.3 @@ -323,14 +323,14 @@
    31.4      THEN' (REPEAT_DETERM1 o
    31.5        (rtac @{thm refl}
    31.6        ORELSE' rtac
    31.7 -        @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}
    31.8 +        @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]}
    31.9        ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
   31.10          (HOLogic.Trueprop_conv
   31.11            (HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
   31.12  
   31.13  fun elim_image_tac ctxt = etac @{thm imageE}
   31.14    THEN' REPEAT_DETERM o CHANGED o
   31.15 -    (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
   31.16 +    (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
   31.17      THEN' REPEAT_DETERM o etac @{thm Pair_inject}
   31.18      THEN' TRY o hyp_subst_tac ctxt)
   31.19  
   31.20 @@ -348,13 +348,13 @@
   31.21      REPEAT_DETERM1 o (atac
   31.22        ORELSE' rtac @{thm SigmaI}
   31.23        ORELSE' ((rtac @{thm CollectI} ORELSE' rtac collectI') THEN'
   31.24 -        TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]))
   31.25 +        TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
   31.26        ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN'
   31.27 -        TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]))
   31.28 +        TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
   31.29        ORELSE' (rtac @{thm image_eqI} THEN'
   31.30      (REPEAT_DETERM o
   31.31        (rtac @{thm refl}
   31.32 -      ORELSE' rtac @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]})))
   31.33 +      ORELSE' rtac @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]})))
   31.34        ORELSE' rtac @{thm UNIV_I}
   31.35        ORELSE' rtac @{thm iffD2[OF Compl_iff]}
   31.36        ORELSE' atac)
   31.37 @@ -375,16 +375,16 @@
   31.38         ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]}
   31.39         ORELSE' etac @{thm conjE}
   31.40         ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
   31.41 -         TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]) THEN'
   31.42 +         TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]) THEN'
   31.43           REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})
   31.44         ORELSE' (etac @{thm imageE}
   31.45           THEN' (REPEAT_DETERM o CHANGED o
   31.46 -         (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
   31.47 +         (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
   31.48           THEN' REPEAT_DETERM o etac @{thm Pair_inject}
   31.49           THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})))
   31.50         ORELSE' etac @{thm ComplE}
   31.51         ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
   31.52 -        THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}])
   31.53 +        THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}])
   31.54          THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl}))
   31.55  
   31.56  fun tac ctxt fm =
   31.57 @@ -427,7 +427,7 @@
   31.58          HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t'')))
   31.59        end;
   31.60      fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (prop_of th))
   31.61 -    val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.cases}
   31.62 +    val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case}
   31.63      fun tac ctxt = 
   31.64        rtac @{thm set_eqI}
   31.65        THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms)
    32.1 --- a/src/HOL/Topological_Spaces.thy	Fri Feb 21 00:09:55 2014 +0100
    32.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Feb 21 00:09:56 2014 +0100
    32.3 @@ -1298,7 +1298,7 @@
    32.4    assume *: "\<forall>n. \<exists>p. ?P p n"
    32.5    def f \<equiv> "rec_nat (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
    32.6    have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
    32.7 -  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(2) ..
    32.8 +  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.rec(2) ..
    32.9    have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
   32.10    have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
   32.11    then have "subseq f" unfolding subseq_Suc_iff by auto
   32.12 @@ -1320,7 +1320,7 @@
   32.13    then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
   32.14    def f \<equiv> "rec_nat (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
   32.15    have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
   32.16 -  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(2) ..
   32.17 +  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.rec(2) ..
   32.18    have P_0: "?P (f 0) (Suc N)"
   32.19      unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
   32.20    { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"