src/HOL/Divides.thy
changeset 41550 efa734d9b221
parent 39489 8bb7f32a3a08
child 41792 ff3cb0c418b7
--- a/src/HOL/Divides.thy	Fri Jan 14 15:43:04 2011 +0100
+++ b/src/HOL/Divides.thy	Fri Jan 14 15:44:47 2011 +0100
@@ -681,8 +681,8 @@
 ML {*
 local
 
-structure CancelDivMod = CancelDivModFun(struct
-
+structure CancelDivMod = CancelDivModFun
+(
   val div_name = @{const_name div};
   val mod_name = @{const_name mod};
   val mk_binop = HOLogic.mk_binop;
@@ -691,12 +691,9 @@
 
   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
 
-  val trans = trans;
-
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
     (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
-
-end)
+)
 
 in
 
@@ -1352,15 +1349,16 @@
 theorem posDivAlg_correct:
   assumes "0 \<le> a" and "0 < b"
   shows "divmod_int_rel a b (posDivAlg a b)"
-using prems apply (induct a b rule: posDivAlg.induct)
-apply auto
-apply (simp add: divmod_int_rel_def)
-apply (subst posDivAlg_eqn, simp add: right_distrib)
-apply (case_tac "a < b")
-apply simp_all
-apply (erule splitE)
-apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
-done
+  using assms
+  apply (induct a b rule: posDivAlg.induct)
+  apply auto
+  apply (simp add: divmod_int_rel_def)
+  apply (subst posDivAlg_eqn, simp add: right_distrib)
+  apply (case_tac "a < b")
+  apply simp_all
+  apply (erule splitE)
+  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
+  done
 
 
 subsubsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*}
@@ -1381,15 +1379,16 @@
 lemma negDivAlg_correct:
   assumes "a < 0" and "b > 0"
   shows "divmod_int_rel a b (negDivAlg a b)"
-using prems apply (induct a b rule: negDivAlg.induct)
-apply (auto simp add: linorder_not_le)
-apply (simp add: divmod_int_rel_def)
-apply (subst negDivAlg_eqn, assumption)
-apply (case_tac "a + b < (0\<Colon>int)")
-apply simp_all
-apply (erule splitE)
-apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
-done
+  using assms
+  apply (induct a b rule: negDivAlg.induct)
+  apply (auto simp add: linorder_not_le)
+  apply (simp add: divmod_int_rel_def)
+  apply (subst negDivAlg_eqn, assumption)
+  apply (case_tac "a + b < (0\<Colon>int)")
+  apply simp_all
+  apply (erule splitE)
+  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
+  done
 
 
 subsubsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
@@ -1440,8 +1439,8 @@
 ML {*
 local
 
-structure CancelDivMod = CancelDivModFun(struct
-
+structure CancelDivMod = CancelDivModFun
+(
   val div_name = @{const_name div};
   val mod_name = @{const_name mod};
   val mk_binop = HOLogic.mk_binop;
@@ -1450,12 +1449,9 @@
 
   val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
 
-  val trans = trans;
-
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
     (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
-
-end)
+)
 
 in