Removed setsubgoaler hack (thanks to strengthened finsum_cong).
authorberghofe
Fri Jul 01 14:03:50 2005 +0200 (2005-07-01)
changeset 166395a89d3622ac0
parent 16638 3dc904d93767
child 16640 03bdf544a552
Removed setsubgoaler hack (thanks to strengthened finsum_cong).
src/HOL/Algebra/UnivPoly.thy
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Jul 01 14:02:58 2005 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Jul 01 14:03:50 2005 +0200
     1.3 @@ -285,10 +285,6 @@
     1.4    shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p"
     1.5    by (rule up_eqI, simp add: a_comm R, simp_all add: R)
     1.6  
     1.7 -ML_setup {*
     1.8 -  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
     1.9 -*}
    1.10 -
    1.11  lemma (in UP_cring) UP_m_assoc:
    1.12    assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
    1.13    shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
    1.14 @@ -318,10 +314,6 @@
    1.15      by (simp add: Pi_def)
    1.16  qed (simp_all add: R)
    1.17  
    1.18 -ML_setup {*
    1.19 -  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    1.20 -*}
    1.21 -
    1.22  lemma (in UP_cring) UP_l_one [simp]:
    1.23    assumes R: "p \<in> carrier P"
    1.24    shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p"
    1.25 @@ -630,10 +622,6 @@
    1.26    "monom P \<zero> n = \<zero>\<^bsub>P\<^esub>"
    1.27    by (simp add: UP_def P_def)
    1.28  
    1.29 -ML_setup {*
    1.30 -  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.31 -*}
    1.32 -
    1.33  lemma (in UP_cring) monom_mult_is_smult:
    1.34    assumes R: "a \<in> carrier R" "p \<in> carrier P"
    1.35    shows "monom P a 0 \<otimes>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p"
    1.36 @@ -651,19 +639,11 @@
    1.37      by (simp add: UP_m_comm)
    1.38  qed (simp_all add: R)
    1.39  
    1.40 -ML_setup {*
    1.41 -  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    1.42 -*}
    1.43 -
    1.44  lemma (in UP_cring) monom_add [simp]:
    1.45    "[| a \<in> carrier R; b \<in> carrier R |] ==>
    1.46    monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n"
    1.47    by (rule up_eqI) simp_all
    1.48  
    1.49 -ML_setup {*
    1.50 -  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.51 -*}
    1.52 -
    1.53  lemma (in UP_cring) monom_one_Suc:
    1.54    "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
    1.55  proof (rule up_eqI)
    1.56 @@ -739,10 +719,6 @@
    1.57    qed
    1.58  qed (simp_all)
    1.59  
    1.60 -ML_setup {*
    1.61 -  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    1.62 -*}
    1.63 -
    1.64  lemma (in UP_cring) monom_mult_smult:
    1.65    "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^bsub>P\<^esub> monom P b n"
    1.66    by (rule up_eqI) simp_all
    1.67 @@ -993,10 +969,6 @@
    1.68    with boundm R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) m = \<zero>" by simp
    1.69  qed (simp add: R)
    1.70  
    1.71 -ML_setup {*
    1.72 -  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.73 -*}
    1.74 -
    1.75  lemma (in UP_domain) deg_mult [simp]:
    1.76    "[| p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
    1.77    deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
    1.78 @@ -1033,10 +1005,6 @@
    1.79      coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
    1.80    using fin by induct (auto simp: Pi_def)
    1.81  
    1.82 -ML_setup {*
    1.83 -  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.84 -*}
    1.85 -
    1.86  lemma (in UP_cring) up_repr:
    1.87    assumes R: "p \<in> carrier P"
    1.88    shows "(\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
    1.89 @@ -1089,10 +1057,6 @@
    1.90    finally show ?thesis .
    1.91  qed
    1.92  
    1.93 -ML_setup {*
    1.94 -  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    1.95 -*}
    1.96 -
    1.97  subsection {* Polynomials over an integral domain form an integral domain *}
    1.98  
    1.99  lemma domainI:
   1.100 @@ -1178,10 +1142,6 @@
   1.101    !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
   1.102    sorry*)
   1.103  
   1.104 -ML_setup {*
   1.105 -  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
   1.106 -*}
   1.107 -
   1.108  theorem (in cring) diagonal_sum:
   1.109    "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
   1.110    (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =