src/HOL/IntDiv.thy
 changeset 30517 51a39ed24c0f parent 30496 7cdcc9dd95cb child 30652 752329615264
```     1.1 --- a/src/HOL/IntDiv.thy	Fri Mar 13 12:29:38 2009 +0100
1.2 +++ b/src/HOL/IntDiv.thy	Fri Mar 13 19:17:57 2009 +0100
1.3 @@ -512,15 +512,12 @@
1.4  (* simprocs adapted from HOL/ex/Binary.thy *)
1.5  ML {*
1.6  local
1.7 -  infix ==;
1.8 -  val op == = Logic.mk_equals;
1.9 -  fun plus m n = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} \$ m \$ n;
1.10 -  fun mult m n = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"} \$ m \$ n;
1.11 -
1.12 -  val binary_ss = HOL_basic_ss addsimps @{thms arithmetic_simps};
1.13 -  fun prove ctxt prop =
1.14 -    Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));
1.15 -
1.16 +  val mk_number = HOLogic.mk_number HOLogic.intT;
1.17 +  fun mk_cert u k l = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} \$
1.18 +    (@{term "times :: int \<Rightarrow> int \<Rightarrow> int"} \$ u \$ mk_number k) \$
1.19 +      mk_number l;
1.20 +  fun prove ctxt prop = Goal.prove ctxt [] [] prop
1.21 +    (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps @{thms arithmetic_simps}))));
1.22    fun binary_proc proc ss ct =
1.23      (case Thm.term_of ct of
1.24        _ \$ t \$ u =>
1.25 @@ -529,16 +526,11 @@
1.26        | NONE => NONE)
1.27      | _ => NONE);
1.28  in
1.29 -
1.30 -fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
1.31 -  if n = 0 then NONE
1.32 -  else
1.33 -    let val (k, l) = Integer.div_mod m n;
1.34 -        fun mk_num x = HOLogic.mk_number HOLogic.intT x;
1.35 -    in SOME (rule OF [prove ctxt (t == plus (mult u (mk_num k)) (mk_num l))])
1.36 -    end);
1.37 -
1.38 -end;
1.39 +  fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
1.40 +    if n = 0 then NONE
1.41 +    else let val (k, l) = Integer.div_mod m n;
1.42 +    in SOME (rule OF [prove ctxt (Logic.mk_equals (t, mk_cert u k l))]) end);
1.43 +end
1.44  *}
1.45
1.46  simproc_setup binary_int_div ("number_of m div number_of n :: int") =
```