induct method: renamed 'fixing' to 'arbitrary';
authorwenzelm
Mon Sep 11 21:35:19 2006 +0200 (2006-09-11)
changeset 20503503ac4c5ef91
parent 20502 08d227db6c74
child 20504 6342e872e71d
induct method: renamed 'fixing' to 'arbitrary';
NEWS
doc-src/IsarRef/generic.tex
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Hoare/Heap.thy
src/HOL/Hyperreal/Fact.thy
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Expr.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Machines.thy
src/HOL/IMP/Natural.thy
src/HOL/IMP/Transition.thy
src/HOL/IMP/VC.thy
src/HOL/Induct/PropLog.thy
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/Isar_examples/Hoare.thy
src/HOL/Isar_examples/Puzzle.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/ListOrder.thy
src/HOL/Lambda/ParRed.thy
src/HOL/Lambda/StrongNorm.thy
src/HOL/Lambda/Type.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/AssocList.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/List.thy
src/HOL/Nominal/Examples/CR.thy
src/HOL/Nominal/Examples/Fsub.thy
src/HOL/Nominal/Examples/Iteration.thy
src/HOL/Nominal/Examples/Weakening.thy
src/HOL/Relation_Power.thy
src/HOL/Unix/Unix.thy
src/HOL/W0/W0.thy
src/HOL/ex/CodeRandom.thy
src/HOL/ex/ReflectionEx.thy
src/HOL/ex/ThreeDivides.thy
src/Provers/induct_method.ML
src/ZF/Induct/Binary_Trees.thy
src/ZF/Induct/Primrec.thy
src/ZF/Induct/PropLog.thy
     1.1 --- a/NEWS	Mon Sep 11 14:35:30 2006 +0200
     1.2 +++ b/NEWS	Mon Sep 11 21:35:19 2006 +0200
     1.3 @@ -301,7 +301,7 @@
     1.4      assumes a: "A n x"
     1.5      shows "P n x"
     1.6      using a                     -- {* make induct insert fact a *}
     1.7 -  proof (induct n fixing: x)    -- {* generalize goal to "!!x. A n x ==> P n x" *}
     1.8 +  proof (induct n arbitrary: x) -- {* generalize goal to "!!x. A n x ==> P n x" *}
     1.9      case 0
    1.10      show ?case sorry
    1.11    next
    1.12 @@ -321,7 +321,7 @@
    1.13      assumes a: "A (a x)"
    1.14      shows "P (a x)"
    1.15      using a
    1.16 -  proof (induct n == "a x" fixing: x)
    1.17 +  proof (induct n == "a x" arbitrary: x)
    1.18      ...
    1.19  
    1.20  See also HOL/Isar_examples/Puzzle.thy for an application of the this
    1.21 @@ -334,7 +334,7 @@
    1.22    lemma
    1.23      fixes n :: nat
    1.24      obtains x :: 'a where "P n x" and "Q n x"
    1.25 -  proof (induct n fixing: thesis)
    1.26 +  proof (induct n arbitrary: thesis)
    1.27      case 0
    1.28      obtain x where "P 0 x" and "Q 0 x" sorry
    1.29      then show thesis by (rule 0)
    1.30 @@ -345,8 +345,8 @@
    1.31      then show thesis by (rule Suc.prems)
    1.32    qed
    1.33  
    1.34 -Here the 'fixing: thesis' specification essentially modifies the scope
    1.35 -of the formal thesis parameter, in order to the get the whole
    1.36 +Here the 'arbitrary: thesis' specification essentially modifies the
    1.37 +scope of the formal thesis parameter, in order to the get the whole
    1.38  existence statement through the induction as expected.
    1.39  
    1.40  * Provers/induct: mutual induction rules are now specified as a list
     2.1 --- a/doc-src/IsarRef/generic.tex	Mon Sep 11 14:35:30 2006 +0200
     2.2 +++ b/doc-src/IsarRef/generic.tex	Mon Sep 11 21:35:19 2006 +0200
     2.3 @@ -1516,7 +1516,7 @@
     2.4  \begin{rail}
     2.5    'cases' open? (insts * 'and') rule?
     2.6    ;
     2.7 -  'induct' open? (definsts * 'and') \\ fixing? taking? rule?
     2.8 +  'induct' open? (definsts * 'and') \\ arbitrary? taking? rule?
     2.9    ;
    2.10    'coinduct' open? insts taking rule?
    2.11    ;
    2.12 @@ -1529,7 +1529,7 @@
    2.13    ;
    2.14    definsts: ( definst *)
    2.15    ;
    2.16 -  fixing: 'fixing' ':' ((term *) 'and' +)
    2.17 +  arbitrary: 'arbitrary' ':' ((term *) 'and' +)
    2.18    ;
    2.19    taking: 'taking' ':' insts
    2.20    ;
    2.21 @@ -1587,11 +1587,11 @@
    2.22    In order to achieve practically useful induction hypotheses, some variables
    2.23    occurring in $t$ need to be fixed (see below).
    2.24    
    2.25 -  The optional ``$fixing\colon \vec x$'' specification generalizes variables
    2.26 -  $\vec x$ of the original goal before applying induction.  Thus induction
    2.27 -  hypotheses may become sufficiently general to get the proof through.
    2.28 -  Together with definitional instantiations, one may effectively perform
    2.29 -  induction over expressions of a certain structure.
    2.30 +  The optional ``$arbitrary\colon \vec x$'' specification generalizes
    2.31 +  variables $\vec x$ of the original goal before applying induction.  Thus
    2.32 +  induction hypotheses may become sufficiently general to get the proof
    2.33 +  through.  Together with definitional instantiations, one may effectively
    2.34 +  perform induction over expressions of a certain structure.
    2.35    
    2.36    The optional ``$taking\colon \vec t$'' specification provides additional
    2.37    instantiations of a prefix of pending variables in the rule.  Such schematic
     3.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Mon Sep 11 14:35:30 2006 +0200
     3.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Mon Sep 11 21:35:19 2006 +0200
     3.3 @@ -2661,7 +2661,7 @@
     3.4          \<Longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1)"
     3.5    from eval and wt da G
     3.6    show ?thesis
     3.7 -  proof (induct fixing: Env T A)
     3.8 +  proof (induct arbitrary: Env T A)
     3.9      case (Abrupt s t xc Env T A)
    3.10      have da: "Env\<turnstile> dom (locals s) \<guillemotright>t\<guillemotright> A" using Abrupt.prems by simp 
    3.11      have "?NormalAssigned (Some xc,s) A" 
     4.1 --- a/src/HOL/Hoare/Heap.thy	Mon Sep 11 14:35:30 2006 +0200
     4.2 +++ b/src/HOL/Hoare/Heap.thy	Mon Sep 11 21:35:19 2006 +0200
     4.3 @@ -131,7 +131,7 @@
     4.4  
     4.5  lemma Path_is_List:
     4.6    "\<lbrakk>Path h b Ps (Ref a); a \<notin> set Ps\<rbrakk> \<Longrightarrow> List (h(a := Null)) b (Ps @ [a])"
     4.7 -apply (induct Ps fixing: b)
     4.8 +apply (induct Ps arbitrary: b)
     4.9  apply (auto simp add:fun_upd_apply)
    4.10  done
    4.11  
     5.1 --- a/src/HOL/Hyperreal/Fact.thy	Mon Sep 11 14:35:30 2006 +0200
     5.2 +++ b/src/HOL/Hyperreal/Fact.thy	Mon Sep 11 21:35:19 2006 +0200
     5.3 @@ -54,7 +54,7 @@
     5.4  
     5.5  lemma fact_diff_Suc [rule_format]:
     5.6      "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
     5.7 -  apply (induct n fixing: m)
     5.8 +  apply (induct n arbitrary: m)
     5.9    apply auto
    5.10    apply (drule_tac x = "m - 1" in meta_spec, auto)
    5.11    done
     6.1 --- a/src/HOL/IMP/Denotation.thy	Mon Sep 11 14:35:30 2006 +0200
     6.2 +++ b/src/HOL/IMP/Denotation.thy	Mon Sep 11 21:35:19 2006 +0200
     6.3 @@ -55,7 +55,7 @@
     6.4  (* Denotational Semantics implies Operational Semantics *)
     6.5  
     6.6  lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
     6.7 -apply (induct c fixing: s t)
     6.8 +apply (induct c arbitrary: s t)
     6.9  
    6.10  apply simp_all
    6.11  apply fast
     7.1 --- a/src/HOL/IMP/Expr.thy	Mon Sep 11 14:35:30 2006 +0200
     7.2 +++ b/src/HOL/IMP/Expr.thy	Mon Sep 11 21:35:19 2006 +0200
     7.3 @@ -135,10 +135,10 @@
     7.4  
     7.5  
     7.6  lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
     7.7 -  by (induct a fixing: n) auto
     7.8 +  by (induct a arbitrary: n) auto
     7.9  
    7.10  lemma bexp_iff:
    7.11    "((b,s) -b-> w) = (B b s = w)"
    7.12 -  by (induct b fixing: w) (auto simp add: aexp_iff)
    7.13 +  by (induct b arbitrary: w) (auto simp add: aexp_iff)
    7.14  
    7.15  end
     8.1 --- a/src/HOL/IMP/Hoare.thy	Mon Sep 11 14:35:30 2006 +0200
     8.2 +++ b/src/HOL/IMP/Hoare.thy	Mon Sep 11 21:35:19 2006 +0200
     8.3 @@ -133,7 +133,7 @@
     8.4  lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
     8.5  
     8.6  lemma wp_is_pre: "|- {wp c Q} c {Q}"
     8.7 -apply (induct c fixing: Q)
     8.8 +apply (induct c arbitrary: Q)
     8.9      apply (simp_all (no_asm))
    8.10      apply fast+
    8.11   apply (blast intro: hoare_conseq1)
     9.1 --- a/src/HOL/IMP/Machines.thy	Mon Sep 11 14:35:30 2006 +0200
     9.2 +++ b/src/HOL/IMP/Machines.thy	Mon Sep 11 21:35:19 2006 +0200
     9.3 @@ -192,7 +192,7 @@
     9.4   "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
     9.5    rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
     9.6            rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
     9.7 -apply(induct fixing: p q p' q' set: exec01)
     9.8 +apply(induct arbitrary: p q p' q' set: exec01)
     9.9     apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
    9.10     apply(drule sym)
    9.11     apply simp
    10.1 --- a/src/HOL/IMP/Natural.thy	Mon Sep 11 14:35:30 2006 +0200
    10.2 +++ b/src/HOL/IMP/Natural.thy	Mon Sep 11 21:35:19 2006 +0200
    10.3 @@ -200,7 +200,7 @@
    10.4    assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
    10.5    shows "u = t"
    10.6    using prems
    10.7 -proof (induct fixing: u set: evalc)
    10.8 +proof (induct arbitrary: u set: evalc)
    10.9    fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   10.10    thus "u = s" by simp
   10.11  next
   10.12 @@ -261,7 +261,7 @@
   10.13    assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
   10.14    shows "u = t"
   10.15    using prems
   10.16 -proof (induct fixing: u)
   10.17 +proof (induct arbitrary: u)
   10.18    -- "the simple @{text \<SKIP>} case for demonstration:"
   10.19    fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
   10.20    thus "u = s" by simp
    11.1 --- a/src/HOL/IMP/Transition.thy	Mon Sep 11 14:35:30 2006 +0200
    11.2 +++ b/src/HOL/IMP/Transition.thy	Mon Sep 11 21:35:19 2006 +0200
    11.3 @@ -223,7 +223,7 @@
    11.4  lemma semiD:
    11.5    "\<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow>
    11.6    \<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"
    11.7 -proof (induct n fixing: c1 c2 s s'')
    11.8 +proof (induct n arbitrary: c1 c2 s s'')
    11.9    case 0
   11.10    then show ?case by simp
   11.11  next
   11.12 @@ -269,7 +269,7 @@
   11.13  
   11.14  lemma semiI:
   11.15    "\<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>"
   11.16 -proof (induct n fixing: c0 s s'')
   11.17 +proof (induct n arbitrary: c0 s s'')
   11.18    case 0
   11.19    from `\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
   11.20    have False by simp
   11.21 @@ -372,7 +372,7 @@
   11.22    then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
   11.23    moreover
   11.24    have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
   11.25 -  proof (induct fixing: c s s' rule: less_induct)
   11.26 +  proof (induct arbitrary: c s s' rule: less_induct)
   11.27      fix n
   11.28      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'"
   11.29      fix c s s'
   11.30 @@ -511,7 +511,7 @@
   11.31  
   11.32  lemma lemma2:
   11.33    "\<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"
   11.34 -apply (induct n fixing: c d s u)
   11.35 +apply (induct n arbitrary: c d s u)
   11.36   -- "case n = 0"
   11.37   apply fastsimp
   11.38  -- "induction step"
   11.39 @@ -521,7 +521,7 @@
   11.40  
   11.41  lemma evalc1_impl_evalc:
   11.42    "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   11.43 -apply (induct c fixing: s t)
   11.44 +apply (induct c arbitrary: s t)
   11.45  apply (safe dest!: rtrancl_imp_UN_rel_pow)
   11.46  
   11.47  -- SKIP
   11.48 @@ -666,7 +666,7 @@
   11.49  lemma FB_lemma3:
   11.50    "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
   11.51    \<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"
   11.52 -  by (induct fixing: t set: evalc1)
   11.53 +  by (induct arbitrary: t set: evalc1)
   11.54      (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
   11.55  
   11.56  lemma FB_lemma2:
    12.1 --- a/src/HOL/IMP/VC.thy	Mon Sep 11 14:35:30 2006 +0200
    12.2 +++ b/src/HOL/IMP/VC.thy	Mon Sep 11 21:35:19 2006 +0200
    12.3 @@ -70,7 +70,7 @@
    12.4  lemma l: "!s. P s --> P s" by fast
    12.5  
    12.6  lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
    12.7 -apply (induct c fixing: Q)
    12.8 +apply (induct c arbitrary: Q)
    12.9      apply (simp_all (no_asm))
   12.10      apply fast
   12.11     apply fast
   12.12 @@ -151,6 +151,6 @@
   12.13  qed
   12.14  
   12.15  lemma vcawp_vc_awp: "vcawp c Q = (vc c Q, awp c Q)"
   12.16 -  by (induct c fixing: Q) (simp_all add: Let_def)
   12.17 +  by (induct c arbitrary: Q) (simp_all add: Let_def)
   12.18  
   12.19  end
    13.1 --- a/src/HOL/Induct/PropLog.thy	Mon Sep 11 14:35:30 2006 +0200
    13.2 +++ b/src/HOL/Induct/PropLog.thy	Mon Sep 11 21:35:19 2006 +0200
    13.3 @@ -259,7 +259,7 @@
    13.4  by (unfold sat_def, auto)
    13.5  
    13.6  theorem completeness: "finite H ==> H |= p ==> H |- p"
    13.7 -apply (induct fixing: p rule: finite_induct)
    13.8 +apply (induct arbitrary: p rule: finite_induct)
    13.9   apply (blast intro: completeness_0)
   13.10  apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
   13.11  done
    14.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Mon Sep 11 14:35:30 2006 +0200
    14.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Mon Sep 11 21:35:19 2006 +0200
    14.3 @@ -114,7 +114,7 @@
    14.4  lemma exec_append:
    14.5    "exec (xs @ ys) stack env =
    14.6      exec ys (exec xs stack env) env"
    14.7 -proof (induct xs fixing: stack)
    14.8 +proof (induct xs arbitrary: stack)
    14.9    case Nil
   14.10    show ?case by simp
   14.11  next
   14.12 @@ -153,7 +153,7 @@
   14.13  
   14.14  lemma exec_append':
   14.15    "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
   14.16 -proof (induct xs fixing: stack)
   14.17 +proof (induct xs arbitrary: stack)
   14.18    case (Nil s)
   14.19    have "exec ([] @ ys) s env = exec ys s env" by simp
   14.20    also have "... = exec ys (exec [] s env) env" by simp
    15.1 --- a/src/HOL/Isar_examples/Hoare.thy	Mon Sep 11 14:35:30 2006 +0200
    15.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Mon Sep 11 21:35:19 2006 +0200
    15.3 @@ -167,7 +167,7 @@
    15.4    assume "Sem (While b X c) s s'"
    15.5    then obtain n where "iter n b (Sem c) s s'" by auto
    15.6    from this and s show "s' : P Int -b"
    15.7 -  proof (induct n fixing: s)
    15.8 +  proof (induct n arbitrary: s)
    15.9      case 0
   15.10      thus ?case by auto
   15.11    next
    16.1 --- a/src/HOL/Isar_examples/Puzzle.thy	Mon Sep 11 14:35:30 2006 +0200
    16.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Mon Sep 11 21:35:19 2006 +0200
    16.3 @@ -21,7 +21,7 @@
    16.4  proof (rule order_antisym)
    16.5    {
    16.6      fix n show "n \<le> f n"
    16.7 -    proof (induct k \<equiv> "f n" fixing: n rule: less_induct)
    16.8 +    proof (induct k \<equiv> "f n" arbitrary: n rule: less_induct)
    16.9        case (less k n)
   16.10        then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
   16.11        show "n \<le> f n"
    17.1 --- a/src/HOL/Lambda/Eta.thy	Mon Sep 11 14:35:30 2006 +0200
    17.2 +++ b/src/HOL/Lambda/Eta.thy	Mon Sep 11 21:35:19 2006 +0200
    17.3 @@ -45,18 +45,18 @@
    17.4  subsection "Properties of eta, subst and free"
    17.5  
    17.6  lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]"
    17.7 -  by (induct s fixing: i t u) (simp_all add: subst_Var)
    17.8 +  by (induct s arbitrary: i t u) (simp_all add: subst_Var)
    17.9  
   17.10  lemma free_lift [simp]:
   17.11      "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
   17.12 -  apply (induct t fixing: i k)
   17.13 +  apply (induct t arbitrary: i k)
   17.14    apply (auto cong: conj_cong)
   17.15    done
   17.16  
   17.17  lemma free_subst [simp]:
   17.18      "free (s[t/k]) i =
   17.19        (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
   17.20 -  apply (induct s fixing: i k t)
   17.21 +  apply (induct s arbitrary: i k t)
   17.22      prefer 2
   17.23      apply simp
   17.24      apply blast
   17.25 @@ -66,7 +66,7 @@
   17.26    done
   17.27  
   17.28  lemma free_eta: "s -e> t ==> free t i = free s i"
   17.29 -  by (induct fixing: i set: eta) (simp_all cong: conj_cong)
   17.30 +  by (induct arbitrary: i set: eta) (simp_all cong: conj_cong)
   17.31  
   17.32  lemma not_free_eta:
   17.33      "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
   17.34 @@ -74,10 +74,10 @@
   17.35  
   17.36  lemma eta_subst [simp]:
   17.37      "s -e> t ==> s[u/i] -e> t[u/i]"
   17.38 -  by (induct fixing: u i set: eta) (simp_all add: subst_subst [symmetric])
   17.39 +  by (induct arbitrary: u i set: eta) (simp_all add: subst_subst [symmetric])
   17.40  
   17.41  theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
   17.42 -  by (induct s fixing: i dummy) simp_all
   17.43 +  by (induct s arbitrary: i dummy) simp_all
   17.44  
   17.45  
   17.46  subsection "Confluence of eta"
   17.47 @@ -121,19 +121,19 @@
   17.48  
   17.49  lemma free_beta:
   17.50      "s -> t ==> free t i \<Longrightarrow> free s i"
   17.51 -  by (induct fixing: i set: beta) auto
   17.52 +  by (induct arbitrary: i set: beta) auto
   17.53  
   17.54  lemma beta_subst [intro]: "s -> t ==> s[u/i] -> t[u/i]"
   17.55 -  by (induct fixing: u i set: beta) (simp_all add: subst_subst [symmetric])
   17.56 +  by (induct arbitrary: u i set: beta) (simp_all add: subst_subst [symmetric])
   17.57  
   17.58  lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
   17.59 -  by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var)
   17.60 +  by (induct t arbitrary: i) (auto elim!: linorder_neqE simp: subst_Var)
   17.61  
   17.62  lemma eta_lift [simp]: "s -e> t ==> lift s i -e> lift t i"
   17.63 -  by (induct fixing: i set: eta) simp_all
   17.64 +  by (induct arbitrary: i set: eta) simp_all
   17.65  
   17.66  lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]"
   17.67 -  apply (induct u fixing: s t i)
   17.68 +  apply (induct u arbitrary: s t i)
   17.69      apply (simp_all add: subst_Var)
   17.70      apply blast
   17.71     apply (blast intro: rtrancl_eta_App)
   17.72 @@ -165,7 +165,7 @@
   17.73  
   17.74  lemma not_free_iff_lifted:
   17.75      "(\<not> free s i) = (\<exists>t. s = lift t i)"
   17.76 -  apply (induct s fixing: i)
   17.77 +  apply (induct s arbitrary: i)
   17.78      apply simp
   17.79      apply (rule iffI)
   17.80       apply (erule linorder_neqE)
   17.81 @@ -240,7 +240,7 @@
   17.82  lemma free_par_eta [simp]:
   17.83    assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
   17.84    shows "free t i = free s i" using eta
   17.85 -  by (induct fixing: i) (simp_all cong: conj_cong)
   17.86 +  by (induct arbitrary: i) (simp_all cong: conj_cong)
   17.87  
   17.88  lemma par_eta_refl [simp]: "t \<Rightarrow>\<^sub>\<eta> t"
   17.89    by (induct t) simp_all
   17.90 @@ -248,12 +248,12 @@
   17.91  lemma par_eta_lift [simp]:
   17.92    assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
   17.93    shows "lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta
   17.94 -  by (induct fixing: i) simp_all
   17.95 +  by (induct arbitrary: i) simp_all
   17.96  
   17.97  lemma par_eta_subst [simp]:
   17.98    assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
   17.99    shows "u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta
  17.100 -  by (induct fixing: u u' i) (simp_all add: subst_subst [symmetric] subst_Var)
  17.101 +  by (induct arbitrary: u u' i) (simp_all add: subst_subst [symmetric] subst_Var)
  17.102  
  17.103  theorem eta_subset_par_eta: "eta \<subseteq> par_eta"
  17.104    apply (rule subsetI)
  17.105 @@ -289,7 +289,7 @@
  17.106  
  17.107  lemma eta_expand_Suc':
  17.108    "eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))"
  17.109 -  by (induct n fixing: t) simp_all
  17.110 +  by (induct n arbitrary: t) simp_all
  17.111  
  17.112  theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)"
  17.113    by (induct k) (simp_all add: lift_lift)
  17.114 @@ -297,7 +297,7 @@
  17.115  theorem eta_expand_beta:
  17.116    assumes u: "u => u'"
  17.117    shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
  17.118 -proof (induct k fixing: t t')
  17.119 +proof (induct k arbitrary: t t')
  17.120    case 0
  17.121    with u show ?case by simp
  17.122  next
  17.123 @@ -313,7 +313,7 @@
  17.124    by (induct k) (simp_all add: t)
  17.125  
  17.126  theorem eta_expand_eta: "t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'"
  17.127 -proof (induct k fixing: t t')
  17.128 +proof (induct k arbitrary: t t')
  17.129    case 0
  17.130    show ?case by simp
  17.131  next
  17.132 @@ -329,7 +329,7 @@
  17.133  theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u"
  17.134    shows "u = u1' \<degree> u2' \<Longrightarrow>
  17.135      \<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
  17.136 -proof (induct fixing: u1' u2')
  17.137 +proof (induct arbitrary: u1' u2')
  17.138    case (app s s' t t')
  17.139    have "s \<degree> t = eta_expand 0 (s \<degree> t)" by simp
  17.140    with app show ?case by blast
  17.141 @@ -359,7 +359,7 @@
  17.142  theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'"
  17.143    shows "t' = Abs u' \<Longrightarrow>
  17.144      \<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta
  17.145 -proof (induct fixing: u')
  17.146 +proof (induct arbitrary: u')
  17.147    case (abs s t)
  17.148    have "Abs s = eta_expand 0 (Abs s)" by simp
  17.149    with abs show ?case by blast
  17.150 @@ -390,7 +390,7 @@
  17.151  *}
  17.152  
  17.153  theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
  17.154 -proof (induct t fixing: s u taking: "size :: dB \<Rightarrow> nat" rule: measure_induct_rule)
  17.155 +proof (induct t arbitrary: s u taking: "size :: dB \<Rightarrow> nat" rule: measure_induct_rule)
  17.156    case (less t)
  17.157    from `t => u`
  17.158    show ?case
  17.159 @@ -439,7 +439,7 @@
  17.160    shows "t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u"
  17.161    using eta [simplified rtrancl_subset
  17.162      [OF eta_subset_par_eta par_eta_subset_eta, symmetric]]
  17.163 -proof (induct fixing: u)
  17.164 +proof (induct arbitrary: u)
  17.165    case 1
  17.166    thus ?case by blast
  17.167  next
    18.1 --- a/src/HOL/Lambda/Lambda.thy	Mon Sep 11 14:35:30 2006 +0200
    18.2 +++ b/src/HOL/Lambda/Lambda.thy	Mon Sep 11 21:35:19 2006 +0200
    18.3 @@ -114,24 +114,24 @@
    18.4  
    18.5  lemma lift_lift:
    18.6      "i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
    18.7 -  by (induct t fixing: i k) auto
    18.8 +  by (induct t arbitrary: i k) auto
    18.9  
   18.10  lemma lift_subst [simp]:
   18.11      "j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
   18.12 -  by (induct t fixing: i j s)
   18.13 +  by (induct t arbitrary: i j s)
   18.14      (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
   18.15  
   18.16  lemma lift_subst_lt:
   18.17      "i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
   18.18 -  by (induct t fixing: i j s) (simp_all add: subst_Var lift_lift)
   18.19 +  by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift)
   18.20  
   18.21  lemma subst_lift [simp]:
   18.22      "(lift t k)[s/k] = t"
   18.23 -  by (induct t fixing: k s) simp_all
   18.24 +  by (induct t arbitrary: k s) simp_all
   18.25  
   18.26  lemma subst_subst:
   18.27      "i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
   18.28 -  by (induct t fixing: i j u v)
   18.29 +  by (induct t arbitrary: i j u v)
   18.30      (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
   18.31        split: nat.split)
   18.32  
   18.33 @@ -139,13 +139,13 @@
   18.34  subsection {* Equivalence proof for optimized substitution *}
   18.35  
   18.36  lemma liftn_0 [simp]: "liftn 0 t k = t"
   18.37 -  by (induct t fixing: k) (simp_all add: subst_Var)
   18.38 +  by (induct t arbitrary: k) (simp_all add: subst_Var)
   18.39  
   18.40  lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
   18.41 -  by (induct t fixing: k) (simp_all add: subst_Var)
   18.42 +  by (induct t arbitrary: k) (simp_all add: subst_Var)
   18.43  
   18.44  lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
   18.45 -  by (induct t fixing: n) (simp_all add: subst_Var)
   18.46 +  by (induct t arbitrary: n) (simp_all add: subst_Var)
   18.47  
   18.48  theorem substn_subst_0: "substn t s 0 = t[s/0]"
   18.49    by simp
   18.50 @@ -158,7 +158,7 @@
   18.51  
   18.52  theorem subst_preserves_beta [simp]:
   18.53      "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
   18.54 -  by (induct fixing: t i set: beta) (simp_all add: subst_subst [symmetric])
   18.55 +  by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
   18.56  
   18.57  theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
   18.58    apply (induct set: rtrancl)
   18.59 @@ -169,7 +169,7 @@
   18.60  
   18.61  theorem lift_preserves_beta [simp]:
   18.62      "r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
   18.63 -  by (induct fixing: i set: beta) auto
   18.64 +  by (induct arbitrary: i set: beta) auto
   18.65  
   18.66  theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
   18.67    apply (induct set: rtrancl)
   18.68 @@ -179,7 +179,7 @@
   18.69    done
   18.70  
   18.71  theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   18.72 -  apply (induct t fixing: r s i)
   18.73 +  apply (induct t arbitrary: r s i)
   18.74      apply (simp add: subst_Var r_into_rtrancl)
   18.75     apply (simp add: rtrancl_beta_App)
   18.76    apply (simp add: rtrancl_beta_Abs)
    19.1 --- a/src/HOL/Lambda/ListApplication.thy	Mon Sep 11 14:35:30 2006 +0200
    19.2 +++ b/src/HOL/Lambda/ListApplication.thy	Mon Sep 11 21:35:19 2006 +0200
    19.3 @@ -16,11 +16,11 @@
    19.4    by (induct ts rule: rev_induct) auto
    19.5  
    19.6  lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
    19.7 -  by (induct ss fixing: s) auto
    19.8 +  by (induct ss arbitrary: s) auto
    19.9  
   19.10  lemma Var_apps_eq_Var_apps_conv [iff]:
   19.11      "(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
   19.12 -  apply (induct rs fixing: ss rule: rev_induct)
   19.13 +  apply (induct rs arbitrary: ss rule: rev_induct)
   19.14     apply simp
   19.15     apply blast
   19.16    apply (induct_tac ss rule: rev_induct)
   19.17 @@ -44,7 +44,7 @@
   19.18  
   19.19  lemma Abs_apps_eq_Abs_apps_conv [iff]:
   19.20      "(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
   19.21 -  apply (induct rs fixing: ss rule: rev_induct)
   19.22 +  apply (induct rs arbitrary: ss rule: rev_induct)
   19.23     apply simp
   19.24     apply blast
   19.25    apply (induct_tac ss rule: rev_induct)
   19.26 @@ -53,11 +53,11 @@
   19.27  
   19.28  lemma Abs_App_neq_Var_apps [iff]:
   19.29      "Abs s \<degree> t \<noteq> Var n \<degree>\<degree> ss"
   19.30 -  by (induct ss fixing: s t rule: rev_induct) auto
   19.31 +  by (induct ss arbitrary: s t rule: rev_induct) auto
   19.32  
   19.33  lemma Var_apps_neq_Abs_apps [iff]:
   19.34      "Var n \<degree>\<degree> ts \<noteq> Abs r \<degree>\<degree> ss"
   19.35 -  apply (induct ss fixing: ts rule: rev_induct)
   19.36 +  apply (induct ss arbitrary: ts rule: rev_induct)
   19.37     apply simp
   19.38    apply (induct_tac ts rule: rev_induct)
   19.39     apply auto
   19.40 @@ -84,11 +84,11 @@
   19.41  
   19.42  lemma lift_map [simp]:
   19.43      "lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
   19.44 -  by (induct ts fixing: t) simp_all
   19.45 +  by (induct ts arbitrary: t) simp_all
   19.46  
   19.47  lemma subst_map [simp]:
   19.48      "subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
   19.49 -  by (induct ts fixing: t) simp_all
   19.50 +  by (induct ts arbitrary: t) simp_all
   19.51  
   19.52  lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
   19.53    by simp
   19.54 @@ -100,7 +100,7 @@
   19.55    assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
   19.56      and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
   19.57    shows "size t = n \<Longrightarrow> P t"
   19.58 -  apply (induct n fixing: t rule: nat_less_induct)
   19.59 +  apply (induct n arbitrary: t rule: nat_less_induct)
   19.60    apply (cut_tac t = t in ex_head_tail)
   19.61    apply clarify
   19.62    apply (erule disjE)
    20.1 --- a/src/HOL/Lambda/ListBeta.thy	Mon Sep 11 14:35:30 2006 +0200
    20.2 +++ b/src/HOL/Lambda/ListBeta.thy	Mon Sep 11 21:35:19 2006 +0200
    20.3 @@ -18,7 +18,7 @@
    20.4  
    20.5  lemma head_Var_reduction:
    20.6    "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
    20.7 -  apply (induct u == "Var n \<degree>\<degree> rs" v fixing: rs set: beta)
    20.8 +  apply (induct u == "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
    20.9       apply simp
   20.10      apply (rule_tac xs = rs in rev_exhaust)
   20.11       apply simp
   20.12 @@ -39,7 +39,7 @@
   20.13     "(\<exists>r'. r -> r' \<and> s = r' \<degree>\<degree> rs) \<or>
   20.14      (\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
   20.15      (\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
   20.16 -    apply (induct u == "r \<degree>\<degree> rs" s fixing: r rs set: beta)
   20.17 +    apply (induct u == "r \<degree>\<degree> rs" s arbitrary: r rs set: beta)
   20.18         apply (case_tac r)
   20.19           apply simp
   20.20          apply (simp add: App_eq_foldl_conv)
   20.21 @@ -78,7 +78,7 @@
   20.22  
   20.23  lemma apps_preserves_betas [simp]:
   20.24      "rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
   20.25 -  apply (induct rs fixing: ss rule: rev_induct)
   20.26 +  apply (induct rs arbitrary: ss rule: rev_induct)
   20.27     apply simp
   20.28    apply simp
   20.29    apply (rule_tac xs = ss in rev_exhaust)
    21.1 --- a/src/HOL/Lambda/ListOrder.thy	Mon Sep 11 14:35:30 2006 +0200
    21.2 +++ b/src/HOL/Lambda/ListOrder.thy	Mon Sep 11 21:35:19 2006 +0200
    21.3 @@ -90,7 +90,7 @@
    21.4  
    21.5  lemma Cons_acc_step1I [intro!]:
    21.6      "x \<in> acc r ==> xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r)"
    21.7 -  apply (induct fixing: xs set: acc)
    21.8 +  apply (induct arbitrary: xs set: acc)
    21.9    apply (erule thin_rl)
   21.10    apply (erule acc_induct)
   21.11    apply (rule accI)
    22.1 --- a/src/HOL/Lambda/ParRed.thy	Mon Sep 11 14:35:30 2006 +0200
    22.2 +++ b/src/HOL/Lambda/ParRed.thy	Mon Sep 11 21:35:19 2006 +0200
    22.3 @@ -68,11 +68,11 @@
    22.4  
    22.5  lemma par_beta_lift [simp]:
    22.6      "t => t' \<Longrightarrow> lift t n => lift t' n"
    22.7 -  by (induct t fixing: t' n) fastsimp+
    22.8 +  by (induct t arbitrary: t' n) fastsimp+
    22.9  
   22.10  lemma par_beta_subst:
   22.11      "s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]"
   22.12 -  apply (induct t fixing: s s' t' n)
   22.13 +  apply (induct t arbitrary: s s' t' n)
   22.14      apply (simp add: subst_Var)
   22.15     apply (erule par_beta_cases)
   22.16      apply simp
   22.17 @@ -104,7 +104,7 @@
   22.18    "cd (Abs s) = Abs (cd s)"
   22.19  
   22.20  lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
   22.21 -  apply (induct s fixing: t rule: cd.induct)
   22.22 +  apply (induct s arbitrary: t rule: cd.induct)
   22.23        apply auto
   22.24    apply (fast intro!: par_beta_subst)
   22.25    done
    23.1 --- a/src/HOL/Lambda/StrongNorm.thy	Mon Sep 11 14:35:30 2006 +0200
    23.2 +++ b/src/HOL/Lambda/StrongNorm.thy	Mon Sep 11 21:35:19 2006 +0200
    23.3 @@ -17,7 +17,7 @@
    23.4  subsection {* Properties of @{text IT} *}
    23.5  
    23.6  lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> lift t i \<in> IT"
    23.7 -  apply (induct fixing: i set: IT)
    23.8 +  apply (induct arbitrary: i set: IT)
    23.9      apply (simp (no_asm))
   23.10      apply (rule conjI)
   23.11       apply
   23.12 @@ -38,7 +38,7 @@
   23.13    by (induct ts) auto
   23.14  
   23.15  lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> r[Var i/j] \<in> IT"
   23.16 -  apply (induct fixing: i j set: IT)
   23.17 +  apply (induct arbitrary: i j set: IT)
   23.18      txt {* Case @{term Var}: *}
   23.19      apply (simp (no_asm) add: subst_Var)
   23.20      apply
    24.1 --- a/src/HOL/Lambda/Type.thy	Mon Sep 11 14:35:30 2006 +0200
    24.2 +++ b/src/HOL/Lambda/Type.thy	Mon Sep 11 21:35:19 2006 +0200
    24.3 @@ -99,7 +99,7 @@
    24.4  
    24.5  lemma lists_typings:
    24.6      "e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
    24.7 -  apply (induct ts fixing: Ts)
    24.8 +  apply (induct ts arbitrary: Ts)
    24.9     apply (case_tac Ts)
   24.10       apply simp
   24.11       apply (rule lists.Nil)
   24.12 @@ -113,7 +113,7 @@
   24.13    done
   24.14  
   24.15  lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
   24.16 -  apply (induct ts fixing: Ts)
   24.17 +  apply (induct ts arbitrary: Ts)
   24.18    apply simp
   24.19    apply (case_tac Ts)
   24.20    apply simp+
   24.21 @@ -121,7 +121,7 @@
   24.22  
   24.23  lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] =
   24.24    (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)"
   24.25 -  apply (induct ts fixing: Ts)
   24.26 +  apply (induct ts arbitrary: Ts)
   24.27    apply (case_tac Ts)
   24.28    apply simp+
   24.29    apply (case_tac Ts)
   24.30 @@ -161,7 +161,7 @@
   24.31  
   24.32  lemma list_app_typeD:
   24.33      "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
   24.34 -  apply (induct ts fixing: t T)
   24.35 +  apply (induct ts arbitrary: t T)
   24.36     apply simp
   24.37    apply atomize
   24.38    apply simp
   24.39 @@ -181,7 +181,7 @@
   24.40  
   24.41  lemma list_app_typeI:
   24.42      "e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
   24.43 -  apply (induct ts fixing: t T Ts)
   24.44 +  apply (induct ts arbitrary: t T Ts)
   24.45     apply simp
   24.46    apply atomize
   24.47    apply (case_tac Ts)
   24.48 @@ -206,7 +206,7 @@
   24.49  
   24.50  theorem var_app_type_eq:
   24.51    "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
   24.52 -  apply (induct ts fixing: T U rule: rev_induct)
   24.53 +  apply (induct ts arbitrary: T U rule: rev_induct)
   24.54    apply simp
   24.55    apply (ind_cases "e \<turnstile> Var i : T")
   24.56    apply (ind_cases "e \<turnstile> Var i : T")
   24.57 @@ -226,7 +226,7 @@
   24.58  
   24.59  lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow>
   24.60    e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us"
   24.61 -  apply (induct us fixing: ts Ts U)
   24.62 +  apply (induct us arbitrary: ts Ts U)
   24.63    apply simp
   24.64    apply (erule var_app_type_eq)
   24.65    apply assumption
   24.66 @@ -293,11 +293,11 @@
   24.67  subsection {* Lifting preserves well-typedness *}
   24.68  
   24.69  lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
   24.70 -  by (induct fixing: i U set: typing) auto
   24.71 +  by (induct arbitrary: i U set: typing) auto
   24.72  
   24.73  lemma lift_types:
   24.74    "e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
   24.75 -  apply (induct ts fixing: Ts)
   24.76 +  apply (induct ts arbitrary: Ts)
   24.77     apply simp
   24.78    apply (case_tac Ts)
   24.79     apply auto
   24.80 @@ -308,7 +308,7 @@
   24.81  
   24.82  lemma subst_lemma:
   24.83      "e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T"
   24.84 -  apply (induct fixing: e' i U u set: typing)
   24.85 +  apply (induct arbitrary: e' i U u set: typing)
   24.86      apply (rule_tac x = x and y = i in linorder_cases)
   24.87        apply auto
   24.88    apply blast
   24.89 @@ -317,7 +317,7 @@
   24.90  lemma substs_lemma:
   24.91    "e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
   24.92       e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
   24.93 -  apply (induct ts fixing: Ts)
   24.94 +  apply (induct ts arbitrary: Ts)
   24.95     apply (case_tac Ts)
   24.96      apply simp
   24.97     apply simp
   24.98 @@ -334,7 +334,7 @@
   24.99  subsection {* Subject reduction *}
  24.100  
  24.101  lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t -> t' \<Longrightarrow> e \<turnstile> t' : T"
  24.102 -  apply (induct fixing: t' set: typing)
  24.103 +  apply (induct arbitrary: t' set: typing)
  24.104      apply blast
  24.105     apply blast
  24.106    apply atomize
    25.1 --- a/src/HOL/Lambda/WeakNorm.thy	Mon Sep 11 14:35:30 2006 +0200
    25.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Mon Sep 11 21:35:19 2006 +0200
    25.3 @@ -114,7 +114,7 @@
    25.4    by (induct ts) simp_all
    25.5  
    25.6  lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
    25.7 -  apply (induct fixing: i j set: NF)
    25.8 +  apply (induct arbitrary: i j set: NF)
    25.9    apply simp
   25.10    apply (frule listall_conj1)
   25.11    apply (drule listall_conj2)
   25.12 @@ -156,7 +156,7 @@
   25.13    by (induct ts) simp_all
   25.14  
   25.15  lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
   25.16 -  apply (induct fixing: i set: NF)
   25.17 +  apply (induct arbitrary: i set: NF)
   25.18    apply (frule listall_conj1)
   25.19    apply (drule listall_conj2)
   25.20    apply (drule_tac i=i in lift_terms_NF)
    26.1 --- a/src/HOL/Library/AssocList.thy	Mon Sep 11 14:35:30 2006 +0200
    26.2 +++ b/src/HOL/Library/AssocList.thy	Mon Sep 11 21:35:19 2006 +0200
    26.3 @@ -332,7 +332,7 @@
    26.4    by (induct al) auto
    26.5  
    26.6  lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v=v'"
    26.7 -proof (induct al fixing: al') 
    26.8 +proof (induct al arbitrary: al') 
    26.9    case Nil thus ?case 
   26.10      by (cases al') (auto split: split_if_asm)
   26.11  next
   26.12 @@ -364,7 +364,7 @@
   26.13  (* ******************************************************************************** *)
   26.14  
   26.15  lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
   26.16 -proof (induct ks fixing: vs al)
   26.17 +proof (induct ks arbitrary: vs al)
   26.18    case Nil
   26.19    thus ?case by simp
   26.20  next
   26.21 @@ -387,11 +387,11 @@
   26.22    assumes "distinct (map fst al)"
   26.23    shows "distinct (map fst (updates ks vs al))"
   26.24    using prems
   26.25 -by (induct ks fixing: vs al) (auto simp add: distinct_update split: list.splits)
   26.26 +by (induct ks arbitrary: vs al) (auto simp add: distinct_update split: list.splits)
   26.27  
   26.28  lemma clearjunk_updates:
   26.29   "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
   26.30 -  by (induct ks fixing: vs al) (auto simp add: clearjunk_update split: list.splits)
   26.31 +  by (induct ks arbitrary: vs al) (auto simp add: clearjunk_update split: list.splits)
   26.32  
   26.33  lemma updates_empty[simp]: "updates vs [] al = al"
   26.34    by (induct vs) auto 
   26.35 @@ -401,12 +401,12 @@
   26.36  
   26.37  lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
   26.38    updates (ks@[k]) vs al = update k (vs!size ks) (updates ks vs al)"
   26.39 -  by (induct ks fixing: vs al) (auto split: list.splits)
   26.40 +  by (induct ks arbitrary: vs al) (auto split: list.splits)
   26.41  
   26.42  lemma updates_list_update_drop[simp]:
   26.43   "\<lbrakk>size ks \<le> i; i < size vs\<rbrakk>
   26.44     \<Longrightarrow> updates ks (vs[i:=v]) al = updates ks vs al"
   26.45 -  by (induct ks fixing: al vs i) (auto split:list.splits nat.splits)
   26.46 +  by (induct ks arbitrary: al vs i) (auto split:list.splits nat.splits)
   26.47  
   26.48  lemma update_updates_conv_if: "
   26.49   map_of (updates xs ys (update x y al)) =
   26.50 @@ -425,11 +425,11 @@
   26.51  
   26.52  lemma updates_append_drop[simp]:
   26.53    "size xs = size ys \<Longrightarrow> updates (xs@zs) ys al = updates xs ys al"
   26.54 -  by (induct xs fixing: ys al) (auto split: list.splits)
   26.55 +  by (induct xs arbitrary: ys al) (auto split: list.splits)
   26.56  
   26.57  lemma updates_append2_drop[simp]:
   26.58    "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
   26.59 -  by (induct xs fixing: ys al) (auto split: list.splits)
   26.60 +  by (induct xs arbitrary: ys al) (auto split: list.splits)
   26.61  
   26.62  (* ******************************************************************************** *)
   26.63  subsection {* @{const map_ran} *}
   26.64 @@ -455,13 +455,13 @@
   26.65  (* ******************************************************************************** *)
   26.66  
   26.67  lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   26.68 -  by (induct ys fixing: xs) (auto simp add: dom_update)
   26.69 +  by (induct ys arbitrary: xs) (auto simp add: dom_update)
   26.70  
   26.71  lemma distinct_merge:
   26.72    assumes "distinct (map fst xs)"
   26.73    shows "distinct (map fst (merge xs ys))"
   26.74    using prems
   26.75 -by (induct ys fixing: xs) (auto simp add: dom_merge distinct_update)
   26.76 +by (induct ys arbitrary: xs) (auto simp add: dom_merge distinct_update)
   26.77  
   26.78  lemma clearjunk_merge:
   26.79   "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
    27.1 --- a/src/HOL/Library/Coinductive_List.thy	Mon Sep 11 14:35:30 2006 +0200
    27.2 +++ b/src/HOL/Library/Coinductive_List.thy	Mon Sep 11 21:35:19 2006 +0200
    27.3 @@ -293,7 +293,7 @@
    27.4  
    27.5  lemma EqLList_implies_ntrunc_equality:
    27.6      "(M, N) \<in> EqLList (diag A) \<Longrightarrow> ntrunc k M = ntrunc k N"
    27.7 -  apply (induct k fixing: M N rule: nat_less_induct)
    27.8 +  apply (induct k arbitrary: M N rule: nat_less_induct)
    27.9    apply (erule EqLList.cases)
   27.10     apply (safe del: equalityI)
   27.11    apply (case_tac n)
    28.1 --- a/src/HOL/Library/ExecutableSet.thy	Mon Sep 11 14:35:30 2006 +0200
    28.2 +++ b/src/HOL/Library/ExecutableSet.thy	Mon Sep 11 21:35:19 2006 +0200
    28.3 @@ -156,7 +156,7 @@
    28.4  
    28.5  lemma iso_union:
    28.6    "set (unionl xs ys) = set xs \<union> set ys"
    28.7 -  unfolding unionl_def by (induct xs fixing: ys) (simp_all add: iso_insert)
    28.8 +  unfolding unionl_def by (induct xs arbitrary: ys) (simp_all add: iso_insert)
    28.9  
   28.10  lemma iso_intersect:
   28.11    "set (intersect xs ys) = set xs \<inter> set ys"
   28.12 @@ -167,7 +167,7 @@
   28.13    assumes distnct: "distinct ys"
   28.14    shows "set (subtract xs ys) = set ys - set xs"
   28.15    and "distinct (subtract xs ys)"
   28.16 -unfolding subtract_def using distnct by (induct xs fixing: ys) (simp_all, auto)
   28.17 +unfolding subtract_def using distnct by (induct xs arbitrary: ys) (simp_all, auto)
   28.18  
   28.19  corollary iso_subtract':
   28.20    fixes xs ys
    29.1 --- a/src/HOL/Library/Multiset.thy	Mon Sep 11 14:35:30 2006 +0200
    29.2 +++ b/src/HOL/Library/Multiset.thy	Mon Sep 11 21:35:19 2006 +0200
    29.3 @@ -746,7 +746,7 @@
    29.4  
    29.5  lemma multiset_of_append [simp]:
    29.6      "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
    29.7 -  by (induct xs fixing: ys) (auto simp: union_ac)
    29.8 +  by (induct xs arbitrary: ys) (auto simp: union_ac)
    29.9  
   29.10  lemma surj_multiset_of: "surj multiset_of"
   29.11    apply (unfold surj_def, rule allI)
    30.1 --- a/src/HOL/Library/Nested_Environment.thy	Mon Sep 11 14:35:30 2006 +0200
    30.2 +++ b/src/HOL/Library/Nested_Environment.thy	Mon Sep 11 21:35:19 2006 +0200
    30.3 @@ -104,7 +104,7 @@
    30.4    assumes "lookup env xs = None"
    30.5    shows "lookup env (xs @ ys) = None"
    30.6    using prems
    30.7 -proof (induct xs fixing: env)
    30.8 +proof (induct xs arbitrary: env)
    30.9    case Nil
   30.10    then have False by simp
   30.11    then show ?case ..
   30.12 @@ -141,7 +141,7 @@
   30.13    assumes "lookup env xs = Some e"
   30.14    shows "lookup env (xs @ ys) = lookup e ys"
   30.15    using prems
   30.16 -proof (induct xs fixing: env e)
   30.17 +proof (induct xs arbitrary: env e)
   30.18    case Nil
   30.19    then have "env = e" by simp
   30.20    then show "lookup env ([] @ ys) = lookup e ys" by simp
   30.21 @@ -209,7 +209,7 @@
   30.22      es' y = Some env' \<and>
   30.23      lookup env' ys = Some e"
   30.24    using prems
   30.25 -proof (induct xs fixing: env e)
   30.26 +proof (induct xs arbitrary: env e)
   30.27    case Nil
   30.28    from Nil.prems have "lookup env (y # ys) = Some e"
   30.29      by simp
   30.30 @@ -329,7 +329,7 @@
   30.31    assumes "lookup env xs = Some e"
   30.32    shows "lookup (update xs (Some env') env) xs = Some env'"
   30.33    using prems
   30.34 -proof (induct xs fixing: env e)
   30.35 +proof (induct xs arbitrary: env e)
   30.36    case Nil
   30.37    then have "env = e" by simp
   30.38    then show ?case by simp
   30.39 @@ -378,7 +378,7 @@
   30.40    assumes "lookup env xs = None"
   30.41    shows "update (xs @ y # ys) opt env = env"
   30.42    using prems
   30.43 -proof (induct xs fixing: env)
   30.44 +proof (induct xs arbitrary: env)
   30.45    case Nil
   30.46    then have False by simp
   30.47    then show ?case ..
   30.48 @@ -421,7 +421,7 @@
   30.49    assumes "lookup env xs = Some e"
   30.50    shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
   30.51    using prems
   30.52 -proof (induct xs fixing: env e)
   30.53 +proof (induct xs arbitrary: env e)
   30.54    case Nil
   30.55    then have "env = e" by simp
   30.56    then show ?case by simp
   30.57 @@ -472,7 +472,7 @@
   30.58    assumes neq: "y \<noteq> (z::'c)"
   30.59    shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
   30.60      lookup env (xs @ y # ys)"
   30.61 -proof (induct xs fixing: env)
   30.62 +proof (induct xs arbitrary: env)
   30.63    case Nil
   30.64    show ?case
   30.65    proof (cases env)
    31.1 --- a/src/HOL/List.thy	Mon Sep 11 14:35:30 2006 +0200
    31.2 +++ b/src/HOL/List.thy	Mon Sep 11 21:35:19 2006 +0200
    31.3 @@ -311,7 +311,8 @@
    31.4  
    31.5  lemma impossible_Cons [rule_format]: 
    31.6    "length xs <= length ys --> xs = x # ys = False"
    31.7 -apply (induct xs, auto)
    31.8 +apply (induct xs)
    31.9 +apply auto
   31.10  done
   31.11  
   31.12  lemma list_induct2[consumes 1]: "\<And>ys.
   31.13 @@ -1356,12 +1357,12 @@
   31.14  lemma takeWhile_cong [fundef_cong, recdef_cong]:
   31.15    "[| l = k; !!x. x : set l ==> P x = Q x |] 
   31.16    ==> takeWhile P l = takeWhile Q k"
   31.17 -  by (induct k fixing: l, simp_all)
   31.18 +  by (induct k arbitrary: l) (simp_all)
   31.19  
   31.20  lemma dropWhile_cong [fundef_cong, recdef_cong]:
   31.21    "[| l = k; !!x. x : set l ==> P x = Q x |] 
   31.22    ==> dropWhile P l = dropWhile Q k"
   31.23 -  by (induct k fixing: l, simp_all)
   31.24 +  by (induct k arbitrary: l, simp_all)
   31.25  
   31.26  
   31.27  subsubsection {* @{text zip} *}
   31.28 @@ -1600,12 +1601,12 @@
   31.29  lemma foldl_cong [fundef_cong, recdef_cong]:
   31.30    "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   31.31    ==> foldl f a l = foldl g b k"
   31.32 -  by (induct k fixing: a b l, simp_all)
   31.33 +  by (induct k arbitrary: a b l) simp_all
   31.34  
   31.35  lemma foldr_cong [fundef_cong, recdef_cong]:
   31.36    "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
   31.37    ==> foldr f l a = foldr g k b"
   31.38 -  by (induct k fixing: a b l, simp_all)
   31.39 +  by (induct k arbitrary: a b l) simp_all
   31.40  
   31.41  lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
   31.42  by (induct xs) auto
    32.1 --- a/src/HOL/Nominal/Examples/CR.thy	Mon Sep 11 14:35:30 2006 +0200
    32.2 +++ b/src/HOL/Nominal/Examples/CR.thy	Mon Sep 11 21:35:19 2006 +0200
    32.3 @@ -530,7 +530,7 @@
    32.4    and     b: "M\<longrightarrow>\<^isub>1M2"
    32.5    shows "\<exists>M3. M1\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3"
    32.6    using a b
    32.7 -proof (induct fixing: M2)
    32.8 +proof (induct arbitrary: M2)
    32.9    case (o1 M) (* case 1 --- M1 = M *)
   32.10    thus "\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and>  M2\<longrightarrow>\<^isub>1M3" by blast
   32.11  next
   32.12 @@ -766,7 +766,7 @@
   32.13    and     b: "t\<longrightarrow>\<^isub>1t2"
   32.14    shows "\<exists>t3. t1\<longrightarrow>\<^isub>1t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3"
   32.15    using a b
   32.16 -proof (induct fixing: t2)
   32.17 +proof (induct arbitrary: t2)
   32.18    case 1 thus ?case by force
   32.19  next
   32.20    case (2 s1 s2)
    33.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Mon Sep 11 14:35:30 2006 +0200
    33.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Mon Sep 11 21:35:19 2006 +0200
    33.3 @@ -801,7 +801,7 @@
    33.4  lemma 
    33.5    shows trans: "\<Gamma>\<turnstile>S<:Q \<Longrightarrow> \<Gamma>\<turnstile>Q<:T \<Longrightarrow> \<Gamma>\<turnstile>S<:T" 
    33.6    and narrow: "(\<Delta>@[(X,Q)]@\<Gamma>)\<turnstile>M<:N \<Longrightarrow> \<Gamma>\<turnstile>P<:Q \<Longrightarrow> (\<Delta>@[(X,P)]@\<Gamma>)\<turnstile>M<:N"
    33.7 -proof (induct Q fixing: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule)
    33.8 +proof (induct Q arbitrary: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule)
    33.9    case (less Q)
   33.10      --{* \begin{minipage}[t]{0.9\textwidth}
   33.11      First we mention the induction hypotheses of the outer induction for later
    34.1 --- a/src/HOL/Nominal/Examples/Iteration.thy	Mon Sep 11 14:35:30 2006 +0200
    34.2 +++ b/src/HOL/Nominal/Examples/Iteration.thy	Mon Sep 11 21:35:19 2006 +0200
    34.3 @@ -57,7 +57,7 @@
    34.4    and     c2: "(t,r')\<in>it f1 f2 f3"
    34.5    shows   "r=r'"
    34.6  using c1 c2
    34.7 -proof (induct fixing: r')
    34.8 +proof (induct arbitrary: r')
    34.9    case it1
   34.10    then show ?case by cases (simp_all add: lam.inject)
   34.11  next
    35.1 --- a/src/HOL/Nominal/Examples/Weakening.thy	Mon Sep 11 14:35:30 2006 +0200
    35.2 +++ b/src/HOL/Nominal/Examples/Weakening.thy	Mon Sep 11 21:35:19 2006 +0200
    35.3 @@ -213,7 +213,7 @@
    35.4    and     c: "\<Gamma>1 \<lless> \<Gamma>2"
    35.5    shows "\<Gamma>2 \<turnstile> t:\<sigma>"
    35.6  using a b c
    35.7 -proof (induct fixing: \<Gamma>2)
    35.8 +proof (induct arbitrary: \<Gamma>2)
    35.9    case (t1 \<Gamma>1 \<tau> a) (* variable case *)
   35.10    have "\<Gamma>1 \<lless> \<Gamma>2" 
   35.11    and  "valid \<Gamma>2"
    36.1 --- a/src/HOL/Relation_Power.thy	Mon Sep 11 14:35:30 2006 +0200
    36.2 +++ b/src/HOL/Relation_Power.thy	Mon Sep 11 21:35:19 2006 +0200
    36.3 @@ -59,7 +59,7 @@
    36.4  
    36.5  lemma rel_pow_Suc_I2:
    36.6      "(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
    36.7 -  apply (induct n fixing: z)
    36.8 +  apply (induct n arbitrary: z)
    36.9     apply simp
   36.10    apply fastsimp
   36.11    done
   36.12 @@ -79,7 +79,7 @@
   36.13  
   36.14  lemma rel_pow_Suc_D2:
   36.15      "(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
   36.16 -  apply (induct n fixing: x z)
   36.17 +  apply (induct n arbitrary: x z)
   36.18     apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
   36.19    apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
   36.20    done
    37.1 --- a/src/HOL/Unix/Unix.thy	Mon Sep 11 14:35:30 2006 +0200
    37.2 +++ b/src/HOL/Unix/Unix.thy	Mon Sep 11 21:35:19 2006 +0200
    37.3 @@ -657,7 +657,7 @@
    37.4  
    37.5  lemma can_exec_snocD: "can_exec root (xs @ [y])
    37.6      \<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''"
    37.7 -proof (induct xs fixing: root)
    37.8 +proof (induct xs arbitrary: root)
    37.9    case Nil
   37.10    then show ?case
   37.11      by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
    38.1 --- a/src/HOL/W0/W0.thy	Mon Sep 11 14:35:30 2006 +0200
    38.2 +++ b/src/HOL/W0/W0.thy	Mon Sep 11 21:35:19 2006 +0200
    38.3 @@ -439,7 +439,7 @@
    38.4       Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
    38.5  
    38.6  theorem W_correct: "Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
    38.7 -proof (induct e fixing: a s t m n)
    38.8 +proof (induct e arbitrary: a s t m n)
    38.9    case (Var i)
   38.10    from `Ok (s, t, m) = \<W> (Var i) a n`
   38.11    show "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
    39.1 --- a/src/HOL/ex/CodeRandom.thy	Mon Sep 11 14:35:30 2006 +0200
    39.2 +++ b/src/HOL/ex/CodeRandom.thy	Mon Sep 11 21:35:19 2006 +0200
    39.3 @@ -72,7 +72,7 @@
    39.4      fix n
    39.5      assume "n < length xs"
    39.6      then show "pick (map (Pair 1) xs) n = nth xs n"
    39.7 -    proof (induct xs fixing: n)
    39.8 +    proof (induct xs arbitrary: n)
    39.9        case Nil then show ?case by simp
   39.10      next
   39.11        case (Cons x xs) show ?case
    40.1 --- a/src/HOL/ex/ReflectionEx.thy	Mon Sep 11 14:35:30 2006 +0200
    40.2 +++ b/src/HOL/ex/ReflectionEx.thy	Mon Sep 11 21:35:19 2006 +0200
    40.3 @@ -173,7 +173,7 @@
    40.4    "lin_mul t = (\<lambda> i. Mul i t)"
    40.5  
    40.6  lemma lin_mul: "Inum bs (lin_mul t i) = Inum bs (Mul i t)"
    40.7 -by (induct t fixing: i rule: lin_mul.induct, auto simp add: ring_eq_simps)
    40.8 +by (induct t arbitrary: i rule: lin_mul.induct) (auto simp add: ring_eq_simps)
    40.9  
   40.10  consts linum:: "num \<Rightarrow> num"
   40.11  recdef linum "measure num_size"
    41.1 --- a/src/HOL/ex/ThreeDivides.thy	Mon Sep 11 14:35:30 2006 +0200
    41.2 +++ b/src/HOL/ex/ThreeDivides.thy	Mon Sep 11 21:35:19 2006 +0200
    41.3 @@ -176,7 +176,7 @@
    41.4  
    41.5  lemma exp_exists:
    41.6    "m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)"
    41.7 -proof (induct nd \<equiv> "nlen m" fixing: m)
    41.8 +proof (induct nd \<equiv> "nlen m" arbitrary: m)
    41.9    case 0 thus ?case by (simp add: nlen_zero)
   41.10  next
   41.11    case (Suc nd)
    42.1 --- a/src/Provers/induct_method.ML	Mon Sep 11 14:35:30 2006 +0200
    42.2 +++ b/src/Provers/induct_method.ML	Mon Sep 11 21:35:19 2006 +0200
    42.3 @@ -357,7 +357,7 @@
    42.4  
    42.5  in
    42.6  
    42.7 -fun induct_tac ctxt is_open def_insts fixing taking opt_rule facts =
    42.8 +fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
    42.9    let
   42.10      val _ = warn_open is_open;
   42.11      val thy = ProofContext.theory_of ctxt;
   42.12 @@ -396,7 +396,7 @@
   42.13              (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
   42.14                THEN' fix_tac defs_ctxt
   42.15                  (nth concls (j - 1) + more_consumes)
   42.16 -                (nth_list fixing (j - 1))))
   42.17 +                (nth_list arbitrary (j - 1))))
   42.18            THEN' inner_atomize_tac) j))
   42.19          THEN' atomize_tac) i st |> Seq.maps (fn st' =>
   42.20              guess_instance (internalize more_consumes rule) i st'
   42.21 @@ -467,7 +467,7 @@
   42.22  (** concrete syntax **)
   42.23  
   42.24  val openN = "open";
   42.25 -val fixingN = "fixing";
   42.26 +val arbitraryN = "arbitrary";
   42.27  val takingN = "taking";
   42.28  val ruleN = "rule";
   42.29  
   42.30 @@ -503,10 +503,10 @@
   42.31    error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
   42.32  
   42.33  fun unless_more_args scan = Scan.unless (Scan.lift
   42.34 -  ((Args.$$$ fixingN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN ||
   42.35 +  ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN ||
   42.36      Args.$$$ InductAttrib.setN || Args.$$$ ruleN) -- Args.colon)) scan;
   42.37  
   42.38 -val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
   42.39 +val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
   42.40    Args.and_list1 (Scan.repeat (unless_more_args free))) [];
   42.41  
   42.42  val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
   42.43 @@ -524,10 +524,10 @@
   42.44  fun induct_meth src =
   42.45    Method.syntax (Args.mode openN --
   42.46      (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
   42.47 -    (fixing -- taking -- Scan.option induct_rule))) src
   42.48 -  #> (fn (ctxt, (is_open, (insts, ((fixing, taking), opt_rule)))) =>
   42.49 +    (arbitrary -- taking -- Scan.option induct_rule))) src
   42.50 +  #> (fn (ctxt, (is_open, (insts, ((arbitrary, taking), opt_rule)))) =>
   42.51      Method.RAW_METHOD_CASES (fn facts =>
   42.52 -      Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts fixing taking opt_rule facts))));
   42.53 +      Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts))));
   42.54  
   42.55  fun coinduct_meth src =
   42.56    Method.syntax (Args.mode openN --
    43.1 --- a/src/ZF/Induct/Binary_Trees.thy	Mon Sep 11 14:35:30 2006 +0200
    43.2 +++ b/src/ZF/Induct/Binary_Trees.thy	Mon Sep 11 21:35:19 2006 +0200
    43.3 @@ -19,7 +19,7 @@
    43.4  declare bt.intros [simp]
    43.5  
    43.6  lemma Br_neq_left: "l \<in> bt(A) ==> Br(x, l, r) \<noteq> l"
    43.7 -  by (induct fixing: x r set: bt) auto
    43.8 +  by (induct arbitrary: x r set: bt) auto
    43.9  
   43.10  lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
   43.11    -- "Proving a freeness theorem."
   43.12 @@ -83,7 +83,7 @@
   43.13  
   43.14  lemma n_nodes_aux_eq:
   43.15      "t \<in> bt(A) ==> k \<in> nat ==> n_nodes_aux(t)`k = n_nodes(t) #+ k"
   43.16 -  apply (induct fixing: k set: bt)
   43.17 +  apply (induct arbitrary: k set: bt)
   43.18     apply simp
   43.19    apply (atomize, simp)
   43.20    done
    44.1 --- a/src/ZF/Induct/Primrec.thy	Mon Sep 11 14:35:30 2006 +0200
    44.2 +++ b/src/ZF/Induct/Primrec.thy	Mon Sep 11 21:35:19 2006 +0200
    44.3 @@ -131,7 +131,7 @@
    44.4  
    44.5  lemma lt_ack2: "i \<in> nat ==> j \<in> nat ==> j < ack(i,j)"
    44.6    -- {* PROPERTY A 4 *}
    44.7 -  apply (induct i fixing: j set: nat)
    44.8 +  apply (induct i arbitrary: j set: nat)
    44.9     apply simp
   44.10    apply (induct_tac j)
   44.11     apply (erule_tac [2] succ_leI [THEN lt_trans1])
    45.1 --- a/src/ZF/Induct/PropLog.thy	Mon Sep 11 14:35:30 2006 +0200
    45.2 +++ b/src/ZF/Induct/PropLog.thy	Mon Sep 11 21:35:19 2006 +0200
    45.3 @@ -327,7 +327,7 @@
    45.4  
    45.5  lemma completeness:
    45.6       "H \<in> Fin(propn) ==> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p"
    45.7 -  apply (induct fixing: p set: Fin)
    45.8 +  apply (induct arbitrary: p set: Fin)
    45.9     apply (safe intro!: completeness_0)
   45.10    apply (rule weaken_left_cons [THEN thms_MP])
   45.11     apply (blast intro!: logcon_Imp propn.intros)