--- a/src/HOL/BNF_Def.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/BNF_Def.thy Fri Feb 21 00:09:56 2014 +0100
@@ -81,7 +81,7 @@
lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)"
unfolding fstOp_def mem_Collect_eq
-by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct1])
+by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1])
lemma fst_fstOp: "fst bc = (fst \<circ> fstOp P Q) bc"
unfolding comp_def fstOp_def by simp
@@ -91,7 +91,7 @@
lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)"
unfolding sndOp_def mem_Collect_eq
-by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct2])
+by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2])
lemma csquare_fstOp_sndOp:
"csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
--- a/src/HOL/BNF_FP_Base.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Fri Feb 21 00:09:56 2014 +0100
@@ -20,7 +20,7 @@
by blast
lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
-by (cases u) (hypsubst, rule unit.cases)
+by (cases u) (hypsubst, rule unit.case)
lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
by simp
--- a/src/HOL/Code_Evaluation.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Code_Evaluation.thy Fri Feb 21 00:09:56 2014 +0100
@@ -107,7 +107,7 @@
subsubsection {* Code generator setup *}
-lemmas [code del] = term.recs term.cases term.size
+lemmas [code del] = term.rec term.case term.size
lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
--- a/src/HOL/Code_Numeral.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Code_Numeral.thy Fri Feb 21 00:09:56 2014 +0100
@@ -888,7 +888,7 @@
"case_natural f g n = (if n = 0 then f else g (n - 1))"
by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
-declare natural.recs [code del]
+declare natural.rec [code del]
lemma [code abstract]:
"integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"
--- a/src/HOL/Datatype.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Datatype.thy Fri Feb 21 00:09:56 2014 +0100
@@ -133,7 +133,7 @@
lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
apply (simp add: Node_def Push_def)
-apply (fast intro!: apfst_conv nat.cases(2)[THEN trans])
+apply (fast intro!: apfst_conv nat.case(2)[THEN trans])
done
--- a/src/HOL/Extraction.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Extraction.thy Fri Feb 21 00:09:56 2014 +0100
@@ -280,28 +280,28 @@
conjunct2: "Null" "conjunct2"
disjI1 (P, Q): "Inl"
- "\<^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)"
+ "\<^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)"
disjI1 (P): "Some"
- "\<^bold>\<lambda>(c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)"
+ "\<^bold>\<lambda>(c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)"
disjI1 (Q): "None"
- "\<^bold>\<lambda>(c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
+ "\<^bold>\<lambda>(c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
disjI1: "Left"
- "\<^bold>\<lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
+ "\<^bold>\<lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
disjI2 (P, Q): "Inr"
- "\<^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)"
+ "\<^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)"
disjI2 (P): "None"
- "\<^bold>\<lambda>(c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
+ "\<^bold>\<lambda>(c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)"
disjI2 (Q): "Some"
- "\<^bold>\<lambda>(c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)"
+ "\<^bold>\<lambda>(c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.case_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)"
disjI2: "Right"
- "\<^bold>\<lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
+ "\<^bold>\<lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.case_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)"
disjE (P, Q, R): "\<lambda>pq pr qr.
(case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)"
--- a/src/HOL/HOLCF/Lift.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/HOLCF/Lift.thy Fri Feb 21 00:09:56 2014 +0100
@@ -74,7 +74,7 @@
subsection {* Continuity of @{const case_lift} *}
lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
-apply (induct x, unfold lift.cases)
+apply (induct x, unfold lift.case)
apply (simp add: Rep_lift_strict)
apply (simp add: Def_def Abs_lift_inverse)
done
--- a/src/HOL/Lazy_Sequence.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Lazy_Sequence.thy Fri Feb 21 00:09:56 2014 +0100
@@ -52,8 +52,8 @@
code_datatype Lazy_Sequence
declare list_of_lazy_sequence.simps [code del]
-declare lazy_sequence.cases [code del]
-declare lazy_sequence.recs [code del]
+declare lazy_sequence.case [code del]
+declare lazy_sequence.rec [code del]
lemma list_of_Lazy_Sequence [simp]:
"list_of_lazy_sequence (Lazy_Sequence f) = (case f () of
--- a/src/HOL/Library/Polynomial.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Library/Polynomial.thy Fri Feb 21 00:09:56 2014 +0100
@@ -406,7 +406,7 @@
{ fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
assume "\<forall>m\<in>set ms. m > 0"
then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
- by (induct ms) (auto, metis Suc_pred' nat.cases(2)) }
+ by (induct ms) (auto, metis Suc_pred' nat.case(2)) }
note * = this
show ?thesis
by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
@@ -452,7 +452,7 @@
lemma coeff_Poly_eq:
"coeff (Poly xs) n = nth_default 0 xs n"
apply (induct xs arbitrary: n) apply simp_all
- by (metis nat.cases not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
+ by (metis nat.case not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
lemma nth_default_coeffs_eq:
"nth_default 0 (coeffs p) = coeff p"
--- a/src/HOL/Library/RBT_Impl.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Library/RBT_Impl.thy Fri Feb 21 00:09:56 2014 +0100
@@ -1753,8 +1753,8 @@
hide_fact (open)
Abs_compare_cases Abs_compare_induct Abs_compare_inject Abs_compare_inverse
Rep_compare Rep_compare_cases Rep_compare_induct Rep_compare_inject Rep_compare_inverse
- compare.simps compare.exhaust compare.induct compare.recs compare.simps
- compare.size compare.case_cong compare.weak_case_cong compare.cases
+ compare.simps compare.exhaust compare.induct compare.rec compare.simps
+ compare.size compare.case_cong compare.weak_case_cong compare.case
compare.nchotomy compare.split compare.split_asm rec_compare_def
compare.eq.refl compare.eq.simps
compare.EQ_def compare.GT_def compare.LT_def
--- a/src/HOL/List.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/List.thy Fri Feb 21 00:09:56 2014 +0100
@@ -1645,10 +1645,10 @@
lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
apply (induct xs, simp, simp)
apply safe
-apply (metis nat.cases(1) nth.simps zero_less_Suc)
+apply (metis nat.case(1) nth.simps zero_less_Suc)
apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
apply (case_tac i, simp)
-apply (metis diff_Suc_Suc nat.cases(2) nth.simps zero_less_diff)
+apply (metis diff_Suc_Suc nat.case(2) nth.simps zero_less_diff)
done
lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
--- a/src/HOL/Nat.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Nat.thy Fri Feb 21 00:09:56 2014 +0100
@@ -112,9 +112,8 @@
lemmas induct = old.nat.induct
lemmas inducts = old.nat.inducts
-lemmas recs = old.nat.recs
-lemmas cases = nat.case
-lemmas simps = nat.inject nat.distinct nat.case old.nat.recs
+lemmas rec = old.nat.rec
+lemmas simps = nat.inject nat.distinct nat.case nat.rec
setup {* Sign.parent_path *}
--- a/src/HOL/Nitpick.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Nitpick.thy Fri Feb 21 00:09:56 2014 +0100
@@ -101,17 +101,17 @@
lemma case_unit_unfold [nitpick_unfold]:
"case_unit x u \<equiv> x"
apply (subgoal_tac "u = ()")
- apply (simp only: unit.cases)
+ apply (simp only: unit.case)
by simp
-declare unit.cases [nitpick_simp del]
+declare unit.case [nitpick_simp del]
lemma case_nat_unfold [nitpick_unfold]:
"case_nat x f n \<equiv> if n = 0 then x else f (n - 1)"
apply (rule eq_reflection)
by (cases n) auto
-declare nat.cases [nitpick_simp del]
+declare nat.case [nitpick_simp del]
lemma list_size_simp [nitpick_simp]:
"list_size f xs = (if xs = [] then 0
--- a/src/HOL/Probability/Caratheodory.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Fri Feb 21 00:09:56 2014 +0100
@@ -528,7 +528,7 @@
with sbBB [of i] obtain j where "x \<in> BB i j"
by blast
thus "\<exists>i. x \<in> split BB (prod_decode i)"
- by (metis prod_encode_inverse prod.cases)
+ by (metis prod_encode_inverse prod.case)
qed
have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
by (rule ext) (auto simp add: C_def)
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Fri Feb 21 00:09:56 2014 +0100
@@ -196,7 +196,7 @@
(\<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))"
proof (induct k)
case 0 with w0 show ?case
- unfolding w_def nat.recs(1) by auto
+ unfolding w_def nat.rec(1) by auto
next
case (Suc k)
then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
@@ -241,7 +241,7 @@
(auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
qed
then have "?P k (w k) (w (Suc k))"
- unfolding w_def nat.recs(2) unfolding w_def[symmetric]
+ unfolding w_def nat.rec(2) unfolding w_def[symmetric]
by (rule someI_ex)
then show ?case by auto
qed
--- a/src/HOL/Probability/Radon_Nikodym.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Fri Feb 21 00:09:56 2014 +0100
@@ -250,7 +250,7 @@
{ fix i have "A i \<in> sets M" unfolding A_def
proof (induct i)
case (Suc i)
- from Ex_P[OF this, of i] show ?case unfolding nat.recs(2)
+ from Ex_P[OF this, of i] show ?case unfolding nat.rec(2)
by (rule someI2_ex) simp
qed simp }
note A_in_sets = this
@@ -281,7 +281,7 @@
from ex_inverse_of_nat_Suc_less[OF this]
obtain n where *: "?d B < - 1 / real (Suc n)"
by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
- have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.recs(2))
+ have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.rec(2))
from epsilon[OF B(1) this] *
show False by auto
qed
--- a/src/HOL/Product_Type.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Product_Type.thy Fri Feb 21 00:09:56 2014 +0100
@@ -29,9 +29,8 @@
lemmas induct = old.bool.induct
lemmas inducts = old.bool.inducts
-lemmas recs = old.bool.recs
-lemmas cases = bool.case
-lemmas simps = bool.distinct bool.case old.bool.recs
+lemmas rec = old.bool.rec
+lemmas simps = bool.distinct bool.case bool.rec
setup {* Sign.parent_path *}
@@ -99,9 +98,8 @@
lemmas induct = old.unit.induct
lemmas inducts = old.unit.inducts
-lemmas recs = old.unit.recs
-lemmas cases = unit.case
-lemmas simps = unit.case old.unit.recs
+lemmas rec = old.unit.rec
+lemmas simps = unit.case unit.rec
setup {* Sign.parent_path *}
@@ -217,9 +215,8 @@
lemmas induct = old.prod.induct
lemmas inducts = old.prod.inducts
-lemmas recs = old.prod.recs
-lemmas cases = prod.case
-lemmas simps = prod.inject prod.case old.prod.recs
+lemmas rec = old.prod.rec
+lemmas simps = prod.inject prod.case prod.rec
setup {* Sign.parent_path *}
@@ -403,7 +400,7 @@
by (simp add: prod_eq_iff)
lemma split_conv [simp, code]: "split f (a, b) = f a b"
- by (fact prod.cases)
+ by (fact prod.case)
lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
by (rule split_conv [THEN iffD2])
@@ -684,7 +681,7 @@
Setup of internal @{text split_rule}.
*}
-lemmas case_prodI = prod.cases [THEN iffD2]
+lemmas case_prodI = prod.case [THEN iffD2]
lemma case_prodI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> case_prod c p"
by (fact splitI2)
--- a/src/HOL/String.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/String.thy Fri Feb 21 00:09:56 2014 +0100
@@ -289,7 +289,7 @@
lemma case_char_code [code]:
"case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
by (cases c)
- (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
+ (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
lemma [code]:
"rec_char = case_char"
--- a/src/HOL/Sum_Type.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Sum_Type.thy Fri Feb 21 00:09:56 2014 +0100
@@ -114,9 +114,8 @@
lemmas induct = old.sum.induct
lemmas inducts = old.sum.inducts
-lemmas recs = old.sum.recs
-lemmas cases = sum.case
-lemmas simps = sum.inject sum.distinct sum.case old.sum.recs
+lemmas rec = old.sum.rec
+lemmas simps = sum.inject sum.distinct sum.case sum.rec
setup {* Sign.parent_path *}
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Fri Feb 21 00:09:56 2014 +0100
@@ -257,7 +257,7 @@
((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
map_comp RS sym, map_id]) RSN (2, trans))),
REPEAT_DETERM_N (2 * live) o atac,
- REPEAT_DETERM_N live o rtac (@{thm prod.cases} RS trans),
+ REPEAT_DETERM_N live o rtac (@{thm prod.case} RS trans),
rtac refl,
rtac @{thm surj_imp_ordLeq}, rtac subsetI, rtac (Drule.rotate_prems 1 @{thm image_eqI}),
REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Feb 21 00:09:56 2014 +0100
@@ -35,7 +35,7 @@
val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
-val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.cases sum.cases sum_map.simps};
+val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps};
val sum_prod_thms_set0 =
@{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Feb 21 00:09:56 2014 +0100
@@ -468,8 +468,8 @@
fun mk_sum_caseN_balanced 1 1 = refl
| mk_sum_caseN_balanced n k =
- Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm case_sum_step(1)},
- right = mk_sum_step @{thm sum.cases(2)} @{thm case_sum_step(2)}, init = refl} n k;
+ Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)},
+ right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k;
fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
let
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Feb 21 00:09:56 2014 +0100
@@ -1129,7 +1129,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val strT_defs = map (fn def =>
- trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.cases}])
+ trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.case}])
strT_def_frees;
val strTs = map (fst o Term.dest_Const o Morphism.term phi) strT_frees;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Feb 21 00:09:56 2014 +0100
@@ -138,7 +138,7 @@
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
etac notE THEN' atac ORELSE'
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
- sum.cases} @ mapsx @ map_comps @ map_idents))) ORELSE'
+ sum.case} @ mapsx @ map_comps @ map_idents))) ORELSE'
fo_rtac @{thm cong} ctxt ORELSE'
rtac ext));
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Feb 21 00:09:56 2014 +0100
@@ -751,7 +751,7 @@
fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
- rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
+ rtac trans, rtac unfold, fo_rtac (@{thm sum.case(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
REPEAT_DETERM_N m o rtac refl,
EVERY' (map (fn thm => rtac @{thm case_sum_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
@@ -1033,8 +1033,8 @@
rtac (map_comp0 RS trans), rtac (map_cong RS trans),
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_comp]},
REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
- etac (@{thm prod.cases} RS map_arg_cong RS trans),
- SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}),
+ etac (@{thm prod.case} RS map_arg_cong RS trans),
+ SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case}),
CONJ_WRAP' (fn set_map0 =>
EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
dtac (set_map0 RS equalityD1 RS set_mp),
@@ -1046,7 +1046,7 @@
ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps)] 1
end;
-val split_id_unfolds = @{thms prod.cases image_id id_apply};
+val split_id_unfolds = @{thms prod.case image_id id_apply};
fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
let val n = length ks;
--- a/src/HOL/Tools/Function/induction_schema.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Fri Feb 21 00:09:56 2014 +0100
@@ -44,7 +44,7 @@
fun meta thm = thm RS eq_reflection
fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
- (map meta (@{thm split_conv} :: @{thms sum.cases}))
+ (map meta (@{thm split_conv} :: @{thms sum.case}))
fun term_conv thy cv t =
cv (cterm_of thy t)
@@ -315,7 +315,7 @@
val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
|> Goal.init
|> (Simplifier.rewrite_goals_tac ctxt
- (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
+ (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.case}))
THEN CONVERSION (ind_rulify ctxt) 1)
|> Seq.hd
|> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Feb 21 00:09:56 2014 +0100
@@ -129,7 +129,7 @@
THEN rtac @{thm CollectI} 1
THEN etac @{thm conjE} 1
THEN etac @{thm ssubst} 1
- THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.cases}
+ THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.case}
(* Sets *)
--- a/src/HOL/Tools/Function/sum_tree.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Function/sum_tree.ML Fri Feb 21 00:09:56 2014 +0100
@@ -22,7 +22,7 @@
(* Theory dependencies *)
val sumcase_split_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
- addsimps (@{thm Product_Type.split} :: @{thms sum.cases}))
+ addsimps (@{thm Product_Type.split} :: @{thms sum.case}))
(* top-down access in balanced tree *)
fun access_top_down {left, right, init} len i =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Feb 21 00:09:56 2014 +0100
@@ -145,7 +145,7 @@
fold (union Thm.eq_thm) (case_thms :: map get_case_rewrite (snd (strip_comb t))) []
end
else []
- val simprules = insert Thm.eq_thm @{thm "unit.cases"} (insert Thm.eq_thm @{thm "prod.cases"}
+ val simprules = insert Thm.eq_thm @{thm "unit.case"} (insert Thm.eq_thm @{thm "prod.case"}
(fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
(* replace TRY by determining if it necessary - are there equations when calling compile match? *)
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Feb 21 00:09:56 2014 +0100
@@ -774,7 +774,7 @@
|> map nickname_of_thm
fun is_size_def [dep] th =
- (case first_field ".recs" dep of
+ (case first_field ".rec" dep of
SOME (pref, _) =>
(case first_field ".size" (nickname_of_thm th) of
SOME (pref', _) => pref = pref'
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Fri Feb 21 00:09:56 2014 +0100
@@ -323,14 +323,14 @@
THEN' (REPEAT_DETERM1 o
(rtac @{thm refl}
ORELSE' rtac
- @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}
+ @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]}
ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
(HOLogic.Trueprop_conv
(HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
fun elim_image_tac ctxt = etac @{thm imageE}
THEN' REPEAT_DETERM o CHANGED o
- (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
+ (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
THEN' REPEAT_DETERM o etac @{thm Pair_inject}
THEN' TRY o hyp_subst_tac ctxt)
@@ -348,13 +348,13 @@
REPEAT_DETERM1 o (atac
ORELSE' rtac @{thm SigmaI}
ORELSE' ((rtac @{thm CollectI} ORELSE' rtac collectI') THEN'
- TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]))
+ TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN'
- TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]))
+ TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
ORELSE' (rtac @{thm image_eqI} THEN'
(REPEAT_DETERM o
(rtac @{thm refl}
- ORELSE' rtac @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]})))
+ ORELSE' rtac @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]})))
ORELSE' rtac @{thm UNIV_I}
ORELSE' rtac @{thm iffD2[OF Compl_iff]}
ORELSE' atac)
@@ -375,16 +375,16 @@
ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]}
ORELSE' etac @{thm conjE}
ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
- TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}]) THEN'
+ TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]) THEN'
REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})
ORELSE' (etac @{thm imageE}
THEN' (REPEAT_DETERM o CHANGED o
- (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.cases})
+ (TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
THEN' REPEAT_DETERM o etac @{thm Pair_inject}
THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})))
ORELSE' etac @{thm ComplE}
ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
- THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.cases}])
+ THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}])
THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl}))
fun tac ctxt fm =
@@ -427,7 +427,7 @@
HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t'')))
end;
fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (prop_of th))
- val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.cases}
+ val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case}
fun tac ctxt =
rtac @{thm set_eqI}
THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms)
--- a/src/HOL/Topological_Spaces.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Feb 21 00:09:56 2014 +0100
@@ -1298,7 +1298,7 @@
assume *: "\<forall>n. \<exists>p. ?P p n"
def f \<equiv> "rec_nat (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
- have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(2) ..
+ have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.rec(2) ..
have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
then have "subseq f" unfolding subseq_Suc_iff by auto
@@ -1320,7 +1320,7 @@
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
def f \<equiv> "rec_nat (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
- have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(2) ..
+ have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.rec(2) ..
have P_0: "?P (f 0) (Suc N)"
unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
{ fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"