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") =