136 thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc1", thm "smult_assoc2"] |
136 thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc1", thm "smult_assoc2"] |
137 delsimprocs [ring_simproc]) 1 *}) |
137 delsimprocs [ring_simproc]) 1 *}) |
138 apply simp |
138 apply simp |
139 done |
139 done |
140 |
140 |
141 ML {* simplify (@{simpset} addsimps [thm "eucl_size_def"] |
141 ML {* |
142 delsimprocs [ring_simproc]) (thm "long_div_eucl_size") *} |
142 bind_thm ("long_div_ring_aux", |
143 |
143 simplify (@{simpset} addsimps [@{thm eucl_size_def}] |
144 thm long_div_eucl_size [simplified] |
144 delsimprocs [ring_simproc]) (@{thm long_div_eucl_size})) |
|
145 *} |
145 |
146 |
146 lemma long_div_ring: |
147 lemma long_div_ring: |
147 "!!g::('a::ring up). g ~= 0 ==> |
148 "!!g::('a::ring up). g ~= 0 ==> |
148 Ex (% (q, r, k). |
149 Ex (% (q, r, k). |
149 (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))" |
150 (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))" |
150 apply (tactic {* forw_inst_tac [("f", "f")] |
151 apply (frule_tac f = f in long_div_ring_aux) |
151 (simplify (@{simpset} addsimps [thm "eucl_size_def"] |
|
152 delsimprocs [ring_simproc]) (thm "long_div_eucl_size")) 1 *}) |
|
153 apply (tactic {* auto_tac (@{claset}, @{simpset} delsimprocs [ring_simproc]) *}) |
152 apply (tactic {* auto_tac (@{claset}, @{simpset} delsimprocs [ring_simproc]) *}) |
154 apply (case_tac "aa = 0") |
153 apply (case_tac "aa = 0") |
155 apply blast |
154 apply blast |
156 (* case "aa ~= 0 *) |
155 (* case "aa ~= 0 *) |
157 apply (rotate_tac -1) |
156 apply (rotate_tac -1) |