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.21      (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
    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.34 -apply (simp add: divmod_int_rel_def)
    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.60 -apply (simp add: divmod_int_rel_def)
    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 
    1.98      (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
    1.99 -
   1.100 -end)
   1.101 +)
   1.102  
   1.103  in
   1.104