# HG changeset patch # User wenzelm # Date 1158003319 -7200 # Node ID 503ac4c5ef9109bc9a11d78bcc75f2cf67fba3e6 # Parent 08d227db6c74af1d485ed4b07a5ef3c83d13d902 induct method: renamed 'fixing' to 'arbitrary'; diff -r 08d227db6c74 -r 503ac4c5ef91 NEWS --- 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 diff -r 08d227db6c74 -r 503ac4c5ef91 doc-src/IsarRef/generic.tex --- 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Bali/DefiniteAssignmentCorrect.thy --- 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 @@ \ ?NormalAssigned s1 A \ ?BreakAssigned s0 s1 A \ ?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\ dom (locals s) \t\ A" using Abrupt.prems by simp have "?NormalAssigned (Some xc,s) A" diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Hoare/Heap.thy --- 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: "\Path h b Ps (Ref a); a \ set Ps\ \ 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Hyperreal/Fact.thy --- 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/IMP/Denotation.thy --- 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) \ C(c) \ \c,s\ \\<^sub>c t" -apply (induct c fixing: s t) +apply (induct c arbitrary: s t) apply simp_all apply fast diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/IMP/Expr.thy --- 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/IMP/Hoare.thy --- 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) diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/IMP/Machines.thy --- 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 \ \sp,s\ -1\ \sp',t\ \ rpq = rev p @ q & sp = size p & sp' = size p' \ rev p' @ q' = rev p @ q \ \q,p,s\ -1\ \q',p',t\" -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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/IMP/Natural.thy --- 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 "\c,s\ \\<^sub>c t" and "\c,s\ \\<^sub>c u" shows "u = t" using prems -proof (induct fixing: u set: evalc) +proof (induct arbitrary: u set: evalc) fix s u assume "\\,s\ \\<^sub>c u" thus "u = s" by simp next @@ -261,7 +261,7 @@ assumes "\c,s\ \\<^sub>c t" and "\c,s\ \\<^sub>c u" shows "u = t" using prems -proof (induct fixing: u) +proof (induct arbitrary: u) -- "the simple @{text \} case for demonstration:" fix s u assume "\\,s\ \\<^sub>c u" thus "u = s" by simp diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/IMP/Transition.thy --- 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: "\c1; c2, s\ -n\\<^sub>1 \s''\ \ \i j s'. \c1, s\ -i\\<^sub>1 \s'\ \ \c2, s'\ -j\\<^sub>1 \s''\ \ 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: "\c0,s\ -n\\<^sub>1 \s''\ \ \c1,s''\ \\<^sub>1\<^sup>* \s'\ \ \c0; c1, s\ \\<^sub>1\<^sup>* \s'\" -proof (induct n fixing: c0 s s'') +proof (induct n arbitrary: c0 s s'') case 0 from `\c0,s\ -(0::nat)\\<^sub>1 \s''\` have False by simp @@ -372,7 +372,7 @@ then obtain n where "\c, s\ -n\\<^sub>1 \s'\" by (blast dest: rtrancl_imp_rel_pow) moreover have "\c, s\ -n\\<^sub>1 \s'\ \ \c,s\ \\<^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: "\m c s s'. m < n \ \c,s\ -m\\<^sub>1 \s'\ \ \c,s\ \\<^sub>c s'" fix c s s' @@ -511,7 +511,7 @@ lemma lemma2: "\c;d,s\ -n\\<^sub>1 \u\ \ \t m. \c,s\ \\<^sub>1\<^sup>* \t\ \ \d,t\ -m\\<^sub>1 \u\ \ m \ 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: "\c,s\ \\<^sub>1\<^sup>* \t\ \ \c,s\ \\<^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) \\<^sub>1 (c',s') \ c \ None \ \if c'=None then \ else the c',s'\ \\<^sub>c t \ \the c,s\ \\<^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: diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/IMP/VC.thy --- 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Induct/PropLog.thy --- 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Isar_examples/ExprCompiler.thy --- 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Isar_examples/Hoare.thy --- 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Isar_examples/Puzzle.thy --- 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 \ f n" - proof (induct k \ "f n" fixing: n rule: less_induct) + proof (induct k \ "f n" arbitrary: n rule: less_induct) case (less k n) then have hyp: "\m. f m < f n \ m \ f m" by (simp only:) show "n \ f n" diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Lambda/Eta.thy --- 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]: "\ free s i \ 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 \ free t i \ k < i \ 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 \ free t i \ 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; \ free s i |] ==> \ 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: "\ free s i \ 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 \ 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 \ 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: "(\ free s i) = (\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 \\<^sub>\ 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 \\<^sub>\ t" by (induct t) simp_all @@ -248,12 +248,12 @@ lemma par_eta_lift [simp]: assumes eta: "s \\<^sub>\ t" shows "lift s i \\<^sub>\ 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 \\<^sub>\ t" shows "u \\<^sub>\ u' \ s[u/i] \\<^sub>\ 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 \ 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 \ 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' \ eta_expand k (Abs t) \ 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 \\<^sub>\ t' \ eta_expand k t \\<^sub>\ 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 \\<^sub>\ u" shows "u = u1' \ u2' \ \u1 u2 k. t = eta_expand k (u1 \ u2) \ u1 \\<^sub>\ u1' \ u2 \\<^sub>\ u2'" using eta -proof (induct fixing: u1' u2') +proof (induct arbitrary: u1' u2') case (app s s' t t') have "s \ t = eta_expand 0 (s \ t)" by simp with app show ?case by blast @@ -359,7 +359,7 @@ theorem par_eta_elim_abs: assumes eta: "t \\<^sub>\ t'" shows "t' = Abs u' \ \u k. t = eta_expand k (Abs u) \ u \\<^sub>\ 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 \\<^sub>\ t \ t => u \ \t'. s => t' \ t' \\<^sub>\ u" -proof (induct t fixing: s u taking: "size :: dB \ nat" rule: measure_induct_rule) +proof (induct t arbitrary: s u taking: "size :: dB \ nat" rule: measure_induct_rule) case (less t) from `t => u` show ?case @@ -439,7 +439,7 @@ shows "t => u \ \t'. s => t' \ 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Lambda/Lambda.thy --- 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 \ 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 \ 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 \ 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 \ 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 \\<^sub>\ s ==> r[t/i] \\<^sub>\ 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 \\<^sub>\\<^sup>* s ==> r[t/i] \\<^sub>\\<^sup>* s[t/i]" apply (induct set: rtrancl) @@ -169,7 +169,7 @@ theorem lift_preserves_beta [simp]: "r \\<^sub>\ s ==> lift r i \\<^sub>\ lift s i" - by (induct fixing: i set: beta) auto + by (induct arbitrary: i set: beta) auto theorem lift_preserves_beta': "r \\<^sub>\\<^sup>* s ==> lift r i \\<^sub>\\<^sup>* lift s i" apply (induct set: rtrancl) @@ -179,7 +179,7 @@ done theorem subst_preserves_beta2 [simp]: "r \\<^sub>\ s ==> t[r/i] \\<^sub>\\<^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) diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Lambda/ListApplication.thy --- 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 \\ ss) = (Var m = s \ ss = [])" - by (induct ss fixing: s) auto + by (induct ss arbitrary: s) auto lemma Var_apps_eq_Var_apps_conv [iff]: "(Var m \\ rs = Var n \\ ss) = (m = n \ 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 \\ rs = Abs s \\ ss) = (r = s \ 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 \ t \ Var n \\ 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 \\ ts \ Abs r \\ 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 \\ ts) i = lift t i \\ map (\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 \\ ts) u i = subst t u i \\ map (\t. subst t u i) ts" - by (induct ts fixing: t) simp_all + by (induct ts arbitrary: t) simp_all lemma app_last: "(t \\ ts) \ u = t \\ (ts @ [u])" by simp @@ -100,7 +100,7 @@ assumes "!!n ts. \t \ set ts. P t ==> P (Var n \\ ts)" and "!!u ts. [| P u; \t \ set ts. P t |] ==> P (Abs u \\ ts)" shows "size t = n \ 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) diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Lambda/ListBeta.thy --- 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 \\ rs -> v \ \ss. rs => ss \ v = Var n \\ ss" - apply (induct u == "Var n \\ rs" v fixing: rs set: beta) + apply (induct u == "Var n \\ rs" v arbitrary: rs set: beta) apply simp apply (rule_tac xs = rs in rev_exhaust) apply simp @@ -39,7 +39,7 @@ "(\r'. r -> r' \ s = r' \\ rs) \ (\rs'. rs => rs' \ s = r \\ rs') \ (\t u us. r = Abs t \ rs = u # us \ s = t[u/0] \\ us)" - apply (induct u == "r \\ rs" s fixing: r rs set: beta) + apply (induct u == "r \\ 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 \ r \\ rs -> r \\ 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) diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Lambda/ListOrder.thy --- 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 \ acc r ==> xs \ acc (step1 r) \ x # xs \ 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) diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Lambda/ParRed.thy --- 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' \ 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' \ t => t' \ 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 \ 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Lambda/StrongNorm.thy --- 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 \ IT \ lift t i \ 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 \ IT \ r[Var i/j] \ 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 diff -r 08d227db6c74 -r 503ac4c5ef91 src/HOL/Lambda/Type.thy --- 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 \ ts : Ts \ ts \ lists {t. \T. e \ 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 \ ts : Ts \ e \ t : T \ e \ 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 \ ts @ [t] : Ts @ [T] = (e \ ts : Ts \ e \ 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 \ t \\ ts : T \ \Ts. e \ t : Ts \ T \ e \ 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 \ t : Ts \ T \ e \ ts : Ts \ e \ t \\ 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 \ Var i \\ ts : T \ e \ Var i \\ ts : U \ 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 \ Var i : T") apply (ind_cases "e \ Var i : T") @@ -226,7 +226,7 @@ lemma var_app_types: "e \ Var i \\ ts \