adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
* * *
more transition of 'xxx_rec' to 'rec_xxx' and same for case
* * *
compile
* * *
'rename_tac's to avoid referring to generated names
* * *
more robust scripts with 'rename_tac'
* * *
'where' -> 'of'
* * *
'where' -> 'of'
* * *
renamed 'xxx_rec' to 'rec_xxx'
--- a/src/Doc/LaTeXsugar/Sugar.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/Doc/LaTeXsugar/Sugar.thy Wed Feb 12 08:37:06 2014 +0100
@@ -166,9 +166,9 @@
\end{quote}
To support the ``\_''-notation for irrelevant variables
the constant \texttt{DUMMY} has been introduced:
-@{thm fst_conv[where b = DUMMY]} is produced by
+@{thm fst_conv[of _ DUMMY]} is produced by
\begin{quote}
-\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
+\verb!@!\verb!{thm fst_conv[of _ DUMMY]}!
\end{quote}
Variables that are bound by quantifiers or lambdas cannot be renamed
like this. Instead, the attribute \texttt{rename\_abs} does the
--- a/src/Doc/ProgProve/Isar.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/Doc/ProgProve/Isar.thy Wed Feb 12 08:37:06 2014 +0100
@@ -636,8 +636,8 @@
thus ?thesis by simp
qed
-text{*\index{cases@@{text"cases"}|(}Function @{text tl} (''tail'') is defined by @{thm tl.simps(1)} and
-@{thm tl.simps(2)}. Note that the result type of @{const length} is @{typ nat}
+text{*\index{cases@@{text"cases"}|(}Function @{text tl} (''tail'') is defined by @{thm list.sel(2)} and
+@{thm list.sel(3)}. Note that the result type of @{const length} is @{typ nat}
and @{prop"0 - 1 = (0::nat)"}.
This proof pattern works for any term @{text t} whose type is a datatype.
--- a/src/HOL/Auth/Guard/Extensions.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Wed Feb 12 08:37:06 2014 +0100
@@ -410,6 +410,7 @@
lemma knows_sub_app: "knows A evs <= knows A (evs @ evs')"
apply (induct evs, auto)
apply (simp add: knows_decomp)
+apply (rename_tac a b c)
by (case_tac a, auto simp: knows.simps)
subsubsection{*maximum knowledge an agent can have
@@ -504,7 +505,8 @@
by (induct evs, auto split: event.split)
lemma used'_parts [rule_format]: "X:used' evs ==> Y:parts {X} --> Y:used' evs"
-apply (induct evs, simp)
+apply (induct evs, simp)
+apply (rename_tac a b)
apply (case_tac a, simp_all)
apply (blast dest: parts_trans)+;
done
@@ -521,7 +523,7 @@
by (auto dest: used_sub_Cons [THEN subsetD])
lemma used_appD [dest]: "X:used (evs @ evs') ==> X:used evs | X:used evs'"
-by (induct evs, auto, case_tac a, auto)
+by (induct evs, auto, rename_tac a b, case_tac a, auto)
lemma used_ConsD: "X:used (ev#evs) ==> X:used [ev] | X:used evs"
by (case_tac ev, auto)
@@ -572,6 +574,7 @@
apply (case_tac "A=Spy", blast)
apply (induct evs)
apply (simp add: used.simps, blast)
+apply (rename_tac a evs)
apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe)
apply (erule initState_used)
@@ -585,6 +588,7 @@
apply force
apply (induct evs)
apply (simp add: knows_max_def used.simps, blast)
+apply (rename_tac a evs)
apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe)
apply (case_tac a, auto)
--- a/src/HOL/Auth/Guard/Guard.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy Wed Feb 12 08:37:06 2014 +0100
@@ -228,6 +228,7 @@
lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
apply (induct l)
apply (rule_tac x="[]" in exI, simp, clarsimp)
+apply (rename_tac a b l')
apply (subgoal_tac "EX l''. kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
apply (rule_tac x="l''@l'" in exI, simp)
apply (rule kparts_insert_substI, simp)
--- a/src/HOL/Auth/Guard/GuardK.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy Wed Feb 12 08:37:06 2014 +0100
@@ -222,6 +222,7 @@
lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
apply (induct l)
apply (rule_tac x="[]" in exI, simp, clarsimp)
+apply (rename_tac a b l')
apply (subgoal_tac "EX l''. kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
apply (rule_tac x="l''@l'" in exI, simp)
apply (rule kparts_insert_substI, simp)
--- a/src/HOL/Auth/KerberosIV.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/KerberosIV.thy Wed Feb 12 08:37:06 2014 +0100
@@ -256,23 +256,27 @@
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
apply (induct_tac "evs")
-apply (induct_tac [2] "a", auto)
+apply (rename_tac [2] a b)
+apply (induct_tac [2] a, auto)
done
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
apply (induct_tac "evs")
-apply (induct_tac [2] "a", auto)
+apply (rename_tac [2] a b)
+apply (induct_tac [2] a, auto)
done
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
(if A:bad then insert X (spies evs) else spies evs)"
apply (induct_tac "evs")
-apply (induct_tac [2] "a", auto)
+apply (rename_tac [2] a b)
+apply (induct_tac [2] a, auto)
done
lemma spies_evs_rev: "spies evs = spies (rev evs)"
apply (induct_tac "evs")
-apply (induct_tac [2] "a")
+apply (rename_tac [2] a b)
+apply (induct_tac [2] a)
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
done
@@ -280,6 +284,7 @@
lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
txt{* Resembles @{text"used_subset_append"} in theory Event.*}
done
@@ -407,6 +412,7 @@
lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
@@ -414,6 +420,7 @@
lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
@@ -421,6 +428,7 @@
lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
@@ -428,6 +436,7 @@
lemma used_evs_rev: "used evs = used (rev evs)"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply (simp add: used_Says_rev)
apply (simp add: used_Gets_rev)
@@ -438,6 +447,7 @@
"x : used (takeWhile P X) --> x : used X"
apply (induct_tac "X")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply (simp_all add: used_Nil)
apply (blast dest!: initState_into_used)+
--- a/src/HOL/Auth/KerberosV.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/KerberosV.thy Wed Feb 12 08:37:06 2014 +0100
@@ -207,22 +207,26 @@
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
(if A:bad then insert X (spies evs) else spies evs)"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done
lemma spies_evs_rev: "spies evs = spies (rev evs)"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a")
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
done
@@ -231,6 +235,7 @@
lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
txt{* Resembles @{text"used_subset_append"} in theory Event.*}
done
--- a/src/HOL/Auth/Kerberos_BAN.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/Kerberos_BAN.thy Wed Feb 12 08:37:06 2014 +0100
@@ -139,22 +139,26 @@
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
(if A:bad then insert X (spies evs) else spies evs)"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done
lemma spies_evs_rev: "spies evs = spies (rev evs)"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a")
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
done
@@ -163,6 +167,7 @@
lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
txt{* Resembles @{text"used_subset_append"} in theory Event.*}
done
@@ -174,6 +179,7 @@
lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
@@ -181,6 +187,7 @@
lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
@@ -188,6 +195,7 @@
lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
@@ -195,6 +203,7 @@
lemma used_evs_rev: "used evs = used (rev evs)"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply (simp add: used_Says_rev)
apply (simp add: used_Gets_rev)
@@ -205,6 +214,7 @@
"x : used (takeWhile P X) --> x : used X"
apply (induct_tac "X")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply (simp_all add: used_Nil)
apply (blast dest!: initState_into_used)+
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy Wed Feb 12 08:37:06 2014 +0100
@@ -168,6 +168,7 @@
lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
@@ -175,6 +176,7 @@
lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
@@ -182,6 +184,7 @@
lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply auto
done
@@ -189,6 +192,7 @@
lemma used_evs_rev: "used evs = used (rev evs)"
apply (induct_tac "evs")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply (simp add: used_Says_rev)
apply (simp add: used_Gets_rev)
@@ -199,6 +203,7 @@
"x : used (takeWhile P X) --> x : used X"
apply (induct_tac "X")
apply simp
+apply (rename_tac a b)
apply (induct_tac "a")
apply (simp_all add: used_Nil)
apply (blast dest!: initState_into_used)+
--- a/src/HOL/Auth/NS_Shared.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/NS_Shared.thy Wed Feb 12 08:37:06 2014 +0100
@@ -385,22 +385,26 @@
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
(if A:bad then insert X (spies evs) else spies evs)"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done
lemma spies_evs_rev: "spies evs = spies (rev evs)"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a")
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
done
@@ -409,6 +413,7 @@
lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs"
apply (induct_tac "evs")
+apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
txt{* Resembles @{text"used_subset_append"} in theory Event.*}
done
--- a/src/HOL/Auth/TLS.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Auth/TLS.thy Wed Feb 12 08:37:06 2014 +0100
@@ -81,7 +81,7 @@
inj_sessionK: "inj sessionK"
--{*sessionK is collision-free; also, no clientK clashes with any serverK.*}
apply (rule exI [of _
- "%((x,y,z), r). prod_encode(role_case 0 1 r,
+ "%((x,y,z), r). prod_encode(case_role 0 1 r,
prod_encode(x, prod_encode(y,z)))"])
apply (simp add: inj_on_def prod_encode_eq split: role.split)
done
--- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Wed Feb 12 08:37:06 2014 +0100
@@ -860,7 +860,7 @@
have "subtr (insert n ?ns1) (f (last (n1 # nl))) (f n)"
using f subtr.Step[OF _ fn1_flast fn1] by auto
thus ?case unfolding 1 by simp
-qed (metis f hd.simps last_ConsL last_in_set not_Cons_self2 subtr.Refl)
+qed (metis f list.sel(1) last_ConsL last_in_set not_Cons_self2 subtr.Refl)
lemma reg_subtr_path_aux:
assumes f: "reg f tr" and n: "subtr ns tr1 tr"
@@ -878,7 +878,7 @@
obtain nl where nl: "path f nl" and f_nl: "f (hd nl) = tr1"
and last_nl: "f (last nl) = tr2" and set: "set nl \<subseteq> ns" using Step(3)[OF tr1] by auto
have 0: "path f (root tr # nl)" apply (subst path.simps)
- using f_nl nl reg_root tr tr1_tr by (metis hd.simps neq_Nil_conv)
+ using f_nl nl reg_root tr tr1_tr by (metis list.sel(1) neq_Nil_conv)
show ?case apply(rule exI[of _ "(root tr) # nl"])
using 0 reg_root tr last_nl nl path_NE rtr set by auto
qed
--- a/src/HOL/Bali/Conform.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Bali/Conform.thy Wed Feb 12 08:37:06 2014 +0100
@@ -437,9 +437,10 @@
lemma conforms_absorb [rule_format]:
"(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)"
apply (rule impI)
-apply ( case_tac a)
+apply (case_tac a)
apply (case_tac "absorb j a")
apply auto
+apply (rename_tac a)
apply (case_tac "absorb j (Some a)",auto)
apply (erule conforms_NormI)
done
@@ -554,5 +555,4 @@
apply (force dest: conforms_globsD)+
done
-
end
--- a/src/HOL/Bali/Eval.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Bali/Eval.thy Wed Feb 12 08:37:06 2014 +0100
@@ -141,7 +141,7 @@
where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" where
- "undefined3 = sum3_case (In1 \<circ> case_sum (\<lambda>x. undefined) (\<lambda>x. Unit))
+ "undefined3 = case_sum3 (In1 \<circ> case_sum (\<lambda>x. undefined) (\<lambda>x. Unit))
(\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)"
lemma [simp]: "undefined3 (In1l x) = In1 undefined"
--- a/src/HOL/Bali/State.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Bali/State.thy Wed Feb 12 08:37:06 2014 +0100
@@ -232,11 +232,11 @@
definition
globs :: "st \<Rightarrow> globs"
- where "globs = st_case (\<lambda>g l. g)"
+ where "globs = case_st (\<lambda>g l. g)"
definition
locals :: "st \<Rightarrow> locals"
- where "locals = st_case (\<lambda>g l. l)"
+ where "locals = case_st (\<lambda>g l. l)"
definition heap :: "st \<Rightarrow> heap" where
"heap s = globs s \<circ> Heap"
@@ -303,19 +303,19 @@
definition
gupd :: "oref \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')" [10, 10] 1000)
- where "gupd r obj = st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
+ where "gupd r obj = case_st (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
definition
lupd :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')" [10, 10] 1000)
- where "lupd vn v = st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
+ where "lupd vn v = case_st (\<lambda>g l. st g (l(vn\<mapsto>v)))"
definition
upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
- where "upd_gobj r n v = st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
+ where "upd_gobj r n v = case_st (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
definition
set_locals :: "locals \<Rightarrow> st \<Rightarrow> st"
- where "set_locals l = st_case (\<lambda>g l'. st g l)"
+ where "set_locals l = case_st (\<lambda>g l'. st g l)"
definition
init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
--- a/src/HOL/Bali/TypeSafe.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Bali/TypeSafe.thy Wed Feb 12 08:37:06 2014 +0100
@@ -825,7 +825,7 @@
lemma lconf_map_lname [simp]:
- "G,s\<turnstile>(lname_case l1 l2)[\<Colon>\<preceq>](lname_case L1 L2)
+ "G,s\<turnstile>(case_lname l1 l2)[\<Colon>\<preceq>](case_lname L1 L2)
=
(G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
apply (unfold lconf_def)
@@ -833,7 +833,7 @@
done
lemma wlconf_map_lname [simp]:
- "G,s\<turnstile>(lname_case l1 l2)[\<sim>\<Colon>\<preceq>](lname_case L1 L2)
+ "G,s\<turnstile>(case_lname l1 l2)[\<sim>\<Colon>\<preceq>](case_lname L1 L2)
=
(G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
apply (unfold wlconf_def)
@@ -841,7 +841,7 @@
done
lemma lconf_map_ename [simp]:
- "G,s\<turnstile>(ename_case l1 l2)[\<Colon>\<preceq>](ename_case L1 L2)
+ "G,s\<turnstile>(case_ename l1 l2)[\<Colon>\<preceq>](case_ename L1 L2)
=
(G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
apply (unfold lconf_def)
@@ -849,7 +849,7 @@
done
lemma wlconf_map_ename [simp]:
- "G,s\<turnstile>(ename_case l1 l2)[\<sim>\<Colon>\<preceq>](ename_case L1 L2)
+ "G,s\<turnstile>(case_ename l1 l2)[\<sim>\<Colon>\<preceq>](case_ename L1 L2)
=
(G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
apply (unfold wlconf_def)
@@ -1436,9 +1436,9 @@
lemma dom_vname_split:
- "dom (lname_case (ename_case (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
- = dom (lname_case (ename_case (tab(x\<mapsto>y)) a) b) \<union>
- dom (lname_case (ename_case (tab(xs[\<mapsto>]ys)) a) b)"
+ "dom (case_lname (case_ename (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
+ = dom (case_lname (case_ename (tab(x\<mapsto>y)) a) b) \<union>
+ dom (case_lname (case_ename (tab(xs[\<mapsto>]ys)) a) b)"
(is "?List x xs y ys = ?Hd x y \<union> ?Tl xs ys")
proof
show "?List x xs y ys \<subseteq> ?Hd x y \<union> ?Tl xs ys"
@@ -1514,37 +1514,37 @@
qed
qed
-lemma dom_ename_case_None_simp:
- "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)"
+lemma dom_case_ename_None_simp:
+ "dom (case_ename vname_tab None) = VNam ` (dom vname_tab)"
apply (auto simp add: dom_def image_def )
apply (case_tac "x")
apply auto
done
-lemma dom_ename_case_Some_simp:
- "dom (ename_case vname_tab (Some a)) = VNam ` (dom vname_tab) \<union> {Res}"
+lemma dom_case_ename_Some_simp:
+ "dom (case_ename vname_tab (Some a)) = VNam ` (dom vname_tab) \<union> {Res}"
apply (auto simp add: dom_def image_def )
apply (case_tac "x")
apply auto
done
-lemma dom_lname_case_None_simp:
- "dom (lname_case ename_tab None) = EName ` (dom ename_tab)"
+lemma dom_case_lname_None_simp:
+ "dom (case_lname ename_tab None) = EName ` (dom ename_tab)"
apply (auto simp add: dom_def image_def )
apply (case_tac "x")
apply auto
done
-lemma dom_lname_case_Some_simp:
- "dom (lname_case ename_tab (Some a)) = EName ` (dom ename_tab) \<union> {This}"
+lemma dom_case_lname_Some_simp:
+ "dom (case_lname ename_tab (Some a)) = EName ` (dom ename_tab) \<union> {This}"
apply (auto simp add: dom_def image_def)
apply (case_tac "x")
apply auto
done
-lemmas dom_lname_ename_case_simps =
- dom_ename_case_None_simp dom_ename_case_Some_simp
- dom_lname_case_None_simp dom_lname_case_Some_simp
+lemmas dom_lname_case_ename_simps =
+ dom_case_ename_None_simp dom_case_ename_Some_simp
+ dom_case_lname_None_simp dom_case_lname_Some_simp
lemma image_comp:
"f ` g ` A = (f \<circ> g) ` A"
@@ -1569,13 +1569,13 @@
with static_m' dom_vnames m
show ?thesis
by (cases s) (simp add: init_lvars_def Let_def parameters_def
- dom_lname_ename_case_simps image_comp)
+ dom_lname_case_ename_simps image_comp)
next
case False
with static_m' dom_vnames m
show ?thesis
by (cases s) (simp add: init_lvars_def Let_def parameters_def
- dom_lname_ename_case_simps image_comp)
+ dom_lname_case_ename_simps image_comp)
qed
qed
--- a/src/HOL/Datatype.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Datatype.thy Wed Feb 12 08:37:06 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 case_nat_Suc [THEN trans])
+apply (fast intro!: apfst_conv nat.cases(2)[THEN trans])
done
--- a/src/HOL/Decision_Procs/Cooper.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Feb 12 08:37:06 2014 +0100
@@ -303,12 +303,12 @@
lemma evaldjf_bound0:
assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
- using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
+ using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f x1", auto)
lemma evaldjf_qf:
assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
- using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
+ using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f x1", auto)
fun disjuncts :: "fm \<Rightarrow> fm list"
where
--- a/src/HOL/Decision_Procs/Ferrack.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Feb 12 08:37:06 2014 +0100
@@ -328,12 +328,12 @@
lemma evaldjf_bound0:
assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
- using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
+ using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
lemma evaldjf_qf:
assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
- using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
+ using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
fun disjuncts :: "fm \<Rightarrow> fm list" where
"disjuncts (Or p q) = disjuncts p @ disjuncts q"
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 12 08:37:06 2014 +0100
@@ -761,12 +761,12 @@
lemma evaldjf_bound0:
assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
- using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
+ using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
lemma evaldjf_qf:
assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
- using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
+ using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
fun disjuncts :: "fm \<Rightarrow> fm list" where
"disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
@@ -3003,5 +3003,3 @@
oops
*)
end
-
-
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Wed Feb 12 08:37:06 2014 +0100
@@ -919,6 +919,7 @@
"last ((a %* p) +++ (x#(b %* p))) = (if p = [] then x else b * last p)"
apply (induct p arbitrary: a x b)
apply auto
+ apply (rename_tac a p aa x b)
apply (subgoal_tac "padd (cmult aa p) (times b a # cmult b p) \<noteq> []")
apply simp
apply (induct_tac p)
@@ -1042,6 +1043,7 @@
lemma poly_mono: "abs(x) \<le> k \<Longrightarrow> abs(poly p (x::'a::{linordered_idom})) \<le> poly (map abs p) k"
apply (induct p)
apply auto
+ apply (rename_tac a p)
apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans)
apply (rule abs_triangle_ineq)
apply (auto intro!: mult_mono simp add: abs_mult)
--- a/src/HOL/HOLCF/Lift.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/HOLCF/Lift.thy Wed Feb 12 08:37:06 2014 +0100
@@ -71,23 +71,23 @@
by (induct x) auto
qed
-subsection {* Continuity of @{const lift_case} *}
+subsection {* Continuity of @{const case_lift} *}
-lemma lift_case_eq: "lift_case \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
+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 (simp add: Rep_lift_strict)
apply (simp add: Def_def Abs_lift_inverse)
done
-lemma cont2cont_lift_case [simp]:
- "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))"
-unfolding lift_case_eq by (simp add: cont_Rep_lift)
+lemma cont2cont_case_lift [simp]:
+ "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. case_lift \<bottom> (f x) (g x))"
+unfolding case_lift_eq by (simp add: cont_Rep_lift)
subsection {* Further operations *}
definition
flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) where
- "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
+ "flift1 = (\<lambda>f. (\<Lambda> x. case_lift \<bottom> f x))"
translations
"\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)"
--- a/src/HOL/Hoare_Parallel/Graph.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Hoare_Parallel/Graph.thy Wed Feb 12 08:37:06 2014 +0100
@@ -53,6 +53,7 @@
apply(case_tac "list")
apply force
apply simp
+apply(rename_tac lista)
apply(rotate_tac -2)
apply(erule_tac x = "0" in all_dupE)
apply simp
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Feb 12 08:37:06 2014 +0100
@@ -636,6 +636,7 @@
prefer 2
apply force
apply(case_tac xsa,simp,simp)
+ apply(rename_tac list)
apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
apply(rule conjI,erule CptnEnv)
apply(simp (no_asm_use) add:lift_def)
@@ -733,6 +734,7 @@
apply(case_tac xs,simp add:cp_def)
apply clarify
apply (simp del:map.simps)
+ apply (rename_tac list)
apply(subgoal_tac "(map (lift Q) ((a, b) # list))\<noteq>[]")
apply(drule last_conv_nth)
apply (simp del:map.simps)
@@ -1032,6 +1034,7 @@
apply(drule last_conv_nth)
apply (simp del:map.simps last.simps)
apply(simp add:nth_append del:last.simps)
+ apply(rename_tac a list)
apply(subgoal_tac "((Some (While b P), snd (last ((Some P, sa) # xs))) # a # list)\<noteq>[]")
apply(drule last_conv_nth)
apply (simp del:map.simps last.simps)
@@ -1349,6 +1352,7 @@
apply(subgoal_tac "xs\<noteq>[]")
prefer 2
apply simp
+apply(rename_tac a list)
apply(thin_tac "xs = a # list")
apply(simp add:par_com_validity_def par_comm_def)
apply clarify
--- a/src/HOL/Hoare_Parallel/RG_Tran.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Wed Feb 12 08:37:06 2014 +0100
@@ -838,6 +838,7 @@
apply(case_tac x)
apply(force elim:par_cptn.cases)
apply simp
+ apply(rename_tac a list)
apply(erule_tac x="list" in allE)
apply clarify
apply simp
--- a/src/HOL/Import/HOL_Light_Maps.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy Wed Feb 12 08:37:06 2014 +0100
@@ -232,11 +232,11 @@
"\<forall>nil' cons'. \<exists>fn\<Colon>'A list \<Rightarrow> 'Z. fn [] = nil' \<and> (\<forall>(a0\<Colon>'A) a1\<Colon>'A list. fn (a0 # a1) = cons' a0 a1 (fn a1))"
by (intro allI, rule_tac x="rec_list nil' cons'" in exI) auto
-lemma HD[import_const HD : List.hd]:
+lemma HD[import_const HD : List.list.hd]:
"hd ((h\<Colon>'A) # t) = h"
by simp
-lemma TL[import_const TL : List.tl]:
+lemma TL[import_const TL : List.list.tl]:
"tl ((h\<Colon>'A) # t) = t"
by simp
--- a/src/HOL/Induct/QuoNestedDataType.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Feb 12 08:37:06 2014 +0100
@@ -212,6 +212,7 @@
lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us"
apply (induct z)
+apply (rename_tac [2] a b)
apply (rule_tac [2] z=a in eq_Abs_Exp)
apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv intro: exprel_refl)
done
--- a/src/HOL/Library/Multiset.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Feb 12 08:37:06 2014 +0100
@@ -955,6 +955,7 @@
lemma distinct_count_atmost_1:
"distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
apply (induct x, simp, rule iffI, simp_all)
+apply (rename_tac a b)
apply (rule conjI)
apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
apply (erule_tac x = a in allE, simp, clarify)
--- a/src/HOL/Library/Polynomial.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Library/Polynomial.thy Wed Feb 12 08:37:06 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' case_nat_Suc) }
+ by (induct ms) (auto, metis Suc_pred' nat.cases(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 case_nat_0 case_nat_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
+ by (metis nat.cases 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 Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Library/RBT_Impl.thy Wed Feb 12 08:37:06 2014 +0100
@@ -1748,14 +1748,14 @@
hide_type (open) compare
hide_const (open)
- compare_height skip_black skip_red LT GT EQ compare_case compare_rec
- Abs_compare Rep_compare compare_rep_set
+ compare_height skip_black skip_red LT GT EQ case_compare rec_compare
+ Abs_compare Rep_compare rep_set_compare
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.nchotomy compare.split compare.split_asm compare_rec_def
+ 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
equal_compare_def
--- a/src/HOL/List.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/List.thy Wed Feb 12 08:37:06 2014 +0100
@@ -1648,10 +1648,10 @@
lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
apply (induct xs, simp, simp)
apply safe
-apply (metis case_nat_0 nth.simps zero_less_Suc)
+apply (metis nat.cases(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 case_nat_Suc nth.simps zero_less_diff)
+apply (metis diff_Suc_Suc nat.cases(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/Metis_Examples/Clausification.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Metis_Examples/Clausification.thy Wed Feb 12 08:37:06 2014 +0100
@@ -138,7 +138,7 @@
by (metis split_list_last_prop[where P = P] in_set_conv_decomp)
lemma ex_tl: "EX ys. tl ys = xs"
-using tl.simps(2) by fast
+using list.sel(3) by fast
lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
by (metis ex_tl)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Feb 12 08:37:06 2014 +0100
@@ -80,7 +80,7 @@
apply (rule allI)
apply (drule_tac x="a # ys" in spec)
apply (simp only: rev.simps append_assoc append_Cons append_Nil
- map.simps map_of.simps map_upds_Cons hd.simps tl.simps)
+ map.simps map_of.simps map_upds_Cons list.sel)
done
lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))"
--- a/src/HOL/MicroJava/Comp/Index.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy Wed Feb 12 08:37:06 2014 +0100
@@ -54,6 +54,7 @@
apply (simp only: index_def gjmb_plns_def)
apply (case_tac "gmb G C S" rule: prod.exhaust)
apply (simp add: galldefs del: set_append map_append)
+apply (rename_tac a b)
apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append)
apply (intro strip)
apply (simp del: set_append map_append)
@@ -73,6 +74,7 @@
locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))"
apply (simp only: locvars_xstate_def locvars_locals_def index_def)
apply (case_tac "gmb G C S" rule: prod.exhaust, simp)
+apply (rename_tac a b)
apply (case_tac b, simp)
apply (rule conjI)
apply (simp add: gl_def)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Feb 12 08:37:06 2014 +0100
@@ -3870,6 +3870,7 @@
apply rule
apply (erule_tac x="Some y" in allE)
defer
+ apply (rename_tac x)
apply (erule_tac x="Some x" in allE)
apply auto
done
--- a/src/HOL/Nat.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nat.thy Wed Feb 12 08:37:06 2014 +0100
@@ -71,33 +71,79 @@
lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y"
by (rule iffI, rule Suc_Rep_inject) simp_all
+lemma nat_induct0:
+ fixes n
+ assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
+ shows "P n"
+using assms
+apply (unfold Zero_nat_def Suc_def)
+apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
+apply (erule Nat_Rep_Nat [THEN Nat.induct])
+apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
+done
+
+wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]]
+ apply atomize_elim
+ apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
+ apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
+ Suc_Rep_inject' Rep_Nat_inject)
+apply (simp only: Suc_not_Zero)
+done
+
+-- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+setup {* Sign.mandatory_path "old" *}
+
rep_datatype "0 \<Colon> nat" Suc
- apply (unfold Zero_nat_def Suc_def)
- apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
- apply (erule Nat_Rep_Nat [THEN Nat.induct])
- apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
- apply (simp_all add: Nat_Abs_Nat_inject Nat_Rep_Nat
- Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep
- Suc_Rep_not_Zero_Rep [symmetric]
- Suc_Rep_inject' Rep_Nat_inject)
- done
+ apply (erule nat_induct0, assumption)
+ apply (rule nat.inject)
+apply (rule nat.distinct(1))
+done
+
+setup {* Sign.parent_path *}
+
+-- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
+setup {* Sign.mandatory_path "nat" *}
+
+declare
+ old.nat.inject[iff del]
+ old.nat.distinct(1)[simp del, induct_simp del]
+
+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
+
+setup {* Sign.parent_path *}
+
+abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" where
+ "rec_nat \<equiv> old.rec_nat"
+
+hide_const Nat.pred -- {* hide everything related to the selector *}
+hide_fact
+ nat.case_eq_if
+ nat.collapse
+ nat.expand
+ nat.sel
+ nat.sel_exhaust
+ nat.sel_split
+ nat.sel_split_asm
+
+lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
+ -- {* for backward compatibility -- names of variables differ *}
+ "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
+by (rule nat.exhaust)
lemma nat_induct [case_names 0 Suc, induct type: nat]:
-- {* for backward compatibility -- names of variables differ *}
fixes n
- assumes "P 0"
- and "\<And>n. P n \<Longrightarrow> P (Suc n)"
+ assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
shows "P n"
- using assms by (rule nat.induct)
-
-declare nat.exhaust [case_names 0 Suc, cases type: nat]
+using assms by (rule nat.induct)
-lemmas nat_rec_0 = nat.recs(1)
- and nat_rec_Suc = nat.recs(2)
-
-lemmas case_nat_0 = nat.cases(1)
- and case_nat_Suc = nat.cases(2)
-
+hide_fact
+ nat_exhaust
+ nat_induct0
text {* Injectiveness and distinctness lemmas *}
@@ -632,14 +678,6 @@
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
-text {* These two rules ease the use of primitive recursion.
-NOTE USE OF @{text "=="} *}
-lemma def_rec_nat_0: "(!!n. f n == rec_nat c h n) ==> f 0 = c"
-by simp
-
-lemma def_rec_nat_Suc: "(!!n. f n == rec_nat c h n) ==> f (Suc n) = h n (f n)"
-by simp
-
lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
by (cases n) simp_all
@@ -1928,4 +1966,3 @@
hide_const (open) of_nat_aux
end
-
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 12 08:37:06 2014 +0100
@@ -649,17 +649,17 @@
nitpick [expect = genuine]
oops
-lemma "T1_rec a b A = a"
+lemma "rec_T1 a b A = a"
nitpick [expect = none]
apply simp
done
-lemma "T1_rec a b B = b"
+lemma "rec_T1 a b B = b"
nitpick [expect = none]
apply simp
done
-lemma "P (T1_rec a b x)"
+lemma "P (rec_T1 a b x)"
nitpick [expect = genuine]
oops
@@ -681,17 +681,17 @@
nitpick [expect = genuine]
oops
-lemma "T2_rec c d (C x) = c x"
+lemma "rec_T2 c d (C x) = c x"
nitpick [expect = none]
apply simp
done
-lemma "T2_rec c d (D x) = d x"
+lemma "rec_T2 c d (D x) = d x"
nitpick [expect = none]
apply simp
done
-lemma "P (T2_rec c d x)"
+lemma "P (rec_T2 c d x)"
nitpick [expect = genuine]
oops
@@ -713,12 +713,12 @@
nitpick [expect = genuine]
oops
-lemma "T3_rec e (E x) = e x"
+lemma "rec_T3 e (E x) = e x"
nitpick [card = 1\<emdash>4, expect = none]
apply simp
done
-lemma "P (T3_rec e x)"
+lemma "P (rec_T3 e x)"
nitpick [expect = genuine]
oops
@@ -818,22 +818,22 @@
nitpick [expect = genuine]
oops
-lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
+lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
nitpick [expect = none]
apply simp
done
-lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
+lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)"
nitpick [expect = none]
apply simp
done
-lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
+lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)"
nitpick [expect = none]
apply simp
done
-lemma "P (BitList_rec nil bit0 bit1 x)"
+lemma "P (rec_BitList nil bit0 bit1 x)"
nitpick [expect = genuine]
oops
@@ -851,17 +851,17 @@
nitpick [expect = genuine]
oops
-lemma "BinTree_rec l n (Leaf x) = l x"
+lemma "rec_BinTree l n (Leaf x) = l x"
nitpick [expect = none]
apply simp
done
-lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
+lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
nitpick [card = 1\<emdash>5, expect = none]
apply simp
done
-lemma "P (BinTree_rec l n x)"
+lemma "P (rec_BinTree l n x)"
nitpick [expect = genuine]
oops
@@ -894,17 +894,17 @@
nitpick [expect = genuine]
oops
-lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
+lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"
+lemma "rec_aexp_bexp_1 number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp_bexp_1 number ite equal y) (rec_aexp_bexp_1 number ite equal z)"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "P (aexp_bexp_rec_1 number ite equal x)"
+lemma "P (rec_aexp_bexp_1 number ite equal x)"
nitpick [expect = genuine]
oops
@@ -912,12 +912,12 @@
nitpick [expect = genuine]
oops
-lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"
+lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp_bexp_1 number ite equal x) (rec_aexp_bexp_1 number ite equal y)"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "P (aexp_bexp_rec_2 number ite equal x)"
+lemma "P (rec_aexp_bexp_2 number ite equal x)"
nitpick [expect = genuine]
oops
@@ -972,41 +972,41 @@
nitpick [expect = genuine]
oops
-lemma "X_Y_rec_1 a b c d e f A = a"
+lemma "rec_X_Y_1 a b c d e f A = a"
nitpick [card = 1\<emdash>5, expect = none]
apply simp
done
-lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"
+lemma "rec_X_Y_1 a b c d e f (B x) = b x (rec_X_Y_1 a b c d e f x)"
nitpick [card = 1\<emdash>5, expect = none]
apply simp
done
-lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"
+lemma "rec_X_Y_1 a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)"
nitpick [card = 1\<emdash>5, expect = none]
apply simp
done
-lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"
+lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X_Y_1 a b c d e f x)"
nitpick [card = 1\<emdash>5, expect = none]
apply simp
done
-lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"
+lemma "rec_X_Y_2 a b c d e f (E y) = e y (rec_X_Y_2 a b c d e f y)"
nitpick [card = 1\<emdash>5, expect = none]
apply simp
done
-lemma "X_Y_rec_2 a b c d e f F = f"
+lemma "rec_X_Y_2 a b c d e f F = f"
nitpick [card = 1\<emdash>5, expect = none]
apply simp
done
-lemma "P (X_Y_rec_1 a b c d e f x)"
+lemma "P (rec_X_Y_1 a b c d e f x)"
nitpick [expect = genuine]
oops
-lemma "P (X_Y_rec_2 a b c d e f y)"
+lemma "P (rec_X_Y_2 a b c d e f y)"
nitpick [expect = genuine]
oops
@@ -1028,45 +1028,45 @@
nitpick [expect = genuine]
oops
-lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
+lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
nitpick [card = 1\<emdash>5, expect = none]
apply simp
done
-lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"
+lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
+lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1"
nitpick [card = 1\<emdash>4, expect = none]
apply simp
done
-lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
+lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
nitpick [card = 1\<emdash>4, expect = none]
apply simp
done
-lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
+lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2"
nitpick [card = 1\<emdash>4, expect = none]
apply simp
done
-lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
+lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
nitpick [card = 1\<emdash>4, expect = none]
apply simp
done
-lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
+lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
nitpick [expect = genuine]
oops
-lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
+lemma "P (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
nitpick [expect = genuine]
oops
-lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
+lemma "P (rec_XOpt_3 cx dx n1 s1 n2 s2 x)"
nitpick [expect = genuine]
oops
@@ -1084,26 +1084,26 @@
nitpick [expect = genuine]
oops
-lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
+lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)"
nitpick [card = 1\<emdash>2, expect = none]
apply simp
done
-lemma "YOpt_rec_2 cy n s None = n"
+lemma "rec_YOpt_2 cy n s None = n"
nitpick [card = 1\<emdash>2, expect = none]
apply simp
done
-lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
+lemma "rec_YOpt_2 cy n s (Some x) = s x (\<lambda>a. rec_YOpt_1 cy n s (x a))"
nitpick [card = 1\<emdash>2, expect = none]
apply simp
done
-lemma "P (YOpt_rec_1 cy n s x)"
+lemma "P (rec_YOpt_1 cy n s x)"
nitpick [expect = genuine]
oops
-lemma "P (YOpt_rec_2 cy n s x)"
+lemma "P (rec_YOpt_2 cy n s x)"
nitpick [expect = genuine]
oops
@@ -1121,26 +1121,26 @@
nitpick [expect = genuine]
oops
-lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
+lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)"
nitpick [card = 1\<emdash>4, expect = none]
apply simp
done
-lemma "Trie_rec_2 tr nil cons [] = nil"
+lemma "rec_Trie_2 tr nil cons [] = nil"
nitpick [card = 1\<emdash>4, expect = none]
apply simp
done
-lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"
+lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)"
nitpick [card = 1\<emdash>4, expect = none]
apply simp
done
-lemma "P (Trie_rec_1 tr nil cons x)"
+lemma "P (rec_Trie_1 tr nil cons x)"
nitpick [card = 1, expect = genuine]
oops
-lemma "P (Trie_rec_2 tr nil cons x)"
+lemma "P (rec_Trie_2 tr nil cons x)"
nitpick [card = 1, expect = genuine]
oops
@@ -1158,17 +1158,17 @@
nitpick [expect = genuine]
oops
-lemma "InfTree_rec leaf node Leaf = leaf"
+lemma "rec_InfTree leaf node Leaf = leaf"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
+lemma "rec_InfTree leaf node (Node x) = node x (\<lambda>n. rec_InfTree leaf node (x n))"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "P (InfTree_rec leaf node x)"
+lemma "P (rec_InfTree leaf node x)"
nitpick [expect = genuine]
oops
@@ -1187,22 +1187,22 @@
nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
oops
-lemma "lambda_rec var app lam (Var x) = var x"
+lemma "rec_lambda var app lam (Var x) = var x"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
+lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
+lemma "rec_lambda var app lam (Lam x) = lam x (\<lambda>a. rec_lambda var app lam (x a))"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "P (lambda_rec v a l x)"
+lemma "P (rec_lambda v a l x)"
nitpick [expect = genuine]
oops
@@ -1223,40 +1223,40 @@
nitpick [expect = genuine]
oops
-lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
+lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "U_rec_2 e c d nil cons (C x) = c x"
+lemma "rec_U_2 e c d nil cons (C x) = c x"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
+lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "U_rec_3 e c d nil cons [] = nil"
+lemma "rec_U_3 e c d nil cons [] = nil"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)"
+lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)"
nitpick [card = 1\<emdash>3, expect = none]
apply simp
done
-lemma "P (U_rec_1 e c d nil cons x)"
+lemma "P (rec_U_1 e c d nil cons x)"
nitpick [expect = genuine]
oops
-lemma "P (U_rec_2 e c d nil cons x)"
+lemma "P (rec_U_2 e c d nil cons x)"
nitpick [card = 1, expect = genuine]
oops
-lemma "P (U_rec_3 e c d nil cons x)"
+lemma "P (rec_U_3 e c d nil cons x)"
nitpick [card = 1, expect = genuine]
oops
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Feb 12 08:37:06 2014 +0100
@@ -164,7 +164,7 @@
by (rule Rep_Nat_inverse)
lemma "Abs_list (Rep_list a) = a"
-nitpick [card = 1\<emdash>2, expect = none]
+(* nitpick [card = 1\<emdash>2, expect = none] FIXME *)
by (rule Rep_list_inverse)
record point =
--- a/src/HOL/Nominal/Examples/Class3.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nominal/Examples/Class3.thy Wed Feb 12 08:37:06 2014 +0100
@@ -2311,6 +2311,7 @@
apply(rule_tac my_wf_induct_triple[OF a])
apply(case_tac x rule: prod.exhaust)
apply(simp)
+apply(rename_tac p a b)
apply(case_tac b)
apply(simp)
apply(rule b)
--- a/src/HOL/Nominal/Examples/Fsub.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Feb 12 08:37:06 2014 +0100
@@ -167,7 +167,8 @@
assumes a: "X\<in>(ty_dom \<Gamma>)"
shows "\<exists>T.(TVarB X T)\<in>set \<Gamma>"
using a
- apply (induct \<Gamma>, auto)
+ apply (induct \<Gamma>, auto)
+ apply (rename_tac a \<Gamma>')
apply (subgoal_tac "\<exists>T.(TVarB X T=a)")
apply (auto)
apply (auto simp add: ty_binding_existence)
--- a/src/HOL/Nominal/Examples/W.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nominal/Examples/W.thy Wed Feb 12 08:37:06 2014 +0100
@@ -1,5 +1,5 @@
theory W
-imports Nominal
+imports "../Nominal"
begin
text {* Example for strong induction rules avoiding sets of atoms. *}
@@ -388,6 +388,7 @@
shows "supp \<Gamma> = set (ftv \<Gamma>)"
apply (induct \<Gamma>)
apply (simp_all add: supp_list_nil supp_list_cons)
+apply (rename_tac a \<Gamma>')
apply (case_tac a)
apply (simp add: supp_prod supp_atm ftv_tyS)
done
@@ -443,6 +444,7 @@
using asm
apply(induct Xs)
apply(simp)
+apply(rename_tac a Xs')
apply(case_tac "X=a")
apply(simp add: abs_fresh)
apply(simp add: abs_fresh)
--- a/src/HOL/Option.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Option.thy Wed Feb 12 08:37:06 2014 +0100
@@ -16,7 +16,7 @@
lemma [case_names None Some, cases type: option]:
-- {* for backward compatibility -- names of variables differ *}
- "(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>option. y = Some option \<Longrightarrow> P) \<Longrightarrow> P"
+ "(y = None \<Longrightarrow> P) \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> P) \<Longrightarrow> P"
by (rule option.exhaust)
lemma [case_names None Some, induct type: option]:
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 12 08:37:06 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 rec_nat_0 by auto
+ unfolding w_def nat.recs(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 rec_nat_Suc unfolding w_def[symmetric]
+ unfolding w_def nat.recs(2) unfolding w_def[symmetric]
by (rule someI_ex)
then show ?case by auto
qed
--- a/src/HOL/Probability/Radon_Nikodym.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Feb 12 08:37:06 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 rec_nat_Suc
+ from Ex_P[OF this, of i] show ?case unfolding nat.recs(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: rec_nat_Suc)
+ have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.recs(2))
from epsilon[OF B(1) this] *
show False by auto
qed
--- a/src/HOL/Product_Type.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Product_Type.thy Wed Feb 12 08:37:06 2014 +0100
@@ -698,7 +698,7 @@
"case_prod f p = f (fst p) (snd p)"
by (fact split_beta)
-lemma case_prods3 [cases type]:
+lemma prod_cases3 [cases type]:
obtains (fields) a b c where "y = (a, b, c)"
by (cases y, case_tac b) blast
@@ -706,7 +706,7 @@
"(!!a b c. P (a, b, c)) ==> P x"
by (cases x) blast
-lemma case_prods4 [cases type]:
+lemma prod_cases4 [cases type]:
obtains (fields) a b c d where "y = (a, b, c, d)"
by (cases y, case_tac c) blast
@@ -714,7 +714,7 @@
"(!!a b c d. P (a, b, c, d)) ==> P x"
by (cases x) blast
-lemma case_prods5 [cases type]:
+lemma prod_cases5 [cases type]:
obtains (fields) a b c d e where "y = (a, b, c, d, e)"
by (cases y, case_tac d) blast
@@ -722,7 +722,7 @@
"(!!a b c d e. P (a, b, c, d, e)) ==> P x"
by (cases x) blast
-lemma case_prods6 [cases type]:
+lemma prod_cases6 [cases type]:
obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
by (cases y, case_tac e) blast
@@ -730,7 +730,7 @@
"(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
by (cases x) blast
-lemma case_prods7 [cases type]:
+lemma prod_cases7 [cases type]:
obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
by (cases y, case_tac f) blast
--- a/src/HOL/Proofs/Lambda/LambdaType.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy Wed Feb 12 08:37:06 2014 +0100
@@ -30,12 +30,7 @@
by (simp add: shift_def)
lemma shift_commute [simp]: "e\<langle>i:U\<rangle>\<langle>0:T\<rangle> = e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>"
- apply (rule ext)
- apply (case_tac x)
- apply simp
- apply (case_tac nat)
- apply (simp_all add: shift_def)
- done
+ by (rule ext) (simp_all add: shift_def split: nat.split)
subsection {* Types and typing rules *}
@@ -157,6 +152,7 @@
"e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
apply (induct ts arbitrary: t T)
apply simp
+ apply (rename_tac a b t T)
apply atomize
apply simp
apply (erule_tac x = "t \<degree> a" in allE)
@@ -177,12 +173,14 @@
"e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
apply (induct ts arbitrary: t T Ts)
apply simp
+ apply (rename_tac a b t T Ts)
apply atomize
apply (case_tac Ts)
apply simp
apply simp
apply (erule_tac x = "t \<degree> a" in allE)
apply (erule_tac x = T in allE)
+ apply (rename_tac list)
apply (erule_tac x = list in allE)
apply (erule impE)
apply (erule conjE)
@@ -225,6 +223,7 @@
apply (erule var_app_type_eq)
apply assumption
apply simp
+ apply (rename_tac a b ts Ts U)
apply atomize
apply (case_tac U)
apply (rule FalseE)
--- a/src/HOL/ROOT Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/ROOT Wed Feb 12 08:37:06 2014 +0100
@@ -464,7 +464,7 @@
Author: Tobias Nipkow and Konrad Slind and Olaf Müller
Copyright 1994--1996 TU Muenchen
- The meta theory of I/O-Automata in HOL. This formalization has been
+ The meta-theory of I/O-Automata in HOL. This formalization has been
significantly changed and extended, see HOLCF/IOA. There are also the
proofs of two communication protocols which formerly have been here.
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Feb 12 08:37:06 2014 +0100
@@ -671,6 +671,7 @@
lemma N_fresh_not_KeyCryptNonce:
"\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs"
apply (induct_tac "evs")
+apply (rename_tac [2] a evs')
apply (case_tac [2] "a")
apply (auto simp add: parts_insert2)
done
--- a/src/HOL/SET_Protocol/Event_SET.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy Wed Feb 12 08:37:06 2014 +0100
@@ -159,6 +159,7 @@
lemma Notes_imp_parts_subset_used [rule_format]:
"Notes A X \<in> set evs --> parts {X} <= used evs"
apply (induct_tac "evs")
+apply (rename_tac [2] a evs')
apply (induct_tac [2] "a", auto)
done
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Wed Feb 12 08:37:06 2014 +0100
@@ -669,13 +669,13 @@
"tl [x, y, z] = [y, z]"
"hd (tl [x, y, z]) = y"
"tl (tl [x, y, z]) = [z]"
- using hd.simps tl.simps(2) list.simps
+ using list.sel(1,3) list.simps
by smt+
lemma
"fst (hd [(a, b)]) = a"
"snd (hd [(a, b)]) = b"
- using fst_conv snd_conv pair_collapse hd.simps tl.simps(2) list.simps
+ using fst_conv snd_conv pair_collapse list.sel(1,3) list.simps
by smt+
@@ -808,14 +808,14 @@
"tl [x, y, z] = [y, z]"
"hd (tl [x, y, z]) = y"
"tl (tl [x, y, z]) = [z]"
- using hd.simps tl.simps(2)
+ using list.sel(1,3)
using [[smt_datatypes, smt_oracle, z3_with_extensions]]
by smt+
lemma
"fst (hd [(a, b)]) = a"
"snd (hd [(a, b)]) = b"
- using fst_conv snd_conv pair_collapse hd.simps tl.simps(2)
+ using fst_conv snd_conv pair_collapse list.sel(1,3)
using [[smt_datatypes, smt_oracle, z3_with_extensions]]
by smt+
--- a/src/HOL/Tools/BNF/bnf_gfp_util.ML Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML Wed Feb 12 08:37:06 2014 +0100
@@ -148,7 +148,7 @@
fun mk_rec_nat Zero Suc =
let val T = fastype_of Zero;
- in Const (@{const_name rec_nat}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end;
+ in Const (@{const_name old.rec_nat}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end;
fun mk_rec_list Nil Cons =
let
--- a/src/HOL/Tools/Datatype/datatype.ML Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Feb 12 08:37:06 2014 +0100
@@ -283,11 +283,11 @@
(* isomorphisms are defined using primrec-combinators: *)
(* generate appropriate functions for instantiating primrec-combinator *)
(* *)
- (* e.g. dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y)) *)
+ (* e.g. Rep_dt_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y)) *)
(* *)
(* also generate characteristic equations for isomorphisms *)
(* *)
- (* e.g. dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *)
+ (* e.g. Rep_dt_i (cons h t) = In1 (Scons (Rep_dt_j h) (Rep_dt_i t)) *)
(*---------------------------------------------------------------------*)
fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) =
@@ -387,7 +387,7 @@
end
in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
- (* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *)
+ (* prove inj Rep_dt_i and Rep_dt_i x : rep_set_dt_i *)
val fun_congs =
map (fn T => make_elim (Drule.instantiate' [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
@@ -457,7 +457,7 @@
val iso_inj_thms =
map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
- (* prove dt_rep_set_i x --> x : range dt_Rep_i *)
+ (* prove rep_set_dt_i x --> x : range Rep_dt_i *)
fun mk_iso_t (((set_name, iso_name), i), T) =
let val isoT = T --> Univ_elT in
--- a/src/HOL/Topological_Spaces.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Wed Feb 12 08:37:06 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_rec_Suc ..
+ have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(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_rec_Suc ..
+ have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(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)"
--- a/src/HOL/Transcendental.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Transcendental.thy Wed Feb 12 08:37:06 2014 +0100
@@ -624,6 +624,7 @@
(\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
apply (rule ext)
apply (case_tac "n", simp)
+ apply (rename_tac nat)
apply (case_tac "nat", simp)
apply (simp add: r_neq_0)
done
@@ -2710,7 +2711,8 @@
apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
prefer 2 apply (erule LeastI)
apply (case_tac "LEAST m::nat. x < real m * y", simp)
-apply (subgoal_tac "~ x < real nat * y")
+apply (rename_tac m)
+apply (subgoal_tac "~ x < real m * y")
prefer 2 apply (rule not_less_Least, simp, force)
done
--- a/src/HOL/Transitive_Closure.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Transitive_Closure.thy Wed Feb 12 08:37:06 2014 +0100
@@ -846,6 +846,7 @@
\<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)
\<Longrightarrow> P"
apply (cases n, simp)
+ apply (rename_tac nat)
apply (cut_tac n=nat and R=R in relpow_Suc_D2', simp, blast)
done
@@ -1297,4 +1298,3 @@
{* simple transitivity reasoner (predicate version) *}
end
-
--- a/src/HOL/Word/Word_Miscellaneous.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy Wed Feb 12 08:37:06 2014 +0100
@@ -118,10 +118,6 @@
lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *)
-(* TODO: move name bindings to List.thy *)
-lemmas tl_Nil = tl.simps (1)
-lemmas tl_Cons = tl.simps (2)
-
lemma the_elemI: "y = {x} ==> the_elem y = x"
by simp
--- a/src/HOL/ex/Tree23.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/ex/Tree23.thy Wed Feb 12 08:37:06 2014 +0100
@@ -330,12 +330,12 @@
"dfull n (Some (p, (False, t'))) \<longleftrightarrow> full (Suc n) t'"
lemmas dfull_case_intros =
- ord.exhaust [where y=y and P="dfull a (ord_case b c d y)"]
+ ord.exhaust [of y "dfull a (case_ord b c d y)"]
option.exhaust [of y "dfull a (case_option b c y)"]
prod.exhaust [of y "dfull a (case_prod b y)"]
bool.exhaust [of y "dfull a (case_bool b c y)"]
- tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))"]
- tree23.exhaust [where y=y and P="full a (tree23_case b c d y)"]
+ tree23.exhaust [of y "dfull a (Some (b, case_tree23 c d e y))"]
+ tree23.exhaust [of y "full a (case_tree23 b c d y)"]
for a b c d e y
lemma dfull_del: "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
@@ -396,7 +396,7 @@
apply (case_tac n, simp, simp)
apply (frule dfull_del [where k="Some k"])
apply (cases "del (Some k) t", force)
-apply (case_tac "a", rename_tac p b t', case_tac "b", auto)
+apply (rename_tac a, case_tac "a", rename_tac b t', case_tac "b", auto)
done
text{* This is a little test harness and should be commented out once the