merged

--- a/src/HOL/Polynomial.thy	Tue Jan 27 19:56:26 2009 +0100
+++ b/src/HOL/Polynomial.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -475,6 +475,16 @@
 lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
   by (induct n, simp add: monom_0, simp add: monom_Suc)
 
+lemma degree_smult_eq [simp]:
+  fixes a :: "'a::idom"
+  shows "degree (smult a p) = (if a = 0 then 0 else degree p)"
+  by (cases "a = 0", simp, simp add: degree_def)
+
+lemma smult_eq_0_iff [simp]:
+  fixes a :: "'a::idom"
+  shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
+  by (simp add: expand_poly_eq)
+
 
 subsection {* Multiplication of polynomials *}
 
@@ -777,6 +787,12 @@
   qed
 qed
 
+lemma pdivmod_rel_0_iff: "pdivmod_rel 0 y q r \<longleftrightarrow> q = 0 \<and> r = 0"
+by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_0)
+
+lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
+by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
+
 lemmas pdivmod_rel_unique_div =
   pdivmod_rel_unique [THEN conjunct1, standard]
 
@@ -861,6 +877,54 @@
   thus "x mod y = x" by (rule mod_poly_eq)
 qed
 
+lemma pdivmod_rel_smult_left:
+  "pdivmod_rel x y q r
+    \<Longrightarrow> pdivmod_rel (smult a x) y (smult a q) (smult a r)"
+  unfolding pdivmod_rel_def by (simp add: smult_add_right)
+
+lemma div_smult_left: "(smult a x) div y = smult a (x div y)"
+  by (rule div_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
+
+lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
+  by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
+
+lemma pdivmod_rel_smult_right:
+  "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
+    \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
+  unfolding pdivmod_rel_def by simp
+
+lemma div_smult_right:
+  "a \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
+  by (rule div_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
+
+lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
+  by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
+
+lemma pdivmod_rel_mult:
+  "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
+    \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"
+apply (cases "z = 0", simp add: pdivmod_rel_def)
+apply (cases "y = 0", simp add: pdivmod_rel_by_0_iff pdivmod_rel_0_iff)
+apply (cases "r = 0")
+apply (cases "r' = 0")
+apply (simp add: pdivmod_rel_def)
+apply (simp add: pdivmod_rel_def ring_simps degree_mult_eq)
+apply (cases "r' = 0")
+apply (simp add: pdivmod_rel_def degree_mult_eq)
+apply (simp add: pdivmod_rel_def ring_simps)
+apply (simp add: degree_mult_eq degree_add_less)
+done
+
+lemma poly_div_mult_right:
+  fixes x y z :: "'a::field poly"
+  shows "x div (y * z) = (x div y) div z"
+  by (rule div_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
+
+lemma poly_mod_mult_right:
+  fixes x y z :: "'a::field poly"
+  shows "x mod (y * z) = y * (x div y mod z) + x mod y"
+  by (rule mod_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
+
 lemma mod_pCons:
   fixes a and x
   assumes y: "y \<noteq> 0"

--- a/src/HOLCF/Tools/cont_proc.ML	Tue Jan 27 19:56:26 2009 +0100
+++ b/src/HOLCF/Tools/cont_proc.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -7,7 +7,7 @@
   val is_lcf_term: term -> bool
   val cont_thms: term -> thm list
   val all_cont_thms: term -> thm list
-  val cont_tac: thm list ref -> int -> tactic
+  val cont_tac: int -> tactic
   val cont_proc: theory -> simproc
   val setup: theory -> theory
 end;
@@ -15,15 +15,6 @@
 structure ContProc: CONT_PROC =
 struct
 
-structure ContProcData = TheoryDataFun
-(
-  type T = thm list ref;
-  val empty = ref [];
-  val copy = I;
-  val extend = I;
-  fun merge _ _ = ref [];
-)
-
 (** theory context references **)
 
 val cont_K = @{thm cont_const};
@@ -107,26 +98,21 @@
   conditional rewrite rule with the unsolved subgoals as premises.
 *)
 
-fun cont_tac prev_cont_thms =
+val cont_tac =
   let
     val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
   
-    fun old_cont_tac i thm =
-      case !prev_cont_thms of
-        [] => no_tac thm
-      | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
-
-    fun new_cont_tac f' i thm =
+    fun new_cont_tac f' i =
       case all_cont_thms f' of
-        [] => no_tac thm
-      | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
+        [] => no_tac
+      | (c::cs) => rtac c i;
 
     fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
       let
         val f' = Const (@{const_name Abs_CFun}, dummyT) $ f;
       in
         if is_lcf_term f'
-        then old_cont_tac ORELSE' new_cont_tac f'
+        then new_cont_tac f'
         else REPEAT_ALL_NEW (resolve_tac rules)
       end
       | cont_tac_of_term _ = K no_tac;
@@ -139,8 +125,7 @@
   fun solve_cont thy _ t =
     let
       val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
-      val prev_thms = ContProcData.get thy
-    in Option.map fst (Seq.pull (cont_tac prev_thms 1 tr)) end
+    in Option.map fst (Seq.pull (cont_tac 1 tr)) end
 in
   fun cont_proc thy =
     Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;