author berghofe Fri, 01 Jul 2005 14:03:50 +0200 changeset 16639 5a89d3622ac0 parent 16638 3dc904d93767 child 16640 03bdf544a552
Removed setsubgoaler hack (thanks to strengthened finsum_cong).
```--- a/src/HOL/Algebra/UnivPoly.thy	Fri Jul 01 14:02:58 2005 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Jul 01 14:03:50 2005 +0200
@@ -285,10 +285,6 @@
shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p"

-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
lemma (in UP_cring) UP_m_assoc:
assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
@@ -318,10 +314,6 @@

-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
-*}
-
lemma (in UP_cring) UP_l_one [simp]:
assumes R: "p \<in> carrier P"
shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p"
@@ -630,10 +622,6 @@
"monom P \<zero> n = \<zero>\<^bsub>P\<^esub>"

-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
lemma (in UP_cring) monom_mult_is_smult:
assumes R: "a \<in> carrier R" "p \<in> carrier P"
shows "monom P a 0 \<otimes>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p"
@@ -651,19 +639,11 @@

-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
-*}
-
"[| a \<in> carrier R; b \<in> carrier R |] ==>
monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n"
by (rule up_eqI) simp_all

-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
lemma (in UP_cring) monom_one_Suc:
"monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
proof (rule up_eqI)
@@ -739,10 +719,6 @@
qed
qed (simp_all)

-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
-*}
-
lemma (in UP_cring) monom_mult_smult:
"[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^bsub>P\<^esub> monom P b n"
by (rule up_eqI) simp_all
@@ -993,10 +969,6 @@
with boundm R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) m = \<zero>" by simp

-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
lemma (in UP_domain) deg_mult [simp]:
"[| p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
@@ -1033,10 +1005,6 @@
coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
using fin by induct (auto simp: Pi_def)

-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
lemma (in UP_cring) up_repr:
assumes R: "p \<in> carrier P"
shows "(\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
@@ -1089,10 +1057,6 @@
finally show ?thesis .
qed

-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
-*}
-
subsection {* Polynomials over an integral domain form an integral domain *}

lemma domainI:
@@ -1178,10 +1142,6 @@
!!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
sorry*)

-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
theorem (in cring) diagonal_sum:
"[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =```