moved int_factor_simprocs.ML to theory Int
authorhaftmann
Fri May 08 08:00:11 2009 +0200 (2009-05-08)
changeset 31065d87465cbfc9e
parent 31064 ce37d8f48a9f
child 31066 972c870da225
moved int_factor_simprocs.ML to theory Int
src/HOL/Int.thy
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/Int.thy	Thu May 07 16:22:35 2009 +0200
     1.2 +++ b/src/HOL/Int.thy	Fri May 08 08:00:11 2009 +0200
     1.3 @@ -15,6 +15,9 @@
     1.4    "~~/src/Provers/Arith/assoc_fold.ML"
     1.5    "~~/src/Provers/Arith/cancel_numerals.ML"
     1.6    "~~/src/Provers/Arith/combine_numerals.ML"
     1.7 +  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
     1.8 +  "~~/src/Provers/Arith/extract_common_term.ML"
     1.9 +  ("Tools/int_factor_simprocs.ML")
    1.10    ("Tools/int_arith.ML")
    1.11  begin
    1.12  
    1.13 @@ -1517,10 +1520,11 @@
    1.14  
    1.15  use "Tools/int_arith.ML"
    1.16  declaration {* K Int_Arith.setup *}
    1.17 +use "Tools/int_factor_simprocs.ML"
    1.18  
    1.19  setup {*
    1.20    ReorientProc.add
    1.21 -    (fn Const(@{const_name number_of}, _) $ _ => true | _ => false)
    1.22 +    (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
    1.23  *}
    1.24  
    1.25  simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc
     2.1 --- a/src/HOL/IntDiv.thy	Thu May 07 16:22:35 2009 +0200
     2.2 +++ b/src/HOL/IntDiv.thy	Fri May 08 08:00:11 2009 +0200
     2.3 @@ -8,10 +8,6 @@
     2.4  
     2.5  theory IntDiv
     2.6  imports Int Divides FunDef
     2.7 -uses
     2.8 -  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
     2.9 -  "~~/src/Provers/Arith/extract_common_term.ML"
    2.10 -  ("Tools/int_factor_simprocs.ML")
    2.11  begin
    2.12  
    2.13  definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
    2.14 @@ -724,7 +720,6 @@
    2.15        apply (auto simp add: divmod_rel_def) 
    2.16        apply (auto simp add: algebra_simps)
    2.17        apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
    2.18 -      apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a])
    2.19        done
    2.20      moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
    2.21      ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
    2.22 @@ -1078,8 +1073,6 @@
    2.23     prefer 2
    2.24     apply (blast intro: order_less_trans)
    2.25    apply (simp add: zero_less_mult_iff)
    2.26 -  apply (subgoal_tac "n * k < n * 1")
    2.27 -   apply (drule mult_less_cancel_left [THEN iffD1], auto)
    2.28    done
    2.29  
    2.30  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
    2.31 @@ -1334,11 +1327,6 @@
    2.32  qed
    2.33  
    2.34  
    2.35 -subsection {* Simproc setup *}
    2.36 -
    2.37 -use "Tools/int_factor_simprocs.ML"
    2.38 -
    2.39 -
    2.40  subsection {* Code generation *}
    2.41  
    2.42  definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where