src/HOL/Divides.thy
 changeset 41550 efa734d9b221 parent 39489 8bb7f32a3a08 child 41792 ff3cb0c418b7
```     1.1 --- a/src/HOL/Divides.thy	Fri Jan 14 15:43:04 2011 +0100
1.2 +++ b/src/HOL/Divides.thy	Fri Jan 14 15:44:47 2011 +0100
1.3 @@ -681,8 +681,8 @@
1.4  ML {*
1.5  local
1.6
1.7 -structure CancelDivMod = CancelDivModFun(struct
1.8 -
1.9 +structure CancelDivMod = CancelDivModFun
1.10 +(
1.11    val div_name = @{const_name div};
1.12    val mod_name = @{const_name mod};
1.13    val mk_binop = HOLogic.mk_binop;
1.14 @@ -691,12 +691,9 @@
1.15
1.16    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
1.17
1.18 -  val trans = trans;
1.19 -
1.20    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
1.22 -
1.23 -end)
1.24 +)
1.25
1.26  in
1.27
1.28 @@ -1352,15 +1349,16 @@
1.29  theorem posDivAlg_correct:
1.30    assumes "0 \<le> a" and "0 < b"
1.31    shows "divmod_int_rel a b (posDivAlg a b)"
1.32 -using prems apply (induct a b rule: posDivAlg.induct)
1.33 -apply auto
1.35 -apply (subst posDivAlg_eqn, simp add: right_distrib)
1.36 -apply (case_tac "a < b")
1.37 -apply simp_all
1.38 -apply (erule splitE)
1.39 -apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
1.40 -done
1.41 +  using assms
1.42 +  apply (induct a b rule: posDivAlg.induct)
1.43 +  apply auto
1.44 +  apply (simp add: divmod_int_rel_def)
1.45 +  apply (subst posDivAlg_eqn, simp add: right_distrib)
1.46 +  apply (case_tac "a < b")
1.47 +  apply simp_all
1.48 +  apply (erule splitE)
1.49 +  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
1.50 +  done
1.51
1.52
1.53  subsubsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*}
1.54 @@ -1381,15 +1379,16 @@
1.55  lemma negDivAlg_correct:
1.56    assumes "a < 0" and "b > 0"
1.57    shows "divmod_int_rel a b (negDivAlg a b)"
1.58 -using prems apply (induct a b rule: negDivAlg.induct)
1.59 -apply (auto simp add: linorder_not_le)
1.61 -apply (subst negDivAlg_eqn, assumption)
1.62 -apply (case_tac "a + b < (0\<Colon>int)")
1.63 -apply simp_all
1.64 -apply (erule splitE)
1.65 -apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
1.66 -done
1.67 +  using assms
1.68 +  apply (induct a b rule: negDivAlg.induct)
1.69 +  apply (auto simp add: linorder_not_le)
1.70 +  apply (simp add: divmod_int_rel_def)
1.71 +  apply (subst negDivAlg_eqn, assumption)
1.72 +  apply (case_tac "a + b < (0\<Colon>int)")
1.73 +  apply simp_all
1.74 +  apply (erule splitE)
1.75 +  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
1.76 +  done
1.77
1.78
1.79  subsubsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
1.80 @@ -1440,8 +1439,8 @@
1.81  ML {*
1.82  local
1.83
1.84 -structure CancelDivMod = CancelDivModFun(struct
1.85 -
1.86 +structure CancelDivMod = CancelDivModFun
1.87 +(
1.88    val div_name = @{const_name div};
1.89    val mod_name = @{const_name mod};
1.90    val mk_binop = HOLogic.mk_binop;
1.91 @@ -1450,12 +1449,9 @@
1.92
1.93    val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
1.94
1.95 -  val trans = trans;
1.96 -
1.97    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac