--- a/src/HOL/Divides.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Divides.thy Sun Oct 08 22:28:21 2017 +0200
@@ -527,25 +527,6 @@
end
-ML \<open>
-structure Cancel_Div_Mod_Int = Cancel_Div_Mod
-(
- val div_name = @{const_name divide};
- val mod_name = @{const_name modulo};
- val mk_binop = HOLogic.mk_binop;
- val mk_sum = Arith_Data.mk_sum HOLogic.intT;
- val dest_sum = Arith_Data.dest_sum;
-
- val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
-
- val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
- @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
-)
-\<close>
-
-simproc_setup cancel_div_mod_int ("(k::int) + l") =
- \<open>K Cancel_Div_Mod_Int.proc\<close>
-
lemma is_unit_int:
"is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
by auto
--- a/src/HOL/Euclidean_Division.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy Sun Oct 08 22:28:21 2017 +0200
@@ -9,16 +9,6 @@
imports Nat_Transfer Lattices_Big
begin
-subsection \<open>Prelude: simproc for cancelling @{const divide} and @{const modulo}\<close>
-
-lemma (in semiring_modulo) cancel_div_mod_rules:
- "((a div b) * b + a mod b) + c = a + c"
- "(b * (a div b) + a mod b) + c = a + c"
- by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
-
-ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
-
-
subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
class euclidean_semiring = semidom_modulo + normalization_semidom +
@@ -767,9 +757,10 @@
val mk_binop = HOLogic.mk_binop;
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
- fun mk_sum [] = HOLogic.zero
- | mk_sum [t] = t
- | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+ fun mk_sum' [] = HOLogic.zero
+ | mk_sum' [t] = t
+ | mk_sum' (t :: ts) = mk_plus (t, mk_sum' ts);
+ fun mk_sum _ = mk_sum';
fun dest_sum tm =
if HOLogic.is_zero tm then []
else
--- a/src/HOL/Nat.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Nat.thy Sun Oct 08 22:28:21 2017 +0200
@@ -10,10 +10,6 @@
imports Inductive Typedef Fun Rings
begin
-named_theorems arith "arith facts -- only ground formulas"
-ML_file "Tools/arith_data.ML"
-
-
subsection \<open>Type \<open>ind\<close>\<close>
typedecl ind
--- a/src/HOL/Rings.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Rings.thy Sun Oct 08 22:28:21 2017 +0200
@@ -1624,8 +1624,39 @@
"b dvd a - a mod b"
by (simp add: minus_mod_eq_div_mult)
+lemma cancel_div_mod_rules:
+ "((a div b) * b + a mod b) + c = a + c"
+ "(b * (a div b) + a mod b) + c = a + c"
+ by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
+
end
+text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
+
+named_theorems arith "arith facts -- only ground formulas"
+ML_file "Tools/arith_data.ML"
+
+ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+
+ML \<open>
+structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
+(
+ val div_name = @{const_name divide};
+ val mod_name = @{const_name modulo};
+ val mk_binop = HOLogic.mk_binop;
+ val mk_sum = Arith_Data.mk_sum;
+ val dest_sum = Arith_Data.dest_sum;
+
+ val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
+
+ val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
+ @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
+)
+\<close>
+
+simproc_setup cancel_div_mod_int ("(a::'a::semidom_modulo) + b") =
+ \<open>K Cancel_Div_Mod_Ring.proc\<close>
+
class idom_modulo = idom + semidom_modulo
begin
--- a/src/Provers/Arith/cancel_div_mod.ML Sun Oct 08 22:28:21 2017 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML Sun Oct 08 22:28:21 2017 +0200
@@ -15,7 +15,7 @@
val div_name: string
val mod_name: string
val mk_binop: string -> term * term -> term
- val mk_sum: term list -> term
+ val mk_sum: typ -> term list -> term
val dest_sum: term -> term list
(*logic*)
val div_mod_eqs: thm list
@@ -34,16 +34,16 @@
functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
struct
-fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
+fun coll_div_mod (Const (@{const_name Groups.plus}, _) $ s $ t) dms =
coll_div_mod t (coll_div_mod s dms)
- | coll_div_mod (Const(@{const_name Groups.times},_) $ m $ (Const(d,_) $ s $ n))
- (dms as (divs,mods)) =
- if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
- | coll_div_mod (Const(@{const_name Groups.times},_) $ (Const(d,_) $ s $ n) $ m)
- (dms as (divs,mods)) =
- if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
- | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
- if m = Data.mod_name then (divs,(s,n)::mods) else dms
+ | coll_div_mod (Const (@{const_name Groups.times}, _) $ m $ (Const (d, _) $ s $ n))
+ (dms as (divs, mods)) =
+ if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms
+ | coll_div_mod (Const (@{const_name Groups.times}, _) $ (Const (d, _) $ s $ n) $ m)
+ (dms as (divs, mods)) =
+ if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms
+ | coll_div_mod (Const (m, _) $ s $ n) (dms as (divs, mods)) =
+ if m = Data.mod_name then (divs, (s, n) :: mods) else dms
| coll_div_mod _ dms = dms;
@@ -58,16 +58,18 @@
val mk_plus = Data.mk_binop @{const_name Groups.plus};
val mk_times = Data.mk_binop @{const_name Groups.times};
-fun rearrange t pq =
- let val ts = Data.dest_sum t;
- val dpq = Data.mk_binop Data.div_name pq
- val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
- val d = if member (op =) ts d1 then d1 else d2
- val m = Data.mk_binop Data.mod_name pq
- in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end
+fun rearrange T t pq =
+ let
+ val ts = Data.dest_sum t;
+ val dpq = Data.mk_binop Data.div_name pq;
+ val d1 = mk_times (snd pq, dpq) and d2 = mk_times (dpq, snd pq);
+ val d = if member (op =) ts d1 then d1 else d2;
+ val m = Data.mk_binop Data.mod_name pq;
+ in mk_plus (mk_plus (d, m), Data.mk_sum T (ts |> remove (op =) d |> remove (op =) m)) end
fun cancel ctxt t pq =
- let val teqt' = Data.prove_eq_sums ctxt (t, rearrange t pq)
+ let
+ val teqt' = Data.prove_eq_sums ctxt (t, rearrange (fastype_of t) t pq);
in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
fun proc ctxt ct =