src/HOL/Algebra/poly/LongDiv.ML

--- a/src/HOL/Algebra/poly/LongDiv.ML	Sat Feb 10 08:49:36 2001 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.ML	Sat Feb 10 08:52:41 2001 +0100
@@ -39,7 +39,7 @@
 qed "deg_lcoeff_cancel2";
 
 Goal
-  "!!g::('a::ring up). g ~= <0> ==> \
+  "!!g::('a::ring up). g ~= 0 ==> \
 \    Ex (% (q, r, k). \
 \      (lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))";
 by (res_inst_tac [("P", "%f. Ex (% (q, r, k). \
@@ -48,16 +48,16 @@
 (* TO DO: replace by measure_induct *)
 by (res_inst_tac [("f", "eucl_size")] wf_measure 1);
 by (case_tac "eucl_size x < eucl_size g" 1);
-by (res_inst_tac [("x", "(<0>, x, 0)")] exI 1);
+by (res_inst_tac [("x", "(0, x, 0)")] exI 1);
 by (Asm_simp_tac 1);
 (* case "eucl_size x >= eucl_size g" *)
 by (dres_inst_tac [("x", "lcoeff g *s x -- (lcoeff x *s monom (deg x - deg g)) * g")] spec 1);
 by (etac impE 1);
 by (full_simp_tac (simpset() addsimps [inv_image_def, measure_def, lcoeff_def]) 1);
-by (case_tac "x = <0>" 1);
+by (case_tac "x = 0" 1);
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
-(* case "x ~= <0> *)
+(* case "x ~= 0 *)
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
 by (Simp_tac 1);
@@ -73,7 +73,10 @@
   by (rtac le_trans 1);
   by (rtac add_le_mono1 1);
   by (rtac deg_smult_ring 1);
-  by (asm_simp_tac (simpset() addsimps [leI]) 1);
+(*  by (asm_simp_tac (simpset() addsimps [leI]) 1); *)
+  by (Asm_simp_tac 1);
+  by (cut_inst_tac [("m", "deg x - deg g"), ("'a", "'a")] deg_monom_ring 1);
+  by (arith_tac 1);
 by (Force_tac 1);
 by (Simp_tac 1);
 by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1);
@@ -97,22 +100,22 @@
 qed "long_div_eucl_size";
 
 Goal
-  "!!g::('a::ring up). g ~= <0> ==> \
+  "!!g::('a::ring up). g ~= 0 ==> \
 \    Ex (% (q, r, k). \
-\      (lcoeff g)^k *s f = q * g + r & (r = <0> | deg r < deg g))";
+\      (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))";
 by (forw_inst_tac [("f", "f")]
   (simplify (simpset() addsimps [eucl_size_def]) long_div_eucl_size) 1);
 by Auto_tac;
-by (case_tac "aa = <0>" 1);
+by (case_tac "aa = 0" 1);
 by (Blast_tac 1);
-(* case "aa ~= <0> *)
+(* case "aa ~= 0 *)
 by (rotate_tac ~1 1);
 by Auto_tac;
 qed "long_div_ring";
 
 Goal
-  "!!g::('a::ring up). [| g ~= <0>; (lcoeff g) dvd <1> |] ==> \
-\    Ex (% (q, r). f = q * g + r & (r = <0> | deg r < deg g))";
+  "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd <1> |] ==> \
+\    Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))";
 by (forw_inst_tac [("f", "f")] long_div_ring 1);
 by (etac exE 1);
 by (res_inst_tac [("x", "((%(q,r,k). (inverse(lcoeff g ^k) *s q)) x, \
@@ -133,36 +136,36 @@
 qed "long_div_unit";
 
 Goal
-  "!!g::('a::field up). g ~= <0> ==> \
-\    Ex (% (q, r). f = q * g + r & (r = <0> | deg r < deg g))";
+  "!!g::('a::field up). g ~= 0 ==> \
+\    Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))";
 by (rtac long_div_unit 1);
 by (assume_tac 1);
 by (asm_simp_tac (simpset() addsimps [lcoeff_def, nonzero_lcoeff, field_ax]) 1);
 qed "long_div_theorem";
 
 Goal
-  "!!g::('a::field up). [| g ~= <0>; \
-\    f = q1 * g + r1; (r1 = <0> | deg r1 < deg g); \
-\    f = q2 * g + r2; (r2 = <0> | deg r2 < deg g) |] ==> q1 = q2";
+  "!!g::('a::field up). [| g ~= 0; \
+\    f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); \
+\    f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2";
 by (subgoal_tac "(q1 -- q2) * g = r2 -- r1" 1); (* 1 *)
 by (thin_tac "f = ?x" 1);
 by (thin_tac "f = ?x" 1);
 by (rtac diff_zero_imp_eq 1);
 by (rtac classical 1);
 by (etac disjE 1);
-(* r1 = <0> *)
+(* r1 = 0 *)
 by (etac disjE 1);
-(* r2 = <0> *)
+(* r2 = 0 *)
 by (force_tac (claset() addDs [integral], simpset()) 1);
-(* r2 ~= <0> *)
+(* r2 ~= 0 *)
 by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
 by (Force_tac 1);
-(* r1 ~=<0> *)
+(* r1 ~=0 *)
 by (etac disjE 1);
-(* r2 = <0> *)
+(* r2 = 0 *)
 by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
 by (Force_tac 1);
-(* r2 ~= <0> *)
+(* r2 ~= 0 *)
 by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1);
 by (Asm_full_simp_tac 1);
 by (dtac (order_eq_refl RS add_leD2) 1);
@@ -177,9 +180,9 @@
 qed "long_div_quo_unique";
 
 Goal
-  "!!g::('a::field up). [| g ~= <0>; \
-\    f = q1 * g + r1; (r1 = <0> | deg r1 < deg g); \
-\    f = q2 * g + r2; (r2 = <0> | deg r2 < deg g) |] ==> r1 = r2";
+  "!!g::('a::field up). [| g ~= 0; \
+\    f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); \
+\    f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2";
 by (subgoal_tac "q1 = q2" 1);
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [a_lcancel_eq]) 1);