author wenzelm Sat, 14 Jun 2008 23:20:06 +0200 changeset 27214 0978b8e32fd0 parent 27213 2c7a628ccdcf child 27215 b43785a81e01
tuned proof;
```--- a/src/HOL/Algebra/poly/LongDiv.thy	Sat Jun 14 23:20:05 2008 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.thy	Sat Jun 14 23:20:06 2008 +0200
@@ -138,18 +138,17 @@
apply simp
done

-ML {* simplify (@{simpset} addsimps [thm "eucl_size_def"]
-    delsimprocs [ring_simproc]) (thm "long_div_eucl_size") *}
-
-thm long_div_eucl_size [simplified]
+ML {*
+ bind_thm ("long_div_ring_aux",
+    simplify (@{simpset} addsimps [@{thm eucl_size_def}]
+    delsimprocs [ring_simproc]) (@{thm long_div_eucl_size}))
+*}

lemma long_div_ring:
"!!g::('a::ring up). g ~= 0 ==>
Ex (% (q, r, k).
(lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"
-  apply (tactic {* forw_inst_tac [("f", "f")]
-    (simplify (@{simpset} addsimps [thm "eucl_size_def"]
-      delsimprocs [ring_simproc]) (thm "long_div_eucl_size")) 1 *})
+  apply (frule_tac f = f in long_div_ring_aux)
apply (tactic {* auto_tac (@{claset}, @{simpset} delsimprocs [ring_simproc]) *})
apply (case_tac "aa = 0")
apply blast```