# HG changeset patch
# User berghofe
# Date 1263145425 -3600
# Node ID 7894c7dab1328f3e9c3890a00770b4299b3a569d
# Parent  e391c3de0f6bd741a74b0df88d6b5d9e04cb3637
Adapted to changes in induct method.

diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -1581,14 +1581,10 @@
     {
       (*JE: we now apply the induction hypothesis with some additional facts required*)
       from f_in_P deg_g_le_deg_f show ?thesis
-      proof (induct n \<equiv> "deg R f" arbitrary: "f" rule: nat_less_induct)
-        fix n f
-        assume hypo: "\<forall>m<n. \<forall>x. x \<in> carrier P \<longrightarrow>
-          deg R g \<le> deg R x \<longrightarrow> 
-          m = deg R x \<longrightarrow>
-          (\<exists>q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and> lcoeff g (^) k \<odot>\<^bsub>P\<^esub> x = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r & (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g))"
-          and prem: "n = deg R f" and f_in_P [simp]: "f \<in> carrier P"
-          and deg_g_le_deg_f: "deg R g \<le> deg R f"
+      proof (induct "deg R f" arbitrary: "f" rule: less_induct)
+        case less
+        note f_in_P [simp] = `f \<in> carrier P`
+          and deg_g_le_deg_f = `deg R g \<le> deg R f`
         let ?k = "1::nat" and ?r = "(g \<otimes>\<^bsub>P\<^esub> (monom P (lcoeff f) (deg R f - deg R g))) \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)"
           and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
         show "\<exists> q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and> lcoeff g (^) k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r & (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g)"
@@ -1631,13 +1627,13 @@
                 {
                   (*JE: now it only remains the case where the induction hypothesis can be used.*)
                   (*JE: we first prove that the degree of the remainder is smaller than the one of f*)
-                  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n"
+                  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f"
                   proof -
                     have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
                     also have "\<dots> < deg R f"
                     proof (rule deg_lcoeff_cancel)
                       show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
-                        using deg_smult_ring [of "lcoeff g" f] using prem
+                        using deg_smult_ring [of "lcoeff g" f]
                         using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
                       show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
                         using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f
@@ -1651,7 +1647,7 @@
                         using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
                         unfolding Pi_def using deg_g_le_deg_f by force
                     qed (simp_all add: deg_f_nzero)
-                    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n" unfolding prem .
+                    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f" .
                   qed
                   moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
                   moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
@@ -1660,7 +1656,7 @@
                   ultimately obtain q' r' k'
                     where rem_desc: "lcoeff g (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?r) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
                     and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
-                    using hypo by blast
+                    using less by blast
                       (*JE: we now prove that the new quotient, remainder and exponent can be used to get 
                       the quotient, remainder and exponent of the long division theorem*)
                   show ?thesis
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Bali/Basis.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/Bali/Basis.thy
-    ID:         $Id$
     Author:     David von Oheimb
-
 *)
 header {* Definitions extending HOL as logical basis of Bali *}
 
@@ -66,8 +64,6 @@
  "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r\<^sup>*; (a,y)\<in>r\<^sup>*\<rbrakk> 
  \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
 proof -
-  note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
-  note converse_rtranclE = converse_rtranclE [consumes 1] 
   assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
   assume "(a,x)\<in>r\<^sup>*" 
   then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
@@ -110,13 +106,6 @@
 apply (auto dest: rtrancl_into_trancl1)
 done
 
-(* ### To Transitive_Closure *)
-theorems converse_rtrancl_induct 
- = converse_rtrancl_induct [consumes 1,case_names Id Step]
-
-theorems converse_trancl_induct 
-         = converse_trancl_induct [consumes 1,case_names Single Step]
-
 (* context (theory "Set") *)
 lemma Ball_weaken:"\<lbrakk>Ball s P;\<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q"
 by auto
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Bali/DeclConcepts.thy
-    ID:         $Id$
     Author:     Norbert Schirmer
 *)
 header {* Advanced concepts on Java declarations like overriding, inheritance,
@@ -2282,74 +2281,47 @@
 done
 
 lemma superclasses_mono:
-"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
-  \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc;
-  x\<in>superclasses G D 
-\<rbrakk> \<Longrightarrow> x\<in>superclasses G C" 
-proof -
-  
-  assume     ws: "ws_prog G"          and 
-          cls_C: "class G C = Some c" and
-             wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
-                  \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
-  assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"           
-  thus "\<And> c. \<lbrakk>class G C = Some c; x\<in>superclasses G D\<rbrakk>\<Longrightarrow>
-        x\<in>superclasses G C" (is "PROP ?P C"  
-                             is "\<And> c. ?CLS C c \<Longrightarrow> ?SUP D \<Longrightarrow> ?SUP C")
-  proof (induct ?P C  rule: converse_trancl_induct)
-    fix C c
-    assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1D" "class G C = Some c" "x \<in> superclasses G D"
-    with wf ws show "?SUP C"
-      by (auto    intro: no_subcls1_Object 
-               simp add: superclasses_rec subcls1_def)
-  next
-    fix C S c
-    assume clsrel': "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S \<prec>\<^sub>C D"
-       and    hyp : "\<And> s. \<lbrakk>class G S = Some s; x \<in> superclasses G D\<rbrakk>
-                           \<Longrightarrow> x \<in> superclasses G S"
-       and  cls_C': "class G C = Some c"
-       and       x: "x \<in> superclasses G D"
-    moreover note wf ws
-    moreover from calculation 
-    have "?SUP S" 
-      by (force intro: no_subcls1_Object simp add: subcls1_def)
-    moreover from calculation 
-    have "super c = S" 
-      by (auto intro: no_subcls1_Object simp add: subcls1_def)
-    ultimately show "?SUP C" 
-      by (auto intro: no_subcls1_Object simp add: superclasses_rec)
-  qed
+  assumes clsrel: "G\<turnstile>C\<prec>\<^sub>C D"
+  and ws: "ws_prog G"
+  and cls_C: "class G C = Some c"
+  and wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
+    \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
+  and x: "x\<in>superclasses G D"
+  shows "x\<in>superclasses G C" using clsrel cls_C x
+proof (induct arbitrary: c rule: converse_trancl_induct)
+  case (base C)
+  with wf ws show ?case
+    by (auto    intro: no_subcls1_Object 
+             simp add: superclasses_rec subcls1_def)
+next
+  case (step C S)
+  moreover note wf ws
+  moreover from calculation 
+  have "x\<in>superclasses G S"
+    by (force intro: no_subcls1_Object simp add: subcls1_def)
+  moreover from calculation 
+  have "super c = S" 
+    by (auto intro: no_subcls1_Object simp add: subcls1_def)
+  ultimately show ?case 
+    by (auto intro: no_subcls1_Object simp add: superclasses_rec)
 qed
 
 lemma subclsEval:
-"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
-  \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc 
- \<rbrakk> \<Longrightarrow> D\<in>superclasses G C" 
-proof -
-  note converse_trancl_induct 
-       = converse_trancl_induct [consumes 1,case_names Single Step]
-  assume 
-             ws: "ws_prog G"          and 
-          cls_C: "class G C = Some c" and
-             wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
-                  \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
-  assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"           
-  thus "\<And> c. class G C = Some c\<Longrightarrow> D\<in>superclasses G C" 
-    (is "PROP ?P C"  is "\<And> c. ?CLS C c  \<Longrightarrow> ?SUP C")
-  proof (induct ?P C  rule: converse_trancl_induct)
-    fix C c
-    assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" "class G C = Some c"
-    with ws wf show "?SUP C"
-      by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def)
-  next
-    fix C S c
-    assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S\<prec>\<^sub>C D" 
-           "\<And>s. class G S = Some s \<Longrightarrow> D \<in> superclasses G S"
-           "class G C = Some c" 
-    with ws wf show "?SUP C"
-      by - (rule superclasses_mono,
-            auto dest: no_subcls1_Object simp add: subcls1_def )
-  qed
+  assumes clsrel: "G\<turnstile>C\<prec>\<^sub>C D"
+  and ws: "ws_prog G"
+  and cls_C: "class G C = Some c"
+  and wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
+    \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
+  shows "D\<in>superclasses G C" using clsrel cls_C
+proof (induct arbitrary: c rule: converse_trancl_induct)
+  case (base C)
+  with ws wf show ?case
+    by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def)
+next
+  case (step C S)
+  with ws wf show ?case
+    by - (rule superclasses_mono,
+          auto dest: no_subcls1_Object simp add: subcls1_def )
 qed
 
 end
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Bali/WellForm.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Bali/WellForm.thy
-    ID:         $Id$
     Author:     David von Oheimb and Norbert Schirmer
 *)
 
@@ -1409,8 +1408,7 @@
   from clsC ws 
   show "methd G C sig = Some m 
         \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
-    (is "PROP ?P C") 
-  proof (induct ?P C rule: ws_class_induct')
+  proof (induct C rule: ws_class_induct')
     case Object
     assume "methd G Object sig = Some m" 
     with wf show ?thesis
@@ -1755,28 +1753,20 @@
 lemma ballE': "\<forall>x\<in>A. P x \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> Q" by blast
 
 lemma subint_widen_imethds: 
- "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow>   
-  \<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and> 
+  assumes irel: "G\<turnstile>I\<preceq>I J"
+  and wf: "wf_prog G"
+  and is_iface: "is_iface G J"
+  and jm: "jm \<in> imethds G J sig"
+  shows "\<exists>im \<in> imethds G I sig. is_static im = is_static jm \<and> 
                           accmodi im = accmodi jm \<and>
                           G\<turnstile>resTy im\<preceq>resTy jm"
-proof -
-  assume irel: "G\<turnstile>I\<preceq>I J" and
-           wf: "wf_prog G" and
-     is_iface: "is_iface G J"
-  from irel show "jm \<in> imethds G J sig \<Longrightarrow> ?thesis" 
-               (is "PROP ?P I" is "PROP ?Prem J \<Longrightarrow> ?Concl I")
-  proof (induct ?P I rule: converse_rtrancl_induct) 
-    case Id
-    assume "jm \<in> imethds G J sig"
-    then show "?Concl J" by  (blast elim: bexI')
+  using irel jm
+proof (induct rule: converse_rtrancl_induct)
+    case base
+    then show ?case by  (blast elim: bexI')
   next
-    case Step
-    fix I SI
-    assume subint1_I_SI: "G\<turnstile>I \<prec>I1 SI" and 
-            subint_SI_J: "G\<turnstile>SI \<preceq>I J" and
-                    hyp: "PROP ?P SI" and
-                     jm: "jm \<in> imethds G J sig"
-    from subint1_I_SI 
+    case (step I SI)
+    from `G\<turnstile>I \<prec>I1 SI`
     obtain i where
       ifI: "iface G I = Some i" and
        SI: "SI \<in> set (isuperIfs i)"
@@ -1784,10 +1774,10 @@
 
     let ?newMethods 
           = "(Option.set \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
-    show "?Concl I"
+    show ?case
     proof (cases "?newMethods sig = {}")
       case True
-      with ifI SI hyp wf jm 
+      with ifI SI step wf
       show "?thesis" 
         by (auto simp add: imethds_rec) 
     next
@@ -1816,7 +1806,7 @@
         wf_SI: "wf_idecl G (SI,si)" 
         by (auto dest!: wf_idecl_supD is_acc_ifaceD
                   dest: wf_prog_idecl)
-      from jm hyp 
+      from step
       obtain sim::"qtname \<times> mhead"  where
                       sim: "sim \<in> imethds G SI sig" and
          eq_static_sim_jm: "is_static sim = is_static jm" and 
@@ -1841,7 +1831,6 @@
       show ?thesis 
         by auto 
     qed
-  qed
 qed
      
 (* Tactical version *)
@@ -1974,30 +1963,20 @@
   from clsC ws 
   show "\<And> m d. \<lbrakk>methd G C sig = Some m; class G (declclass m) = Some d\<rbrakk>
         \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)" 
-         (is "PROP ?P C") 
-  proof (induct ?P C rule: ws_class_induct)
+  proof (induct rule: ws_class_induct)
     case Object
-    fix m d
-    assume "methd G Object sig = Some m" 
-           "class G (declclass m) = Some d"
     with wf show "?thesis m d" by auto
   next
-    case Subcls
-    fix C c m d
-    assume hyp: "PROP ?P (super c)"
-    and      m: "methd G C sig = Some m"
-    and  declC: "class G (declclass m) = Some d"
-    and   clsC: "class G C = Some c"
-    and   nObj: "C \<noteq> Object"
+    case (Subcls C c)
     let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig"
     show "?thesis m d" 
     proof (cases "?newMethods")
       case None
-      from None clsC nObj ws m declC
-      show "?thesis" by (auto simp add: methd_rec) (rule hyp)
+      from None ws Subcls
+      show "?thesis" by (auto simp add: methd_rec) (rule Subcls)
     next
       case Some
-      from Some clsC nObj ws m declC
+      from Some ws Subcls
       show "?thesis" 
         by (auto simp add: methd_rec
                      dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Code_Numeral.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -83,7 +83,7 @@
     then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
     then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
   from init step have "P (of_nat (nat_of k))"
-    by (induct "nat_of k") simp_all
+    by (induct ("nat_of k")) simp_all
   then show "P k" by simp
 qed simp_all
 
@@ -100,7 +100,7 @@
   fix k
   have "code_numeral_size k = nat_size (nat_of k)"
     by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
-  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
+  also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all
   finally show "code_numeral_size k = nat_of k" .
 qed
 
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -987,16 +987,14 @@
   assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{ring_char_0,power,division_by_zero,field})"
   shows "p = 0\<^sub>p"
 using nq eq
-proof (induct n\<equiv>"maxindex p" arbitrary: p n0 rule: nat_less_induct)
-  fix n p n0
-  assume H: "\<forall>m<n. \<forall>p n0. isnpolyh p n0 \<longrightarrow>
-    (\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)) \<longrightarrow> m = maxindex p \<longrightarrow> p = 0\<^sub>p"
-    and np: "isnpolyh p n0" and zp: "\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" and n: "n = maxindex p"
-  {assume nz: "n = 0"
-    then obtain c where "p = C c" using n np by (cases p, auto)
+proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
+  case less
+  note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)`
+  {assume nz: "maxindex p = 0"
+    then obtain c where "p = C c" using np by (cases p, auto)
     with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}
   moreover
-  {assume nz: "n \<noteq> 0"
+  {assume nz: "maxindex p \<noteq> 0"
     let ?h = "head p"
     let ?hd = "decrpoly ?h"
     let ?ihd = "maxindex ?hd"
@@ -1005,24 +1003,23 @@
     hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast
     
     from maxindex_coefficients[of p] coefficients_head[of p, symmetric]
-    have mihn: "maxindex ?h \<le> n" unfolding n by auto
-    with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < n" by auto
+    have mihn: "maxindex ?h \<le> maxindex p" by auto
+    with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < maxindex p" by auto
     {fix bs:: "'a list"  assume bs: "wf_bs bs ?hd"
       let ?ts = "take ?ihd bs"
       let ?rs = "drop ?ihd bs"
       have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp
       have bs_ts_eq: "?ts@ ?rs = bs" by simp
       from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp
-      from ihd_lt_n have "ALL x. length (x#?ts) \<le> n" by simp
-      with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = n" by blast
-      hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" using n unfolding wf_bs_def by simp
+      from ihd_lt_n have "ALL x. length (x#?ts) \<le> maxindex p" by simp
+      with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast
+      hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp
       with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast
       hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp
       with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
       have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
       hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) 
       hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
-        thm poly_zero
         using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
       with coefficients_head[of p, symmetric]
       have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
@@ -1031,7 +1028,7 @@
       with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp }
     then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast
     
-    from H[rule_format, OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
+    from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
     hence "?h = 0\<^sub>p" by simp
     with head_nz[OF np] have "p = 0\<^sub>p" by simp}
   ultimately show "p = 0\<^sub>p" by blast
@@ -1357,8 +1354,8 @@
   (polydivide_aux (a,n,p,k,s) = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p) 
           \<and> (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
   using ns
-proof(induct d\<equiv>"degree s" arbitrary: s k k' r n1 rule: nat_less_induct)
-  fix d s k k' r n1
+proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
+  case less
   let ?D = "polydivide_aux_dom"
   let ?dths = "?D (a, n, p, k, s)"
   let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
@@ -1366,20 +1363,13 @@
     \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
   let ?ths = "?dths \<and> ?qrths"
   let ?b = "head s"
-  let ?p' = "funpow (d - n) shift1 p"
-  let ?xdn = "funpow (d - n) shift1 1\<^sub>p"
+  let ?p' = "funpow (degree s - n) shift1 p"
+  let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p"
   let ?akk' = "a ^\<^sub>p (k' - k)"
-  assume H: "\<forall>m<d. \<forall>x xa xb xc xd.
-    isnpolyh x xd \<longrightarrow>
-    m = degree x \<longrightarrow> ?D (a, n, p, xa, x) \<and>
-    (polydivide_aux (a, n, p, xa, x) = (xb, xc) \<longrightarrow>
-    xa \<le> xb \<and> (degree xc = 0 \<or> degree xc < degree p) \<and> 
-    (\<exists> nr. isnpolyh xc nr) \<and>
-    (\<exists>q n1. isnpolyh q n1 \<and> a ^\<^sub>p xb - xa *\<^sub>p x = p *\<^sub>p q +\<^sub>p xc))"
-    and ns: "isnpolyh s n1" and ds: "d = degree s"
+  note ns = `isnpolyh s n1`
   from np have np0: "isnpolyh p 0" 
     using isnpolyh_mono[where n="n0" and n'="0" and p="p"]  by simp
-  have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="d -n"] isnpoly_def by simp
+  have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="degree s - n"] isnpoly_def by simp
   have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp
   from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
   from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap 
@@ -1391,31 +1381,31 @@
     hence ?ths using dom by blast}
   moreover
   {assume sz: "s \<noteq> 0\<^sub>p"
-    {assume dn: "d < n"
-      with sz ds  have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all) 
-      from polydivide_aux.psimps[OF dom] sz dn ds
+    {assume dn: "degree s < n"
+      with sz have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all) 
+      from polydivide_aux.psimps[OF dom] sz dn
       have "?qrths" using ns ndp np by auto (rule exI[where x="0\<^sub>p"],simp)
       with dom have ?ths by blast}
     moreover 
-    {assume dn': "\<not> d < n" hence dn: "d \<ge> n" by arith
+    {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith
       have degsp': "degree s = degree ?p'" 
-        using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
+        using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] by simp
       {assume ba: "?b = a"
         hence headsp': "head s = head ?p'" using ap headp' by simp
         have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
-        from ds degree_polysub_samehead[OF ns np' headsp' degsp']
-        have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
+        from degree_polysub_samehead[OF ns np' headsp' degsp']
+        have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
         moreover 
-        {assume deglt:"degree (s -\<^sub>p ?p') < d"
-          from  H[rule_format, OF deglt nr,simplified] 
+        {assume deglt:"degree (s -\<^sub>p ?p') < degree s"
+          from  less(1)[OF deglt nr] 
           have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast 
           have dom: ?dths apply (rule polydivide_aux_real_domintros) 
-            using ba ds dn' domsp by simp_all
-          from polydivide_aux.psimps[OF dom] sz dn' ba ds
+            using ba dn' domsp by simp_all
+          from polydivide_aux.psimps[OF dom] sz dn' ba
           have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
             by (simp add: Let_def)
           {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
-            from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
+            from less(1)[OF deglt nr, of k k' r]
               trans[OF eq[symmetric] h1]
             have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
               and q1:"\<exists>q nq. isnpolyh q nq \<and> (a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r)" by auto
@@ -1434,19 +1424,19 @@
               Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
               by (simp add: ring_simps)
             hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
-              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p) 
+              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p) 
               + Ipoly bs p * Ipoly bs q + Ipoly bs r"
               by (auto simp only: funpow_shift1_1) 
             hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
-              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p) 
+              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p) 
               + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
             hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
-              Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp
+              Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp
             with isnpolyh_unique[OF nakks' nqr']
             have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
-              p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast
+              p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast
             hence ?qths using nq'
-              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
+              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
               apply (rule_tac x="0" in exI) by simp
             with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
               by blast } hence ?qrths by blast
@@ -1456,25 +1446,23 @@
           hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" 
             apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
           have dom: ?dths apply (rule polydivide_aux_real_domintros) 
-            using ba ds dn' domsp by simp_all
+            using ba dn' domsp by simp_all
           from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{ring_char_0,division_by_zero,field}"]
           have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
           hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
             by (simp only: funpow_shift1_1) simp
           hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
           {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
-            from polydivide_aux.psimps[OF dom] sz dn' ba ds
+            from polydivide_aux.psimps[OF dom] sz dn' ba
             have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
               by (simp add: Let_def)
             also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
             finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
-            with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
+            with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
               polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
               apply auto
               apply (rule exI[where x="?xdn"])        
-              apply auto
-              apply (rule polymul_commute)
-              apply simp_all
+              apply (auto simp add: polymul_commute[of p])
               done}
           with dom have ?ths by blast}
         ultimately have ?ths by blast }
@@ -1488,31 +1476,30 @@
             polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
             funpow_shift1_nz[OF pnz] by simp_all
         from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
-          polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
+          polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="degree s - n"]
         have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" 
           using head_head[OF ns] funpow_shift1_head[OF np pnz]
             polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
           by (simp add: ap)
         from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
           head_nz[OF np] pnz sz ap[symmetric]
-          funpow_shift1_nz[OF pnz, where n="d - n"]
+          funpow_shift1_nz[OF pnz, where n="degree s - n"]
           polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
-          ndp ds[symmetric] dn
+          ndp dn
         have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
           by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
-        {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
+        {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s"
           have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
-            using H[rule_format, OF dth nth, simplified] by blast 
-          have dom: ?dths
-            using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)  
-            using ba ds dn'  by simp_all
+            using less(1)[OF dth nth] by blast 
+          have dom: ?dths using ba dn' th
+            by - (rule polydivide_aux_real_domintros, simp_all)
           from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
           ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
           {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
-            from h1  polydivide_aux.psimps[OF dom] sz dn' ba ds
+            from h1  polydivide_aux.psimps[OF dom] sz dn' ba
             have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
               by (simp add: Let_def)
-            with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
+            with less(1)[OF dth nasbp', of "Suc k" k' r]
             obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" 
               and dr: "degree r = 0 \<or> degree r < degree p"
               and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto
@@ -1524,7 +1511,7 @@
             hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r"
               by (simp add: ring_simps power_Suc)
             hence "Ipoly bs a ^ (k' - k)  * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r"
-              by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
+              by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
             hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
               by (simp add: ring_simps)}
             hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
@@ -1546,13 +1533,13 @@
         {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
           hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" 
             apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
-          have dom: ?dths using sz ba dn' ds domsp 
+          have dom: ?dths using sz ba dn' domsp 
             by - (rule polydivide_aux_real_domintros, simp_all)
           {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
             from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
           have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
           hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
-            by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
+            by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
           hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
         }
         hence hth: "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
@@ -1562,7 +1549,7 @@
                     polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
               simplified ap] by simp
           {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
-          from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] 
+          from h1 sz ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] 
           have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
           with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
             polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
@@ -1573,7 +1560,7 @@
         hence ?qrths by blast
         with dom have ?ths by blast}
         ultimately have ?ths using  degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
-          head_nz[OF np] pnz sz ap[symmetric] ds[symmetric] 
+          head_nz[OF np] pnz sz ap[symmetric]
           by (simp add: degree_eq_degreen0[symmetric]) blast }
       ultimately have ?ths by blast
     }
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/GCD.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -16,7 +16,7 @@
 another extension of the notions to the integers, and added a number
 of results to "Primes" and "GCD". IntPrimes also defined and developed
 the congruence relations on the integers. The notion was extended to
-the natural numbers by Chiaeb.
+the natural numbers by Chaieb.
 
 Jeremy Avigad combined all of these, made everything uniform for the
 natural numbers and the integers, and added a number of new theorems.
@@ -25,7 +25,7 @@
 *)
 
 
-header {* Greates common divisor and least common multiple *}
+header {* Greatest common divisor and least common multiple *}
 
 theory GCD
 imports Fact Parity
@@ -1074,34 +1074,35 @@
   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
   shows "P a b"
-proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
-  fix n a b
-  assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
+proof(induct "a + b" arbitrary: a b rule: less_induct)
+  case less
   have "a = b \<or> a < b \<or> b < a" by arith
   moreover {assume eq: "a= b"
     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
     by simp}
   moreover
   {assume lt: "a < b"
-    hence "a + b - a < n \<or> a = 0"  using H(2) by arith
+    hence "a + b - a < a + b \<or> a = 0" by arith
     moreover
     {assume "a =0" with z c have "P a b" by blast }
     moreover
-    {assume ab: "a + b - a < n"
-      have th0: "a + b - a = a + (b - a)" using lt by arith
-      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
-      have "P a b" by (simp add: th0[symmetric])}
+    {assume "a + b - a < a + b"
+      also have th0: "a + b - a = a + (b - a)" using lt by arith
+      finally have "a + (b - a) < a + b" .
+      then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
+      then have "P a b" by (simp add: th0[symmetric])}
     ultimately have "P a b" by blast}
   moreover
   {assume lt: "a > b"
-    hence "b + a - b < n \<or> b = 0"  using H(2) by arith
+    hence "b + a - b < a + b \<or> b = 0" by arith
     moreover
     {assume "b =0" with z c have "P a b" by blast }
     moreover
-    {assume ab: "b + a - b < n"
-      have th0: "b + a - b = b + (a - b)" using lt by arith
-      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
-      have "P b a" by (simp add: th0[symmetric])
+    {assume "b + a - b < a + b"
+      also have th0: "b + a - b = b + (a - b)" using lt by arith
+      finally have "b + (a - b) < a + b" .
+      then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
+      then have "P b a" by (simp add: th0[symmetric])
       hence "P a b" using c by blast }
     ultimately have "P a b" by blast}
 ultimately  show "P a b" by blast
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Induct/Common_Patterns.thy
--- a/src/HOL/Induct/Common_Patterns.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Induct/Common_Patterns.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -73,7 +73,7 @@
   show "P (a x)" sorry
 next
   case (Suc n)
-  note hyp = `\<And>x. A (a x) \<Longrightarrow> n = a x \<Longrightarrow> P (a x)`
+  note hyp = `\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)`
     and prem = `A (a x)`
     and defn = `Suc n = a x`
   show "P (a x)" sorry
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Isar_Examples/Puzzle.thy
--- a/src/HOL/Isar_Examples/Puzzle.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Isar_Examples/Puzzle.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -22,17 +22,16 @@
 proof (rule order_antisym)
   {
     fix n show "n \<le> f n"
-    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:)
+    proof (induct "f n" arbitrary: n rule: less_induct)
+      case less
       show "n \<le> f n"
       proof (cases n)
         case (Suc m)
         from f_ax have "f (f m) < f n" by (simp only: Suc)
-        with hyp have "f m \<le> f (f m)" .
+        with less have "f m \<le> f (f m)" .
         also from f_ax have "\<dots> < f n" by (simp only: Suc)
         finally have "f m < f n" .
-        with hyp have "m \<le> f m" .
+        with less have "m \<le> f m" .
         also note `\<dots> < f n`
         finally have "m < f n" .
         then have "n \<le> f n" by (simp only: Suc)
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -621,19 +621,18 @@
     done
 qed
 
-text{* Fundamental theorem of algebral *}
+text{* Fundamental theorem of algebra *}
 
 lemma fundamental_theorem_of_algebra:
   assumes nc: "~constant(poly p)"
   shows "\<exists>z::complex. poly p z = 0"
 using nc
-proof(induct n\<equiv> "psize p" arbitrary: p rule: nat_less_induct)
-  fix n fix p :: "complex poly"
+proof(induct "psize p" arbitrary: p rule: less_induct)
+  case less
   let ?p = "poly p"
-  assume H: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = psize p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = psize p"
   let ?ths = "\<exists>z. ?p z = 0"
 
-  from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n)
+  from nonconstant_length[OF less(2)] have n2: "psize p \<ge> 2" .
   from poly_minimum_modulus obtain c where
     c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)" by blast
   {assume pc: "?p c = 0" hence ?ths by blast}
@@ -649,7 +648,7 @@
           using h unfolding constant_def by blast
         also have "\<dots> = ?p y" using th by auto
         finally have "?p x = ?p y" .}
-      with nc have False unfolding constant_def by blast }
+      with less(2) have False unfolding constant_def by blast }
     hence qnc: "\<not> constant (poly q)" by blast
     from q(2) have pqc0: "?p c = poly q 0" by simp
     from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp
@@ -682,8 +681,8 @@
     from poly_decompose[OF rnc] obtain k a s where
       kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r"
       "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
-    {assume "k + 1 = n"
-      with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto
+    {assume "psize p = k + 1"
+      with kas(3) lgqr[symmetric] q(1) have s0:"s=0" by auto
       {fix w
         have "cmod (poly ?r w) = cmod (1 + a * w ^ k)"
           using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)}
@@ -691,15 +690,15 @@
         from reduce_poly_simple[OF kas(1,2)]
       have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
     moreover
-    {assume kn: "k+1 \<noteq> n"
-      from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp
+    {assume kn: "psize p \<noteq> k+1"
+      from kn kas(3) q(1) lgqr have k1n: "k + 1 < psize p" by simp
       have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
         unfolding constant_def poly_pCons poly_monom
         using kas(1) apply simp
         by (rule exI[where x=0], rule exI[where x=1], simp)
       from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))"
         by (simp add: psize_def degree_monom_eq)
-      from H[rule_format, OF k1n th01 th02]
+      from less(1) [OF k1n [simplified th02] th01]
       obtain w where w: "1 + w^k * a = 0"
         unfolding poly_pCons poly_monom
         using kas(2) by (cases k, auto simp add: algebra_simps)
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Library/Polynomial.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -1384,7 +1384,7 @@
     with k have "degree p = Suc (degree k)"
       by (simp add: degree_mult_eq del: mult_pCons_left)
     with `Suc n = degree p` have "n = degree k" by simp
-    with `k \<noteq> 0` have "finite {x. poly k x = 0}" by (rule Suc.hyps)
+    then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
     then have "finite (insert a {x. poly k x = 0})" by simp
     then show "finite {x. poly p x = 0}"
       by (simp add: k uminus_add_conv_diff Collect_disj_eq
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Library/Word.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -436,7 +436,7 @@
       show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
       proof -
         have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
-          by (induct "length xs",simp_all)
+          by (induct ("length xs")) simp_all
         hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
           bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
           by simp
@@ -2165,13 +2165,13 @@
   apply (simp add: bv_extend_def)
   apply (subst bv_to_nat_dist_append)
   apply simp
-  apply (induct "n - length w")
+  apply (induct ("n - length w"))
    apply simp_all
   done
 
 lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
   apply (simp add: bv_extend_def)
-  apply (induct "n - length w")
+  apply (cases "n - length w")
    apply simp_all
   done
 
@@ -2188,7 +2188,7 @@
   show ?thesis
     apply (simp add: bv_to_int_def)
     apply (simp add: bv_extend_def)
-    apply (induct "n - length w",simp_all)
+    apply (induct ("n - length w"), simp_all)
     done
 qed
 
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -15,12 +15,13 @@
 
 lemma sup_loc_some [rule_format]:
 "\<forall>y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = OK t \<longrightarrow> 
-  (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
-proof (induct ?P b)
-  show "?P []" by simp
+  (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))"
+proof (induct b)
+  case Nil
+  show ?case by simp
 next
   case (Cons a list)
-  show "?P (a#list)" 
+  show ?case 
   proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def)
     fix z zs n
     assume *: 
@@ -60,13 +61,14 @@
  
 
 lemma append_length_n [rule_format]: 
-"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
-proof (induct ?P x)
-  show "?P []" by simp
+"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)"
+proof (induct x)
+  case Nil
+  show ?case by simp
 next
-  fix l ls assume Cons: "?P ls"
+  case (Cons l ls)
 
-  show "?P (l#ls)"
+  show ?case
   proof (intro allI impI)
     fix n
     assume l: "n \<le> length (l # ls)"
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -170,8 +170,8 @@
   next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s)
       case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real"
       assume IA:"\<And>u s.  \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s;
-               s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n \<equiv> card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and
-        as:"Suc n \<equiv> card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
+               s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n = card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and
+        as:"Suc n = card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
            "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1"
       have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr)
         assume " \<not> (\<exists>x\<in>s. u x \<noteq> 1)" hence "setsum u s = real_of_nat (card s)" unfolding card_eq_setsum by auto
@@ -1345,7 +1345,7 @@
 next
   case False then obtain w where "w\<in>s" by auto
   show ?thesis unfolding caratheodory[of s]
-  proof(induct "CARD('n) + 1")
+  proof(induct ("CARD('n) + 1"))
     have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}" 
       using compact_empty by (auto simp add: convex_hull_empty)
     case 0 thus ?case unfolding * by simp
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -3542,17 +3542,9 @@
   and sp:"s \<subseteq> span t"
   shows "\<exists>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
 using f i sp
-proof(induct c\<equiv>"card(t - s)" arbitrary: s t rule: nat_less_induct)
-  fix n:: nat and s t :: "('a ^'n) set"
-  assume H: " \<forall>m<n. \<forall>(x:: ('a ^'n) set) xa.
-                finite xa \<longrightarrow>
-                independent x \<longrightarrow>
-                x \<subseteq> span xa \<longrightarrow>
-                m = card (xa - x) \<longrightarrow>
-                (\<exists>t'. (card t' = card xa) \<and> finite t' \<and>
-                      x \<subseteq> t' \<and> t' \<subseteq> x \<union> xa \<and> x \<subseteq> span t')"
-    and ft: "finite t" and s: "independent s" and sp: "s \<subseteq> span t"
-    and n: "n = card (t - s)"
+proof(induct "card (t - s)" arbitrary: s t rule: less_induct)
+  case less
+  note ft = `finite t` and s = `independent s` and sp = `s \<subseteq> span t`
   let ?P = "\<lambda>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
   let ?ths = "\<exists>t'. ?P t'"
   {assume st: "s \<subseteq> t"
@@ -3568,12 +3560,12 @@
   {assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
     from st(2) obtain b where b: "b \<in> t" "b \<notin> s" by blast
       from b have "t - {b} - s \<subset> t - s" by blast
-      then have cardlt: "card (t - {b} - s) < n" using n ft
+      then have cardlt: "card (t - {b} - s) < card (t - s)" using ft
         by (auto intro: psubset_card_mono)
       from b ft have ct0: "card t \<noteq> 0" by auto
     {assume stb: "s \<subseteq> span(t -{b})"
       from ft have ftb: "finite (t -{b})" by auto
-      from H[rule_format, OF cardlt ftb s stb]
+      from less(1)[OF cardlt ftb s stb]
       obtain u where u: "card u = card (t-{b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u" and fu: "finite u" by blast
       let ?w = "insert b u"
       have th0: "s \<subseteq> insert b u" using u by blast
@@ -3594,8 +3586,8 @@
       from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})" by blast
       have ab: "a \<noteq> b" using a b by blast
       have at: "a \<notin> t" using a ab span_superset[of a "t- {b}"] by auto
-      have mlt: "card ((insert a (t - {b})) - s) < n"
-        using cardlt ft n  a b by auto
+      have mlt: "card ((insert a (t - {b})) - s) < card (t - s)"
+        using cardlt ft a b by auto
       have ft': "finite (insert a (t - {b}))" using ft by auto
       {fix x assume xs: "x \<in> s"
         have t: "t \<subseteq> (insert b (insert a (t -{b})))" using b by auto
@@ -3608,7 +3600,7 @@
         from span_trans[OF bs x] have "x \<in> span (insert a (t - {b}))"  .}
       then have sp': "s \<subseteq> span (insert a (t - {b}))" by blast
 
-      from H[rule_format, OF mlt ft' s sp' refl] obtain u where
+      from less(1)[OF mlt ft' s sp'] obtain u where
         u: "card u = card (insert a (t -{b}))" "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t -{b})"
         "s \<subseteq> span u" by blast
       from u a b ft at ct0 have "?P u" by auto
@@ -3657,11 +3649,9 @@
   assumes sv: "(S::(real^'n) set) \<subseteq> V" and iS: "independent S"
   shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
   using sv iS
-proof(induct d\<equiv> "CARD('n) - card S" arbitrary: S rule: nat_less_induct)
-  fix n and S:: "(real^'n) set"
-  assume H: "\<forall>m<n. \<forall>S \<subseteq> V. independent S \<longrightarrow> m = CARD('n) - card S \<longrightarrow>
-              (\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B)"
-    and sv: "S \<subseteq> V" and i: "independent S" and n: "n = CARD('n) - card S"
+proof(induct "CARD('n) - card S" arbitrary: S rule: less_induct)
+  case less
+  note sv = `S \<subseteq> V` and i = `independent S`
   let ?P = "\<lambda>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
   let ?ths = "\<exists>x. ?P x"
   let ?d = "CARD('n)"
@@ -3674,11 +3664,11 @@
     have th0: "insert a S \<subseteq> V" using a sv by blast
     from independent_insert[of a S]  i a
     have th1: "independent (insert a S)" by auto
-    have mlt: "?d - card (insert a S) < n"
-      using aS a n independent_bound[OF th1]
+    have mlt: "?d - card (insert a S) < ?d - card S"
+      using aS a independent_bound[OF th1]
       by auto
 
-    from H[rule_format, OF mlt th0 th1 refl]
+    from less(1)[OF mlt th0 th1]
     obtain B where B: "insert a S \<subseteq> B" "B \<subseteq> V" "independent B" " V \<subseteq> span B"
       by blast
     from B have "?P B" by auto
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Nominal/Examples/Class.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -15069,11 +15069,9 @@
   assumes a: "(M[a\<turnstile>c>b]) \<longrightarrow>\<^isub>a M'" "a\<noteq>b"
   shows "\<exists>M0. M0[a\<turnstile>c>b]=M' \<and> M \<longrightarrow>\<^isub>a M0"
 using a
-apply(nominal_induct M\<equiv>"M[a\<turnstile>c>b]" M' avoiding: M a b rule: a_redu.strong_induct)
-apply(simp)
+apply(nominal_induct "M[a\<turnstile>c>b]" M' avoiding: M a b rule: a_redu.strong_induct)
 apply(drule  crename_lredu)
 apply(blast)
-apply(simp)
 apply(drule  crename_credu)
 apply(blast)
 (* Cut *)
@@ -16132,11 +16130,9 @@
   assumes a: "(M[x\<turnstile>n>y]) \<longrightarrow>\<^isub>a M'" "x\<noteq>y"
   shows "\<exists>M0. M0[x\<turnstile>n>y]=M' \<and> M \<longrightarrow>\<^isub>a M0"
 using a
-apply(nominal_induct M\<equiv>"M[x\<turnstile>n>y]" M' avoiding: M x y rule: a_redu.strong_induct)
-apply(simp)
+apply(nominal_induct "M[x\<turnstile>n>y]" M' avoiding: M x y rule: a_redu.strong_induct)
 apply(drule  nrename_lredu)
 apply(blast)
-apply(simp)
 apply(drule  nrename_credu)
 apply(blast)
 (* Cut *)
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -982,19 +982,18 @@
     from `(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N` 
       and `\<Gamma> \<turnstile> P<:Q` 
     show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> M <: N" 
-    proof (induct \<Gamma>\<equiv>"\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct) 
-      case (SA_Top _ S \<Gamma> X \<Delta>)
-      then have lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" 
-        and lh_drv_prm\<^isub>2: "S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
-      have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
-      hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
-      with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: replace_type)
+    proof (induct "\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct) 
+      case (SA_Top S \<Gamma> X \<Delta>)
+      from `\<Gamma> \<turnstile> P <: Q`
+      have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
+      with `\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok` have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
+        by (simp add: replace_type)
       moreover
-      from lh_drv_prm\<^isub>2 have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)" 
+      from `S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)` have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)" 
         by (simp add: closed_in_def doms_append)
       ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.SA_Top)
     next
-      case (SA_trans_TVar Y S _ N \<Gamma> X \<Delta>) 
+      case (SA_trans_TVar Y S N \<Gamma> X \<Delta>) 
       then have IH_inner: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N"
         and lh_drv_prm: "(TVarB Y S) \<in> set (\<Delta>@[(TVarB X Q)]@\<Gamma>)"
         and rh_drv: "\<Gamma> \<turnstile> P<:Q"
@@ -1020,23 +1019,23 @@
         then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by auto
       qed
     next
-      case (SA_refl_TVar _ Y \<Gamma> X \<Delta>)
-      then have lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" 
-        and lh_drv_prm\<^isub>2: "Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
-      have "\<Gamma> \<turnstile> P <: Q" by fact
-      hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
-      with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: replace_type)
+      case (SA_refl_TVar Y \<Gamma> X \<Delta>)
+      from `\<Gamma> \<turnstile> P <: Q`
+      have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
+      with `\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok` have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
+        by (simp add: replace_type)
       moreover
-      from lh_drv_prm\<^isub>2 have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)" by (simp add: doms_append)
+      from `Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)` have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)"
+        by (simp add: doms_append)
       ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.SA_refl_TVar)
     next
-      case (SA_arrow _ S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \<Gamma> X \<Delta>) 
+      case (SA_arrow S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \<Gamma> X \<Delta>) 
       then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2" by blast 
     next
-      case (SA_all _ T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Gamma> X \<Delta>)
-      from SA_all(2,4,5,6)
+      case (SA_all T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Gamma> X \<Delta>)
       have IH_inner\<^isub>1: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1" 
-        and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" by force+
+        and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"
+        by (fastsimp intro: SA_all)+
       then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^isub>1. S\<^isub>2) <: (\<forall>Y<:T\<^isub>1. T\<^isub>2)" by auto
     qed
   } 
@@ -1263,7 +1262,7 @@
   assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok"
   shows "\<turnstile> (\<Gamma> @ \<Delta>) ok"
   using assms
-proof (induct  \<Gamma>' \<equiv> "\<Gamma> @ VarB x Q # \<Delta>" arbitrary: \<Gamma> \<Delta>)
+proof (induct "\<Gamma> @ VarB x Q # \<Delta>" arbitrary: \<Gamma> \<Delta>)
   case valid_nil
   have "[] = \<Gamma> @ VarB x Q # \<Delta>" by fact
   then have "False" by auto
@@ -1314,14 +1313,14 @@
   and     "\<turnstile> (\<Delta> @ B # \<Gamma>) ok"
   shows   "(\<Delta> @ B # \<Gamma>) \<turnstile> t : T"
 using assms
-proof(nominal_induct \<Gamma>'\<equiv> "\<Delta> @ \<Gamma>" t T avoiding: \<Delta> \<Gamma> B rule: typing.strong_induct)
-  case (T_Var x' T \<Gamma>' \<Gamma>'' \<Delta>')
+proof(nominal_induct "\<Delta> @ \<Gamma>" t T avoiding: \<Delta> \<Gamma> B rule: typing.strong_induct)
+  case (T_Var x T)
   then show ?case by auto
 next
-  case (T_App \<Gamma> t\<^isub>1 T\<^isub>1 T\<^isub>2 t\<^isub>2 \<Gamma> \<Delta>)
+  case (T_App X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
   then show ?case by force
 next
-  case (T_Abs y T\<^isub>1 \<Gamma>' t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
+  case (T_Abs y T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
   then have "VarB y T\<^isub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
   then have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
     by (auto dest: typing_ok)
@@ -1336,22 +1335,22 @@
     apply (rule closed)
     done
   then have "\<turnstile> ((VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
-  then have "(VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
-    by (rule T_Abs) (simp add: T_Abs)
+  with _ have "(VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
+    by (rule T_Abs) simp
   then have "VarB y T\<^isub>1 # \<Delta> @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
   then show ?case by (rule typing.T_Abs)
 next
-  case (T_Sub \<Gamma>' t S T \<Delta> \<Gamma>)
-  from `\<turnstile> (\<Delta> @ B # \<Gamma>) ok` and `\<Gamma>' = \<Delta> @ \<Gamma>`
+  case (T_Sub t S T \<Delta> \<Gamma>)
+  from refl and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
   have "\<Delta> @ B # \<Gamma> \<turnstile> t : S" by (rule T_Sub)
-  moreover from  `\<Gamma>'\<turnstile>S<:T` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
+  moreover from  `(\<Delta> @ \<Gamma>)\<turnstile>S<:T` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
   have "(\<Delta> @ B # \<Gamma>)\<turnstile>S<:T"
     by (rule weakening) (simp add: extends_def T_Sub)
   ultimately show ?case by (rule typing.T_Sub)
 next
-  case (T_TAbs X T\<^isub>1 \<Gamma>' t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
-  then have "TVarB X T\<^isub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
-  then have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
+  case (T_TAbs X T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
+  from `TVarB X T\<^isub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2`
+  have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
     by (auto dest: typing_ok)
   have "\<turnstile> (TVarB X T\<^isub>1 # \<Delta> @ B # \<Gamma>) ok"
     apply (rule valid_consT)
@@ -1364,15 +1363,15 @@
     apply (rule closed)
     done
   then have "\<turnstile> ((TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
-  then have "(TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
-    by (rule T_TAbs) (simp add: T_TAbs)
+  with _ have "(TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
+    by (rule T_TAbs) simp
   then have "TVarB X T\<^isub>1 # \<Delta> @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
   then show ?case by (rule typing.T_TAbs)
 next
-  case (T_TApp X \<Gamma>' t\<^isub>1 T2 T11 T12 \<Delta> \<Gamma>)
+  case (T_TApp X t\<^isub>1 T2 T11 T12 \<Delta> \<Gamma>)
   have "\<Delta> @ B # \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T11. T12)"
-    by (rule T_TApp)+
-  moreover from `\<Gamma>'\<turnstile>T2<:T11` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
+    by (rule T_TApp refl)+
+  moreover from `(\<Delta> @ \<Gamma>)\<turnstile>T2<:T11` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
   have "(\<Delta> @ B # \<Gamma>)\<turnstile>T2<:T11"
     by (rule weakening) (simp add: extends_def T_TApp)
   ultimately show ?case by (rule better_T_TApp)
@@ -1393,24 +1392,22 @@
   assumes "(\<Gamma> @ VarB x Q # \<Delta>) \<turnstile> S <: T"
   shows  "(\<Gamma>@\<Delta>) \<turnstile> S <: T"
   using assms
-proof (induct  \<Gamma>' \<equiv> "\<Gamma> @ VarB x Q # \<Delta>" S T arbitrary: \<Gamma>)
-  case (SA_Top G' S G)
-  then have "\<turnstile> (G @ \<Delta>) ok" by (auto dest: valid_cons')
-  moreover have "S closed_in (G @ \<Delta>)" using SA_Top by (auto dest: closed_in_cons)
+proof (induct "\<Gamma> @ VarB x Q # \<Delta>" S T arbitrary: \<Gamma>)
+  case (SA_Top S)
+  then have "\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons')
+  moreover have "S closed_in (\<Gamma> @ \<Delta>)" using SA_Top by (auto dest: closed_in_cons)
   ultimately show ?case using subtype_of.SA_Top by auto
 next
-  case (SA_refl_TVar G X' G')
-  then have "\<turnstile> (G' @ VarB x Q # \<Delta>) ok" by simp
-  then have h1:"\<turnstile> (G' @ \<Delta>) ok" by (auto dest: valid_cons')
-  have "X' \<in> ty_dom (G' @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
-  then have h2:"X' \<in> ty_dom (G' @ \<Delta>)" using ty_dom_vrs by auto
+  case (SA_refl_TVar X)
+  from `\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok`
+  have h1:"\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons')
+  have "X \<in> ty_dom (\<Gamma> @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
+  then have h2:"X \<in> ty_dom (\<Gamma> @ \<Delta>)" using ty_dom_vrs by auto
   show ?case using h1 h2 by auto
 next
-  case (SA_all G T1 S1 X S2 T2 G')
-  have ih1:"TVarB X T1 # G = (TVarB X T1 # G') @ VarB x Q # \<Delta> \<Longrightarrow> ((TVarB X T1 # G') @ \<Delta>)\<turnstile>S2<:T2" by fact
-  then have h1:"(TVarB X T1 # (G' @ \<Delta>))\<turnstile>S2<:T2" using SA_all by auto
-  have ih2:"G = G' @ VarB x Q # \<Delta> \<Longrightarrow> (G' @ \<Delta>)\<turnstile>T1<:S1" by fact
-  then have h2:"(G' @ \<Delta>)\<turnstile>T1<:S1" using SA_all by auto
+  case (SA_all T1 S1 X S2 T2)
+  have h1:"((TVarB X T1 # \<Gamma>) @ \<Delta>)\<turnstile>S2<:T2" by (fastsimp intro: SA_all)
+  have h2:"(\<Gamma> @ \<Delta>)\<turnstile>T1<:S1" using SA_all by auto
   then show ?case using h1 h2 by auto
 qed (auto)
 
@@ -1418,26 +1415,26 @@
   assumes H: "\<Delta> @ (TVarB X Q) # \<Gamma> \<turnstile> t : T"
   shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> \<Delta> @ (TVarB X P) # \<Gamma> \<turnstile> t : T"
   using H
-  proof (nominal_induct \<Gamma>' \<equiv> "\<Delta> @ (TVarB X Q) # \<Gamma>" t T avoiding: P arbitrary: \<Delta> rule: typing.strong_induct)
-    case (T_Var x T G P D)
+  proof (nominal_induct "\<Delta> @ (TVarB X Q) # \<Gamma>" t T avoiding: P arbitrary: \<Delta> rule: typing.strong_induct)
+    case (T_Var x T P D)
     then have "VarB x T \<in> set (D @ TVarB X P # \<Gamma>)" 
       and "\<turnstile>  (D @ TVarB X P # \<Gamma>) ok"
       by (auto intro: replace_type dest!: subtype_implies_closed)
     then show ?case by auto
   next
-    case (T_App G t1 T1 T2 t2 P D)
+    case (T_App t1 T1 T2 t2 P D)
     then show ?case by force
   next
-    case (T_Abs x T1 G t2 T2 P D)
+    case (T_Abs x T1 t2 T2 P D)
     then show ?case by (fastsimp dest: typing_ok)
   next
-    case (T_Sub G t S T D)
+    case (T_Sub t S T P D)
     then show ?case using subtype_narrow by fastsimp
   next
-    case (T_TAbs X' T1 G t2 T2 P D)
+    case (T_TAbs X' T1 t2 T2 P D)
     then show ?case by (fastsimp dest: typing_ok)
   next
-    case (T_TApp X' G t1 T2 T11 T12 P D)
+    case (T_TApp X' t1 T2 T11 T12 P D)
     then have "D @ TVarB X P # \<Gamma> \<turnstile> t1 : Forall X' T12 T11" by fastsimp
     moreover have "(D @ [TVarB X Q] @ \<Gamma>) \<turnstile> T2<:T11" using T_TApp by auto
     then have "(D @ [TVarB X P] @ \<Gamma>) \<turnstile> T2<:T11" using `\<Gamma>\<turnstile>P<:Q`
@@ -1454,8 +1451,8 @@
 theorem subst_type: -- {* A.8 *}
   assumes H: "(\<Delta> @ (VarB x U) # \<Gamma>) \<turnstile> t : T"
   shows "\<Gamma> \<turnstile> u : U \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t[x \<mapsto> u] : T" using H
- proof (nominal_induct \<Gamma>' \<equiv> "\<Delta> @ (VarB x U) # \<Gamma>" t T avoiding: x u arbitrary: \<Delta> rule: typing.strong_induct)
-   case (T_Var y T G x u D)
+ proof (nominal_induct "\<Delta> @ (VarB x U) # \<Gamma>" t T avoiding: x u arbitrary: \<Delta> rule: typing.strong_induct)
+   case (T_Var y T x u D)
    show ?case
    proof (cases "x = y")
      assume eq:"x=y"
@@ -1468,23 +1465,23 @@
        by (auto simp add:binding.inject dest: valid_cons')
    qed
  next
-   case (T_App G t1 T1 T2 t2 x u D)
+   case (T_App t1 T1 T2 t2 x u D)
    then show ?case by force
  next
-   case (T_Abs y T1 G t2 T2 x u D)
+   case (T_Abs y T1 t2 T2 x u D)
    then show ?case by force
  next
-   case (T_Sub G t S T x u D)
+   case (T_Sub t S T x u D)
    then have "D @ \<Gamma> \<turnstile> t[x \<mapsto> u] : S" by auto
    moreover have "(D @ \<Gamma>) \<turnstile> S<:T" using T_Sub by (auto dest: strengthening)
    ultimately show ?case by auto 
  next
-   case (T_TAbs X T1 G t2 T2 x u D)
-   from `TVarB X T1 # G \<turnstile> t2 : T2` have "X \<sharp> T1"
+   case (T_TAbs X T1 t2 T2 x u D)
+   from `TVarB X T1 # D @ VarB x U # \<Gamma> \<turnstile> t2 : T2` have "X \<sharp> T1"
      by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh)
    with `X \<sharp> u` and T_TAbs show ?case by fastsimp
  next
-   case (T_TApp X G t1 T2 T11 T12 x u D)
+   case (T_TApp X t1 T2 T11 T12 x u D)
    then have "(D@\<Gamma>) \<turnstile>T2<:T11" using T_TApp by (auto dest: strengthening)
    then show "((D @ \<Gamma>) \<turnstile> ((t1 \<cdot>\<^sub>\<tau> T2)[x \<mapsto> u]) : (T12[X \<mapsto> T2]\<^sub>\<tau>))" using T_TApp
      by (force simp add: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar)
@@ -1496,8 +1493,8 @@
   assumes H: "(\<Delta> @ ((TVarB X Q) # \<Gamma>)) \<turnstile> S <: T"
   shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> (\<Delta>[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>" 
   using H
-proof (nominal_induct \<Gamma>' \<equiv> "\<Delta> @ TVarB X Q # \<Gamma>" S T avoiding: X P arbitrary: \<Delta> rule: subtype_of.strong_induct)
-  case (SA_Top G S X P D)
+proof (nominal_induct "\<Delta> @ TVarB X Q # \<Gamma>" S T avoiding: X P arbitrary: \<Delta> rule: subtype_of.strong_induct)
+  case (SA_Top S X P D)
   then have "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by simp
   moreover have closed: "P closed_in \<Gamma>" using SA_Top subtype_implies_closed by auto 
   ultimately have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule valid_subst)
@@ -1505,17 +1502,18 @@
   then have "S[X \<mapsto> P]\<^sub>\<tau> closed_in  (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" using closed by (rule subst_closed_in)
   ultimately show ?case by auto
 next
-  case (SA_trans_TVar Y S G T X P D)
-  have h:"G\<turnstile>S<:T" by fact
+  case (SA_trans_TVar Y S T X P D)
+  have h:"(D @ TVarB X Q # \<Gamma>)\<turnstile>S<:T" by fact
   then have ST: "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>" using SA_trans_TVar by auto
-  from `G\<turnstile>S<:T` have G_ok: "\<turnstile> G ok" by (rule subtype_implies_ok)
+  from h have G_ok: "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by (rule subtype_implies_ok)
   from G_ok and SA_trans_TVar have X\<Gamma>_ok: "\<turnstile> (TVarB X Q # \<Gamma>) ok"
     by (auto intro: validE_append)
   show "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> Tvar Y[X \<mapsto> P]\<^sub>\<tau><:T[X \<mapsto> P]\<^sub>\<tau>"
   proof (cases "X = Y")
     assume eq: "X = Y"
-    from eq and SA_trans_TVar have "TVarB Y Q \<in> set G" by simp
-    with G_ok have QS: "Q = S" using `TVarB Y S \<in> set G` by (rule uniqueness_of_ctxt)
+    from eq and SA_trans_TVar have "TVarB Y Q \<in> set (D @ TVarB X Q # \<Gamma>)" by simp
+    with G_ok have QS: "Q = S" using `TVarB Y S \<in> set (D @ TVarB X Q # \<Gamma>)`
+      by (rule uniqueness_of_ctxt)
     from X\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto
     then have XQ: "X \<sharp> Q" by (rule closed_in_fresh)
     note `\<Gamma>\<turnstile>P<:Q`
@@ -1552,8 +1550,8 @@
     qed
   qed
 next
-  case (SA_refl_TVar G Y X P D)
-  then have "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by simp
+  case (SA_refl_TVar Y X P D)
+  note `\<turnstile> (D @ TVarB X Q # \<Gamma>) ok`
   moreover from SA_refl_TVar have closed: "P closed_in \<Gamma>"
     by (auto dest: subtype_implies_closed)
   ultimately have ok: "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using valid_subst by auto
@@ -1571,12 +1569,12 @@
     with neq and ok show ?thesis by auto
   qed
 next
-  case (SA_arrow G T1 S1 S2 T2 X P D)
+  case (SA_arrow T1 S1 S2 T2 X P D)
   then have h1:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>T1[X \<mapsto> P]\<^sub>\<tau><:S1[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto
   from SA_arrow have h2:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S2[X \<mapsto> P]\<^sub>\<tau><:T2[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto
   show ?case using subtype_of.SA_arrow h1 h2 by auto
 next
-  case (SA_all G T1 S1 Y S2 T2 X P D)
+  case (SA_all T1 S1 Y S2 T2 X P D)
   then have Y: "Y \<sharp> ty_dom (D @ TVarB X Q # \<Gamma>)"
     by (auto dest: subtype_implies_ok intro: fresh_dom)
   moreover from SA_all have "S1 closed_in (D @ TVarB X Q # \<Gamma>)"
@@ -1594,13 +1592,13 @@
   assumes H: "(D @ TVarB X Q # G) \<turnstile> t : T"
   shows "G \<turnstile> P <: Q \<Longrightarrow>
     (D[X \<mapsto> P]\<^sub>e @ G) \<turnstile> t[X \<mapsto>\<^sub>\<tau> P] : T[X \<mapsto> P]\<^sub>\<tau>" using H
-proof (nominal_induct \<Gamma>'\<equiv>"(D @ TVarB X Q # G)" t T avoiding: X P arbitrary: D rule: typing.strong_induct)
-  case (T_Var x T G' X P D')
+proof (nominal_induct "D @ TVarB X Q # G" t T avoiding: X P arbitrary: D rule: typing.strong_induct)
+  case (T_Var x T X P D')
   have "G\<turnstile>P<:Q" by fact
   then have "P closed_in G" using subtype_implies_closed by auto
-  moreover have "\<turnstile> (D' @ TVarB X Q # G) ok" using T_Var by auto
+  moreover note `\<turnstile> (D' @ TVarB X Q # G) ok`
   ultimately have "\<turnstile> (D'[X \<mapsto> P]\<^sub>e @ G) ok" using valid_subst by auto
-  moreover have "VarB x T \<in> set (D' @ TVarB X Q # G)" using T_Var by auto
+  moreover note `VarB x T \<in> set (D' @ TVarB X Q # G)`
   then have "VarB x T \<in> set D' \<or> VarB x T \<in> set G" by simp
   then have "(VarB x (T[X \<mapsto> P]\<^sub>\<tau>)) \<in> set (D'[X \<mapsto> P]\<^sub>e @ G)"
   proof
@@ -1621,25 +1619,25 @@
   qed
   ultimately show ?case by auto
 next
-  case (T_App G' t1 T1 T2 t2 X P D')
+  case (T_App t1 T1 T2 t2 X P D')
   then have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t1[X \<mapsto>\<^sub>\<tau> P] : (T1 \<rightarrow> T2)[X \<mapsto> P]\<^sub>\<tau>" by auto
   moreover from T_App have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t2[X \<mapsto>\<^sub>\<tau> P] : T1[X \<mapsto> P]\<^sub>\<tau>" by auto
   ultimately show ?case by auto
 next
-  case (T_Abs x T1 G' t2 T2 X P D')
+  case (T_Abs x T1 t2 T2 X P D')
   then show ?case by force
 next
-  case (T_Sub G' t S T X P D')
+  case (T_Sub t S T X P D')
   then show ?case using substT_subtype by force
 next
-  case (T_TAbs X' G' T1 t2 T2 X P D')
+  case (T_TAbs X' T1 t2 T2 X P D')
   then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)"
-  and "G' closed_in (D' @ TVarB X Q # G)"
+  and "T1 closed_in (D' @ TVarB X Q # G)"
     by (auto dest: typing_ok)
-  then have "X' \<sharp> G'" by (rule closed_in_fresh)
+  then have "X' \<sharp> T1" by (rule closed_in_fresh)
   with T_TAbs show ?case by force
 next
-  case (T_TApp X' G' t1 T2 T11 T12 X P D')
+  case (T_TApp X' t1 T2 T11 T12 X P D')
   then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)"
     by (simp add: fresh_dom)
   moreover from T_TApp have "T11 closed_in (D' @ TVarB X Q # G)"
@@ -1824,22 +1822,22 @@
 lemma Fun_canonical: -- {* A.14(1) *}
   assumes ty: "[] \<turnstile> v : T\<^isub>1 \<rightarrow> T\<^isub>2"
   shows "val v \<Longrightarrow> \<exists>x t S. v = (\<lambda>x:S. t)" using ty
-proof (induct \<Gamma>\<equiv>"[]::env" v T\<equiv>"T\<^isub>1 \<rightarrow> T\<^isub>2" arbitrary: T\<^isub>1 T\<^isub>2)
-  case (T_Sub \<Gamma> t S T)
-  hence "\<Gamma> \<turnstile> S <: T\<^isub>1 \<rightarrow> T\<^isub>2" by simp
-  then obtain S\<^isub>1 S\<^isub>2 where S: "S = S\<^isub>1 \<rightarrow> S\<^isub>2" 
+proof (induct "[]::env" v "T\<^isub>1 \<rightarrow> T\<^isub>2" arbitrary: T\<^isub>1 T\<^isub>2)
+  case (T_Sub t S)
+  from `[] \<turnstile> S <: T\<^isub>1 \<rightarrow> T\<^isub>2`
+  obtain S\<^isub>1 S\<^isub>2 where S: "S = S\<^isub>1 \<rightarrow> S\<^isub>2" 
     by cases (auto simp add: T_Sub)
-  with `val t` and `\<Gamma> = []` show ?case by (rule T_Sub)
+  then show ?case using `val t` by (rule T_Sub)
 qed (auto)
 
 lemma TyAll_canonical: -- {* A.14(3) *}
   fixes X::tyvrs
   assumes ty: "[] \<turnstile> v : (\<forall>X<:T\<^isub>1. T\<^isub>2)"
   shows "val v \<Longrightarrow> \<exists>X t S. v = (\<lambda>X<:S. t)" using ty
-proof (induct \<Gamma>\<equiv>"[]::env" v T\<equiv>"\<forall>X<:T\<^isub>1. T\<^isub>2" arbitrary: X T\<^isub>1 T\<^isub>2)
-  case (T_Sub  \<Gamma> t S T)
-  hence "\<Gamma> \<turnstile> S <: (\<forall>X<:T\<^isub>1. T\<^isub>2)" by simp
-  then obtain X S\<^isub>1 S\<^isub>2 where S: "S = (\<forall>X<:S\<^isub>1. S\<^isub>2)"
+proof (induct "[]::env" v "\<forall>X<:T\<^isub>1. T\<^isub>2" arbitrary: X T\<^isub>1 T\<^isub>2)
+  case (T_Sub t S)
+  from `[] \<turnstile> S <: (\<forall>X<:T\<^isub>1. T\<^isub>2)`
+  obtain X S\<^isub>1 S\<^isub>2 where S: "S = (\<forall>X<:S\<^isub>1. S\<^isub>2)"
     by cases (auto simp add: T_Sub)
   then show ?case using T_Sub by auto 
 qed (auto)
@@ -1848,8 +1846,8 @@
   assumes "[] \<turnstile> t : T"
   shows "val t \<or> (\<exists>t'. t \<longmapsto> t')" 
 using assms
-proof (induct \<Gamma> \<equiv> "[]::env" t T)
-  case (T_App \<Gamma> t\<^isub>1 T\<^isub>1\<^isub>1  T\<^isub>1\<^isub>2 t\<^isub>2)
+proof (induct "[]::env" t T)
+  case (T_App t\<^isub>1 T\<^isub>1\<^isub>1  T\<^isub>1\<^isub>2 t\<^isub>2)
   hence "val t\<^isub>1 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
   thus ?case
   proof
@@ -1875,7 +1873,7 @@
     thus ?case by auto
   qed
 next
-  case (T_TApp X \<Gamma> t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
+  case (T_TApp X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
   hence "val t\<^isub>1 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
   thus ?case
   proof
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -410,37 +410,34 @@
   and b: "\<Gamma> \<turnstile> u : U"
   shows "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" using a b
 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, U)] @ \<Gamma>" t T avoiding: x u \<Delta> rule: typing.strong_induct)
-  case (Var \<Gamma>' y T x u \<Delta>)
-  then have a1: "valid (\<Delta> @ [(x, U)] @ \<Gamma>)" 
-       and  a2: "(y, T) \<in> set (\<Delta> @ [(x, U)] @ \<Gamma>)" 
-       and  a3: "\<Gamma> \<turnstile> u : U" by simp_all
-  from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
+  case (Var y T x u \<Delta>)
+  from `valid (\<Delta> @ [(x, U)] @ \<Gamma>)`
+  have valid: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
   show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T"
   proof cases
     assume eq: "x = y"
-    from a1 a2 have "T = U" using eq by (auto intro: context_unique)
-    with a3 show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using eq a4 by (auto intro: weakening)
+    from Var eq have "T = U" by (auto intro: context_unique)
+    with Var eq valid show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" by (auto intro: weakening)
   next
     assume ineq: "x \<noteq> y"
-    from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
-    then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq a4 by auto
+    from Var ineq have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" by simp
+    then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq valid by auto
   qed
 next
-  case (Tuple \<Gamma>' t\<^isub>1 T\<^isub>1 t\<^isub>2 T\<^isub>2)
-  from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
+  case (Tuple t\<^isub>1 T\<^isub>1 t\<^isub>2 T\<^isub>2)
+  from refl `\<Gamma> \<turnstile> u : U`
   have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>1[x\<mapsto>u] : T\<^isub>1" by (rule Tuple)
-  moreover from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
+  moreover from refl `\<Gamma> \<turnstile> u : U`
   have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>2[x\<mapsto>u] : T\<^isub>2" by (rule Tuple)
   ultimately have "\<Delta> @ \<Gamma> \<turnstile> \<langle>t\<^isub>1[x\<mapsto>u], t\<^isub>2[x\<mapsto>u]\<rangle> : T\<^isub>1 \<otimes> T\<^isub>2" ..
   then show ?case by simp
 next
-  case (Let p t \<Gamma>' T \<Delta>' s S)
-  from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
+  case (Let p t T \<Delta>' s S)
+  from refl `\<Gamma> \<turnstile> u : U`
   have "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" by (rule Let)
   moreover note `\<turnstile> p : T \<Rightarrow> \<Delta>'`
-  moreover from `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
-  have "\<Delta>' @ \<Gamma>' = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp
-  with `\<Gamma> \<turnstile> u : U` have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by (rule Let)
+  moreover have "\<Delta>' @ (\<Delta> @ [(x, U)] @ \<Gamma>) = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp
+  then have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" using `\<Gamma> \<turnstile> u : U` by (rule Let)
   then have "\<Delta>' @ \<Delta> @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by simp
   ultimately have "\<Delta> @ \<Gamma> \<turnstile> (LET p = t[x\<mapsto>u] IN s[x\<mapsto>u]) : S"
     by (rule better_T_Let)
@@ -448,10 +445,10 @@
     by (simp add: fresh_star_def fresh_list_nil fresh_list_cons)
   ultimately show ?case by simp
 next
-  case (Abs y T \<Gamma>' t S)
-  from `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` have "(y, T) # \<Gamma>' = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>"
+  case (Abs y T t S)
+  have "(y, T) # \<Delta> @ [(x, U)] @ \<Gamma> = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>"
     by simp
-  with `\<Gamma> \<turnstile> u : U` have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by (rule Abs)
+  then have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" using `\<Gamma> \<turnstile> u : U` by (rule Abs)
   then have "(y, T) # \<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by simp
   then have "\<Delta> @ \<Gamma> \<turnstile> (\<lambda>y:T. t[x\<mapsto>u]) : T \<rightarrow> S"
     by (rule typing.Abs)
@@ -459,10 +456,10 @@
     by (simp add: fresh_list_nil fresh_list_cons)
   ultimately show ?case by simp
 next
-  case (App \<Gamma>' t\<^isub>1 T S t\<^isub>2)
-  from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
+  case (App t\<^isub>1 T S t\<^isub>2)
+  from refl `\<Gamma> \<turnstile> u : U`
   have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>1[x\<mapsto>u] : T \<rightarrow> S" by (rule App)
-  moreover from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
+  moreover from refl `\<Gamma> \<turnstile> u : U`
   have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>2[x\<mapsto>u] : T" by (rule App)
   ultimately have "\<Delta> @ \<Gamma> \<turnstile> (t\<^isub>1[x\<mapsto>u]) \<cdot> (t\<^isub>2[x\<mapsto>u]) : S"
     by (rule typing.App)
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Nominal/Examples/SOS.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -220,10 +220,10 @@
   shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 
 using a b 
 proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: e' \<Delta> rule: typing.strong_induct)
-  case (t_Var \<Gamma>' y T e' \<Delta>)
+  case (t_Var y T e' \<Delta>)
   then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 
        and  a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 
-       and  a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
+       and  a3: "\<Gamma> \<turnstile> e' : T'" .
   from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
   { assume eq: "x=y"
     from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -233,37 +233,39 @@
   with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
 qed
 
-lemma ind_euclid: 
-  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
-  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
+lemma ind_euclid:
+  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
+  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
   shows "P a b"
-proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
-  fix n a b
-  assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
+proof(induct "a + b" arbitrary: a b rule: less_induct)
+  case less
   have "a = b \<or> a < b \<or> b < a" by arith
   moreover {assume eq: "a= b"
-    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp}
+    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
+    by simp}
   moreover
   {assume lt: "a < b"
-    hence "a + b - a < n \<or> a = 0"  using H(2) by arith
+    hence "a + b - a < a + b \<or> a = 0" by arith
     moreover
     {assume "a =0" with z c have "P a b" by blast }
     moreover
-    {assume ab: "a + b - a < n"
-      have th0: "a + b - a = a + (b - a)" using lt by arith
-      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
-      have "P a b" by (simp add: th0[symmetric])}
+    {assume "a + b - a < a + b"
+      also have th0: "a + b - a = a + (b - a)" using lt by arith
+      finally have "a + (b - a) < a + b" .
+      then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
+      then have "P a b" by (simp add: th0[symmetric])}
     ultimately have "P a b" by blast}
   moreover
   {assume lt: "a > b"
-    hence "b + a - b < n \<or> b = 0"  using H(2) by arith
+    hence "b + a - b < a + b \<or> b = 0" by arith
     moreover
     {assume "b =0" with z c have "P a b" by blast }
     moreover
-    {assume ab: "b + a - b < n"
-      have th0: "b + a - b = b + (a - b)" using lt by arith
-      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
-      have "P b a" by (simp add: th0[symmetric])
+    {assume "b + a - b < a + b"
+      also have th0: "b + a - b = b + (a - b)" using lt by arith
+      finally have "b + (a - b) < a + b" .
+      then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
+      then have "P b a" by (simp add: th0[symmetric])
       hence "P a b" using c by blast }
     ultimately have "P a b" by blast}
 ultimately  show "P a b" by blast
diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOL/ex/ThreeDivides.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -178,21 +178,17 @@
 
 lemma exp_exists:
   "m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)"
-proof (induct nd \<equiv> "nlen m" arbitrary: m)
+proof (induct "nlen m" arbitrary: m)
   case 0 thus ?case by (simp add: nlen_zero)
 next
   case (Suc nd)
-  hence IH:
-    "nd = nlen (m div 10) \<Longrightarrow>
-    m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
-    by blast
   obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10"
     and cdef: "c = m mod 10" by simp
   show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)"
   proof -
     from `Suc nd = nlen m`
     have "nd = nlen (m div 10)" by (rule nlen_suc)
-    with IH have
+    with Suc have
       "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)" by simp
     with mexp have
       "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
diff -r e391c3de0f6b -r 7894c7dab132 src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Sun Jan 10 18:41:07 2010 +0100
+++ b/src/HOLCF/Universal.thy	Sun Jan 10 18:43:45 2010 +0100
@@ -694,13 +694,8 @@
 
 lemma basis_emb_mono:
   "x \<sqsubseteq> y \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)"
-proof (induct n \<equiv> "max (place x) (place y)" arbitrary: x y rule: less_induct)
-  case (less n)
-  hence IH:
-    "\<And>(a::'a compact_basis) b.
-     \<lbrakk>max (place a) (place b) < max (place x) (place y); a \<sqsubseteq> b\<rbrakk>
-        \<Longrightarrow> ubasis_le (basis_emb a) (basis_emb b)"
-    by simp
+proof (induct "max (place x) (place y)" arbitrary: x y rule: less_induct)
+  case less
   show ?case proof (rule linorder_cases)
     assume "place x < place y"
     then have "rank x < rank y"
@@ -709,7 +704,7 @@
       apply (case_tac "y = compact_bot", simp)
       apply (simp add: basis_emb.simps [of y])
       apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]])
-      apply (rule IH)
+      apply (rule less)
        apply (simp add: less_max_iff_disj)
        apply (erule place_sub_less)
       apply (erule rank_less_imp_below_sub [OF `x \<sqsubseteq> y`])
@@ -724,7 +719,7 @@
       apply (case_tac "x = compact_bot", simp add: ubasis_le_minimal)
       apply (simp add: basis_emb.simps [of x])
       apply (rule ubasis_le_upper [OF fin2], simp)
-      apply (rule IH)
+      apply (rule less)
        apply (simp add: less_max_iff_disj)
        apply (erule place_sub_less)
       apply (erule rev_below_trans)