generalized simproc
authorhaftmann
Sun Oct 08 22:28:21 2017 +0200 (19 months ago)
changeset 66810cc2b490f9dc4
parent 66809 f6a30d48aab0
child 66811 aa288270732a
generalized simproc
src/HOL/Divides.thy
src/HOL/Euclidean_Division.thy
src/HOL/Nat.thy
src/HOL/Rings.thy
src/Provers/Arith/cancel_div_mod.ML
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -527,25 +527,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -ML \<open>
     1.8 -structure Cancel_Div_Mod_Int = Cancel_Div_Mod
     1.9 -(
    1.10 -  val div_name = @{const_name divide};
    1.11 -  val mod_name = @{const_name modulo};
    1.12 -  val mk_binop = HOLogic.mk_binop;
    1.13 -  val mk_sum = Arith_Data.mk_sum HOLogic.intT;
    1.14 -  val dest_sum = Arith_Data.dest_sum;
    1.15 -
    1.16 -  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
    1.17 -
    1.18 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
    1.19 -    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
    1.20 -)
    1.21 -\<close>
    1.22 -
    1.23 -simproc_setup cancel_div_mod_int ("(k::int) + l") =
    1.24 -  \<open>K Cancel_Div_Mod_Int.proc\<close>
    1.25 -
    1.26  lemma is_unit_int:
    1.27    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
    1.28    by auto
     2.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     2.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     2.3 @@ -9,16 +9,6 @@
     2.4    imports Nat_Transfer Lattices_Big
     2.5  begin
     2.6  
     2.7 -subsection \<open>Prelude: simproc for cancelling @{const divide} and @{const modulo}\<close>
     2.8 -
     2.9 -lemma (in semiring_modulo) cancel_div_mod_rules:
    2.10 -  "((a div b) * b + a mod b) + c = a + c"
    2.11 -  "(b * (a div b) + a mod b) + c = a + c"
    2.12 -  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
    2.13 -
    2.14 -ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
    2.15 -
    2.16 -
    2.17  subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
    2.18    
    2.19  class euclidean_semiring = semidom_modulo + normalization_semidom + 
    2.20 @@ -767,9 +757,10 @@
    2.21    val mk_binop = HOLogic.mk_binop;
    2.22    val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    2.23    val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
    2.24 -  fun mk_sum [] = HOLogic.zero
    2.25 -    | mk_sum [t] = t
    2.26 -    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    2.27 +  fun mk_sum' [] = HOLogic.zero
    2.28 +    | mk_sum' [t] = t
    2.29 +    | mk_sum' (t :: ts) = mk_plus (t, mk_sum' ts);
    2.30 +  fun mk_sum _ = mk_sum';
    2.31    fun dest_sum tm =
    2.32      if HOLogic.is_zero tm then []
    2.33      else
     3.1 --- a/src/HOL/Nat.thy	Sun Oct 08 22:28:21 2017 +0200
     3.2 +++ b/src/HOL/Nat.thy	Sun Oct 08 22:28:21 2017 +0200
     3.3 @@ -10,10 +10,6 @@
     3.4  imports Inductive Typedef Fun Rings
     3.5  begin
     3.6  
     3.7 -named_theorems arith "arith facts -- only ground formulas"
     3.8 -ML_file "Tools/arith_data.ML"
     3.9 -
    3.10 -
    3.11  subsection \<open>Type \<open>ind\<close>\<close>
    3.12  
    3.13  typedecl ind
     4.1 --- a/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
     4.2 +++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
     4.3 @@ -1624,8 +1624,39 @@
     4.4    "b dvd a - a mod b"
     4.5    by (simp add: minus_mod_eq_div_mult)
     4.6  
     4.7 +lemma cancel_div_mod_rules:
     4.8 +  "((a div b) * b + a mod b) + c = a + c"
     4.9 +  "(b * (a div b) + a mod b) + c = a + c"
    4.10 +  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
    4.11 +
    4.12  end
    4.13  
    4.14 +text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
    4.15 +
    4.16 +named_theorems arith "arith facts -- only ground formulas"
    4.17 +ML_file "Tools/arith_data.ML"
    4.18 +
    4.19 +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
    4.20 +
    4.21 +ML \<open>
    4.22 +structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
    4.23 +(
    4.24 +  val div_name = @{const_name divide};
    4.25 +  val mod_name = @{const_name modulo};
    4.26 +  val mk_binop = HOLogic.mk_binop;
    4.27 +  val mk_sum = Arith_Data.mk_sum;
    4.28 +  val dest_sum = Arith_Data.dest_sum;
    4.29 +
    4.30 +  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
    4.31 +
    4.32 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
    4.33 +    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
    4.34 +)
    4.35 +\<close>
    4.36 +
    4.37 +simproc_setup cancel_div_mod_int ("(a::'a::semidom_modulo) + b") =
    4.38 +  \<open>K Cancel_Div_Mod_Ring.proc\<close>
    4.39 +
    4.40  class idom_modulo = idom + semidom_modulo
    4.41  begin
    4.42  
     5.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Sun Oct 08 22:28:21 2017 +0200
     5.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Sun Oct 08 22:28:21 2017 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4    val div_name: string
     5.5    val mod_name: string
     5.6    val mk_binop: string -> term * term -> term
     5.7 -  val mk_sum: term list -> term
     5.8 +  val mk_sum: typ -> term list -> term
     5.9    val dest_sum: term -> term list
    5.10    (*logic*)
    5.11    val div_mod_eqs: thm list
    5.12 @@ -34,16 +34,16 @@
    5.13  functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
    5.14  struct
    5.15  
    5.16 -fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
    5.17 +fun coll_div_mod (Const (@{const_name Groups.plus}, _) $ s $ t) dms =
    5.18        coll_div_mod t (coll_div_mod s dms)
    5.19 -  | coll_div_mod (Const(@{const_name Groups.times},_) $ m $ (Const(d,_) $ s $ n))
    5.20 -                 (dms as (divs,mods)) =
    5.21 -      if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
    5.22 -  | coll_div_mod (Const(@{const_name Groups.times},_) $ (Const(d,_) $ s $ n) $ m)
    5.23 -                 (dms as (divs,mods)) =
    5.24 -      if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
    5.25 -  | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
    5.26 -      if m = Data.mod_name then (divs,(s,n)::mods) else dms
    5.27 +  | coll_div_mod (Const (@{const_name Groups.times}, _) $ m $ (Const (d, _) $ s $ n))
    5.28 +                 (dms as (divs, mods)) =
    5.29 +      if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms
    5.30 +  | coll_div_mod (Const (@{const_name Groups.times}, _) $ (Const (d, _) $ s $ n) $ m)
    5.31 +                 (dms as (divs, mods)) =
    5.32 +      if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms
    5.33 +  | coll_div_mod (Const (m, _) $ s $ n) (dms as (divs, mods)) =
    5.34 +      if m = Data.mod_name then (divs, (s, n) :: mods) else dms
    5.35    | coll_div_mod _ dms = dms;
    5.36  
    5.37  
    5.38 @@ -58,16 +58,18 @@
    5.39  val mk_plus = Data.mk_binop @{const_name Groups.plus};
    5.40  val mk_times = Data.mk_binop @{const_name Groups.times};
    5.41  
    5.42 -fun rearrange t pq =
    5.43 -  let val ts = Data.dest_sum t;
    5.44 -      val dpq = Data.mk_binop Data.div_name pq
    5.45 -      val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
    5.46 -      val d = if member (op =) ts d1 then d1 else d2
    5.47 -      val m = Data.mk_binop Data.mod_name pq
    5.48 -  in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end
    5.49 +fun rearrange T t pq =
    5.50 +  let
    5.51 +    val ts = Data.dest_sum t;
    5.52 +    val dpq = Data.mk_binop Data.div_name pq;
    5.53 +    val d1 = mk_times (snd pq, dpq) and d2 = mk_times (dpq, snd pq);
    5.54 +    val d = if member (op =) ts d1 then d1 else d2;
    5.55 +    val m = Data.mk_binop Data.mod_name pq;
    5.56 +  in mk_plus (mk_plus (d, m), Data.mk_sum T (ts |> remove (op =) d |> remove (op =) m)) end
    5.57  
    5.58  fun cancel ctxt t pq =
    5.59 -  let val teqt' = Data.prove_eq_sums ctxt (t, rearrange t pq)
    5.60 +  let
    5.61 +    val teqt' = Data.prove_eq_sums ctxt (t, rearrange (fastype_of t) t pq);
    5.62    in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
    5.63  
    5.64  fun proc ctxt ct =