merged
authorberghofe
Fri Jan 15 14:43:00 2010 +0100 (2010-01-15)
changeset 3491751829fe604a7
parent 34906 bb9dad7de515
parent 34916 f625d8d6fcf3
child 34918 81c7ec7c1b91
merged
src/HOL/Code_Numeral.thy
src/HOL/HOL.thy
src/HOL/List.thy
     1.1 --- a/src/FOL/FOL.thy	Fri Jan 15 08:27:21 2010 +0100
     1.2 +++ b/src/FOL/FOL.thy	Fri Jan 15 14:43:00 2010 +0100
     1.3 @@ -383,6 +383,8 @@
     1.4      val atomize = @{thms induct_atomize}
     1.5      val rulify = @{thms induct_rulify}
     1.6      val rulify_fallback = @{thms induct_rulify_fallback}
     1.7 +    fun dest_def _ = NONE
     1.8 +    fun trivial_tac _ = no_tac
     1.9    );
    1.10  *}
    1.11  
     2.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Jan 15 08:27:21 2010 +0100
     2.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Jan 15 14:43:00 2010 +0100
     2.3 @@ -1581,14 +1581,10 @@
     2.4      {
     2.5        (*JE: we now apply the induction hypothesis with some additional facts required*)
     2.6        from f_in_P deg_g_le_deg_f show ?thesis
     2.7 -      proof (induct n \<equiv> "deg R f" arbitrary: "f" rule: nat_less_induct)
     2.8 -        fix n f
     2.9 -        assume hypo: "\<forall>m<n. \<forall>x. x \<in> carrier P \<longrightarrow>
    2.10 -          deg R g \<le> deg R x \<longrightarrow> 
    2.11 -          m = deg R x \<longrightarrow>
    2.12 -          (\<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))"
    2.13 -          and prem: "n = deg R f" and f_in_P [simp]: "f \<in> carrier P"
    2.14 -          and deg_g_le_deg_f: "deg R g \<le> deg R f"
    2.15 +      proof (induct "deg R f" arbitrary: "f" rule: less_induct)
    2.16 +        case less
    2.17 +        note f_in_P [simp] = `f \<in> carrier P`
    2.18 +          and deg_g_le_deg_f = `deg R g \<le> deg R f`
    2.19          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)"
    2.20            and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
    2.21          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)"
    2.22 @@ -1631,13 +1627,13 @@
    2.23                  {
    2.24                    (*JE: now it only remains the case where the induction hypothesis can be used.*)
    2.25                    (*JE: we first prove that the degree of the remainder is smaller than the one of f*)
    2.26 -                  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n"
    2.27 +                  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f"
    2.28                    proof -
    2.29                      have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
    2.30                      also have "\<dots> < deg R f"
    2.31                      proof (rule deg_lcoeff_cancel)
    2.32                        show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
    2.33 -                        using deg_smult_ring [of "lcoeff g" f] using prem
    2.34 +                        using deg_smult_ring [of "lcoeff g" f]
    2.35                          using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
    2.36                        show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
    2.37                          using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f
    2.38 @@ -1651,7 +1647,7 @@
    2.39                          using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
    2.40                          unfolding Pi_def using deg_g_le_deg_f by force
    2.41                      qed (simp_all add: deg_f_nzero)
    2.42 -                    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n" unfolding prem .
    2.43 +                    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R f" .
    2.44                    qed
    2.45                    moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
    2.46                    moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
    2.47 @@ -1660,7 +1656,7 @@
    2.48                    ultimately obtain q' r' k'
    2.49                      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)"
    2.50                      and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
    2.51 -                    using hypo by blast
    2.52 +                    using less by blast
    2.53                        (*JE: we now prove that the new quotient, remainder and exponent can be used to get 
    2.54                        the quotient, remainder and exponent of the long division theorem*)
    2.55                    show ?thesis
     3.1 --- a/src/HOL/Bali/Basis.thy	Fri Jan 15 08:27:21 2010 +0100
     3.2 +++ b/src/HOL/Bali/Basis.thy	Fri Jan 15 14:43:00 2010 +0100
     3.3 @@ -1,7 +1,5 @@
     3.4  (*  Title:      HOL/Bali/Basis.thy
     3.5 -    ID:         $Id$
     3.6      Author:     David von Oheimb
     3.7 -
     3.8  *)
     3.9  header {* Definitions extending HOL as logical basis of Bali *}
    3.10  
    3.11 @@ -66,8 +64,6 @@
    3.12   "\<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> 
    3.13   \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    3.14  proof -
    3.15 -  note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
    3.16 -  note converse_rtranclE = converse_rtranclE [consumes 1] 
    3.17    assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
    3.18    assume "(a,x)\<in>r\<^sup>*" 
    3.19    then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    3.20 @@ -110,13 +106,6 @@
    3.21  apply (auto dest: rtrancl_into_trancl1)
    3.22  done
    3.23  
    3.24 -(* ### To Transitive_Closure *)
    3.25 -theorems converse_rtrancl_induct 
    3.26 - = converse_rtrancl_induct [consumes 1,case_names Id Step]
    3.27 -
    3.28 -theorems converse_trancl_induct 
    3.29 -         = converse_trancl_induct [consumes 1,case_names Single Step]
    3.30 -
    3.31  (* context (theory "Set") *)
    3.32  lemma Ball_weaken:"\<lbrakk>Ball s P;\<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q"
    3.33  by auto
     4.1 --- a/src/HOL/Bali/DeclConcepts.thy	Fri Jan 15 08:27:21 2010 +0100
     4.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Fri Jan 15 14:43:00 2010 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/Bali/DeclConcepts.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Norbert Schirmer
     4.7  *)
     4.8  header {* Advanced concepts on Java declarations like overriding, inheritance,
     4.9 @@ -2282,74 +2281,47 @@
    4.10  done
    4.11  
    4.12  lemma superclasses_mono:
    4.13 -"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
    4.14 -  \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc;
    4.15 -  x\<in>superclasses G D 
    4.16 -\<rbrakk> \<Longrightarrow> x\<in>superclasses G C" 
    4.17 -proof -
    4.18 -  
    4.19 -  assume     ws: "ws_prog G"          and 
    4.20 -          cls_C: "class G C = Some c" and
    4.21 -             wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
    4.22 -                  \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
    4.23 -  assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"           
    4.24 -  thus "\<And> c. \<lbrakk>class G C = Some c; x\<in>superclasses G D\<rbrakk>\<Longrightarrow>
    4.25 -        x\<in>superclasses G C" (is "PROP ?P C"  
    4.26 -                             is "\<And> c. ?CLS C c \<Longrightarrow> ?SUP D \<Longrightarrow> ?SUP C")
    4.27 -  proof (induct ?P C  rule: converse_trancl_induct)
    4.28 -    fix C c
    4.29 -    assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1D" "class G C = Some c" "x \<in> superclasses G D"
    4.30 -    with wf ws show "?SUP C"
    4.31 -      by (auto    intro: no_subcls1_Object 
    4.32 -               simp add: superclasses_rec subcls1_def)
    4.33 -  next
    4.34 -    fix C S c
    4.35 -    assume clsrel': "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S \<prec>\<^sub>C D"
    4.36 -       and    hyp : "\<And> s. \<lbrakk>class G S = Some s; x \<in> superclasses G D\<rbrakk>
    4.37 -                           \<Longrightarrow> x \<in> superclasses G S"
    4.38 -       and  cls_C': "class G C = Some c"
    4.39 -       and       x: "x \<in> superclasses G D"
    4.40 -    moreover note wf ws
    4.41 -    moreover from calculation 
    4.42 -    have "?SUP S" 
    4.43 -      by (force intro: no_subcls1_Object simp add: subcls1_def)
    4.44 -    moreover from calculation 
    4.45 -    have "super c = S" 
    4.46 -      by (auto intro: no_subcls1_Object simp add: subcls1_def)
    4.47 -    ultimately show "?SUP C" 
    4.48 -      by (auto intro: no_subcls1_Object simp add: superclasses_rec)
    4.49 -  qed
    4.50 +  assumes clsrel: "G\<turnstile>C\<prec>\<^sub>C D"
    4.51 +  and ws: "ws_prog G"
    4.52 +  and cls_C: "class G C = Some c"
    4.53 +  and wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
    4.54 +    \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
    4.55 +  and x: "x\<in>superclasses G D"
    4.56 +  shows "x\<in>superclasses G C" using clsrel cls_C x
    4.57 +proof (induct arbitrary: c rule: converse_trancl_induct)
    4.58 +  case (base C)
    4.59 +  with wf ws show ?case
    4.60 +    by (auto    intro: no_subcls1_Object 
    4.61 +             simp add: superclasses_rec subcls1_def)
    4.62 +next
    4.63 +  case (step C S)
    4.64 +  moreover note wf ws
    4.65 +  moreover from calculation 
    4.66 +  have "x\<in>superclasses G S"
    4.67 +    by (force intro: no_subcls1_Object simp add: subcls1_def)
    4.68 +  moreover from calculation 
    4.69 +  have "super c = S" 
    4.70 +    by (auto intro: no_subcls1_Object simp add: subcls1_def)
    4.71 +  ultimately show ?case 
    4.72 +    by (auto intro: no_subcls1_Object simp add: superclasses_rec)
    4.73  qed
    4.74  
    4.75  lemma subclsEval:
    4.76 -"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
    4.77 -  \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc 
    4.78 - \<rbrakk> \<Longrightarrow> D\<in>superclasses G C" 
    4.79 -proof -
    4.80 -  note converse_trancl_induct 
    4.81 -       = converse_trancl_induct [consumes 1,case_names Single Step]
    4.82 -  assume 
    4.83 -             ws: "ws_prog G"          and 
    4.84 -          cls_C: "class G C = Some c" and
    4.85 -             wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
    4.86 -                  \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
    4.87 -  assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"           
    4.88 -  thus "\<And> c. class G C = Some c\<Longrightarrow> D\<in>superclasses G C" 
    4.89 -    (is "PROP ?P C"  is "\<And> c. ?CLS C c  \<Longrightarrow> ?SUP C")
    4.90 -  proof (induct ?P C  rule: converse_trancl_induct)
    4.91 -    fix C c
    4.92 -    assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" "class G C = Some c"
    4.93 -    with ws wf show "?SUP C"
    4.94 -      by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def)
    4.95 -  next
    4.96 -    fix C S c
    4.97 -    assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S\<prec>\<^sub>C D" 
    4.98 -           "\<And>s. class G S = Some s \<Longrightarrow> D \<in> superclasses G S"
    4.99 -           "class G C = Some c" 
   4.100 -    with ws wf show "?SUP C"
   4.101 -      by - (rule superclasses_mono,
   4.102 -            auto dest: no_subcls1_Object simp add: subcls1_def )
   4.103 -  qed
   4.104 +  assumes clsrel: "G\<turnstile>C\<prec>\<^sub>C D"
   4.105 +  and ws: "ws_prog G"
   4.106 +  and cls_C: "class G C = Some c"
   4.107 +  and wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
   4.108 +    \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
   4.109 +  shows "D\<in>superclasses G C" using clsrel cls_C
   4.110 +proof (induct arbitrary: c rule: converse_trancl_induct)
   4.111 +  case (base C)
   4.112 +  with ws wf show ?case
   4.113 +    by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def)
   4.114 +next
   4.115 +  case (step C S)
   4.116 +  with ws wf show ?case
   4.117 +    by - (rule superclasses_mono,
   4.118 +          auto dest: no_subcls1_Object simp add: subcls1_def )
   4.119  qed
   4.120  
   4.121  end
     5.1 --- a/src/HOL/Bali/WellForm.thy	Fri Jan 15 08:27:21 2010 +0100
     5.2 +++ b/src/HOL/Bali/WellForm.thy	Fri Jan 15 14:43:00 2010 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Bali/WellForm.thy
     5.5 -    ID:         $Id$
     5.6      Author:     David von Oheimb and Norbert Schirmer
     5.7  *)
     5.8  
     5.9 @@ -1409,8 +1408,7 @@
    5.10    from clsC ws 
    5.11    show "methd G C sig = Some m 
    5.12          \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
    5.13 -    (is "PROP ?P C") 
    5.14 -  proof (induct ?P C rule: ws_class_induct')
    5.15 +  proof (induct C rule: ws_class_induct')
    5.16      case Object
    5.17      assume "methd G Object sig = Some m" 
    5.18      with wf show ?thesis
    5.19 @@ -1755,28 +1753,20 @@
    5.20  lemma ballE': "\<forall>x\<in>A. P x \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> Q" by blast
    5.21  
    5.22  lemma subint_widen_imethds: 
    5.23 - "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow>   
    5.24 -  \<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and> 
    5.25 +  assumes irel: "G\<turnstile>I\<preceq>I J"
    5.26 +  and wf: "wf_prog G"
    5.27 +  and is_iface: "is_iface G J"
    5.28 +  and jm: "jm \<in> imethds G J sig"
    5.29 +  shows "\<exists>im \<in> imethds G I sig. is_static im = is_static jm \<and> 
    5.30                            accmodi im = accmodi jm \<and>
    5.31                            G\<turnstile>resTy im\<preceq>resTy jm"
    5.32 -proof -
    5.33 -  assume irel: "G\<turnstile>I\<preceq>I J" and
    5.34 -           wf: "wf_prog G" and
    5.35 -     is_iface: "is_iface G J"
    5.36 -  from irel show "jm \<in> imethds G J sig \<Longrightarrow> ?thesis" 
    5.37 -               (is "PROP ?P I" is "PROP ?Prem J \<Longrightarrow> ?Concl I")
    5.38 -  proof (induct ?P I rule: converse_rtrancl_induct) 
    5.39 -    case Id
    5.40 -    assume "jm \<in> imethds G J sig"
    5.41 -    then show "?Concl J" by  (blast elim: bexI')
    5.42 +  using irel jm
    5.43 +proof (induct rule: converse_rtrancl_induct)
    5.44 +    case base
    5.45 +    then show ?case by  (blast elim: bexI')
    5.46    next
    5.47 -    case Step
    5.48 -    fix I SI
    5.49 -    assume subint1_I_SI: "G\<turnstile>I \<prec>I1 SI" and 
    5.50 -            subint_SI_J: "G\<turnstile>SI \<preceq>I J" and
    5.51 -                    hyp: "PROP ?P SI" and
    5.52 -                     jm: "jm \<in> imethds G J sig"
    5.53 -    from subint1_I_SI 
    5.54 +    case (step I SI)
    5.55 +    from `G\<turnstile>I \<prec>I1 SI`
    5.56      obtain i where
    5.57        ifI: "iface G I = Some i" and
    5.58         SI: "SI \<in> set (isuperIfs i)"
    5.59 @@ -1784,10 +1774,10 @@
    5.60  
    5.61      let ?newMethods 
    5.62            = "(Option.set \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
    5.63 -    show "?Concl I"
    5.64 +    show ?case
    5.65      proof (cases "?newMethods sig = {}")
    5.66        case True
    5.67 -      with ifI SI hyp wf jm 
    5.68 +      with ifI SI step wf
    5.69        show "?thesis" 
    5.70          by (auto simp add: imethds_rec) 
    5.71      next
    5.72 @@ -1816,7 +1806,7 @@
    5.73          wf_SI: "wf_idecl G (SI,si)" 
    5.74          by (auto dest!: wf_idecl_supD is_acc_ifaceD
    5.75                    dest: wf_prog_idecl)
    5.76 -      from jm hyp 
    5.77 +      from step
    5.78        obtain sim::"qtname \<times> mhead"  where
    5.79                        sim: "sim \<in> imethds G SI sig" and
    5.80           eq_static_sim_jm: "is_static sim = is_static jm" and 
    5.81 @@ -1841,7 +1831,6 @@
    5.82        show ?thesis 
    5.83          by auto 
    5.84      qed
    5.85 -  qed
    5.86  qed
    5.87       
    5.88  (* Tactical version *)
    5.89 @@ -1974,30 +1963,20 @@
    5.90    from clsC ws 
    5.91    show "\<And> m d. \<lbrakk>methd G C sig = Some m; class G (declclass m) = Some d\<rbrakk>
    5.92          \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)" 
    5.93 -         (is "PROP ?P C") 
    5.94 -  proof (induct ?P C rule: ws_class_induct)
    5.95 +  proof (induct rule: ws_class_induct)
    5.96      case Object
    5.97 -    fix m d
    5.98 -    assume "methd G Object sig = Some m" 
    5.99 -           "class G (declclass m) = Some d"
   5.100      with wf show "?thesis m d" by auto
   5.101    next
   5.102 -    case Subcls
   5.103 -    fix C c m d
   5.104 -    assume hyp: "PROP ?P (super c)"
   5.105 -    and      m: "methd G C sig = Some m"
   5.106 -    and  declC: "class G (declclass m) = Some d"
   5.107 -    and   clsC: "class G C = Some c"
   5.108 -    and   nObj: "C \<noteq> Object"
   5.109 +    case (Subcls C c)
   5.110      let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig"
   5.111      show "?thesis m d" 
   5.112      proof (cases "?newMethods")
   5.113        case None
   5.114 -      from None clsC nObj ws m declC
   5.115 -      show "?thesis" by (auto simp add: methd_rec) (rule hyp)
   5.116 +      from None ws Subcls
   5.117 +      show "?thesis" by (auto simp add: methd_rec) (rule Subcls)
   5.118      next
   5.119        case Some
   5.120 -      from Some clsC nObj ws m declC
   5.121 +      from Some ws Subcls
   5.122        show "?thesis" 
   5.123          by (auto simp add: methd_rec
   5.124                       dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
     6.1 --- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Fri Jan 15 08:27:21 2010 +0100
     6.2 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Fri Jan 15 14:43:00 2010 +0100
     6.3 @@ -69,8 +69,9 @@
     6.4        |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #>
     6.5      Seq.maps (fn (names, st) =>
     6.6        CASES
     6.7 -        (Rule_Cases.make_common false
     6.8 -          (ProofContext.theory_of ctxt, Thm.prop_of st) names)
     6.9 +        (Rule_Cases.make_common
    6.10 +          (ProofContext.theory_of ctxt,
    6.11 +           Thm.prop_of (Rule_Cases.internalize_params st)) names)
    6.12          Tactical.all_tac st))
    6.13  in
    6.14  val setup_boogie_cases = Method.setup @{binding boogie_cases}
     7.1 --- a/src/HOL/Code_Numeral.thy	Fri Jan 15 08:27:21 2010 +0100
     7.2 +++ b/src/HOL/Code_Numeral.thy	Fri Jan 15 14:43:00 2010 +0100
     7.3 @@ -83,7 +83,7 @@
     7.4      then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
     7.5      then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
     7.6    from init step have "P (of_nat (nat_of k))"
     7.7 -    by (induct "nat_of k") simp_all
     7.8 +    by (induct ("nat_of k")) simp_all
     7.9    then show "P k" by simp
    7.10  qed simp_all
    7.11  
    7.12 @@ -100,7 +100,7 @@
    7.13    fix k
    7.14    have "code_numeral_size k = nat_size (nat_of k)"
    7.15      by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
    7.16 -  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
    7.17 +  also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all
    7.18    finally show "code_numeral_size k = nat_of k" .
    7.19  qed
    7.20  
     8.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Jan 15 08:27:21 2010 +0100
     8.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Jan 15 14:43:00 2010 +0100
     8.3 @@ -987,16 +987,14 @@
     8.4    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})"
     8.5    shows "p = 0\<^sub>p"
     8.6  using nq eq
     8.7 -proof (induct n\<equiv>"maxindex p" arbitrary: p n0 rule: nat_less_induct)
     8.8 -  fix n p n0
     8.9 -  assume H: "\<forall>m<n. \<forall>p n0. isnpolyh p n0 \<longrightarrow>
    8.10 -    (\<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"
    8.11 -    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"
    8.12 -  {assume nz: "n = 0"
    8.13 -    then obtain c where "p = C c" using n np by (cases p, auto)
    8.14 +proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
    8.15 +  case less
    8.16 +  note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)`
    8.17 +  {assume nz: "maxindex p = 0"
    8.18 +    then obtain c where "p = C c" using np by (cases p, auto)
    8.19      with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}
    8.20    moreover
    8.21 -  {assume nz: "n \<noteq> 0"
    8.22 +  {assume nz: "maxindex p \<noteq> 0"
    8.23      let ?h = "head p"
    8.24      let ?hd = "decrpoly ?h"
    8.25      let ?ihd = "maxindex ?hd"
    8.26 @@ -1005,24 +1003,23 @@
    8.27      hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast
    8.28      
    8.29      from maxindex_coefficients[of p] coefficients_head[of p, symmetric]
    8.30 -    have mihn: "maxindex ?h \<le> n" unfolding n by auto
    8.31 -    with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < n" by auto
    8.32 +    have mihn: "maxindex ?h \<le> maxindex p" by auto
    8.33 +    with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < maxindex p" by auto
    8.34      {fix bs:: "'a list"  assume bs: "wf_bs bs ?hd"
    8.35        let ?ts = "take ?ihd bs"
    8.36        let ?rs = "drop ?ihd bs"
    8.37        have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp
    8.38        have bs_ts_eq: "?ts@ ?rs = bs" by simp
    8.39        from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp
    8.40 -      from ihd_lt_n have "ALL x. length (x#?ts) \<le> n" by simp
    8.41 -      with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = n" by blast
    8.42 -      hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" using n unfolding wf_bs_def by simp
    8.43 +      from ihd_lt_n have "ALL x. length (x#?ts) \<le> maxindex p" by simp
    8.44 +      with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast
    8.45 +      hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp
    8.46        with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast
    8.47        hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp
    8.48        with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
    8.49        have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
    8.50        hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) 
    8.51        hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
    8.52 -        thm poly_zero
    8.53          using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
    8.54        with coefficients_head[of p, symmetric]
    8.55        have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
    8.56 @@ -1031,7 +1028,7 @@
    8.57        with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp }
    8.58      then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast
    8.59      
    8.60 -    from H[rule_format, OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
    8.61 +    from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
    8.62      hence "?h = 0\<^sub>p" by simp
    8.63      with head_nz[OF np] have "p = 0\<^sub>p" by simp}
    8.64    ultimately show "p = 0\<^sub>p" by blast
    8.65 @@ -1357,8 +1354,8 @@
    8.66    (polydivide_aux (a,n,p,k,s) = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p) 
    8.67            \<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)))"
    8.68    using ns
    8.69 -proof(induct d\<equiv>"degree s" arbitrary: s k k' r n1 rule: nat_less_induct)
    8.70 -  fix d s k k' r n1
    8.71 +proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
    8.72 +  case less
    8.73    let ?D = "polydivide_aux_dom"
    8.74    let ?dths = "?D (a, n, p, k, s)"
    8.75    let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
    8.76 @@ -1366,20 +1363,13 @@
    8.77      \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
    8.78    let ?ths = "?dths \<and> ?qrths"
    8.79    let ?b = "head s"
    8.80 -  let ?p' = "funpow (d - n) shift1 p"
    8.81 -  let ?xdn = "funpow (d - n) shift1 1\<^sub>p"
    8.82 +  let ?p' = "funpow (degree s - n) shift1 p"
    8.83 +  let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p"
    8.84    let ?akk' = "a ^\<^sub>p (k' - k)"
    8.85 -  assume H: "\<forall>m<d. \<forall>x xa xb xc xd.
    8.86 -    isnpolyh x xd \<longrightarrow>
    8.87 -    m = degree x \<longrightarrow> ?D (a, n, p, xa, x) \<and>
    8.88 -    (polydivide_aux (a, n, p, xa, x) = (xb, xc) \<longrightarrow>
    8.89 -    xa \<le> xb \<and> (degree xc = 0 \<or> degree xc < degree p) \<and> 
    8.90 -    (\<exists> nr. isnpolyh xc nr) \<and>
    8.91 -    (\<exists>q n1. isnpolyh q n1 \<and> a ^\<^sub>p xb - xa *\<^sub>p x = p *\<^sub>p q +\<^sub>p xc))"
    8.92 -    and ns: "isnpolyh s n1" and ds: "d = degree s"
    8.93 +  note ns = `isnpolyh s n1`
    8.94    from np have np0: "isnpolyh p 0" 
    8.95      using isnpolyh_mono[where n="n0" and n'="0" and p="p"]  by simp
    8.96 -  have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="d -n"] isnpoly_def by simp
    8.97 +  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
    8.98    have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp
    8.99    from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
   8.100    from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap 
   8.101 @@ -1391,31 +1381,31 @@
   8.102      hence ?ths using dom by blast}
   8.103    moreover
   8.104    {assume sz: "s \<noteq> 0\<^sub>p"
   8.105 -    {assume dn: "d < n"
   8.106 -      with sz ds  have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all) 
   8.107 -      from polydivide_aux.psimps[OF dom] sz dn ds
   8.108 +    {assume dn: "degree s < n"
   8.109 +      with sz have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all) 
   8.110 +      from polydivide_aux.psimps[OF dom] sz dn
   8.111        have "?qrths" using ns ndp np by auto (rule exI[where x="0\<^sub>p"],simp)
   8.112        with dom have ?ths by blast}
   8.113      moreover 
   8.114 -    {assume dn': "\<not> d < n" hence dn: "d \<ge> n" by arith
   8.115 +    {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith
   8.116        have degsp': "degree s = degree ?p'" 
   8.117 -        using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
   8.118 +        using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] by simp
   8.119        {assume ba: "?b = a"
   8.120          hence headsp': "head s = head ?p'" using ap headp' by simp
   8.121          have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
   8.122 -        from ds degree_polysub_samehead[OF ns np' headsp' degsp']
   8.123 -        have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
   8.124 +        from degree_polysub_samehead[OF ns np' headsp' degsp']
   8.125 +        have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
   8.126          moreover 
   8.127 -        {assume deglt:"degree (s -\<^sub>p ?p') < d"
   8.128 -          from  H[rule_format, OF deglt nr,simplified] 
   8.129 +        {assume deglt:"degree (s -\<^sub>p ?p') < degree s"
   8.130 +          from  less(1)[OF deglt nr] 
   8.131            have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast 
   8.132            have dom: ?dths apply (rule polydivide_aux_real_domintros) 
   8.133 -            using ba ds dn' domsp by simp_all
   8.134 -          from polydivide_aux.psimps[OF dom] sz dn' ba ds
   8.135 +            using ba dn' domsp by simp_all
   8.136 +          from polydivide_aux.psimps[OF dom] sz dn' ba
   8.137            have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
   8.138              by (simp add: Let_def)
   8.139            {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
   8.140 -            from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
   8.141 +            from less(1)[OF deglt nr, of k k' r]
   8.142                trans[OF eq[symmetric] h1]
   8.143              have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
   8.144                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
   8.145 @@ -1434,19 +1424,19 @@
   8.146                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
   8.147                by (simp add: ring_simps)
   8.148              hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   8.149 -              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p) 
   8.150 +              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p) 
   8.151                + Ipoly bs p * Ipoly bs q + Ipoly bs r"
   8.152                by (auto simp only: funpow_shift1_1) 
   8.153              hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   8.154 -              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p) 
   8.155 +              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p) 
   8.156                + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
   8.157              hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   8.158 -              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
   8.159 +              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
   8.160              with isnpolyh_unique[OF nakks' nqr']
   8.161              have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
   8.162 -              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
   8.163 +              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
   8.164              hence ?qths using nq'
   8.165 -              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
   8.166 +              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
   8.167                apply (rule_tac x="0" in exI) by simp
   8.168              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"
   8.169                by blast } hence ?qrths by blast
   8.170 @@ -1456,25 +1446,23 @@
   8.171            hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" 
   8.172              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   8.173            have dom: ?dths apply (rule polydivide_aux_real_domintros) 
   8.174 -            using ba ds dn' domsp by simp_all
   8.175 +            using ba dn' domsp by simp_all
   8.176            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}"]
   8.177            have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
   8.178            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
   8.179              by (simp only: funpow_shift1_1) simp
   8.180            hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
   8.181            {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
   8.182 -            from polydivide_aux.psimps[OF dom] sz dn' ba ds
   8.183 +            from polydivide_aux.psimps[OF dom] sz dn' ba
   8.184              have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
   8.185                by (simp add: Let_def)
   8.186              also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
   8.187              finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
   8.188 -            with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
   8.189 +            with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
   8.190                polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
   8.191                apply auto
   8.192                apply (rule exI[where x="?xdn"])        
   8.193 -              apply auto
   8.194 -              apply (rule polymul_commute)
   8.195 -              apply simp_all
   8.196 +              apply (auto simp add: polymul_commute[of p])
   8.197                done}
   8.198            with dom have ?ths by blast}
   8.199          ultimately have ?ths by blast }
   8.200 @@ -1488,31 +1476,30 @@
   8.201              polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
   8.202              funpow_shift1_nz[OF pnz] by simp_all
   8.203          from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
   8.204 -          polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
   8.205 +          polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="degree s - n"]
   8.206          have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" 
   8.207            using head_head[OF ns] funpow_shift1_head[OF np pnz]
   8.208              polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
   8.209            by (simp add: ap)
   8.210          from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
   8.211            head_nz[OF np] pnz sz ap[symmetric]
   8.212 -          funpow_shift1_nz[OF pnz, where n="d - n"]
   8.213 +          funpow_shift1_nz[OF pnz, where n="degree s - n"]
   8.214            polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
   8.215 -          ndp ds[symmetric] dn
   8.216 +          ndp dn
   8.217          have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
   8.218            by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
   8.219 -        {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
   8.220 +        {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s"
   8.221            have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
   8.222 -            using H[rule_format, OF dth nth, simplified] by blast 
   8.223 -          have dom: ?dths
   8.224 -            using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)  
   8.225 -            using ba ds dn'  by simp_all
   8.226 +            using less(1)[OF dth nth] by blast 
   8.227 +          have dom: ?dths using ba dn' th
   8.228 +            by - (rule polydivide_aux_real_domintros, simp_all)
   8.229            from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
   8.230            ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
   8.231            {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
   8.232 -            from h1  polydivide_aux.psimps[OF dom] sz dn' ba ds
   8.233 +            from h1  polydivide_aux.psimps[OF dom] sz dn' ba
   8.234              have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
   8.235                by (simp add: Let_def)
   8.236 -            with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
   8.237 +            with less(1)[OF dth nasbp', of "Suc k" k' r]
   8.238              obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" 
   8.239                and dr: "degree r = 0 \<or> degree r < degree p"
   8.240                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
   8.241 @@ -1524,7 +1511,7 @@
   8.242              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"
   8.243                by (simp add: ring_simps power_Suc)
   8.244              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"
   8.245 -              by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
   8.246 +              by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
   8.247              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"
   8.248                by (simp add: ring_simps)}
   8.249              hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   8.250 @@ -1546,13 +1533,13 @@
   8.251          {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
   8.252            hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" 
   8.253              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   8.254 -          have dom: ?dths using sz ba dn' ds domsp 
   8.255 +          have dom: ?dths using sz ba dn' domsp 
   8.256              by - (rule polydivide_aux_real_domintros, simp_all)
   8.257            {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
   8.258              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
   8.259            have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
   8.260            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
   8.261 -            by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
   8.262 +            by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
   8.263            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
   8.264          }
   8.265          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))" ..
   8.266 @@ -1562,7 +1549,7 @@
   8.267                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
   8.268                simplified ap] by simp
   8.269            {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
   8.270 -          from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] 
   8.271 +          from h1 sz ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] 
   8.272            have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
   8.273            with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
   8.274              polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
   8.275 @@ -1573,7 +1560,7 @@
   8.276          hence ?qrths by blast
   8.277          with dom have ?ths by blast}
   8.278          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"]
   8.279 -          head_nz[OF np] pnz sz ap[symmetric] ds[symmetric] 
   8.280 +          head_nz[OF np] pnz sz ap[symmetric]
   8.281            by (simp add: degree_eq_degreen0[symmetric]) blast }
   8.282        ultimately have ?ths by blast
   8.283      }
     9.1 --- a/src/HOL/Extraction.thy	Fri Jan 15 08:27:21 2010 +0100
     9.2 +++ b/src/HOL/Extraction.thy	Fri Jan 15 14:43:00 2010 +0100
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      HOL/Extraction.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Stefan Berghofer, TU Muenchen
     9.7  *)
     9.8  
     9.9 @@ -28,11 +27,13 @@
    9.10    allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
    9.11    notE' impE' impE iffE imp_cong simp_thms eq_True eq_False
    9.12    induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
    9.13 -  induct_atomize induct_rulify induct_rulify_fallback
    9.14 +  induct_atomize induct_atomize' induct_rulify induct_rulify'
    9.15 +  induct_rulify_fallback induct_trueI
    9.16    True_implies_equals TrueE
    9.17  
    9.18  lemmas [extraction_expand_def] =
    9.19    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    9.20 +  induct_true_def induct_false_def
    9.21  
    9.22  datatype sumbool = Left | Right
    9.23  
    10.1 --- a/src/HOL/GCD.thy	Fri Jan 15 08:27:21 2010 +0100
    10.2 +++ b/src/HOL/GCD.thy	Fri Jan 15 14:43:00 2010 +0100
    10.3 @@ -16,7 +16,7 @@
    10.4  another extension of the notions to the integers, and added a number
    10.5  of results to "Primes" and "GCD". IntPrimes also defined and developed
    10.6  the congruence relations on the integers. The notion was extended to
    10.7 -the natural numbers by Chiaeb.
    10.8 +the natural numbers by Chaieb.
    10.9  
   10.10  Jeremy Avigad combined all of these, made everything uniform for the
   10.11  natural numbers and the integers, and added a number of new theorems.
   10.12 @@ -25,7 +25,7 @@
   10.13  *)
   10.14  
   10.15  
   10.16 -header {* Greates common divisor and least common multiple *}
   10.17 +header {* Greatest common divisor and least common multiple *}
   10.18  
   10.19  theory GCD
   10.20  imports Fact Parity
   10.21 @@ -1074,34 +1074,35 @@
   10.22    assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
   10.23    and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
   10.24    shows "P a b"
   10.25 -proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
   10.26 -  fix n a b
   10.27 -  assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
   10.28 +proof(induct "a + b" arbitrary: a b rule: less_induct)
   10.29 +  case less
   10.30    have "a = b \<or> a < b \<or> b < a" by arith
   10.31    moreover {assume eq: "a= b"
   10.32      from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
   10.33      by simp}
   10.34    moreover
   10.35    {assume lt: "a < b"
   10.36 -    hence "a + b - a < n \<or> a = 0"  using H(2) by arith
   10.37 +    hence "a + b - a < a + b \<or> a = 0" by arith
   10.38      moreover
   10.39      {assume "a =0" with z c have "P a b" by blast }
   10.40      moreover
   10.41 -    {assume ab: "a + b - a < n"
   10.42 -      have th0: "a + b - a = a + (b - a)" using lt by arith
   10.43 -      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
   10.44 -      have "P a b" by (simp add: th0[symmetric])}
   10.45 +    {assume "a + b - a < a + b"
   10.46 +      also have th0: "a + b - a = a + (b - a)" using lt by arith
   10.47 +      finally have "a + (b - a) < a + b" .
   10.48 +      then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
   10.49 +      then have "P a b" by (simp add: th0[symmetric])}
   10.50      ultimately have "P a b" by blast}
   10.51    moreover
   10.52    {assume lt: "a > b"
   10.53 -    hence "b + a - b < n \<or> b = 0"  using H(2) by arith
   10.54 +    hence "b + a - b < a + b \<or> b = 0" by arith
   10.55      moreover
   10.56      {assume "b =0" with z c have "P a b" by blast }
   10.57      moreover
   10.58 -    {assume ab: "b + a - b < n"
   10.59 -      have th0: "b + a - b = b + (a - b)" using lt by arith
   10.60 -      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
   10.61 -      have "P b a" by (simp add: th0[symmetric])
   10.62 +    {assume "b + a - b < a + b"
   10.63 +      also have th0: "b + a - b = b + (a - b)" using lt by arith
   10.64 +      finally have "b + (a - b) < a + b" .
   10.65 +      then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
   10.66 +      then have "P b a" by (simp add: th0[symmetric])
   10.67        hence "P a b" using c by blast }
   10.68      ultimately have "P a b" by blast}
   10.69  ultimately  show "P a b" by blast
    11.1 --- a/src/HOL/HOL.thy	Fri Jan 15 08:27:21 2010 +0100
    11.2 +++ b/src/HOL/HOL.thy	Fri Jan 15 14:43:00 2010 +0100
    11.3 @@ -1398,6 +1398,8 @@
    11.4    induct_implies where "induct_implies A B == A \<longrightarrow> B"
    11.5    induct_equal where "induct_equal x y == x = y"
    11.6    induct_conj where "induct_conj A B == A \<and> B"
    11.7 +  induct_true where "induct_true == True"
    11.8 +  induct_false where "induct_false == False"
    11.9  
   11.10  lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (\<lambda>x. P x))"
   11.11    by (unfold atomize_all induct_forall_def)
   11.12 @@ -1411,10 +1413,13 @@
   11.13  lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)"
   11.14    by (unfold atomize_conj induct_conj_def)
   11.15  
   11.16 -lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
   11.17 +lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
   11.18 +lemmas induct_atomize = induct_atomize' induct_equal_eq
   11.19 +lemmas induct_rulify' [symmetric, standard] = induct_atomize'
   11.20  lemmas induct_rulify [symmetric, standard] = induct_atomize
   11.21  lemmas induct_rulify_fallback =
   11.22    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
   11.23 +  induct_true_def induct_false_def
   11.24  
   11.25  
   11.26  lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
   11.27 @@ -1436,7 +1441,8 @@
   11.28  
   11.29  lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry
   11.30  
   11.31 -hide const induct_forall induct_implies induct_equal induct_conj
   11.32 +lemma induct_trueI: "induct_true"
   11.33 +  by (simp add: induct_true_def)
   11.34  
   11.35  text {* Method setup. *}
   11.36  
   11.37 @@ -1445,12 +1451,93 @@
   11.38  (
   11.39    val cases_default = @{thm case_split}
   11.40    val atomize = @{thms induct_atomize}
   11.41 -  val rulify = @{thms induct_rulify}
   11.42 +  val rulify = @{thms induct_rulify'}
   11.43    val rulify_fallback = @{thms induct_rulify_fallback}
   11.44 +  fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u)
   11.45 +    | dest_def _ = NONE
   11.46 +  val trivial_tac = match_tac @{thms induct_trueI}
   11.47  )
   11.48  *}
   11.49  
   11.50 -setup Induct.setup
   11.51 +setup {*
   11.52 +  Induct.setup #>
   11.53 +  Context.theory_map (Induct.map_simpset (fn ss => ss
   11.54 +    setmksimps (Simpdata.mksimps Simpdata.mksimps_pairs #>
   11.55 +      map (Simplifier.rewrite_rule (map Thm.symmetric
   11.56 +        @{thms induct_rulify_fallback induct_true_def induct_false_def})))
   11.57 +    addsimprocs
   11.58 +      [Simplifier.simproc @{theory} "swap_induct_false"
   11.59 +         ["induct_false ==> PROP P ==> PROP Q"]
   11.60 +         (fn _ => fn _ =>
   11.61 +            (fn _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
   11.62 +                  if P <> Q then SOME Drule.swap_prems_eq else NONE
   11.63 +              | _ => NONE)),
   11.64 +       Simplifier.simproc @{theory} "induct_equal_conj_curry"
   11.65 +         ["induct_conj P Q ==> PROP R"]
   11.66 +         (fn _ => fn _ =>
   11.67 +            (fn _ $ (_ $ P) $ _ =>
   11.68 +                let
   11.69 +                  fun is_conj (@{const induct_conj} $ P $ Q) =
   11.70 +                        is_conj P andalso is_conj Q
   11.71 +                    | is_conj (Const (@{const_name induct_equal}, _) $ _ $ _) = true
   11.72 +                    | is_conj @{const induct_true} = true
   11.73 +                    | is_conj @{const induct_false} = true
   11.74 +                    | is_conj _ = false
   11.75 +                in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
   11.76 +              | _ => NONE))]))
   11.77 +*}
   11.78 +
   11.79 +text {* Pre-simplification of induction and cases rules *}
   11.80 +
   11.81 +lemma [induct_simp]: "(!!x. induct_equal x t ==> PROP P x) == PROP P t"
   11.82 +  unfolding induct_equal_def
   11.83 +proof
   11.84 +  assume R: "!!x. x = t ==> PROP P x"
   11.85 +  show "PROP P t" by (rule R [OF refl])
   11.86 +next
   11.87 +  fix x assume "PROP P t" "x = t"
   11.88 +  then show "PROP P x" by simp
   11.89 +qed
   11.90 +
   11.91 +lemma [induct_simp]: "(!!x. induct_equal t x ==> PROP P x) == PROP P t"
   11.92 +  unfolding induct_equal_def
   11.93 +proof
   11.94 +  assume R: "!!x. t = x ==> PROP P x"
   11.95 +  show "PROP P t" by (rule R [OF refl])
   11.96 +next
   11.97 +  fix x assume "PROP P t" "t = x"
   11.98 +  then show "PROP P x" by simp
   11.99 +qed
  11.100 +
  11.101 +lemma [induct_simp]: "(induct_false ==> P) == Trueprop induct_true"
  11.102 +  unfolding induct_false_def induct_true_def
  11.103 +  by (iprover intro: equal_intr_rule)
  11.104 +
  11.105 +lemma [induct_simp]: "(induct_true ==> PROP P) == PROP P"
  11.106 +  unfolding induct_true_def
  11.107 +proof
  11.108 +  assume R: "True \<Longrightarrow> PROP P"
  11.109 +  from TrueI show "PROP P" by (rule R)
  11.110 +next
  11.111 +  assume "PROP P"
  11.112 +  then show "PROP P" .
  11.113 +qed
  11.114 +
  11.115 +lemma [induct_simp]: "(PROP P ==> induct_true) == Trueprop induct_true"
  11.116 +  unfolding induct_true_def
  11.117 +  by (iprover intro: equal_intr_rule)
  11.118 +
  11.119 +lemma [induct_simp]: "(!!x. induct_true) == Trueprop induct_true"
  11.120 +  unfolding induct_true_def
  11.121 +  by (iprover intro: equal_intr_rule)
  11.122 +
  11.123 +lemma [induct_simp]: "induct_implies induct_true P == P"
  11.124 +  by (simp add: induct_implies_def induct_true_def)
  11.125 +
  11.126 +lemma [induct_simp]: "(x = x) = True" 
  11.127 +  by (rule simp_thms)
  11.128 +
  11.129 +hide const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
  11.130  
  11.131  use "~~/src/Tools/induct_tacs.ML"
  11.132  setup InductTacs.setup
    12.1 --- a/src/HOL/Induct/Common_Patterns.thy	Fri Jan 15 08:27:21 2010 +0100
    12.2 +++ b/src/HOL/Induct/Common_Patterns.thy	Fri Jan 15 14:43:00 2010 +0100
    12.3 @@ -73,7 +73,7 @@
    12.4    show "P (a x)" sorry
    12.5  next
    12.6    case (Suc n)
    12.7 -  note hyp = `\<And>x. A (a x) \<Longrightarrow> n = a x \<Longrightarrow> P (a x)`
    12.8 +  note hyp = `\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)`
    12.9      and prem = `A (a x)`
   12.10      and defn = `Suc n = a x`
   12.11    show "P (a x)" sorry
    13.1 --- a/src/HOL/Isar_Examples/Puzzle.thy	Fri Jan 15 08:27:21 2010 +0100
    13.2 +++ b/src/HOL/Isar_Examples/Puzzle.thy	Fri Jan 15 14:43:00 2010 +0100
    13.3 @@ -22,17 +22,16 @@
    13.4  proof (rule order_antisym)
    13.5    {
    13.6      fix n show "n \<le> f n"
    13.7 -    proof (induct k \<equiv> "f n" arbitrary: n rule: less_induct)
    13.8 -      case (less k n)
    13.9 -      then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)
   13.10 +    proof (induct "f n" arbitrary: n rule: less_induct)
   13.11 +      case less
   13.12        show "n \<le> f n"
   13.13        proof (cases n)
   13.14          case (Suc m)
   13.15          from f_ax have "f (f m) < f n" by (simp only: Suc)
   13.16 -        with hyp have "f m \<le> f (f m)" .
   13.17 +        with less have "f m \<le> f (f m)" .
   13.18          also from f_ax have "\<dots> < f n" by (simp only: Suc)
   13.19          finally have "f m < f n" .
   13.20 -        with hyp have "m \<le> f m" .
   13.21 +        with less have "m \<le> f m" .
   13.22          also note `\<dots> < f n`
   13.23          finally have "m < f n" .
   13.24          then have "n \<le> f n" by (simp only: Suc)
    14.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Jan 15 08:27:21 2010 +0100
    14.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Jan 15 14:43:00 2010 +0100
    14.3 @@ -621,19 +621,18 @@
    14.4      done
    14.5  qed
    14.6  
    14.7 -text{* Fundamental theorem of algebral *}
    14.8 +text{* Fundamental theorem of algebra *}
    14.9  
   14.10  lemma fundamental_theorem_of_algebra:
   14.11    assumes nc: "~constant(poly p)"
   14.12    shows "\<exists>z::complex. poly p z = 0"
   14.13  using nc
   14.14 -proof(induct n\<equiv> "psize p" arbitrary: p rule: nat_less_induct)
   14.15 -  fix n fix p :: "complex poly"
   14.16 +proof(induct "psize p" arbitrary: p rule: less_induct)
   14.17 +  case less
   14.18    let ?p = "poly p"
   14.19 -  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"
   14.20    let ?ths = "\<exists>z. ?p z = 0"
   14.21  
   14.22 -  from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n)
   14.23 +  from nonconstant_length[OF less(2)] have n2: "psize p \<ge> 2" .
   14.24    from poly_minimum_modulus obtain c where
   14.25      c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)" by blast
   14.26    {assume pc: "?p c = 0" hence ?ths by blast}
   14.27 @@ -649,7 +648,7 @@
   14.28            using h unfolding constant_def by blast
   14.29          also have "\<dots> = ?p y" using th by auto
   14.30          finally have "?p x = ?p y" .}
   14.31 -      with nc have False unfolding constant_def by blast }
   14.32 +      with less(2) have False unfolding constant_def by blast }
   14.33      hence qnc: "\<not> constant (poly q)" by blast
   14.34      from q(2) have pqc0: "?p c = poly q 0" by simp
   14.35      from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp
   14.36 @@ -682,8 +681,8 @@
   14.37      from poly_decompose[OF rnc] obtain k a s where
   14.38        kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r"
   14.39        "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
   14.40 -    {assume "k + 1 = n"
   14.41 -      with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto
   14.42 +    {assume "psize p = k + 1"
   14.43 +      with kas(3) lgqr[symmetric] q(1) have s0:"s=0" by auto
   14.44        {fix w
   14.45          have "cmod (poly ?r w) = cmod (1 + a * w ^ k)"
   14.46            using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)}
   14.47 @@ -691,15 +690,15 @@
   14.48          from reduce_poly_simple[OF kas(1,2)]
   14.49        have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
   14.50      moreover
   14.51 -    {assume kn: "k+1 \<noteq> n"
   14.52 -      from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp
   14.53 +    {assume kn: "psize p \<noteq> k+1"
   14.54 +      from kn kas(3) q(1) lgqr have k1n: "k + 1 < psize p" by simp
   14.55        have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
   14.56          unfolding constant_def poly_pCons poly_monom
   14.57          using kas(1) apply simp
   14.58          by (rule exI[where x=0], rule exI[where x=1], simp)
   14.59        from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))"
   14.60          by (simp add: psize_def degree_monom_eq)
   14.61 -      from H[rule_format, OF k1n th01 th02]
   14.62 +      from less(1) [OF k1n [simplified th02] th01]
   14.63        obtain w where w: "1 + w^k * a = 0"
   14.64          unfolding poly_pCons poly_monom
   14.65          using kas(2) by (cases k, auto simp add: algebra_simps)
    15.1 --- a/src/HOL/Library/Polynomial.thy	Fri Jan 15 08:27:21 2010 +0100
    15.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Jan 15 14:43:00 2010 +0100
    15.3 @@ -1384,7 +1384,7 @@
    15.4      with k have "degree p = Suc (degree k)"
    15.5        by (simp add: degree_mult_eq del: mult_pCons_left)
    15.6      with `Suc n = degree p` have "n = degree k" by simp
    15.7 -    with `k \<noteq> 0` have "finite {x. poly k x = 0}" by (rule Suc.hyps)
    15.8 +    then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
    15.9      then have "finite (insert a {x. poly k x = 0})" by simp
   15.10      then show "finite {x. poly p x = 0}"
   15.11        by (simp add: k uminus_add_conv_diff Collect_disj_eq
    16.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Fri Jan 15 08:27:21 2010 +0100
    16.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Fri Jan 15 14:43:00 2010 +0100
    16.3 @@ -17,11 +17,11 @@
    16.4    assume "r\<^sup>*\<^sup>* x y"
    16.5    then show "\<exists>xs. rtrancl_path r x xs y"
    16.6    proof (induct rule: converse_rtranclp_induct)
    16.7 -    case 1
    16.8 +    case base
    16.9      have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
   16.10      then show ?case ..
   16.11    next
   16.12 -    case (2 x z)
   16.13 +    case (step x z)
   16.14      from `\<exists>xs. rtrancl_path r z xs y`
   16.15      obtain xs where "rtrancl_path r z xs y" ..
   16.16      with `r x z` have "rtrancl_path r x (z # xs) y"
    17.1 --- a/src/HOL/Library/Word.thy	Fri Jan 15 08:27:21 2010 +0100
    17.2 +++ b/src/HOL/Library/Word.thy	Fri Jan 15 14:43:00 2010 +0100
    17.3 @@ -436,7 +436,7 @@
    17.4        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"
    17.5        proof -
    17.6          have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
    17.7 -          by (induct "length xs",simp_all)
    17.8 +          by (induct ("length xs")) simp_all
    17.9          hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
   17.10            bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
   17.11            by simp
   17.12 @@ -2165,13 +2165,13 @@
   17.13    apply (simp add: bv_extend_def)
   17.14    apply (subst bv_to_nat_dist_append)
   17.15    apply simp
   17.16 -  apply (induct "n - length w")
   17.17 +  apply (induct ("n - length w"))
   17.18     apply simp_all
   17.19    done
   17.20  
   17.21  lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
   17.22    apply (simp add: bv_extend_def)
   17.23 -  apply (induct "n - length w")
   17.24 +  apply (cases "n - length w")
   17.25     apply simp_all
   17.26    done
   17.27  
   17.28 @@ -2188,7 +2188,7 @@
   17.29    show ?thesis
   17.30      apply (simp add: bv_to_int_def)
   17.31      apply (simp add: bv_extend_def)
   17.32 -    apply (induct "n - length w",simp_all)
   17.33 +    apply (induct ("n - length w"), simp_all)
   17.34      done
   17.35  qed
   17.36  
    18.1 --- a/src/HOL/List.thy	Fri Jan 15 08:27:21 2010 +0100
    18.2 +++ b/src/HOL/List.thy	Fri Jan 15 14:43:00 2010 +0100
    18.3 @@ -578,13 +578,13 @@
    18.4  apply fastsimp
    18.5  done
    18.6  
    18.7 -lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"
    18.8 +lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"
    18.9  by simp
   18.10  
   18.11  lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"
   18.12  by simp
   18.13  
   18.14 -lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)"
   18.15 +lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)"
   18.16  by simp
   18.17  
   18.18  lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"
    19.1 --- a/src/HOL/MicroJava/BV/EffectMono.thy	Fri Jan 15 08:27:21 2010 +0100
    19.2 +++ b/src/HOL/MicroJava/BV/EffectMono.thy	Fri Jan 15 14:43:00 2010 +0100
    19.3 @@ -15,12 +15,13 @@
    19.4  
    19.5  lemma sup_loc_some [rule_format]:
    19.6  "\<forall>y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = OK t \<longrightarrow> 
    19.7 -  (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
    19.8 -proof (induct ?P b)
    19.9 -  show "?P []" by simp
   19.10 +  (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))"
   19.11 +proof (induct b)
   19.12 +  case Nil
   19.13 +  show ?case by simp
   19.14  next
   19.15    case (Cons a list)
   19.16 -  show "?P (a#list)" 
   19.17 +  show ?case 
   19.18    proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def)
   19.19      fix z zs n
   19.20      assume *: 
   19.21 @@ -60,13 +61,14 @@
   19.22   
   19.23  
   19.24  lemma append_length_n [rule_format]: 
   19.25 -"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
   19.26 -proof (induct ?P x)
   19.27 -  show "?P []" by simp
   19.28 +"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)"
   19.29 +proof (induct x)
   19.30 +  case Nil
   19.31 +  show ?case by simp
   19.32  next
   19.33 -  fix l ls assume Cons: "?P ls"
   19.34 +  case (Cons l ls)
   19.35  
   19.36 -  show "?P (l#ls)"
   19.37 +  show ?case
   19.38    proof (intro allI impI)
   19.39      fix n
   19.40      assume l: "n \<le> length (l # ls)"
    20.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 15 08:27:21 2010 +0100
    20.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 15 14:43:00 2010 +0100
    20.3 @@ -170,8 +170,8 @@
    20.4    next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s)
    20.5        case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real"
    20.6        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;
    20.7 -               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
    20.8 -        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"
    20.9 +               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
   20.10 +        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"
   20.11             "finite s" "s \<noteq> {}" "s \<subseteq> V" "setsum u s = 1"
   20.12        have "\<exists>x\<in>s. u x \<noteq> 1" proof(rule_tac ccontr)
   20.13          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
   20.14 @@ -1345,7 +1345,7 @@
   20.15  next
   20.16    case False then obtain w where "w\<in>s" by auto
   20.17    show ?thesis unfolding caratheodory[of s]
   20.18 -  proof(induct "CARD('n) + 1")
   20.19 +  proof(induct ("CARD('n) + 1"))
   20.20      have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}" 
   20.21        using compact_empty by (auto simp add: convex_hull_empty)
   20.22      case 0 thus ?case unfolding * by simp
    21.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Jan 15 08:27:21 2010 +0100
    21.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Jan 15 14:43:00 2010 +0100
    21.3 @@ -3542,17 +3542,9 @@
    21.4    and sp:"s \<subseteq> span t"
    21.5    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'"
    21.6  using f i sp
    21.7 -proof(induct c\<equiv>"card(t - s)" arbitrary: s t rule: nat_less_induct)
    21.8 -  fix n:: nat and s t :: "('a ^'n) set"
    21.9 -  assume H: " \<forall>m<n. \<forall>(x:: ('a ^'n) set) xa.
   21.10 -                finite xa \<longrightarrow>
   21.11 -                independent x \<longrightarrow>
   21.12 -                x \<subseteq> span xa \<longrightarrow>
   21.13 -                m = card (xa - x) \<longrightarrow>
   21.14 -                (\<exists>t'. (card t' = card xa) \<and> finite t' \<and>
   21.15 -                      x \<subseteq> t' \<and> t' \<subseteq> x \<union> xa \<and> x \<subseteq> span t')"
   21.16 -    and ft: "finite t" and s: "independent s" and sp: "s \<subseteq> span t"
   21.17 -    and n: "n = card (t - s)"
   21.18 +proof(induct "card (t - s)" arbitrary: s t rule: less_induct)
   21.19 +  case less
   21.20 +  note ft = `finite t` and s = `independent s` and sp = `s \<subseteq> span t`
   21.21    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'"
   21.22    let ?ths = "\<exists>t'. ?P t'"
   21.23    {assume st: "s \<subseteq> t"
   21.24 @@ -3568,12 +3560,12 @@
   21.25    {assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
   21.26      from st(2) obtain b where b: "b \<in> t" "b \<notin> s" by blast
   21.27        from b have "t - {b} - s \<subset> t - s" by blast
   21.28 -      then have cardlt: "card (t - {b} - s) < n" using n ft
   21.29 +      then have cardlt: "card (t - {b} - s) < card (t - s)" using ft
   21.30          by (auto intro: psubset_card_mono)
   21.31        from b ft have ct0: "card t \<noteq> 0" by auto
   21.32      {assume stb: "s \<subseteq> span(t -{b})"
   21.33        from ft have ftb: "finite (t -{b})" by auto
   21.34 -      from H[rule_format, OF cardlt ftb s stb]
   21.35 +      from less(1)[OF cardlt ftb s stb]
   21.36        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
   21.37        let ?w = "insert b u"
   21.38        have th0: "s \<subseteq> insert b u" using u by blast
   21.39 @@ -3594,8 +3586,8 @@
   21.40        from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})" by blast
   21.41        have ab: "a \<noteq> b" using a b by blast
   21.42        have at: "a \<notin> t" using a ab span_superset[of a "t- {b}"] by auto
   21.43 -      have mlt: "card ((insert a (t - {b})) - s) < n"
   21.44 -        using cardlt ft n  a b by auto
   21.45 +      have mlt: "card ((insert a (t - {b})) - s) < card (t - s)"
   21.46 +        using cardlt ft a b by auto
   21.47        have ft': "finite (insert a (t - {b}))" using ft by auto
   21.48        {fix x assume xs: "x \<in> s"
   21.49          have t: "t \<subseteq> (insert b (insert a (t -{b})))" using b by auto
   21.50 @@ -3608,7 +3600,7 @@
   21.51          from span_trans[OF bs x] have "x \<in> span (insert a (t - {b}))"  .}
   21.52        then have sp': "s \<subseteq> span (insert a (t - {b}))" by blast
   21.53  
   21.54 -      from H[rule_format, OF mlt ft' s sp' refl] obtain u where
   21.55 +      from less(1)[OF mlt ft' s sp'] obtain u where
   21.56          u: "card u = card (insert a (t -{b}))" "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t -{b})"
   21.57          "s \<subseteq> span u" by blast
   21.58        from u a b ft at ct0 have "?P u" by auto
   21.59 @@ -3657,11 +3649,9 @@
   21.60    assumes sv: "(S::(real^'n) set) \<subseteq> V" and iS: "independent S"
   21.61    shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
   21.62    using sv iS
   21.63 -proof(induct d\<equiv> "CARD('n) - card S" arbitrary: S rule: nat_less_induct)
   21.64 -  fix n and S:: "(real^'n) set"
   21.65 -  assume H: "\<forall>m<n. \<forall>S \<subseteq> V. independent S \<longrightarrow> m = CARD('n) - card S \<longrightarrow>
   21.66 -              (\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B)"
   21.67 -    and sv: "S \<subseteq> V" and i: "independent S" and n: "n = CARD('n) - card S"
   21.68 +proof(induct "CARD('n) - card S" arbitrary: S rule: less_induct)
   21.69 +  case less
   21.70 +  note sv = `S \<subseteq> V` and i = `independent S`
   21.71    let ?P = "\<lambda>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
   21.72    let ?ths = "\<exists>x. ?P x"
   21.73    let ?d = "CARD('n)"
   21.74 @@ -3674,11 +3664,11 @@
   21.75      have th0: "insert a S \<subseteq> V" using a sv by blast
   21.76      from independent_insert[of a S]  i a
   21.77      have th1: "independent (insert a S)" by auto
   21.78 -    have mlt: "?d - card (insert a S) < n"
   21.79 -      using aS a n independent_bound[OF th1]
   21.80 +    have mlt: "?d - card (insert a S) < ?d - card S"
   21.81 +      using aS a independent_bound[OF th1]
   21.82        by auto
   21.83  
   21.84 -    from H[rule_format, OF mlt th0 th1 refl]
   21.85 +    from less(1)[OF mlt th0 th1]
   21.86      obtain B where B: "insert a S \<subseteq> B" "B \<subseteq> V" "independent B" " V \<subseteq> span B"
   21.87        by blast
   21.88      from B have "?P B" by auto
    22.1 --- a/src/HOL/Nominal/Examples/Class.thy	Fri Jan 15 08:27:21 2010 +0100
    22.2 +++ b/src/HOL/Nominal/Examples/Class.thy	Fri Jan 15 14:43:00 2010 +0100
    22.3 @@ -15069,11 +15069,9 @@
    22.4    assumes a: "(M[a\<turnstile>c>b]) \<longrightarrow>\<^isub>a M'" "a\<noteq>b"
    22.5    shows "\<exists>M0. M0[a\<turnstile>c>b]=M' \<and> M \<longrightarrow>\<^isub>a M0"
    22.6  using a
    22.7 -apply(nominal_induct M\<equiv>"M[a\<turnstile>c>b]" M' avoiding: M a b rule: a_redu.strong_induct)
    22.8 -apply(simp)
    22.9 +apply(nominal_induct "M[a\<turnstile>c>b]" M' avoiding: M a b rule: a_redu.strong_induct)
   22.10  apply(drule  crename_lredu)
   22.11  apply(blast)
   22.12 -apply(simp)
   22.13  apply(drule  crename_credu)
   22.14  apply(blast)
   22.15  (* Cut *)
   22.16 @@ -16132,11 +16130,9 @@
   22.17    assumes a: "(M[x\<turnstile>n>y]) \<longrightarrow>\<^isub>a M'" "x\<noteq>y"
   22.18    shows "\<exists>M0. M0[x\<turnstile>n>y]=M' \<and> M \<longrightarrow>\<^isub>a M0"
   22.19  using a
   22.20 -apply(nominal_induct M\<equiv>"M[x\<turnstile>n>y]" M' avoiding: M x y rule: a_redu.strong_induct)
   22.21 -apply(simp)
   22.22 +apply(nominal_induct "M[x\<turnstile>n>y]" M' avoiding: M x y rule: a_redu.strong_induct)
   22.23  apply(drule  nrename_lredu)
   22.24  apply(blast)
   22.25 -apply(simp)
   22.26  apply(drule  nrename_credu)
   22.27  apply(blast)
   22.28  (* Cut *)
    23.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Fri Jan 15 08:27:21 2010 +0100
    23.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Fri Jan 15 14:43:00 2010 +0100
    23.3 @@ -982,19 +982,18 @@
    23.4      from `(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N` 
    23.5        and `\<Gamma> \<turnstile> P<:Q` 
    23.6      show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> M <: N" 
    23.7 -    proof (induct \<Gamma>\<equiv>"\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct) 
    23.8 -      case (SA_Top _ S \<Gamma> X \<Delta>)
    23.9 -      then have lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" 
   23.10 -        and lh_drv_prm\<^isub>2: "S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
   23.11 -      have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
   23.12 -      hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   23.13 -      with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: replace_type)
   23.14 +    proof (induct "\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct) 
   23.15 +      case (SA_Top S \<Gamma> X \<Delta>)
   23.16 +      from `\<Gamma> \<turnstile> P <: Q`
   23.17 +      have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   23.18 +      with `\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok` have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
   23.19 +        by (simp add: replace_type)
   23.20        moreover
   23.21 -      from lh_drv_prm\<^isub>2 have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)" 
   23.22 +      from `S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)` have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)" 
   23.23          by (simp add: closed_in_def doms_append)
   23.24        ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.SA_Top)
   23.25      next
   23.26 -      case (SA_trans_TVar Y S _ N \<Gamma> X \<Delta>) 
   23.27 +      case (SA_trans_TVar Y S N \<Gamma> X \<Delta>) 
   23.28        then have IH_inner: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N"
   23.29          and lh_drv_prm: "(TVarB Y S) \<in> set (\<Delta>@[(TVarB X Q)]@\<Gamma>)"
   23.30          and rh_drv: "\<Gamma> \<turnstile> P<:Q"
   23.31 @@ -1020,23 +1019,23 @@
   23.32          then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by auto
   23.33        qed
   23.34      next
   23.35 -      case (SA_refl_TVar _ Y \<Gamma> X \<Delta>)
   23.36 -      then have lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" 
   23.37 -        and lh_drv_prm\<^isub>2: "Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
   23.38 -      have "\<Gamma> \<turnstile> P <: Q" by fact
   23.39 -      hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   23.40 -      with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: replace_type)
   23.41 +      case (SA_refl_TVar Y \<Gamma> X \<Delta>)
   23.42 +      from `\<Gamma> \<turnstile> P <: Q`
   23.43 +      have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
   23.44 +      with `\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok` have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
   23.45 +        by (simp add: replace_type)
   23.46        moreover
   23.47 -      from lh_drv_prm\<^isub>2 have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)" by (simp add: doms_append)
   23.48 +      from `Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)` have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)"
   23.49 +        by (simp add: doms_append)
   23.50        ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.SA_refl_TVar)
   23.51      next
   23.52 -      case (SA_arrow _ S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \<Gamma> X \<Delta>) 
   23.53 +      case (SA_arrow S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \<Gamma> X \<Delta>) 
   23.54        then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2" by blast 
   23.55      next
   23.56 -      case (SA_all _ T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Gamma> X \<Delta>)
   23.57 -      from SA_all(2,4,5,6)
   23.58 +      case (SA_all T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Gamma> X \<Delta>)
   23.59        have IH_inner\<^isub>1: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1" 
   23.60 -        and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" by force+
   23.61 +        and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"
   23.62 +        by (fastsimp intro: SA_all)+
   23.63        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
   23.64      qed
   23.65    } 
   23.66 @@ -1263,7 +1262,7 @@
   23.67    assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok"
   23.68    shows "\<turnstile> (\<Gamma> @ \<Delta>) ok"
   23.69    using assms
   23.70 -proof (induct  \<Gamma>' \<equiv> "\<Gamma> @ VarB x Q # \<Delta>" arbitrary: \<Gamma> \<Delta>)
   23.71 +proof (induct "\<Gamma> @ VarB x Q # \<Delta>" arbitrary: \<Gamma> \<Delta>)
   23.72    case valid_nil
   23.73    have "[] = \<Gamma> @ VarB x Q # \<Delta>" by fact
   23.74    then have "False" by auto
   23.75 @@ -1314,14 +1313,14 @@
   23.76    and     "\<turnstile> (\<Delta> @ B # \<Gamma>) ok"
   23.77    shows   "(\<Delta> @ B # \<Gamma>) \<turnstile> t : T"
   23.78  using assms
   23.79 -proof(nominal_induct \<Gamma>'\<equiv> "\<Delta> @ \<Gamma>" t T avoiding: \<Delta> \<Gamma> B rule: typing.strong_induct)
   23.80 -  case (T_Var x' T \<Gamma>' \<Gamma>'' \<Delta>')
   23.81 +proof(nominal_induct "\<Delta> @ \<Gamma>" t T avoiding: \<Delta> \<Gamma> B rule: typing.strong_induct)
   23.82 +  case (T_Var x T)
   23.83    then show ?case by auto
   23.84  next
   23.85 -  case (T_App \<Gamma> t\<^isub>1 T\<^isub>1 T\<^isub>2 t\<^isub>2 \<Gamma> \<Delta>)
   23.86 +  case (T_App X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
   23.87    then show ?case by force
   23.88  next
   23.89 -  case (T_Abs y T\<^isub>1 \<Gamma>' t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
   23.90 +  case (T_Abs y T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
   23.91    then have "VarB y T\<^isub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
   23.92    then have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
   23.93      by (auto dest: typing_ok)
   23.94 @@ -1336,22 +1335,22 @@
   23.95      apply (rule closed)
   23.96      done
   23.97    then have "\<turnstile> ((VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
   23.98 -  then have "(VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
   23.99 -    by (rule T_Abs) (simp add: T_Abs)
  23.100 +  with _ have "(VarB y T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
  23.101 +    by (rule T_Abs) simp
  23.102    then have "VarB y T\<^isub>1 # \<Delta> @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
  23.103    then show ?case by (rule typing.T_Abs)
  23.104  next
  23.105 -  case (T_Sub \<Gamma>' t S T \<Delta> \<Gamma>)
  23.106 -  from `\<turnstile> (\<Delta> @ B # \<Gamma>) ok` and `\<Gamma>' = \<Delta> @ \<Gamma>`
  23.107 +  case (T_Sub t S T \<Delta> \<Gamma>)
  23.108 +  from refl and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
  23.109    have "\<Delta> @ B # \<Gamma> \<turnstile> t : S" by (rule T_Sub)
  23.110 -  moreover from  `\<Gamma>'\<turnstile>S<:T` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
  23.111 +  moreover from  `(\<Delta> @ \<Gamma>)\<turnstile>S<:T` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
  23.112    have "(\<Delta> @ B # \<Gamma>)\<turnstile>S<:T"
  23.113      by (rule weakening) (simp add: extends_def T_Sub)
  23.114    ultimately show ?case by (rule typing.T_Sub)
  23.115  next
  23.116 -  case (T_TAbs X T\<^isub>1 \<Gamma>' t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
  23.117 -  then have "TVarB X T\<^isub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
  23.118 -  then have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
  23.119 +  case (T_TAbs X T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Delta> \<Gamma>)
  23.120 +  from `TVarB X T\<^isub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2`
  23.121 +  have closed: "T\<^isub>1 closed_in (\<Delta> @ \<Gamma>)"
  23.122      by (auto dest: typing_ok)
  23.123    have "\<turnstile> (TVarB X T\<^isub>1 # \<Delta> @ B # \<Gamma>) ok"
  23.124      apply (rule valid_consT)
  23.125 @@ -1364,15 +1363,15 @@
  23.126      apply (rule closed)
  23.127      done
  23.128    then have "\<turnstile> ((TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
  23.129 -  then have "(TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
  23.130 -    by (rule T_TAbs) (simp add: T_TAbs)
  23.131 +  with _ have "(TVarB X T\<^isub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2"
  23.132 +    by (rule T_TAbs) simp
  23.133    then have "TVarB X T\<^isub>1 # \<Delta> @ B # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2" by simp
  23.134    then show ?case by (rule typing.T_TAbs)
  23.135  next
  23.136 -  case (T_TApp X \<Gamma>' t\<^isub>1 T2 T11 T12 \<Delta> \<Gamma>)
  23.137 +  case (T_TApp X t\<^isub>1 T2 T11 T12 \<Delta> \<Gamma>)
  23.138    have "\<Delta> @ B # \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T11. T12)"
  23.139 -    by (rule T_TApp)+
  23.140 -  moreover from `\<Gamma>'\<turnstile>T2<:T11` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
  23.141 +    by (rule T_TApp refl)+
  23.142 +  moreover from `(\<Delta> @ \<Gamma>)\<turnstile>T2<:T11` and `\<turnstile> (\<Delta> @ B # \<Gamma>) ok`
  23.143    have "(\<Delta> @ B # \<Gamma>)\<turnstile>T2<:T11"
  23.144      by (rule weakening) (simp add: extends_def T_TApp)
  23.145    ultimately show ?case by (rule better_T_TApp)
  23.146 @@ -1393,24 +1392,22 @@
  23.147    assumes "(\<Gamma> @ VarB x Q # \<Delta>) \<turnstile> S <: T"
  23.148    shows  "(\<Gamma>@\<Delta>) \<turnstile> S <: T"
  23.149    using assms
  23.150 -proof (induct  \<Gamma>' \<equiv> "\<Gamma> @ VarB x Q # \<Delta>" S T arbitrary: \<Gamma>)
  23.151 -  case (SA_Top G' S G)
  23.152 -  then have "\<turnstile> (G @ \<Delta>) ok" by (auto dest: valid_cons')
  23.153 -  moreover have "S closed_in (G @ \<Delta>)" using SA_Top by (auto dest: closed_in_cons)
  23.154 +proof (induct "\<Gamma> @ VarB x Q # \<Delta>" S T arbitrary: \<Gamma>)
  23.155 +  case (SA_Top S)
  23.156 +  then have "\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons')
  23.157 +  moreover have "S closed_in (\<Gamma> @ \<Delta>)" using SA_Top by (auto dest: closed_in_cons)
  23.158    ultimately show ?case using subtype_of.SA_Top by auto
  23.159  next
  23.160 -  case (SA_refl_TVar G X' G')
  23.161 -  then have "\<turnstile> (G' @ VarB x Q # \<Delta>) ok" by simp
  23.162 -  then have h1:"\<turnstile> (G' @ \<Delta>) ok" by (auto dest: valid_cons')
  23.163 -  have "X' \<in> ty_dom (G' @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
  23.164 -  then have h2:"X' \<in> ty_dom (G' @ \<Delta>)" using ty_dom_vrs by auto
  23.165 +  case (SA_refl_TVar X)
  23.166 +  from `\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok`
  23.167 +  have h1:"\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons')
  23.168 +  have "X \<in> ty_dom (\<Gamma> @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
  23.169 +  then have h2:"X \<in> ty_dom (\<Gamma> @ \<Delta>)" using ty_dom_vrs by auto
  23.170    show ?case using h1 h2 by auto
  23.171  next
  23.172 -  case (SA_all G T1 S1 X S2 T2 G')
  23.173 -  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
  23.174 -  then have h1:"(TVarB X T1 # (G' @ \<Delta>))\<turnstile>S2<:T2" using SA_all by auto
  23.175 -  have ih2:"G = G' @ VarB x Q # \<Delta> \<Longrightarrow> (G' @ \<Delta>)\<turnstile>T1<:S1" by fact
  23.176 -  then have h2:"(G' @ \<Delta>)\<turnstile>T1<:S1" using SA_all by auto
  23.177 +  case (SA_all T1 S1 X S2 T2)
  23.178 +  have h1:"((TVarB X T1 # \<Gamma>) @ \<Delta>)\<turnstile>S2<:T2" by (fastsimp intro: SA_all)
  23.179 +  have h2:"(\<Gamma> @ \<Delta>)\<turnstile>T1<:S1" using SA_all by auto
  23.180    then show ?case using h1 h2 by auto
  23.181  qed (auto)
  23.182  
  23.183 @@ -1418,26 +1415,26 @@
  23.184    assumes H: "\<Delta> @ (TVarB X Q) # \<Gamma> \<turnstile> t : T"
  23.185    shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> \<Delta> @ (TVarB X P) # \<Gamma> \<turnstile> t : T"
  23.186    using H
  23.187 -  proof (nominal_induct \<Gamma>' \<equiv> "\<Delta> @ (TVarB X Q) # \<Gamma>" t T avoiding: P arbitrary: \<Delta> rule: typing.strong_induct)
  23.188 -    case (T_Var x T G P D)
  23.189 +  proof (nominal_induct "\<Delta> @ (TVarB X Q) # \<Gamma>" t T avoiding: P arbitrary: \<Delta> rule: typing.strong_induct)
  23.190 +    case (T_Var x T P D)
  23.191      then have "VarB x T \<in> set (D @ TVarB X P # \<Gamma>)" 
  23.192        and "\<turnstile>  (D @ TVarB X P # \<Gamma>) ok"
  23.193        by (auto intro: replace_type dest!: subtype_implies_closed)
  23.194      then show ?case by auto
  23.195    next
  23.196 -    case (T_App G t1 T1 T2 t2 P D)
  23.197 +    case (T_App t1 T1 T2 t2 P D)
  23.198      then show ?case by force
  23.199    next
  23.200 -    case (T_Abs x T1 G t2 T2 P D)
  23.201 +    case (T_Abs x T1 t2 T2 P D)
  23.202      then show ?case by (fastsimp dest: typing_ok)
  23.203    next
  23.204 -    case (T_Sub G t S T D)
  23.205 +    case (T_Sub t S T P D)
  23.206      then show ?case using subtype_narrow by fastsimp
  23.207    next
  23.208 -    case (T_TAbs X' T1 G t2 T2 P D)
  23.209 +    case (T_TAbs X' T1 t2 T2 P D)
  23.210      then show ?case by (fastsimp dest: typing_ok)
  23.211    next
  23.212 -    case (T_TApp X' G t1 T2 T11 T12 P D)
  23.213 +    case (T_TApp X' t1 T2 T11 T12 P D)
  23.214      then have "D @ TVarB X P # \<Gamma> \<turnstile> t1 : Forall X' T12 T11" by fastsimp
  23.215      moreover have "(D @ [TVarB X Q] @ \<Gamma>) \<turnstile> T2<:T11" using T_TApp by auto
  23.216      then have "(D @ [TVarB X P] @ \<Gamma>) \<turnstile> T2<:T11" using `\<Gamma>\<turnstile>P<:Q`
  23.217 @@ -1454,8 +1451,8 @@
  23.218  theorem subst_type: -- {* A.8 *}
  23.219    assumes H: "(\<Delta> @ (VarB x U) # \<Gamma>) \<turnstile> t : T"
  23.220    shows "\<Gamma> \<turnstile> u : U \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t[x \<mapsto> u] : T" using H
  23.221 - proof (nominal_induct \<Gamma>' \<equiv> "\<Delta> @ (VarB x U) # \<Gamma>" t T avoiding: x u arbitrary: \<Delta> rule: typing.strong_induct)
  23.222 -   case (T_Var y T G x u D)
  23.223 + proof (nominal_induct "\<Delta> @ (VarB x U) # \<Gamma>" t T avoiding: x u arbitrary: \<Delta> rule: typing.strong_induct)
  23.224 +   case (T_Var y T x u D)
  23.225     show ?case
  23.226     proof (cases "x = y")
  23.227       assume eq:"x=y"
  23.228 @@ -1468,23 +1465,23 @@
  23.229         by (auto simp add:binding.inject dest: valid_cons')
  23.230     qed
  23.231   next
  23.232 -   case (T_App G t1 T1 T2 t2 x u D)
  23.233 +   case (T_App t1 T1 T2 t2 x u D)
  23.234     then show ?case by force
  23.235   next
  23.236 -   case (T_Abs y T1 G t2 T2 x u D)
  23.237 +   case (T_Abs y T1 t2 T2 x u D)
  23.238     then show ?case by force
  23.239   next
  23.240 -   case (T_Sub G t S T x u D)
  23.241 +   case (T_Sub t S T x u D)
  23.242     then have "D @ \<Gamma> \<turnstile> t[x \<mapsto> u] : S" by auto
  23.243     moreover have "(D @ \<Gamma>) \<turnstile> S<:T" using T_Sub by (auto dest: strengthening)
  23.244     ultimately show ?case by auto 
  23.245   next
  23.246 -   case (T_TAbs X T1 G t2 T2 x u D)
  23.247 -   from `TVarB X T1 # G \<turnstile> t2 : T2` have "X \<sharp> T1"
  23.248 +   case (T_TAbs X T1 t2 T2 x u D)
  23.249 +   from `TVarB X T1 # D @ VarB x U # \<Gamma> \<turnstile> t2 : T2` have "X \<sharp> T1"
  23.250       by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh)
  23.251     with `X \<sharp> u` and T_TAbs show ?case by fastsimp
  23.252   next
  23.253 -   case (T_TApp X G t1 T2 T11 T12 x u D)
  23.254 +   case (T_TApp X t1 T2 T11 T12 x u D)
  23.255     then have "(D@\<Gamma>) \<turnstile>T2<:T11" using T_TApp by (auto dest: strengthening)
  23.256     then show "((D @ \<Gamma>) \<turnstile> ((t1 \<cdot>\<^sub>\<tau> T2)[x \<mapsto> u]) : (T12[X \<mapsto> T2]\<^sub>\<tau>))" using T_TApp
  23.257       by (force simp add: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar)
  23.258 @@ -1496,8 +1493,8 @@
  23.259    assumes H: "(\<Delta> @ ((TVarB X Q) # \<Gamma>)) \<turnstile> S <: T"
  23.260    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>" 
  23.261    using H
  23.262 -proof (nominal_induct \<Gamma>' \<equiv> "\<Delta> @ TVarB X Q # \<Gamma>" S T avoiding: X P arbitrary: \<Delta> rule: subtype_of.strong_induct)
  23.263 -  case (SA_Top G S X P D)
  23.264 +proof (nominal_induct "\<Delta> @ TVarB X Q # \<Gamma>" S T avoiding: X P arbitrary: \<Delta> rule: subtype_of.strong_induct)
  23.265 +  case (SA_Top S X P D)
  23.266    then have "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by simp
  23.267    moreover have closed: "P closed_in \<Gamma>" using SA_Top subtype_implies_closed by auto 
  23.268    ultimately have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule valid_subst)
  23.269 @@ -1505,17 +1502,18 @@
  23.270    then have "S[X \<mapsto> P]\<^sub>\<tau> closed_in  (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" using closed by (rule subst_closed_in)
  23.271    ultimately show ?case by auto
  23.272  next
  23.273 -  case (SA_trans_TVar Y S G T X P D)
  23.274 -  have h:"G\<turnstile>S<:T" by fact
  23.275 +  case (SA_trans_TVar Y S T X P D)
  23.276 +  have h:"(D @ TVarB X Q # \<Gamma>)\<turnstile>S<:T" by fact
  23.277    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
  23.278 -  from `G\<turnstile>S<:T` have G_ok: "\<turnstile> G ok" by (rule subtype_implies_ok)
  23.279 +  from h have G_ok: "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by (rule subtype_implies_ok)
  23.280    from G_ok and SA_trans_TVar have X\<Gamma>_ok: "\<turnstile> (TVarB X Q # \<Gamma>) ok"
  23.281      by (auto intro: validE_append)
  23.282    show "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> Tvar Y[X \<mapsto> P]\<^sub>\<tau><:T[X \<mapsto> P]\<^sub>\<tau>"
  23.283    proof (cases "X = Y")
  23.284      assume eq: "X = Y"
  23.285 -    from eq and SA_trans_TVar have "TVarB Y Q \<in> set G" by simp
  23.286 -    with G_ok have QS: "Q = S" using `TVarB Y S \<in> set G` by (rule uniqueness_of_ctxt)
  23.287 +    from eq and SA_trans_TVar have "TVarB Y Q \<in> set (D @ TVarB X Q # \<Gamma>)" by simp
  23.288 +    with G_ok have QS: "Q = S" using `TVarB Y S \<in> set (D @ TVarB X Q # \<Gamma>)`
  23.289 +      by (rule uniqueness_of_ctxt)
  23.290      from X\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto
  23.291      then have XQ: "X \<sharp> Q" by (rule closed_in_fresh)
  23.292      note `\<Gamma>\<turnstile>P<:Q`
  23.293 @@ -1552,8 +1550,8 @@
  23.294      qed
  23.295    qed
  23.296  next
  23.297 -  case (SA_refl_TVar G Y X P D)
  23.298 -  then have "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by simp
  23.299 +  case (SA_refl_TVar Y X P D)
  23.300 +  note `\<turnstile> (D @ TVarB X Q # \<Gamma>) ok`
  23.301    moreover from SA_refl_TVar have closed: "P closed_in \<Gamma>"
  23.302      by (auto dest: subtype_implies_closed)
  23.303    ultimately have ok: "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using valid_subst by auto
  23.304 @@ -1571,12 +1569,12 @@
  23.305      with neq and ok show ?thesis by auto
  23.306    qed
  23.307  next
  23.308 -  case (SA_arrow G T1 S1 S2 T2 X P D)
  23.309 +  case (SA_arrow T1 S1 S2 T2 X P D)
  23.310    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
  23.311    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
  23.312    show ?case using subtype_of.SA_arrow h1 h2 by auto
  23.313  next
  23.314 -  case (SA_all G T1 S1 Y S2 T2 X P D)
  23.315 +  case (SA_all T1 S1 Y S2 T2 X P D)
  23.316    then have Y: "Y \<sharp> ty_dom (D @ TVarB X Q # \<Gamma>)"
  23.317      by (auto dest: subtype_implies_ok intro: fresh_dom)
  23.318    moreover from SA_all have "S1 closed_in (D @ TVarB X Q # \<Gamma>)"
  23.319 @@ -1594,13 +1592,13 @@
  23.320    assumes H: "(D @ TVarB X Q # G) \<turnstile> t : T"
  23.321    shows "G \<turnstile> P <: Q \<Longrightarrow>
  23.322      (D[X \<mapsto> P]\<^sub>e @ G) \<turnstile> t[X \<mapsto>\<^sub>\<tau> P] : T[X \<mapsto> P]\<^sub>\<tau>" using H
  23.323 -proof (nominal_induct \<Gamma>'\<equiv>"(D @ TVarB X Q # G)" t T avoiding: X P arbitrary: D rule: typing.strong_induct)
  23.324 -  case (T_Var x T G' X P D')
  23.325 +proof (nominal_induct "D @ TVarB X Q # G" t T avoiding: X P arbitrary: D rule: typing.strong_induct)
  23.326 +  case (T_Var x T X P D')
  23.327    have "G\<turnstile>P<:Q" by fact
  23.328    then have "P closed_in G" using subtype_implies_closed by auto
  23.329 -  moreover have "\<turnstile> (D' @ TVarB X Q # G) ok" using T_Var by auto
  23.330 +  moreover note `\<turnstile> (D' @ TVarB X Q # G) ok`
  23.331    ultimately have "\<turnstile> (D'[X \<mapsto> P]\<^sub>e @ G) ok" using valid_subst by auto
  23.332 -  moreover have "VarB x T \<in> set (D' @ TVarB X Q # G)" using T_Var by auto
  23.333 +  moreover note `VarB x T \<in> set (D' @ TVarB X Q # G)`
  23.334    then have "VarB x T \<in> set D' \<or> VarB x T \<in> set G" by simp
  23.335    then have "(VarB x (T[X \<mapsto> P]\<^sub>\<tau>)) \<in> set (D'[X \<mapsto> P]\<^sub>e @ G)"
  23.336    proof
  23.337 @@ -1621,25 +1619,25 @@
  23.338    qed
  23.339    ultimately show ?case by auto
  23.340  next
  23.341 -  case (T_App G' t1 T1 T2 t2 X P D')
  23.342 +  case (T_App t1 T1 T2 t2 X P D')
  23.343    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
  23.344    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
  23.345    ultimately show ?case by auto
  23.346  next
  23.347 -  case (T_Abs x T1 G' t2 T2 X P D')
  23.348 +  case (T_Abs x T1 t2 T2 X P D')
  23.349    then show ?case by force
  23.350  next
  23.351 -  case (T_Sub G' t S T X P D')
  23.352 +  case (T_Sub t S T X P D')
  23.353    then show ?case using substT_subtype by force
  23.354  next
  23.355 -  case (T_TAbs X' G' T1 t2 T2 X P D')
  23.356 +  case (T_TAbs X' T1 t2 T2 X P D')
  23.357    then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)"
  23.358 -  and "G' closed_in (D' @ TVarB X Q # G)"
  23.359 +  and "T1 closed_in (D' @ TVarB X Q # G)"
  23.360      by (auto dest: typing_ok)
  23.361 -  then have "X' \<sharp> G'" by (rule closed_in_fresh)
  23.362 +  then have "X' \<sharp> T1" by (rule closed_in_fresh)
  23.363    with T_TAbs show ?case by force
  23.364  next
  23.365 -  case (T_TApp X' G' t1 T2 T11 T12 X P D')
  23.366 +  case (T_TApp X' t1 T2 T11 T12 X P D')
  23.367    then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)"
  23.368      by (simp add: fresh_dom)
  23.369    moreover from T_TApp have "T11 closed_in (D' @ TVarB X Q # G)"
  23.370 @@ -1824,22 +1822,22 @@
  23.371  lemma Fun_canonical: -- {* A.14(1) *}
  23.372    assumes ty: "[] \<turnstile> v : T\<^isub>1 \<rightarrow> T\<^isub>2"
  23.373    shows "val v \<Longrightarrow> \<exists>x t S. v = (\<lambda>x:S. t)" using ty
  23.374 -proof (induct \<Gamma>\<equiv>"[]::env" v T\<equiv>"T\<^isub>1 \<rightarrow> T\<^isub>2" arbitrary: T\<^isub>1 T\<^isub>2)
  23.375 -  case (T_Sub \<Gamma> t S T)
  23.376 -  hence "\<Gamma> \<turnstile> S <: T\<^isub>1 \<rightarrow> T\<^isub>2" by simp
  23.377 -  then obtain S\<^isub>1 S\<^isub>2 where S: "S = S\<^isub>1 \<rightarrow> S\<^isub>2" 
  23.378 +proof (induct "[]::env" v "T\<^isub>1 \<rightarrow> T\<^isub>2" arbitrary: T\<^isub>1 T\<^isub>2)
  23.379 +  case (T_Sub t S)
  23.380 +  from `[] \<turnstile> S <: T\<^isub>1 \<rightarrow> T\<^isub>2`
  23.381 +  obtain S\<^isub>1 S\<^isub>2 where S: "S = S\<^isub>1 \<rightarrow> S\<^isub>2" 
  23.382      by cases (auto simp add: T_Sub)
  23.383 -  with `val t` and `\<Gamma> = []` show ?case by (rule T_Sub)
  23.384 +  then show ?case using `val t` by (rule T_Sub)
  23.385  qed (auto)
  23.386  
  23.387  lemma TyAll_canonical: -- {* A.14(3) *}
  23.388    fixes X::tyvrs
  23.389    assumes ty: "[] \<turnstile> v : (\<forall>X<:T\<^isub>1. T\<^isub>2)"
  23.390    shows "val v \<Longrightarrow> \<exists>X t S. v = (\<lambda>X<:S. t)" using ty
  23.391 -proof (induct \<Gamma>\<equiv>"[]::env" v T\<equiv>"\<forall>X<:T\<^isub>1. T\<^isub>2" arbitrary: X T\<^isub>1 T\<^isub>2)
  23.392 -  case (T_Sub  \<Gamma> t S T)
  23.393 -  hence "\<Gamma> \<turnstile> S <: (\<forall>X<:T\<^isub>1. T\<^isub>2)" by simp
  23.394 -  then obtain X S\<^isub>1 S\<^isub>2 where S: "S = (\<forall>X<:S\<^isub>1. S\<^isub>2)"
  23.395 +proof (induct "[]::env" v "\<forall>X<:T\<^isub>1. T\<^isub>2" arbitrary: X T\<^isub>1 T\<^isub>2)
  23.396 +  case (T_Sub t S)
  23.397 +  from `[] \<turnstile> S <: (\<forall>X<:T\<^isub>1. T\<^isub>2)`
  23.398 +  obtain X S\<^isub>1 S\<^isub>2 where S: "S = (\<forall>X<:S\<^isub>1. S\<^isub>2)"
  23.399      by cases (auto simp add: T_Sub)
  23.400    then show ?case using T_Sub by auto 
  23.401  qed (auto)
  23.402 @@ -1848,8 +1846,8 @@
  23.403    assumes "[] \<turnstile> t : T"
  23.404    shows "val t \<or> (\<exists>t'. t \<longmapsto> t')" 
  23.405  using assms
  23.406 -proof (induct \<Gamma> \<equiv> "[]::env" t T)
  23.407 -  case (T_App \<Gamma> t\<^isub>1 T\<^isub>1\<^isub>1  T\<^isub>1\<^isub>2 t\<^isub>2)
  23.408 +proof (induct "[]::env" t T)
  23.409 +  case (T_App t\<^isub>1 T\<^isub>1\<^isub>1  T\<^isub>1\<^isub>2 t\<^isub>2)
  23.410    hence "val t\<^isub>1 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
  23.411    thus ?case
  23.412    proof
  23.413 @@ -1875,7 +1873,7 @@
  23.414      thus ?case by auto
  23.415    qed
  23.416  next
  23.417 -  case (T_TApp X \<Gamma> t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
  23.418 +  case (T_TApp X t\<^isub>1 T\<^isub>2 T\<^isub>1\<^isub>1 T\<^isub>1\<^isub>2)
  23.419    hence "val t\<^isub>1 \<or> (\<exists>t'. t\<^isub>1 \<longmapsto> t')" by simp
  23.420    thus ?case
  23.421    proof
    24.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Fri Jan 15 08:27:21 2010 +0100
    24.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Fri Jan 15 14:43:00 2010 +0100
    24.3 @@ -410,37 +410,34 @@
    24.4    and b: "\<Gamma> \<turnstile> u : U"
    24.5    shows "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" using a b
    24.6  proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, U)] @ \<Gamma>" t T avoiding: x u \<Delta> rule: typing.strong_induct)
    24.7 -  case (Var \<Gamma>' y T x u \<Delta>)
    24.8 -  then have a1: "valid (\<Delta> @ [(x, U)] @ \<Gamma>)" 
    24.9 -       and  a2: "(y, T) \<in> set (\<Delta> @ [(x, U)] @ \<Gamma>)" 
   24.10 -       and  a3: "\<Gamma> \<turnstile> u : U" by simp_all
   24.11 -  from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
   24.12 +  case (Var y T x u \<Delta>)
   24.13 +  from `valid (\<Delta> @ [(x, U)] @ \<Gamma>)`
   24.14 +  have valid: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
   24.15    show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T"
   24.16    proof cases
   24.17      assume eq: "x = y"
   24.18 -    from a1 a2 have "T = U" using eq by (auto intro: context_unique)
   24.19 -    with a3 show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using eq a4 by (auto intro: weakening)
   24.20 +    from Var eq have "T = U" by (auto intro: context_unique)
   24.21 +    with Var eq valid show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" by (auto intro: weakening)
   24.22    next
   24.23      assume ineq: "x \<noteq> y"
   24.24 -    from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
   24.25 -    then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq a4 by auto
   24.26 +    from Var ineq have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" by simp
   24.27 +    then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq valid by auto
   24.28    qed
   24.29  next
   24.30 -  case (Tuple \<Gamma>' t\<^isub>1 T\<^isub>1 t\<^isub>2 T\<^isub>2)
   24.31 -  from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   24.32 +  case (Tuple t\<^isub>1 T\<^isub>1 t\<^isub>2 T\<^isub>2)
   24.33 +  from refl `\<Gamma> \<turnstile> u : U`
   24.34    have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>1[x\<mapsto>u] : T\<^isub>1" by (rule Tuple)
   24.35 -  moreover from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   24.36 +  moreover from refl `\<Gamma> \<turnstile> u : U`
   24.37    have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>2[x\<mapsto>u] : T\<^isub>2" by (rule Tuple)
   24.38    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" ..
   24.39    then show ?case by simp
   24.40  next
   24.41 -  case (Let p t \<Gamma>' T \<Delta>' s S)
   24.42 -  from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   24.43 +  case (Let p t T \<Delta>' s S)
   24.44 +  from refl `\<Gamma> \<turnstile> u : U`
   24.45    have "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" by (rule Let)
   24.46    moreover note `\<turnstile> p : T \<Rightarrow> \<Delta>'`
   24.47 -  moreover from `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   24.48 -  have "\<Delta>' @ \<Gamma>' = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp
   24.49 -  with `\<Gamma> \<turnstile> u : U` have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by (rule Let)
   24.50 +  moreover have "\<Delta>' @ (\<Delta> @ [(x, U)] @ \<Gamma>) = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp
   24.51 +  then have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" using `\<Gamma> \<turnstile> u : U` by (rule Let)
   24.52    then have "\<Delta>' @ \<Delta> @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by simp
   24.53    ultimately have "\<Delta> @ \<Gamma> \<turnstile> (LET p = t[x\<mapsto>u] IN s[x\<mapsto>u]) : S"
   24.54      by (rule better_T_Let)
   24.55 @@ -448,10 +445,10 @@
   24.56      by (simp add: fresh_star_def fresh_list_nil fresh_list_cons)
   24.57    ultimately show ?case by simp
   24.58  next
   24.59 -  case (Abs y T \<Gamma>' t S)
   24.60 -  from `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` have "(y, T) # \<Gamma>' = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>"
   24.61 +  case (Abs y T t S)
   24.62 +  have "(y, T) # \<Delta> @ [(x, U)] @ \<Gamma> = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>"
   24.63      by simp
   24.64 -  with `\<Gamma> \<turnstile> u : U` have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by (rule Abs)
   24.65 +  then have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" using `\<Gamma> \<turnstile> u : U` by (rule Abs)
   24.66    then have "(y, T) # \<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by simp
   24.67    then have "\<Delta> @ \<Gamma> \<turnstile> (\<lambda>y:T. t[x\<mapsto>u]) : T \<rightarrow> S"
   24.68      by (rule typing.Abs)
   24.69 @@ -459,10 +456,10 @@
   24.70      by (simp add: fresh_list_nil fresh_list_cons)
   24.71    ultimately show ?case by simp
   24.72  next
   24.73 -  case (App \<Gamma>' t\<^isub>1 T S t\<^isub>2)
   24.74 -  from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   24.75 +  case (App t\<^isub>1 T S t\<^isub>2)
   24.76 +  from refl `\<Gamma> \<turnstile> u : U`
   24.77    have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>1[x\<mapsto>u] : T \<rightarrow> S" by (rule App)
   24.78 -  moreover from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   24.79 +  moreover from refl `\<Gamma> \<turnstile> u : U`
   24.80    have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>2[x\<mapsto>u] : T" by (rule App)
   24.81    ultimately have "\<Delta> @ \<Gamma> \<turnstile> (t\<^isub>1[x\<mapsto>u]) \<cdot> (t\<^isub>2[x\<mapsto>u]) : S"
   24.82      by (rule typing.App)
    25.1 --- a/src/HOL/Nominal/Examples/SOS.thy	Fri Jan 15 08:27:21 2010 +0100
    25.2 +++ b/src/HOL/Nominal/Examples/SOS.thy	Fri Jan 15 14:43:00 2010 +0100
    25.3 @@ -220,10 +220,10 @@
    25.4    shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 
    25.5  using a b 
    25.6  proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: e' \<Delta> rule: typing.strong_induct)
    25.7 -  case (t_Var \<Gamma>' y T e' \<Delta>)
    25.8 +  case (t_Var y T e' \<Delta>)
    25.9    then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 
   25.10         and  a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 
   25.11 -       and  a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
   25.12 +       and  a3: "\<Gamma> \<turnstile> e' : T'" .
   25.13    from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
   25.14    { assume eq: "x=y"
   25.15      from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
    26.1 --- a/src/HOL/Nominal/nominal_induct.ML	Fri Jan 15 08:27:21 2010 +0100
    26.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Fri Jan 15 14:43:00 2010 +0100
    26.3 @@ -5,7 +5,7 @@
    26.4  
    26.5  structure NominalInduct:
    26.6  sig
    26.7 -  val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
    26.8 +  val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    26.9      (string * typ) list -> (string * typ) list list -> thm list ->
   26.10      thm list -> int -> Rule_Cases.cases_tactic
   26.11    val nominal_induct_method: (Proof.context -> Proof.method) context_parser
   26.12 @@ -74,26 +74,29 @@
   26.13            else map (tune o #1) (take (p - n) ps) @ xs;
   26.14        in Logic.list_rename_params (ys, prem) end;
   26.15      fun rename_prems prop =
   26.16 -      let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
   26.17 +      let val (As, C) = Logic.strip_horn prop
   26.18        in Logic.list_implies (map rename As, C) end;
   26.19    in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
   26.20  
   26.21  
   26.22  (* nominal_induct_tac *)
   26.23  
   26.24 -fun nominal_induct_tac ctxt def_insts avoiding fixings rules facts =
   26.25 +fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
   26.26    let
   26.27      val thy = ProofContext.theory_of ctxt;
   26.28      val cert = Thm.cterm_of thy;
   26.29  
   26.30      val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
   26.31 -    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
   26.32 +    val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs;
   26.33  
   26.34      val finish_rule =
   26.35        split_all_tuples
   26.36        #> rename_params_rule true
   26.37          (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
   26.38 -    fun rule_cases r = Rule_Cases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
   26.39 +
   26.40 +    fun rule_cases ctxt r =
   26.41 +      let val r' = if simp then Induct.simplified_rule ctxt r else r
   26.42 +      in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end;
   26.43    in
   26.44      (fn i => fn st =>
   26.45        rules
   26.46 @@ -102,19 +105,32 @@
   26.47        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   26.48          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   26.49            (CONJUNCTS (ALLGOALS
   26.50 -            (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
   26.51 -              THEN' Induct.fix_tac defs_ctxt
   26.52 -                (nth concls (j - 1) + more_consumes)
   26.53 -                (nth_list fixings (j - 1))))
   26.54 +            let
   26.55 +              val adefs = nth_list atomized_defs (j - 1);
   26.56 +              val frees = fold (Term.add_frees o prop_of) adefs [];
   26.57 +              val xs = nth_list fixings (j - 1);
   26.58 +              val k = nth concls (j - 1) + more_consumes
   26.59 +            in
   26.60 +              Method.insert_tac (more_facts @ adefs) THEN'
   26.61 +                (if simp then
   26.62 +                   Induct.rotate_tac k (length adefs) THEN'
   26.63 +                   Induct.fix_tac defs_ctxt k
   26.64 +                     (List.partition (member op = frees) xs |> op @)
   26.65 +                 else
   26.66 +                   Induct.fix_tac defs_ctxt k xs)
   26.67 +            end)
   26.68            THEN' Induct.inner_atomize_tac) j))
   26.69          THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
   26.70              Induct.guess_instance ctxt
   26.71                (finish_rule (Induct.internalize more_consumes rule)) i st'
   26.72              |> Seq.maps (fn rule' =>
   26.73 -              CASES (rule_cases rule' cases)
   26.74 +              CASES (rule_cases ctxt rule' cases)
   26.75                  (Tactic.rtac (rename_params_rule false [] rule') i THEN
   26.76                    PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
   26.77 -    THEN_ALL_NEW_CASES Induct.rulify_tac
   26.78 +    THEN_ALL_NEW_CASES
   26.79 +      ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
   26.80 +        else K all_tac)
   26.81 +       THEN_ALL_NEW Induct.rulify_tac)
   26.82    end;
   26.83  
   26.84  
   26.85 @@ -128,11 +144,14 @@
   26.86  val fixingN = "arbitrary";  (* to be consistent with induct; hopefully this changes again *)
   26.87  val ruleN = "rule";
   26.88  
   26.89 -val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
   26.90 +val inst = Scan.lift (Args.$$$ "_") >> K NONE ||
   26.91 +  Args.term >> (SOME o rpair false) ||
   26.92 +  Scan.lift (Args.$$$ "(") |-- (Args.term >> (SOME o rpair true)) --|
   26.93 +    Scan.lift (Args.$$$ ")");
   26.94  
   26.95  val def_inst =
   26.96    ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
   26.97 -      -- Args.term) >> SOME ||
   26.98 +      -- (Args.term >> rpair false)) >> SOME ||
   26.99      inst >> Option.map (pair NONE);
  26.100  
  26.101  val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
  26.102 @@ -153,11 +172,11 @@
  26.103  in
  26.104  
  26.105  val nominal_induct_method =
  26.106 -  P.and_list' (Scan.repeat (unless_more_args def_inst)) --
  26.107 -  avoiding -- fixing -- rule_spec >>
  26.108 -  (fn (((x, y), z), w) => fn ctxt =>
  26.109 +  Args.mode Induct.no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
  26.110 +  avoiding -- fixing -- rule_spec) >>
  26.111 +  (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
  26.112      RAW_METHOD_CASES (fn facts =>
  26.113 -      HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
  26.114 +      HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));
  26.115  
  26.116  end;
  26.117  
    27.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Fri Jan 15 08:27:21 2010 +0100
    27.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Fri Jan 15 14:43:00 2010 +0100
    27.3 @@ -233,37 +233,39 @@
    27.4    with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
    27.5  qed
    27.6  
    27.7 -lemma ind_euclid: 
    27.8 -  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0" 
    27.9 -  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)" 
   27.10 +lemma ind_euclid:
   27.11 +  assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
   27.12 +  and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
   27.13    shows "P a b"
   27.14 -proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
   27.15 -  fix n a b
   27.16 -  assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
   27.17 +proof(induct "a + b" arbitrary: a b rule: less_induct)
   27.18 +  case less
   27.19    have "a = b \<or> a < b \<or> b < a" by arith
   27.20    moreover {assume eq: "a= b"
   27.21 -    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq by simp}
   27.22 +    from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
   27.23 +    by simp}
   27.24    moreover
   27.25    {assume lt: "a < b"
   27.26 -    hence "a + b - a < n \<or> a = 0"  using H(2) by arith
   27.27 +    hence "a + b - a < a + b \<or> a = 0" by arith
   27.28      moreover
   27.29      {assume "a =0" with z c have "P a b" by blast }
   27.30      moreover
   27.31 -    {assume ab: "a + b - a < n"
   27.32 -      have th0: "a + b - a = a + (b - a)" using lt by arith
   27.33 -      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
   27.34 -      have "P a b" by (simp add: th0[symmetric])}
   27.35 +    {assume "a + b - a < a + b"
   27.36 +      also have th0: "a + b - a = a + (b - a)" using lt by arith
   27.37 +      finally have "a + (b - a) < a + b" .
   27.38 +      then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
   27.39 +      then have "P a b" by (simp add: th0[symmetric])}
   27.40      ultimately have "P a b" by blast}
   27.41    moreover
   27.42    {assume lt: "a > b"
   27.43 -    hence "b + a - b < n \<or> b = 0"  using H(2) by arith
   27.44 +    hence "b + a - b < a + b \<or> b = 0" by arith
   27.45      moreover
   27.46      {assume "b =0" with z c have "P a b" by blast }
   27.47      moreover
   27.48 -    {assume ab: "b + a - b < n"
   27.49 -      have th0: "b + a - b = b + (a - b)" using lt by arith
   27.50 -      from add[rule_format, OF H(1)[rule_format, OF ab th0]]
   27.51 -      have "P b a" by (simp add: th0[symmetric])
   27.52 +    {assume "b + a - b < a + b"
   27.53 +      also have th0: "b + a - b = b + (a - b)" using lt by arith
   27.54 +      finally have "b + (a - b) < a + b" .
   27.55 +      then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
   27.56 +      then have "P b a" by (simp add: th0[symmetric])
   27.57        hence "P a b" using c by blast }
   27.58      ultimately have "P a b" by blast}
   27.59  ultimately  show "P a b" by blast
    28.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Jan 15 08:27:21 2010 +0100
    28.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Jan 15 14:43:00 2010 +0100
    28.3 @@ -341,7 +341,8 @@
    28.4          ((Binding.empty, flat inject), [iff_add]),
    28.5          ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
    28.6            [Classical.safe_elim NONE]),
    28.7 -        ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
    28.8 +        ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]),
    28.9 +        ((Binding.empty, flat (distinct @ inject)), [Induct.add_simp_rule])]
   28.10          @ named_rules @ unnamed_rules)
   28.11      |> snd
   28.12      |> add_case_tr' case_names
    29.1 --- a/src/HOL/Transitive_Closure.thy	Fri Jan 15 08:27:21 2010 +0100
    29.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Jan 15 14:43:00 2010 +0100
    29.3 @@ -106,12 +106,8 @@
    29.4  theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]:
    29.5    assumes a: "r^** a b"
    29.6      and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z"
    29.7 -  shows "P b"
    29.8 -proof -
    29.9 -  from a have "a = a --> P b"
   29.10 -    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
   29.11 -  then show ?thesis by iprover
   29.12 -qed
   29.13 +  shows "P b" using a
   29.14 +  by (induct x\<equiv>a b) (rule cases)+
   29.15  
   29.16  lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set]
   29.17  
   29.18 @@ -257,7 +253,7 @@
   29.19  lemma sym_rtrancl: "sym r ==> sym (r^*)"
   29.20    by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric])
   29.21  
   29.22 -theorem converse_rtranclp_induct[consumes 1]:
   29.23 +theorem converse_rtranclp_induct [consumes 1, case_names base step]:
   29.24    assumes major: "r^** a b"
   29.25      and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y"
   29.26    shows "P a"
   29.27 @@ -274,7 +270,7 @@
   29.28    converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),
   29.29                   consumes 1, case_names refl step]
   29.30  
   29.31 -lemma converse_rtranclpE:
   29.32 +lemma converse_rtranclpE [consumes 1, case_names base step]:
   29.33    assumes major: "r^** x z"
   29.34      and cases: "x=z ==> P"
   29.35        "!!y. [| r x y; r^** y z |] ==> P"
   29.36 @@ -352,15 +348,11 @@
   29.37  
   29.38  text {* Nice induction rule for @{text trancl} *}
   29.39  lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]:
   29.40 -  assumes "r^++ a b"
   29.41 +  assumes a: "r^++ a b"
   29.42    and cases: "!!y. r a y ==> P y"
   29.43      "!!y z. r^++ a y ==> r y z ==> P y ==> P z"
   29.44 -  shows "P b"
   29.45 -proof -
   29.46 -  from `r^++ a b` have "a = a --> P b"
   29.47 -    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
   29.48 -  then show ?thesis by iprover
   29.49 -qed
   29.50 +  shows "P b" using a
   29.51 +  by (induct x\<equiv>a b) (iprover intro: cases)+
   29.52  
   29.53  lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set]
   29.54  
   29.55 @@ -484,7 +476,7 @@
   29.56  lemma sym_trancl: "sym r ==> sym (r^+)"
   29.57    by (simp only: sym_conv_converse_eq trancl_converse [symmetric])
   29.58  
   29.59 -lemma converse_tranclp_induct:
   29.60 +lemma converse_tranclp_induct [consumes 1, case_names base step]:
   29.61    assumes major: "r^++ a b"
   29.62      and cases: "!!y. r y b ==> P(y)"
   29.63        "!!y z.[| r y z;  r^++ z b;  P(z) |] ==> P(y)"
    30.1 --- a/src/HOL/ex/ThreeDivides.thy	Fri Jan 15 08:27:21 2010 +0100
    30.2 +++ b/src/HOL/ex/ThreeDivides.thy	Fri Jan 15 14:43:00 2010 +0100
    30.3 @@ -178,21 +178,17 @@
    30.4  
    30.5  lemma exp_exists:
    30.6    "m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)"
    30.7 -proof (induct nd \<equiv> "nlen m" arbitrary: m)
    30.8 +proof (induct "nlen m" arbitrary: m)
    30.9    case 0 thus ?case by (simp add: nlen_zero)
   30.10  next
   30.11    case (Suc nd)
   30.12 -  hence IH:
   30.13 -    "nd = nlen (m div 10) \<Longrightarrow>
   30.14 -    m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
   30.15 -    by blast
   30.16    obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10"
   30.17      and cdef: "c = m mod 10" by simp
   30.18    show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)"
   30.19    proof -
   30.20      from `Suc nd = nlen m`
   30.21      have "nd = nlen (m div 10)" by (rule nlen_suc)
   30.22 -    with IH have
   30.23 +    with Suc have
   30.24        "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)" by simp
   30.25      with mexp have
   30.26        "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
    31.1 --- a/src/HOLCF/Universal.thy	Fri Jan 15 08:27:21 2010 +0100
    31.2 +++ b/src/HOLCF/Universal.thy	Fri Jan 15 14:43:00 2010 +0100
    31.3 @@ -694,13 +694,8 @@
    31.4  
    31.5  lemma basis_emb_mono:
    31.6    "x \<sqsubseteq> y \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)"
    31.7 -proof (induct n \<equiv> "max (place x) (place y)" arbitrary: x y rule: less_induct)
    31.8 -  case (less n)
    31.9 -  hence IH:
   31.10 -    "\<And>(a::'a compact_basis) b.
   31.11 -     \<lbrakk>max (place a) (place b) < max (place x) (place y); a \<sqsubseteq> b\<rbrakk>
   31.12 -        \<Longrightarrow> ubasis_le (basis_emb a) (basis_emb b)"
   31.13 -    by simp
   31.14 +proof (induct "max (place x) (place y)" arbitrary: x y rule: less_induct)
   31.15 +  case less
   31.16    show ?case proof (rule linorder_cases)
   31.17      assume "place x < place y"
   31.18      then have "rank x < rank y"
   31.19 @@ -709,7 +704,7 @@
   31.20        apply (case_tac "y = compact_bot", simp)
   31.21        apply (simp add: basis_emb.simps [of y])
   31.22        apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]])
   31.23 -      apply (rule IH)
   31.24 +      apply (rule less)
   31.25         apply (simp add: less_max_iff_disj)
   31.26         apply (erule place_sub_less)
   31.27        apply (erule rank_less_imp_below_sub [OF `x \<sqsubseteq> y`])
   31.28 @@ -724,7 +719,7 @@
   31.29        apply (case_tac "x = compact_bot", simp add: ubasis_le_minimal)
   31.30        apply (simp add: basis_emb.simps [of x])
   31.31        apply (rule ubasis_le_upper [OF fin2], simp)
   31.32 -      apply (rule IH)
   31.33 +      apply (rule less)
   31.34         apply (simp add: less_max_iff_disj)
   31.35         apply (erule place_sub_less)
   31.36        apply (erule rev_below_trans)
    32.1 --- a/src/Pure/Isar/proof.ML	Fri Jan 15 08:27:21 2010 +0100
    32.2 +++ b/src/Pure/Isar/proof.ML	Fri Jan 15 14:43:00 2010 +0100
    32.3 @@ -387,7 +387,7 @@
    32.4  fun no_goal_cases st = map (rpair NONE) (goals st);
    32.5  
    32.6  fun goal_cases st =
    32.7 -  Rule_Cases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
    32.8 +  Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
    32.9  
   32.10  fun apply_method current_context meth state =
   32.11    let
    33.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Jan 15 08:27:21 2010 +0100
    33.2 +++ b/src/Pure/Isar/rule_cases.ML	Fri Jan 15 14:43:00 2010 +0100
    33.3 @@ -25,8 +25,8 @@
    33.4      binds: (indexname * term option) list,
    33.5      cases: (string * T) list}
    33.6    val strip_params: term -> (string * typ) list
    33.7 -  val make_common: bool -> theory * term -> (string * string list) list -> cases
    33.8 -  val make_nested: bool -> term -> theory * term -> (string * string list) list -> cases
    33.9 +  val make_common: theory * term -> (string * string list) list -> cases
   33.10 +  val make_nested: term -> theory * term -> (string * string list) list -> cases
   33.11    val apply: term list -> T -> T
   33.12    val consume: thm list -> thm list -> ('a * int) * thm ->
   33.13      (('a * (int * thm list)) * thm) Seq.seq
   33.14 @@ -43,6 +43,7 @@
   33.15    val get: thm -> (string * string list) list * int
   33.16    val rename_params: string list list -> thm -> thm
   33.17    val params: string list list -> attribute
   33.18 +  val internalize_params: thm -> thm
   33.19    val mutual_rule: Proof.context -> thm list -> (int list * thm) option
   33.20    val strict_mutual_rule: Proof.context -> thm list -> int list * thm
   33.21  end;
   33.22 @@ -90,18 +91,15 @@
   33.23          chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
   33.24        in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
   33.25  
   33.26 -fun extract_case is_open thy (case_outline, raw_prop) name concls =
   33.27 +fun extract_case thy (case_outline, raw_prop) name concls =
   33.28    let
   33.29 -    val rename = if is_open then I else apfst (Name.internal o Name.clean);
   33.30 -
   33.31      val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
   33.32      val len = length props;
   33.33      val nested = is_some case_outline andalso len > 1;
   33.34  
   33.35      fun extract prop =
   33.36        let
   33.37 -        val (fixes1, fixes2) = extract_fixes case_outline prop
   33.38 -          |> apfst (map rename);
   33.39 +        val (fixes1, fixes2) = extract_fixes case_outline prop;
   33.40          val abs_fixes = abs (fixes1 @ fixes2);
   33.41          fun abs_fixes1 t =
   33.42            if not nested then abs_fixes t
   33.43 @@ -135,7 +133,7 @@
   33.44      else SOME (nested_case (hd cases))
   33.45    end;
   33.46  
   33.47 -fun make is_open rule_struct (thy, prop) cases =
   33.48 +fun make rule_struct (thy, prop) cases =
   33.49    let
   33.50      val n = length cases;
   33.51      val nprems = Logic.count_prems prop;
   33.52 @@ -143,13 +141,13 @@
   33.53        ((case try (fn () =>
   33.54            (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
   33.55          NONE => (name, NONE)
   33.56 -      | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1);
   33.57 +      | SOME p => (name, extract_case thy p name concls)) :: cs, i - 1);
   33.58    in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
   33.59  
   33.60  in
   33.61  
   33.62 -fun make_common is_open = make is_open NONE;
   33.63 -fun make_nested is_open rule_struct = make is_open (SOME rule_struct);
   33.64 +val make_common = make NONE;
   33.65 +fun make_nested rule_struct = make (SOME rule_struct);
   33.66  
   33.67  fun apply args =
   33.68    let
   33.69 @@ -334,6 +332,20 @@
   33.70  fun params xss = Thm.rule_attribute (K (rename_params xss));
   33.71  
   33.72  
   33.73 +(* internalize parameter names *)
   33.74 +
   33.75 +fun internalize_params rule =
   33.76 +  let
   33.77 +    fun rename prem =
   33.78 +      let val xs =
   33.79 +        map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
   33.80 +      in Logic.list_rename_params (xs, prem) end;
   33.81 +    fun rename_prems prop =
   33.82 +      let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
   33.83 +      in Logic.list_implies (map rename As, C) end;
   33.84 +  in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
   33.85 +
   33.86 +
   33.87  
   33.88  (** mutual_rule **)
   33.89  
    34.1 --- a/src/Tools/induct.ML	Fri Jan 15 08:27:21 2010 +0100
    34.2 +++ b/src/Tools/induct.ML	Fri Jan 15 14:43:00 2010 +0100
    34.3 @@ -10,6 +10,8 @@
    34.4    val atomize: thm list
    34.5    val rulify: thm list
    34.6    val rulify_fallback: thm list
    34.7 +  val dest_def: term -> (term * term) option
    34.8 +  val trivial_tac: int -> tactic
    34.9  end;
   34.10  
   34.11  signature INDUCT =
   34.12 @@ -42,6 +44,9 @@
   34.13    val coinduct_type: string -> attribute
   34.14    val coinduct_pred: string -> attribute
   34.15    val coinduct_del: attribute
   34.16 +  val map_simpset: (simpset -> simpset) -> Context.generic -> Context.generic
   34.17 +  val add_simp_rule: attribute
   34.18 +  val no_simpN: string
   34.19    val casesN: string
   34.20    val inductN: string
   34.21    val coinductN: string
   34.22 @@ -50,19 +55,24 @@
   34.23    val setN: string
   34.24    (*proof methods*)
   34.25    val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
   34.26 -  val add_defs: (binding option * term) option list -> Proof.context ->
   34.27 +  val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
   34.28      (term option list * thm list) * Proof.context
   34.29    val atomize_term: theory -> term -> term
   34.30 +  val atomize_cterm: conv
   34.31    val atomize_tac: int -> tactic
   34.32    val inner_atomize_tac: int -> tactic
   34.33    val rulified_term: thm -> theory * term
   34.34    val rulify_tac: int -> tactic
   34.35 +  val simplified_rule: Proof.context -> thm -> thm
   34.36 +  val simplify_tac: Proof.context -> int -> tactic
   34.37 +  val trivial_tac: int -> tactic
   34.38 +  val rotate_tac: int -> int -> int -> tactic
   34.39    val internalize: int -> thm -> thm
   34.40    val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
   34.41    val cases_tac: Proof.context -> term option list list -> thm option ->
   34.42      thm list -> int -> cases_tactic
   34.43    val get_inductT: Proof.context -> term option list list -> thm list list
   34.44 -  val induct_tac: Proof.context -> (binding option * term) option list list ->
   34.45 +  val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
   34.46      (string * typ) list list -> term option list -> thm list option ->
   34.47      thm list -> int -> cases_tactic
   34.48    val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
   34.49 @@ -107,6 +117,77 @@
   34.50  
   34.51  
   34.52  
   34.53 +(** constraint simplification **)
   34.54 +
   34.55 +(* rearrange parameters and premises to allow application of one-point-rules *)
   34.56 +
   34.57 +fun swap_params_conv ctxt i j cv =
   34.58 +  let
   34.59 +    fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
   34.60 +      | conv1 k ctxt =
   34.61 +          Conv.rewr_conv @{thm swap_params} then_conv
   34.62 +          Conv.forall_conv (conv1 (k-1) o snd) ctxt
   34.63 +    fun conv2 0 ctxt = conv1 j ctxt
   34.64 +      | conv2 k ctxt = Conv.forall_conv (conv2 (k-1) o snd) ctxt
   34.65 +  in conv2 i ctxt end;
   34.66 +
   34.67 +fun swap_prems_conv 0 = Conv.all_conv
   34.68 +  | swap_prems_conv i =
   34.69 +      Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
   34.70 +      Conv.rewr_conv Drule.swap_prems_eq
   34.71 +
   34.72 +fun drop_judgment ctxt = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt);
   34.73 +
   34.74 +fun find_eq ctxt t =
   34.75 +  let
   34.76 +    val l = length (Logic.strip_params t);
   34.77 +    val Hs = Logic.strip_assums_hyp t;
   34.78 +    fun find (i, t) =
   34.79 +      case Data.dest_def (drop_judgment ctxt t) of
   34.80 +        SOME (Bound j, _) => SOME (i, j)
   34.81 +      | SOME (_, Bound j) => SOME (i, j)
   34.82 +      | _ => NONE
   34.83 +  in
   34.84 +    case get_first find (map_index I Hs) of
   34.85 +      NONE => NONE
   34.86 +    | SOME (0, 0) => NONE
   34.87 +    | SOME (i, j) => SOME (i, l-j-1, j)
   34.88 +  end;
   34.89 +
   34.90 +fun mk_swap_rrule ctxt ct = case find_eq ctxt (term_of ct) of
   34.91 +    NONE => NONE
   34.92 +  | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct);
   34.93 +
   34.94 +val rearrange_eqs_simproc = Simplifier.simproc
   34.95 +  (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
   34.96 +  (fn thy => fn ss => fn t =>
   34.97 +     mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t))
   34.98 +
   34.99 +(* rotate k premises to the left by j, skipping over first j premises *)
  34.100 +
  34.101 +fun rotate_conv 0 j 0 = Conv.all_conv
  34.102 +  | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k-1)
  34.103 +  | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i-1) j k);
  34.104 +
  34.105 +fun rotate_tac j 0 = K all_tac
  34.106 +  | rotate_tac j k = SUBGOAL (fn (goal, i) => CONVERSION (rotate_conv
  34.107 +      j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
  34.108 +
  34.109 +(* rulify operators around definition *)
  34.110 +
  34.111 +fun rulify_defs_conv ctxt ct =
  34.112 +  if exists_subterm (is_some o Data.dest_def) (term_of ct) andalso
  34.113 +    not (is_some (Data.dest_def (drop_judgment ctxt (term_of ct))))
  34.114 +  then
  34.115 +    (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv
  34.116 +     Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt))
  34.117 +       (Conv.try_conv (rulify_defs_conv ctxt)) else_conv
  34.118 +     Conv.first_conv (map Conv.rewr_conv Data.rulify) then_conv
  34.119 +       Conv.try_conv (rulify_defs_conv ctxt)) ct
  34.120 +  else Conv.no_conv ct;
  34.121 +
  34.122 +
  34.123 +
  34.124  (** induct data **)
  34.125  
  34.126  (* rules *)
  34.127 @@ -132,23 +213,25 @@
  34.128  
  34.129  structure InductData = Generic_Data
  34.130  (
  34.131 -  type T = (rules * rules) * (rules * rules) * (rules * rules);
  34.132 +  type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset;
  34.133    val empty =
  34.134      ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
  34.135       (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
  34.136 -     (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
  34.137 +     (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)),
  34.138 +     empty_ss addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]);
  34.139    val extend = I;
  34.140 -  fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
  34.141 -      ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
  34.142 +  fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1),
  34.143 +      ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) =
  34.144      ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
  34.145 -      (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
  34.146 -      (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)));
  34.147 +     (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
  34.148 +     (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)),
  34.149 +     merge_ss (simpset1, simpset2));
  34.150  );
  34.151  
  34.152  val get_local = InductData.get o Context.Proof;
  34.153  
  34.154  fun dest_rules ctxt =
  34.155 -  let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
  34.156 +  let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in
  34.157      {type_cases = Item_Net.content casesT,
  34.158       pred_cases = Item_Net.content casesP,
  34.159       type_induct = Item_Net.content inductT,
  34.160 @@ -158,7 +241,7 @@
  34.161    end;
  34.162  
  34.163  fun print_rules ctxt =
  34.164 -  let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
  34.165 +  let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in
  34.166     [pretty_rules ctxt "coinduct type:" coinductT,
  34.167      pretty_rules ctxt "coinduct pred:" coinductP,
  34.168      pretty_rules ctxt "induct type:" inductT,
  34.169 @@ -206,9 +289,10 @@
  34.170  fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
  34.171    fold Item_Net.remove (filter_rules rs th) rs))));
  34.172  
  34.173 -fun map1 f (x, y, z) = (f x, y, z);
  34.174 -fun map2 f (x, y, z) = (x, f y, z);
  34.175 -fun map3 f (x, y, z) = (x, y, f z);
  34.176 +fun map1 f (x, y, z, s) = (f x, y, z, s);
  34.177 +fun map2 f (x, y, z, s) = (x, f y, z, s);
  34.178 +fun map3 f (x, y, z, s) = (x, y, f z, s);
  34.179 +fun map4 f (x, y, z, s) = (x, y, z, f s);
  34.180  
  34.181  fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x;
  34.182  fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x;
  34.183 @@ -234,12 +318,17 @@
  34.184  val coinduct_pred = mk_att add_coinductP consumes1;
  34.185  val coinduct_del = del_att map3;
  34.186  
  34.187 +fun map_simpset f = InductData.map (map4 f);
  34.188 +fun add_simp_rule (ctxt, thm) =
  34.189 +  (map_simpset (fn ss => ss addsimps [thm]) ctxt, thm);
  34.190 +
  34.191  end;
  34.192  
  34.193  
  34.194  
  34.195  (** attribute syntax **)
  34.196  
  34.197 +val no_simpN = "no_simp";
  34.198  val casesN = "cases";
  34.199  val inductN = "induct";
  34.200  val coinductN = "coinduct";
  34.201 @@ -268,7 +357,9 @@
  34.202    Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
  34.203      "declaration of induction rule" #>
  34.204    Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
  34.205 -    "declaration of coinduction rule";
  34.206 +    "declaration of coinduction rule" #>
  34.207 +  Attrib.setup @{binding induct_simp} (Scan.succeed add_simp_rule)
  34.208 +    "declaration of rules for simplifying induction or cases rules";
  34.209  
  34.210  end;
  34.211  
  34.212 @@ -362,7 +453,8 @@
  34.213        ruleq
  34.214        |> Seq.maps (Rule_Cases.consume [] facts)
  34.215        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
  34.216 -        CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule) cases)
  34.217 +        CASES (Rule_Cases.make_common (thy,
  34.218 +            Thm.prop_of (Rule_Cases.internalize_params rule)) cases)
  34.219            (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
  34.220    end;
  34.221  
  34.222 @@ -409,6 +501,22 @@
  34.223    (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
  34.224  
  34.225  
  34.226 +(* simplify *)
  34.227 +
  34.228 +fun simplify_conv ctxt ct =
  34.229 +  if exists_subterm (is_some o Data.dest_def) (term_of ct) then
  34.230 +    (Conv.try_conv (rulify_defs_conv ctxt) then_conv
  34.231 +       Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)))) ct
  34.232 +  else Conv.all_conv ct;
  34.233 +
  34.234 +fun simplified_rule ctxt thm =
  34.235 +  Conv.fconv_rule (Conv.prems_conv ~1 (simplify_conv ctxt)) thm;
  34.236 +
  34.237 +fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
  34.238 +
  34.239 +val trivial_tac = Data.trivial_tac;
  34.240 +
  34.241 +
  34.242  (* prepare rule *)
  34.243  
  34.244  fun rule_instance ctxt inst rule =
  34.245 @@ -548,11 +656,19 @@
  34.246  
  34.247  fun add_defs def_insts =
  34.248    let
  34.249 -    fun add (SOME (SOME x, t)) ctxt =
  34.250 +    fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
  34.251 +      | add (SOME (SOME x, (t, _))) ctxt =
  34.252            let val ([(lhs, (_, th))], ctxt') =
  34.253              LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
  34.254            in ((SOME lhs, [th]), ctxt') end
  34.255 -      | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
  34.256 +      | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
  34.257 +      | add (SOME (NONE, (t, _))) ctxt =
  34.258 +          let
  34.259 +            val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
  34.260 +            val ([(lhs, (_, th))], ctxt') =
  34.261 +              LocalDefs.add_defs [((Binding.name s, NoSyn),
  34.262 +                (Thm.empty_binding, t))] ctxt
  34.263 +          in ((SOME lhs, [th]), ctxt') end
  34.264        | add NONE ctxt = ((NONE, []), ctxt);
  34.265    in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
  34.266  
  34.267 @@ -576,12 +692,12 @@
  34.268  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
  34.269    | get_inductP _ _ = [];
  34.270  
  34.271 -fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
  34.272 +fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts =
  34.273    let
  34.274      val thy = ProofContext.theory_of ctxt;
  34.275  
  34.276      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
  34.277 -    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
  34.278 +    val atomized_defs = map (map (Conv.fconv_rule atomize_cterm)) defs;
  34.279  
  34.280      fun inst_rule (concls, r) =
  34.281        (if null insts then `Rule_Cases.get r
  34.282 @@ -601,8 +717,10 @@
  34.283            |> tap (trace_rules ctxt inductN o map #2)
  34.284            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
  34.285  
  34.286 -    fun rule_cases rule =
  34.287 -      Rule_Cases.make_nested false (Thm.prop_of rule) (rulified_term rule);
  34.288 +    fun rule_cases ctxt rule =
  34.289 +      let val rule' = (if simp then simplified_rule ctxt else I)
  34.290 +        (Rule_Cases.internalize_params rule);
  34.291 +      in Rule_Cases.make_nested (Thm.prop_of rule') (rulified_term rule') end;
  34.292    in
  34.293      (fn i => fn st =>
  34.294        ruleq
  34.295 @@ -610,19 +728,32 @@
  34.296        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
  34.297          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
  34.298            (CONJUNCTS (ALLGOALS
  34.299 -            (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
  34.300 -              THEN' fix_tac defs_ctxt
  34.301 -                (nth concls (j - 1) + more_consumes)
  34.302 -                (nth_list arbitrary (j - 1))))
  34.303 +            let
  34.304 +              val adefs = nth_list atomized_defs (j - 1);
  34.305 +              val frees = fold (Term.add_frees o prop_of) adefs [];
  34.306 +              val xs = nth_list arbitrary (j - 1);
  34.307 +              val k = nth concls (j - 1) + more_consumes
  34.308 +            in
  34.309 +              Method.insert_tac (more_facts @ adefs) THEN'
  34.310 +                (if simp then
  34.311 +                   rotate_tac k (length adefs) THEN'
  34.312 +                   fix_tac defs_ctxt k
  34.313 +                     (List.partition (member op = frees) xs |> op @)
  34.314 +                 else
  34.315 +                   fix_tac defs_ctxt k xs)
  34.316 +             end)
  34.317            THEN' inner_atomize_tac) j))
  34.318          THEN' atomize_tac) i st |> Seq.maps (fn st' =>
  34.319              guess_instance ctxt (internalize more_consumes rule) i st'
  34.320              |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
  34.321              |> Seq.maps (fn rule' =>
  34.322 -              CASES (rule_cases rule' cases)
  34.323 +              CASES (rule_cases ctxt rule' cases)
  34.324                  (Tactic.rtac rule' i THEN
  34.325                    PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
  34.326 -    THEN_ALL_NEW_CASES rulify_tac
  34.327 +    THEN_ALL_NEW_CASES
  34.328 +      ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
  34.329 +        else K all_tac)
  34.330 +       THEN_ALL_NEW rulify_tac)
  34.331    end;
  34.332  
  34.333  
  34.334 @@ -672,7 +803,8 @@
  34.335          guess_instance ctxt rule i st
  34.336          |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
  34.337          |> Seq.maps (fn rule' =>
  34.338 -          CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule') cases)
  34.339 +          CASES (Rule_Cases.make_common (thy,
  34.340 +              Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
  34.341              (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
  34.342    end;
  34.343  
  34.344 @@ -711,10 +843,15 @@
  34.345  
  34.346  val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
  34.347  
  34.348 +val inst' = Scan.lift (Args.$$$ "_") >> K NONE ||
  34.349 +  Args.term >> (SOME o rpair false) ||
  34.350 +  Scan.lift (Args.$$$ "(") |-- (Args.term >> (SOME o rpair true)) --|
  34.351 +    Scan.lift (Args.$$$ ")");
  34.352 +
  34.353  val def_inst =
  34.354    ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
  34.355 -      -- Args.term) >> SOME ||
  34.356 -    inst >> Option.map (pair NONE);
  34.357 +      -- (Args.term >> rpair false)) >> SOME ||
  34.358 +    inst' >> Option.map (pair NONE);
  34.359  
  34.360  val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
  34.361    error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
  34.362 @@ -740,11 +877,11 @@
  34.363  
  34.364  val induct_setup =
  34.365    Method.setup @{binding induct}
  34.366 -    (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
  34.367 -      (arbitrary -- taking -- Scan.option induct_rule) >>
  34.368 -      (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
  34.369 +    (Args.mode no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
  34.370 +      (arbitrary -- taking -- Scan.option induct_rule)) >>
  34.371 +      (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
  34.372          RAW_METHOD_CASES (fn facts =>
  34.373 -          Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))))
  34.374 +          Seq.DETERM (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
  34.375      "induction on types or predicates/sets";
  34.376  
  34.377  val coinduct_setup =