--- a/NEWS Mon Sep 11 14:35:30 2006 +0200
+++ b/NEWS Mon Sep 11 21:35:19 2006 +0200
@@ -301,7 +301,7 @@
assumes a: "A n x"
shows "P n x"
using a -- {* make induct insert fact a *}
- proof (induct n fixing: x) -- {* generalize goal to "!!x. A n x ==> P n x" *}
+ proof (induct n arbitrary: x) -- {* generalize goal to "!!x. A n x ==> P n x" *}
case 0
show ?case sorry
next
@@ -321,7 +321,7 @@
assumes a: "A (a x)"
shows "P (a x)"
using a
- proof (induct n == "a x" fixing: x)
+ proof (induct n == "a x" arbitrary: x)
...
See also HOL/Isar_examples/Puzzle.thy for an application of the this
@@ -334,7 +334,7 @@
lemma
fixes n :: nat
obtains x :: 'a where "P n x" and "Q n x"
- proof (induct n fixing: thesis)
+ proof (induct n arbitrary: thesis)
case 0
obtain x where "P 0 x" and "Q 0 x" sorry
then show thesis by (rule 0)
@@ -345,8 +345,8 @@
then show thesis by (rule Suc.prems)
qed
-Here the 'fixing: thesis' specification essentially modifies the scope
-of the formal thesis parameter, in order to the get the whole
+Here the 'arbitrary: thesis' specification essentially modifies the
+scope of the formal thesis parameter, in order to the get the whole
existence statement through the induction as expected.
* Provers/induct: mutual induction rules are now specified as a list
--- a/doc-src/IsarRef/generic.tex Mon Sep 11 14:35:30 2006 +0200
+++ b/doc-src/IsarRef/generic.tex Mon Sep 11 21:35:19 2006 +0200
@@ -1516,7 +1516,7 @@
\begin{rail}
'cases' open? (insts * 'and') rule?
;
- 'induct' open? (definsts * 'and') \\ fixing? taking? rule?
+ 'induct' open? (definsts * 'and') \\ arbitrary? taking? rule?
;
'coinduct' open? insts taking rule?
;
@@ -1529,7 +1529,7 @@
;
definsts: ( definst *)
;
- fixing: 'fixing' ':' ((term *) 'and' +)
+ arbitrary: 'arbitrary' ':' ((term *) 'and' +)
;
taking: 'taking' ':' insts
;
@@ -1587,11 +1587,11 @@
In order to achieve practically useful induction hypotheses, some variables
occurring in $t$ need to be fixed (see below).
- The optional ``$fixing\colon \vec x$'' specification generalizes variables
- $\vec x$ of the original goal before applying induction. Thus induction
- hypotheses may become sufficiently general to get the proof through.
- Together with definitional instantiations, one may effectively perform
- induction over expressions of a certain structure.
+ The optional ``$arbitrary\colon \vec x$'' specification generalizes
+ variables $\vec x$ of the original goal before applying induction. Thus
+ induction hypotheses may become sufficiently general to get the proof
+ through. Together with definitional instantiations, one may effectively
+ perform induction over expressions of a certain structure.
The optional ``$taking\colon \vec t$'' specification provides additional
instantiations of a prefix of pending variables in the rule. Such schematic
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Sep 11 21:35:19 2006 +0200
@@ -2661,7 +2661,7 @@
\<Longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1)"
from eval and wt da G
show ?thesis
- proof (induct fixing: Env T A)
+ proof (induct arbitrary: Env T A)
case (Abrupt s t xc Env T A)
have da: "Env\<turnstile> dom (locals s) \<guillemotright>t\<guillemotright> A" using Abrupt.prems by simp
have "?NormalAssigned (Some xc,s) A"
--- a/src/HOL/Hoare/Heap.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Hoare/Heap.thy Mon Sep 11 21:35:19 2006 +0200
@@ -131,7 +131,7 @@
lemma Path_is_List:
"\<lbrakk>Path h b Ps (Ref a); a \<notin> set Ps\<rbrakk> \<Longrightarrow> List (h(a := Null)) b (Ps @ [a])"
-apply (induct Ps fixing: b)
+apply (induct Ps arbitrary: b)
apply (auto simp add:fun_upd_apply)
done
--- a/src/HOL/Hyperreal/Fact.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Hyperreal/Fact.thy Mon Sep 11 21:35:19 2006 +0200
@@ -54,7 +54,7 @@
lemma fact_diff_Suc [rule_format]:
"n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
- apply (induct n fixing: m)
+ apply (induct n arbitrary: m)
apply auto
apply (drule_tac x = "m - 1" in meta_spec, auto)
done
--- a/src/HOL/IMP/Denotation.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/IMP/Denotation.thy Mon Sep 11 21:35:19 2006 +0200
@@ -55,7 +55,7 @@
(* Denotational Semantics implies Operational Semantics *)
lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-apply (induct c fixing: s t)
+apply (induct c arbitrary: s t)
apply simp_all
apply fast
--- a/src/HOL/IMP/Expr.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/IMP/Expr.thy Mon Sep 11 21:35:19 2006 +0200
@@ -135,10 +135,10 @@
lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
- by (induct a fixing: n) auto
+ by (induct a arbitrary: n) auto
lemma bexp_iff:
"((b,s) -b-> w) = (B b s = w)"
- by (induct b fixing: w) (auto simp add: aexp_iff)
+ by (induct b arbitrary: w) (auto simp add: aexp_iff)
end
--- a/src/HOL/IMP/Hoare.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/IMP/Hoare.thy Mon Sep 11 21:35:19 2006 +0200
@@ -133,7 +133,7 @@
lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
lemma wp_is_pre: "|- {wp c Q} c {Q}"
-apply (induct c fixing: Q)
+apply (induct c arbitrary: Q)
apply (simp_all (no_asm))
apply fast+
apply (blast intro: hoare_conseq1)
--- a/src/HOL/IMP/Machines.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/IMP/Machines.thy Mon Sep 11 21:35:19 2006 +0200
@@ -192,7 +192,7 @@
"rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
-apply(induct fixing: p q p' q' set: exec01)
+apply(induct arbitrary: p q p' q' set: exec01)
apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
apply(drule sym)
apply simp
--- a/src/HOL/IMP/Natural.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/IMP/Natural.thy Mon Sep 11 21:35:19 2006 +0200
@@ -200,7 +200,7 @@
assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
shows "u = t"
using prems
-proof (induct fixing: u set: evalc)
+proof (induct arbitrary: u set: evalc)
fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
thus "u = s" by simp
next
@@ -261,7 +261,7 @@
assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
shows "u = t"
using prems
-proof (induct fixing: u)
+proof (induct arbitrary: u)
-- "the simple @{text \<SKIP>} case for demonstration:"
fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
thus "u = s" by simp
--- a/src/HOL/IMP/Transition.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/IMP/Transition.thy Mon Sep 11 21:35:19 2006 +0200
@@ -223,7 +223,7 @@
lemma semiD:
"\<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow>
\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> n = i+j"
-proof (induct n fixing: c1 c2 s s'')
+proof (induct n arbitrary: c1 c2 s s'')
case 0
then show ?case by simp
next
@@ -269,7 +269,7 @@
lemma semiI:
"\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-proof (induct n fixing: c0 s s'')
+proof (induct n arbitrary: c0 s s'')
case 0
from `\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
have False by simp
@@ -372,7 +372,7 @@
then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
moreover
have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- proof (induct fixing: c s s' rule: less_induct)
+ proof (induct arbitrary: c s s' rule: less_induct)
fix n
assume IH: "\<And>m c s s'. m < n \<Longrightarrow> \<langle>c,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
fix c s s'
@@ -511,7 +511,7 @@
lemma lemma2:
"\<langle>c;d,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<Longrightarrow> \<exists>t m. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<and> \<langle>d,t\<rangle> -m\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<and> m \<le> n"
-apply (induct n fixing: c d s u)
+apply (induct n arbitrary: c d s u)
-- "case n = 0"
apply fastsimp
-- "induction step"
@@ -521,7 +521,7 @@
lemma evalc1_impl_evalc:
"\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-apply (induct c fixing: s t)
+apply (induct c arbitrary: s t)
apply (safe dest!: rtrancl_imp_UN_rel_pow)
-- SKIP
@@ -666,7 +666,7 @@
lemma FB_lemma3:
"(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
\<langle>if c'=None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
- by (induct fixing: t set: evalc1)
+ by (induct arbitrary: t set: evalc1)
(auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
lemma FB_lemma2:
--- a/src/HOL/IMP/VC.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/IMP/VC.thy Mon Sep 11 21:35:19 2006 +0200
@@ -70,7 +70,7 @@
lemma l: "!s. P s --> P s" by fast
lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
-apply (induct c fixing: Q)
+apply (induct c arbitrary: Q)
apply (simp_all (no_asm))
apply fast
apply fast
@@ -151,6 +151,6 @@
qed
lemma vcawp_vc_awp: "vcawp c Q = (vc c Q, awp c Q)"
- by (induct c fixing: Q) (simp_all add: Let_def)
+ by (induct c arbitrary: Q) (simp_all add: Let_def)
end
--- a/src/HOL/Induct/PropLog.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Induct/PropLog.thy Mon Sep 11 21:35:19 2006 +0200
@@ -259,7 +259,7 @@
by (unfold sat_def, auto)
theorem completeness: "finite H ==> H |= p ==> H |- p"
-apply (induct fixing: p rule: finite_induct)
+apply (induct arbitrary: p rule: finite_induct)
apply (blast intro: completeness_0)
apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
done
--- a/src/HOL/Isar_examples/ExprCompiler.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Mon Sep 11 21:35:19 2006 +0200
@@ -114,7 +114,7 @@
lemma exec_append:
"exec (xs @ ys) stack env =
exec ys (exec xs stack env) env"
-proof (induct xs fixing: stack)
+proof (induct xs arbitrary: stack)
case Nil
show ?case by simp
next
@@ -153,7 +153,7 @@
lemma exec_append':
"exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
-proof (induct xs fixing: stack)
+proof (induct xs arbitrary: stack)
case (Nil s)
have "exec ([] @ ys) s env = exec ys s env" by simp
also have "... = exec ys (exec [] s env) env" by simp
--- a/src/HOL/Isar_examples/Hoare.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy Mon Sep 11 21:35:19 2006 +0200
@@ -167,7 +167,7 @@
assume "Sem (While b X c) s s'"
then obtain n where "iter n b (Sem c) s s'" by auto
from this and s show "s' : P Int -b"
- proof (induct n fixing: s)
+ proof (induct n arbitrary: s)
case 0
thus ?case by auto
next
--- a/src/HOL/Isar_examples/Puzzle.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy Mon Sep 11 21:35:19 2006 +0200
@@ -21,7 +21,7 @@
proof (rule order_antisym)
{
fix n show "n \<le> f n"
- proof (induct k \<equiv> "f n" fixing: n rule: less_induct)
+ proof (induct k \<equiv> "f n" arbitrary: n rule: less_induct)
case (less k n)
then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
show "n \<le> f n"
--- a/src/HOL/Lambda/Eta.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/Eta.thy Mon Sep 11 21:35:19 2006 +0200
@@ -45,18 +45,18 @@
subsection "Properties of eta, subst and free"
lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]"
- by (induct s fixing: i t u) (simp_all add: subst_Var)
+ by (induct s arbitrary: i t u) (simp_all add: subst_Var)
lemma free_lift [simp]:
"free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
- apply (induct t fixing: i k)
+ apply (induct t arbitrary: i k)
apply (auto cong: conj_cong)
done
lemma free_subst [simp]:
"free (s[t/k]) i =
(free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
- apply (induct s fixing: i k t)
+ apply (induct s arbitrary: i k t)
prefer 2
apply simp
apply blast
@@ -66,7 +66,7 @@
done
lemma free_eta: "s -e> t ==> free t i = free s i"
- by (induct fixing: i set: eta) (simp_all cong: conj_cong)
+ by (induct arbitrary: i set: eta) (simp_all cong: conj_cong)
lemma not_free_eta:
"[| s -e> t; \<not> free s i |] ==> \<not> free t i"
@@ -74,10 +74,10 @@
lemma eta_subst [simp]:
"s -e> t ==> s[u/i] -e> t[u/i]"
- by (induct fixing: u i set: eta) (simp_all add: subst_subst [symmetric])
+ by (induct arbitrary: u i set: eta) (simp_all add: subst_subst [symmetric])
theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
- by (induct s fixing: i dummy) simp_all
+ by (induct s arbitrary: i dummy) simp_all
subsection "Confluence of eta"
@@ -121,19 +121,19 @@
lemma free_beta:
"s -> t ==> free t i \<Longrightarrow> free s i"
- by (induct fixing: i set: beta) auto
+ by (induct arbitrary: i set: beta) auto
lemma beta_subst [intro]: "s -> t ==> s[u/i] -> t[u/i]"
- by (induct fixing: u i set: beta) (simp_all add: subst_subst [symmetric])
+ by (induct arbitrary: u i set: beta) (simp_all add: subst_subst [symmetric])
lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
- by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var)
+ by (induct t arbitrary: i) (auto elim!: linorder_neqE simp: subst_Var)
lemma eta_lift [simp]: "s -e> t ==> lift s i -e> lift t i"
- by (induct fixing: i set: eta) simp_all
+ by (induct arbitrary: i set: eta) simp_all
lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]"
- apply (induct u fixing: s t i)
+ apply (induct u arbitrary: s t i)
apply (simp_all add: subst_Var)
apply blast
apply (blast intro: rtrancl_eta_App)
@@ -165,7 +165,7 @@
lemma not_free_iff_lifted:
"(\<not> free s i) = (\<exists>t. s = lift t i)"
- apply (induct s fixing: i)
+ apply (induct s arbitrary: i)
apply simp
apply (rule iffI)
apply (erule linorder_neqE)
@@ -240,7 +240,7 @@
lemma free_par_eta [simp]:
assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
shows "free t i = free s i" using eta
- by (induct fixing: i) (simp_all cong: conj_cong)
+ by (induct arbitrary: i) (simp_all cong: conj_cong)
lemma par_eta_refl [simp]: "t \<Rightarrow>\<^sub>\<eta> t"
by (induct t) simp_all
@@ -248,12 +248,12 @@
lemma par_eta_lift [simp]:
assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
shows "lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta
- by (induct fixing: i) simp_all
+ by (induct arbitrary: i) simp_all
lemma par_eta_subst [simp]:
assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
shows "u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta
- by (induct fixing: u u' i) (simp_all add: subst_subst [symmetric] subst_Var)
+ by (induct arbitrary: u u' i) (simp_all add: subst_subst [symmetric] subst_Var)
theorem eta_subset_par_eta: "eta \<subseteq> par_eta"
apply (rule subsetI)
@@ -289,7 +289,7 @@
lemma eta_expand_Suc':
"eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))"
- by (induct n fixing: t) simp_all
+ by (induct n arbitrary: t) simp_all
theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)"
by (induct k) (simp_all add: lift_lift)
@@ -297,7 +297,7 @@
theorem eta_expand_beta:
assumes u: "u => u'"
shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
-proof (induct k fixing: t t')
+proof (induct k arbitrary: t t')
case 0
with u show ?case by simp
next
@@ -313,7 +313,7 @@
by (induct k) (simp_all add: t)
theorem eta_expand_eta: "t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'"
-proof (induct k fixing: t t')
+proof (induct k arbitrary: t t')
case 0
show ?case by simp
next
@@ -329,7 +329,7 @@
theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u"
shows "u = u1' \<degree> u2' \<Longrightarrow>
\<exists>u1 u2 k. t = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2'" using eta
-proof (induct fixing: u1' u2')
+proof (induct arbitrary: u1' u2')
case (app s s' t t')
have "s \<degree> t = eta_expand 0 (s \<degree> t)" by simp
with app show ?case by blast
@@ -359,7 +359,7 @@
theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'"
shows "t' = Abs u' \<Longrightarrow>
\<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta
-proof (induct fixing: u')
+proof (induct arbitrary: u')
case (abs s t)
have "Abs s = eta_expand 0 (Abs s)" by simp
with abs show ?case by blast
@@ -390,7 +390,7 @@
*}
theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
-proof (induct t fixing: s u taking: "size :: dB \<Rightarrow> nat" rule: measure_induct_rule)
+proof (induct t arbitrary: s u taking: "size :: dB \<Rightarrow> nat" rule: measure_induct_rule)
case (less t)
from `t => u`
show ?case
@@ -439,7 +439,7 @@
shows "t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u"
using eta [simplified rtrancl_subset
[OF eta_subset_par_eta par_eta_subset_eta, symmetric]]
-proof (induct fixing: u)
+proof (induct arbitrary: u)
case 1
thus ?case by blast
next
--- a/src/HOL/Lambda/Lambda.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/Lambda.thy Mon Sep 11 21:35:19 2006 +0200
@@ -114,24 +114,24 @@
lemma lift_lift:
"i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
- by (induct t fixing: i k) auto
+ by (induct t arbitrary: i k) auto
lemma lift_subst [simp]:
"j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
- by (induct t fixing: i j s)
+ by (induct t arbitrary: i j s)
(simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
lemma lift_subst_lt:
"i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
- by (induct t fixing: i j s) (simp_all add: subst_Var lift_lift)
+ by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift)
lemma subst_lift [simp]:
"(lift t k)[s/k] = t"
- by (induct t fixing: k s) simp_all
+ by (induct t arbitrary: k s) simp_all
lemma subst_subst:
"i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
- by (induct t fixing: i j u v)
+ by (induct t arbitrary: i j u v)
(simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
split: nat.split)
@@ -139,13 +139,13 @@
subsection {* Equivalence proof for optimized substitution *}
lemma liftn_0 [simp]: "liftn 0 t k = t"
- by (induct t fixing: k) (simp_all add: subst_Var)
+ by (induct t arbitrary: k) (simp_all add: subst_Var)
lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
- by (induct t fixing: k) (simp_all add: subst_Var)
+ by (induct t arbitrary: k) (simp_all add: subst_Var)
lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
- by (induct t fixing: n) (simp_all add: subst_Var)
+ by (induct t arbitrary: n) (simp_all add: subst_Var)
theorem substn_subst_0: "substn t s 0 = t[s/0]"
by simp
@@ -158,7 +158,7 @@
theorem subst_preserves_beta [simp]:
"r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
- by (induct fixing: t i set: beta) (simp_all add: subst_subst [symmetric])
+ by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
apply (induct set: rtrancl)
@@ -169,7 +169,7 @@
theorem lift_preserves_beta [simp]:
"r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
- by (induct fixing: i set: beta) auto
+ by (induct arbitrary: i set: beta) auto
theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
apply (induct set: rtrancl)
@@ -179,7 +179,7 @@
done
theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
- apply (induct t fixing: r s i)
+ apply (induct t arbitrary: r s i)
apply (simp add: subst_Var r_into_rtrancl)
apply (simp add: rtrancl_beta_App)
apply (simp add: rtrancl_beta_Abs)
--- a/src/HOL/Lambda/ListApplication.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Mon Sep 11 21:35:19 2006 +0200
@@ -16,11 +16,11 @@
by (induct ts rule: rev_induct) auto
lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
- by (induct ss fixing: s) auto
+ by (induct ss arbitrary: s) auto
lemma Var_apps_eq_Var_apps_conv [iff]:
"(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
- apply (induct rs fixing: ss rule: rev_induct)
+ apply (induct rs arbitrary: ss rule: rev_induct)
apply simp
apply blast
apply (induct_tac ss rule: rev_induct)
@@ -44,7 +44,7 @@
lemma Abs_apps_eq_Abs_apps_conv [iff]:
"(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
- apply (induct rs fixing: ss rule: rev_induct)
+ apply (induct rs arbitrary: ss rule: rev_induct)
apply simp
apply blast
apply (induct_tac ss rule: rev_induct)
@@ -53,11 +53,11 @@
lemma Abs_App_neq_Var_apps [iff]:
"Abs s \<degree> t \<noteq> Var n \<degree>\<degree> ss"
- by (induct ss fixing: s t rule: rev_induct) auto
+ by (induct ss arbitrary: s t rule: rev_induct) auto
lemma Var_apps_neq_Abs_apps [iff]:
"Var n \<degree>\<degree> ts \<noteq> Abs r \<degree>\<degree> ss"
- apply (induct ss fixing: ts rule: rev_induct)
+ apply (induct ss arbitrary: ts rule: rev_induct)
apply simp
apply (induct_tac ts rule: rev_induct)
apply auto
@@ -84,11 +84,11 @@
lemma lift_map [simp]:
"lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
- by (induct ts fixing: t) simp_all
+ by (induct ts arbitrary: t) simp_all
lemma subst_map [simp]:
"subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
- by (induct ts fixing: t) simp_all
+ by (induct ts arbitrary: t) simp_all
lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
by simp
@@ -100,7 +100,7 @@
assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
shows "size t = n \<Longrightarrow> P t"
- apply (induct n fixing: t rule: nat_less_induct)
+ apply (induct n arbitrary: t rule: nat_less_induct)
apply (cut_tac t = t in ex_head_tail)
apply clarify
apply (erule disjE)
--- a/src/HOL/Lambda/ListBeta.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/ListBeta.thy Mon Sep 11 21:35:19 2006 +0200
@@ -18,7 +18,7 @@
lemma head_Var_reduction:
"Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
- apply (induct u == "Var n \<degree>\<degree> rs" v fixing: rs set: beta)
+ apply (induct u == "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
apply simp
apply (rule_tac xs = rs in rev_exhaust)
apply simp
@@ -39,7 +39,7 @@
"(\<exists>r'. r -> r' \<and> s = r' \<degree>\<degree> rs) \<or>
(\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
(\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
- apply (induct u == "r \<degree>\<degree> rs" s fixing: r rs set: beta)
+ apply (induct u == "r \<degree>\<degree> rs" s arbitrary: r rs set: beta)
apply (case_tac r)
apply simp
apply (simp add: App_eq_foldl_conv)
@@ -78,7 +78,7 @@
lemma apps_preserves_betas [simp]:
"rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
- apply (induct rs fixing: ss rule: rev_induct)
+ apply (induct rs arbitrary: ss rule: rev_induct)
apply simp
apply simp
apply (rule_tac xs = ss in rev_exhaust)
--- a/src/HOL/Lambda/ListOrder.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/ListOrder.thy Mon Sep 11 21:35:19 2006 +0200
@@ -90,7 +90,7 @@
lemma Cons_acc_step1I [intro!]:
"x \<in> acc r ==> xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r)"
- apply (induct fixing: xs set: acc)
+ apply (induct arbitrary: xs set: acc)
apply (erule thin_rl)
apply (erule acc_induct)
apply (rule accI)
--- a/src/HOL/Lambda/ParRed.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/ParRed.thy Mon Sep 11 21:35:19 2006 +0200
@@ -68,11 +68,11 @@
lemma par_beta_lift [simp]:
"t => t' \<Longrightarrow> lift t n => lift t' n"
- by (induct t fixing: t' n) fastsimp+
+ by (induct t arbitrary: t' n) fastsimp+
lemma par_beta_subst:
"s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]"
- apply (induct t fixing: s s' t' n)
+ apply (induct t arbitrary: s s' t' n)
apply (simp add: subst_Var)
apply (erule par_beta_cases)
apply simp
@@ -104,7 +104,7 @@
"cd (Abs s) = Abs (cd s)"
lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
- apply (induct s fixing: t rule: cd.induct)
+ apply (induct s arbitrary: t rule: cd.induct)
apply auto
apply (fast intro!: par_beta_subst)
done
--- a/src/HOL/Lambda/StrongNorm.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/StrongNorm.thy Mon Sep 11 21:35:19 2006 +0200
@@ -17,7 +17,7 @@
subsection {* Properties of @{text IT} *}
lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> lift t i \<in> IT"
- apply (induct fixing: i set: IT)
+ apply (induct arbitrary: i set: IT)
apply (simp (no_asm))
apply (rule conjI)
apply
@@ -38,7 +38,7 @@
by (induct ts) auto
lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> r[Var i/j] \<in> IT"
- apply (induct fixing: i j set: IT)
+ apply (induct arbitrary: i j set: IT)
txt {* Case @{term Var}: *}
apply (simp (no_asm) add: subst_Var)
apply
--- a/src/HOL/Lambda/Type.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/Type.thy Mon Sep 11 21:35:19 2006 +0200
@@ -99,7 +99,7 @@
lemma lists_typings:
"e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
- apply (induct ts fixing: Ts)
+ apply (induct ts arbitrary: Ts)
apply (case_tac Ts)
apply simp
apply (rule lists.Nil)
@@ -113,7 +113,7 @@
done
lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
- apply (induct ts fixing: Ts)
+ apply (induct ts arbitrary: Ts)
apply simp
apply (case_tac Ts)
apply simp+
@@ -121,7 +121,7 @@
lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] =
(e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)"
- apply (induct ts fixing: Ts)
+ apply (induct ts arbitrary: Ts)
apply (case_tac Ts)
apply simp+
apply (case_tac Ts)
@@ -161,7 +161,7 @@
lemma list_app_typeD:
"e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
- apply (induct ts fixing: t T)
+ apply (induct ts arbitrary: t T)
apply simp
apply atomize
apply simp
@@ -181,7 +181,7 @@
lemma list_app_typeI:
"e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
- apply (induct ts fixing: t T Ts)
+ apply (induct ts arbitrary: t T Ts)
apply simp
apply atomize
apply (case_tac Ts)
@@ -206,7 +206,7 @@
theorem var_app_type_eq:
"e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
- apply (induct ts fixing: T U rule: rev_induct)
+ apply (induct ts arbitrary: T U rule: rev_induct)
apply simp
apply (ind_cases "e \<turnstile> Var i : T")
apply (ind_cases "e \<turnstile> Var i : T")
@@ -226,7 +226,7 @@
lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow>
e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us"
- apply (induct us fixing: ts Ts U)
+ apply (induct us arbitrary: ts Ts U)
apply simp
apply (erule var_app_type_eq)
apply assumption
@@ -293,11 +293,11 @@
subsection {* Lifting preserves well-typedness *}
lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
- by (induct fixing: i U set: typing) auto
+ by (induct arbitrary: i U set: typing) auto
lemma lift_types:
"e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
- apply (induct ts fixing: Ts)
+ apply (induct ts arbitrary: Ts)
apply simp
apply (case_tac Ts)
apply auto
@@ -308,7 +308,7 @@
lemma subst_lemma:
"e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T"
- apply (induct fixing: e' i U u set: typing)
+ apply (induct arbitrary: e' i U u set: typing)
apply (rule_tac x = x and y = i in linorder_cases)
apply auto
apply blast
@@ -317,7 +317,7 @@
lemma substs_lemma:
"e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
- apply (induct ts fixing: Ts)
+ apply (induct ts arbitrary: Ts)
apply (case_tac Ts)
apply simp
apply simp
@@ -334,7 +334,7 @@
subsection {* Subject reduction *}
lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t -> t' \<Longrightarrow> e \<turnstile> t' : T"
- apply (induct fixing: t' set: typing)
+ apply (induct arbitrary: t' set: typing)
apply blast
apply blast
apply atomize
--- a/src/HOL/Lambda/WeakNorm.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Mon Sep 11 21:35:19 2006 +0200
@@ -114,7 +114,7 @@
by (induct ts) simp_all
lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
- apply (induct fixing: i j set: NF)
+ apply (induct arbitrary: i j set: NF)
apply simp
apply (frule listall_conj1)
apply (drule listall_conj2)
@@ -156,7 +156,7 @@
by (induct ts) simp_all
lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
- apply (induct fixing: i set: NF)
+ apply (induct arbitrary: i set: NF)
apply (frule listall_conj1)
apply (drule listall_conj2)
apply (drule_tac i=i in lift_terms_NF)
--- a/src/HOL/Library/AssocList.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Library/AssocList.thy Mon Sep 11 21:35:19 2006 +0200
@@ -332,7 +332,7 @@
by (induct al) auto
lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v=v'"
-proof (induct al fixing: al')
+proof (induct al arbitrary: al')
case Nil thus ?case
by (cases al') (auto split: split_if_asm)
next
@@ -364,7 +364,7 @@
(* ******************************************************************************** *)
lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
-proof (induct ks fixing: vs al)
+proof (induct ks arbitrary: vs al)
case Nil
thus ?case by simp
next
@@ -387,11 +387,11 @@
assumes "distinct (map fst al)"
shows "distinct (map fst (updates ks vs al))"
using prems
-by (induct ks fixing: vs al) (auto simp add: distinct_update split: list.splits)
+by (induct ks arbitrary: vs al) (auto simp add: distinct_update split: list.splits)
lemma clearjunk_updates:
"clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
- by (induct ks fixing: vs al) (auto simp add: clearjunk_update split: list.splits)
+ by (induct ks arbitrary: vs al) (auto simp add: clearjunk_update split: list.splits)
lemma updates_empty[simp]: "updates vs [] al = al"
by (induct vs) auto
@@ -401,12 +401,12 @@
lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
- by (induct ks fixing: vs al) (auto split: list.splits)
+ by (induct ks arbitrary: vs al) (auto split: list.splits)
lemma updates_list_update_drop[simp]:
"\<lbrakk>size ks \<le> i; i < size vs\<rbrakk>
\<Longrightarrow> updates ks (vs[i:=v]) al = updates ks vs al"
- by (induct ks fixing: al vs i) (auto split:list.splits nat.splits)
+ by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits)
lemma update_updates_conv_if: "
map_of (updates xs ys (update x y al)) =
@@ -425,11 +425,11 @@
lemma updates_append_drop[simp]:
"size xs = size ys \<Longrightarrow> updates (xs@zs) ys al = updates xs ys al"
- by (induct xs fixing: ys al) (auto split: list.splits)
+ by (induct xs arbitrary: ys al) (auto split: list.splits)
lemma updates_append2_drop[simp]:
"size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
- by (induct xs fixing: ys al) (auto split: list.splits)
+ by (induct xs arbitrary: ys al) (auto split: list.splits)
(* ******************************************************************************** *)
subsection {* @{const map_ran} *}
@@ -455,13 +455,13 @@
(* ******************************************************************************** *)
lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
- by (induct ys fixing: xs) (auto simp add: dom_update)
+ by (induct ys arbitrary: xs) (auto simp add: dom_update)
lemma distinct_merge:
assumes "distinct (map fst xs)"
shows "distinct (map fst (merge xs ys))"
using prems
-by (induct ys fixing: xs) (auto simp add: dom_merge distinct_update)
+by (induct ys arbitrary: xs) (auto simp add: dom_merge distinct_update)
lemma clearjunk_merge:
"clearjunk (merge xs ys) = merge (clearjunk xs) ys"
--- a/src/HOL/Library/Coinductive_List.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Library/Coinductive_List.thy Mon Sep 11 21:35:19 2006 +0200
@@ -293,7 +293,7 @@
lemma EqLList_implies_ntrunc_equality:
"(M, N) \<in> EqLList (diag A) \<Longrightarrow> ntrunc k M = ntrunc k N"
- apply (induct k fixing: M N rule: nat_less_induct)
+ apply (induct k arbitrary: M N rule: nat_less_induct)
apply (erule EqLList.cases)
apply (safe del: equalityI)
apply (case_tac n)
--- a/src/HOL/Library/ExecutableSet.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy Mon Sep 11 21:35:19 2006 +0200
@@ -156,7 +156,7 @@
lemma iso_union:
"set (unionl xs ys) = set xs \<union> set ys"
- unfolding unionl_def by (induct xs fixing: ys) (simp_all add: iso_insert)
+ unfolding unionl_def by (induct xs arbitrary: ys) (simp_all add: iso_insert)
lemma iso_intersect:
"set (intersect xs ys) = set xs \<inter> set ys"
@@ -167,7 +167,7 @@
assumes distnct: "distinct ys"
shows "set (subtract xs ys) = set ys - set xs"
and "distinct (subtract xs ys)"
-unfolding subtract_def using distnct by (induct xs fixing: ys) (simp_all, auto)
+unfolding subtract_def using distnct by (induct xs arbitrary: ys) (simp_all, auto)
corollary iso_subtract':
fixes xs ys
--- a/src/HOL/Library/Multiset.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Sep 11 21:35:19 2006 +0200
@@ -746,7 +746,7 @@
lemma multiset_of_append [simp]:
"multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
- by (induct xs fixing: ys) (auto simp: union_ac)
+ by (induct xs arbitrary: ys) (auto simp: union_ac)
lemma surj_multiset_of: "surj multiset_of"
apply (unfold surj_def, rule allI)
--- a/src/HOL/Library/Nested_Environment.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Library/Nested_Environment.thy Mon Sep 11 21:35:19 2006 +0200
@@ -104,7 +104,7 @@
assumes "lookup env xs = None"
shows "lookup env (xs @ ys) = None"
using prems
-proof (induct xs fixing: env)
+proof (induct xs arbitrary: env)
case Nil
then have False by simp
then show ?case ..
@@ -141,7 +141,7 @@
assumes "lookup env xs = Some e"
shows "lookup env (xs @ ys) = lookup e ys"
using prems
-proof (induct xs fixing: env e)
+proof (induct xs arbitrary: env e)
case Nil
then have "env = e" by simp
then show "lookup env ([] @ ys) = lookup e ys" by simp
@@ -209,7 +209,7 @@
es' y = Some env' \<and>
lookup env' ys = Some e"
using prems
-proof (induct xs fixing: env e)
+proof (induct xs arbitrary: env e)
case Nil
from Nil.prems have "lookup env (y # ys) = Some e"
by simp
@@ -329,7 +329,7 @@
assumes "lookup env xs = Some e"
shows "lookup (update xs (Some env') env) xs = Some env'"
using prems
-proof (induct xs fixing: env e)
+proof (induct xs arbitrary: env e)
case Nil
then have "env = e" by simp
then show ?case by simp
@@ -378,7 +378,7 @@
assumes "lookup env xs = None"
shows "update (xs @ y # ys) opt env = env"
using prems
-proof (induct xs fixing: env)
+proof (induct xs arbitrary: env)
case Nil
then have False by simp
then show ?case ..
@@ -421,7 +421,7 @@
assumes "lookup env xs = Some e"
shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
using prems
-proof (induct xs fixing: env e)
+proof (induct xs arbitrary: env e)
case Nil
then have "env = e" by simp
then show ?case by simp
@@ -472,7 +472,7 @@
assumes neq: "y \<noteq> (z::'c)"
shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
lookup env (xs @ y # ys)"
-proof (induct xs fixing: env)
+proof (induct xs arbitrary: env)
case Nil
show ?case
proof (cases env)
--- a/src/HOL/List.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/List.thy Mon Sep 11 21:35:19 2006 +0200
@@ -311,7 +311,8 @@
lemma impossible_Cons [rule_format]:
"length xs <= length ys --> xs = x # ys = False"
-apply (induct xs, auto)
+apply (induct xs)
+apply auto
done
lemma list_induct2[consumes 1]: "\<And>ys.
@@ -1356,12 +1357,12 @@
lemma takeWhile_cong [fundef_cong, recdef_cong]:
"[| l = k; !!x. x : set l ==> P x = Q x |]
==> takeWhile P l = takeWhile Q k"
- by (induct k fixing: l, simp_all)
+ by (induct k arbitrary: l) (simp_all)
lemma dropWhile_cong [fundef_cong, recdef_cong]:
"[| l = k; !!x. x : set l ==> P x = Q x |]
==> dropWhile P l = dropWhile Q k"
- by (induct k fixing: l, simp_all)
+ by (induct k arbitrary: l, simp_all)
subsubsection {* @{text zip} *}
@@ -1600,12 +1601,12 @@
lemma foldl_cong [fundef_cong, recdef_cong]:
"[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
==> foldl f a l = foldl g b k"
- by (induct k fixing: a b l, simp_all)
+ by (induct k arbitrary: a b l) simp_all
lemma foldr_cong [fundef_cong, recdef_cong]:
"[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]
==> foldr f l a = foldr g k b"
- by (induct k fixing: a b l, simp_all)
+ by (induct k arbitrary: a b l) simp_all
lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
by (induct xs) auto
--- a/src/HOL/Nominal/Examples/CR.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy Mon Sep 11 21:35:19 2006 +0200
@@ -530,7 +530,7 @@
and b: "M\<longrightarrow>\<^isub>1M2"
shows "\<exists>M3. M1\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3"
using a b
-proof (induct fixing: M2)
+proof (induct arbitrary: M2)
case (o1 M) (* case 1 --- M1 = M *)
thus "\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
next
@@ -766,7 +766,7 @@
and b: "t\<longrightarrow>\<^isub>1t2"
shows "\<exists>t3. t1\<longrightarrow>\<^isub>1t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3"
using a b
-proof (induct fixing: t2)
+proof (induct arbitrary: t2)
case 1 thus ?case by force
next
case (2 s1 s2)
--- a/src/HOL/Nominal/Examples/Fsub.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Mon Sep 11 21:35:19 2006 +0200
@@ -801,7 +801,7 @@
lemma
shows trans: "\<Gamma>\<turnstile>S<:Q \<Longrightarrow> \<Gamma>\<turnstile>Q<:T \<Longrightarrow> \<Gamma>\<turnstile>S<:T"
and narrow: "(\<Delta>@[(X,Q)]@\<Gamma>)\<turnstile>M<:N \<Longrightarrow> \<Gamma>\<turnstile>P<:Q \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>)\<turnstile>M<:N"
-proof (induct Q fixing: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule)
+proof (induct Q arbitrary: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule)
case (less Q)
--{* \begin{minipage}[t]{0.9\textwidth}
First we mention the induction hypotheses of the outer induction for later
--- a/src/HOL/Nominal/Examples/Iteration.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Nominal/Examples/Iteration.thy Mon Sep 11 21:35:19 2006 +0200
@@ -57,7 +57,7 @@
and c2: "(t,r')\<in>it f1 f2 f3"
shows "r=r'"
using c1 c2
-proof (induct fixing: r')
+proof (induct arbitrary: r')
case it1
then show ?case by cases (simp_all add: lam.inject)
next
--- a/src/HOL/Nominal/Examples/Weakening.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy Mon Sep 11 21:35:19 2006 +0200
@@ -213,7 +213,7 @@
and c: "\<Gamma>1 \<lless> \<Gamma>2"
shows "\<Gamma>2 \<turnstile> t:\<sigma>"
using a b c
-proof (induct fixing: \<Gamma>2)
+proof (induct arbitrary: \<Gamma>2)
case (t1 \<Gamma>1 \<tau> a) (* variable case *)
have "\<Gamma>1 \<lless> \<Gamma>2"
and "valid \<Gamma>2"
--- a/src/HOL/Relation_Power.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Relation_Power.thy Mon Sep 11 21:35:19 2006 +0200
@@ -59,7 +59,7 @@
lemma rel_pow_Suc_I2:
"(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
- apply (induct n fixing: z)
+ apply (induct n arbitrary: z)
apply simp
apply fastsimp
done
@@ -79,7 +79,7 @@
lemma rel_pow_Suc_D2:
"(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
- apply (induct n fixing: x z)
+ apply (induct n arbitrary: x z)
apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
done
--- a/src/HOL/Unix/Unix.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Unix/Unix.thy Mon Sep 11 21:35:19 2006 +0200
@@ -657,7 +657,7 @@
lemma can_exec_snocD: "can_exec root (xs @ [y])
\<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''"
-proof (induct xs fixing: root)
+proof (induct xs arbitrary: root)
case Nil
then show ?case
by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
--- a/src/HOL/W0/W0.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/W0/W0.thy Mon Sep 11 21:35:19 2006 +0200
@@ -439,7 +439,7 @@
Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
theorem W_correct: "Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
-proof (induct e fixing: a s t m n)
+proof (induct e arbitrary: a s t m n)
case (Var i)
from `Ok (s, t, m) = \<W> (Var i) a n`
show "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
--- a/src/HOL/ex/CodeRandom.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/ex/CodeRandom.thy Mon Sep 11 21:35:19 2006 +0200
@@ -72,7 +72,7 @@
fix n
assume "n < length xs"
then show "pick (map (Pair 1) xs) n = nth xs n"
- proof (induct xs fixing: n)
+ proof (induct xs arbitrary: n)
case Nil then show ?case by simp
next
case (Cons x xs) show ?case
--- a/src/HOL/ex/ReflectionEx.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/ex/ReflectionEx.thy Mon Sep 11 21:35:19 2006 +0200
@@ -173,7 +173,7 @@
"lin_mul t = (\<lambda> i. Mul i t)"
lemma lin_mul: "Inum bs (lin_mul t i) = Inum bs (Mul i t)"
-by (induct t fixing: i rule: lin_mul.induct, auto simp add: ring_eq_simps)
+by (induct t arbitrary: i rule: lin_mul.induct) (auto simp add: ring_eq_simps)
consts linum:: "num \<Rightarrow> num"
recdef linum "measure num_size"
--- a/src/HOL/ex/ThreeDivides.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/ex/ThreeDivides.thy Mon Sep 11 21:35:19 2006 +0200
@@ -176,7 +176,7 @@
lemma exp_exists:
"m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)"
-proof (induct nd \<equiv> "nlen m" fixing: m)
+proof (induct nd \<equiv> "nlen m" arbitrary: m)
case 0 thus ?case by (simp add: nlen_zero)
next
case (Suc nd)
--- a/src/Provers/induct_method.ML Mon Sep 11 14:35:30 2006 +0200
+++ b/src/Provers/induct_method.ML Mon Sep 11 21:35:19 2006 +0200
@@ -357,7 +357,7 @@
in
-fun induct_tac ctxt is_open def_insts fixing taking opt_rule facts =
+fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
let
val _ = warn_open is_open;
val thy = ProofContext.theory_of ctxt;
@@ -396,7 +396,7 @@
(Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
THEN' fix_tac defs_ctxt
(nth concls (j - 1) + more_consumes)
- (nth_list fixing (j - 1))))
+ (nth_list arbitrary (j - 1))))
THEN' inner_atomize_tac) j))
THEN' atomize_tac) i st |> Seq.maps (fn st' =>
guess_instance (internalize more_consumes rule) i st'
@@ -467,7 +467,7 @@
(** concrete syntax **)
val openN = "open";
-val fixingN = "fixing";
+val arbitraryN = "arbitrary";
val takingN = "taking";
val ruleN = "rule";
@@ -503,10 +503,10 @@
error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
fun unless_more_args scan = Scan.unless (Scan.lift
- ((Args.$$$ fixingN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN ||
+ ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN ||
Args.$$$ InductAttrib.setN || Args.$$$ ruleN) -- Args.colon)) scan;
-val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
+val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
Args.and_list1 (Scan.repeat (unless_more_args free))) [];
val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
@@ -524,10 +524,10 @@
fun induct_meth src =
Method.syntax (Args.mode openN --
(Args.and_list (Scan.repeat (unless_more_args def_inst)) --
- (fixing -- taking -- Scan.option induct_rule))) src
- #> (fn (ctxt, (is_open, (insts, ((fixing, taking), opt_rule)))) =>
+ (arbitrary -- taking -- Scan.option induct_rule))) src
+ #> (fn (ctxt, (is_open, (insts, ((arbitrary, taking), opt_rule)))) =>
Method.RAW_METHOD_CASES (fn facts =>
- Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts fixing taking opt_rule facts))));
+ Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts))));
fun coinduct_meth src =
Method.syntax (Args.mode openN --
--- a/src/ZF/Induct/Binary_Trees.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/ZF/Induct/Binary_Trees.thy Mon Sep 11 21:35:19 2006 +0200
@@ -19,7 +19,7 @@
declare bt.intros [simp]
lemma Br_neq_left: "l \<in> bt(A) ==> Br(x, l, r) \<noteq> l"
- by (induct fixing: x r set: bt) auto
+ by (induct arbitrary: x r set: bt) auto
lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
-- "Proving a freeness theorem."
@@ -83,7 +83,7 @@
lemma n_nodes_aux_eq:
"t \<in> bt(A) ==> k \<in> nat ==> n_nodes_aux(t)`k = n_nodes(t) #+ k"
- apply (induct fixing: k set: bt)
+ apply (induct arbitrary: k set: bt)
apply simp
apply (atomize, simp)
done
--- a/src/ZF/Induct/Primrec.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/ZF/Induct/Primrec.thy Mon Sep 11 21:35:19 2006 +0200
@@ -131,7 +131,7 @@
lemma lt_ack2: "i \<in> nat ==> j \<in> nat ==> j < ack(i,j)"
-- {* PROPERTY A 4 *}
- apply (induct i fixing: j set: nat)
+ apply (induct i arbitrary: j set: nat)
apply simp
apply (induct_tac j)
apply (erule_tac [2] succ_leI [THEN lt_trans1])
--- a/src/ZF/Induct/PropLog.thy Mon Sep 11 14:35:30 2006 +0200
+++ b/src/ZF/Induct/PropLog.thy Mon Sep 11 21:35:19 2006 +0200
@@ -327,7 +327,7 @@
lemma completeness:
"H \<in> Fin(propn) ==> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p"
- apply (induct fixing: p set: Fin)
+ apply (induct arbitrary: p set: Fin)
apply (safe intro!: completeness_0)
apply (rule weaken_left_cons [THEN thms_MP])
apply (blast intro!: logcon_Imp propn.intros)