src/Provers/Arith/cancel_div_mod.ML
changeset 66810 cc2b490f9dc4
parent 59582 0fbed69ff081
child 69593 3dda49e08b9d
     1.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val div_name: string
     1.5    val mod_name: string
     1.6    val mk_binop: string -> term * term -> term
     1.7 -  val mk_sum: term list -> term
     1.8 +  val mk_sum: typ -> term list -> term
     1.9    val dest_sum: term -> term list
    1.10    (*logic*)
    1.11    val div_mod_eqs: thm list
    1.12 @@ -34,16 +34,16 @@
    1.13  functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
    1.14  struct
    1.15  
    1.16 -fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
    1.17 +fun coll_div_mod (Const (@{const_name Groups.plus}, _) $ s $ t) dms =
    1.18        coll_div_mod t (coll_div_mod s dms)
    1.19 -  | coll_div_mod (Const(@{const_name Groups.times},_) $ m $ (Const(d,_) $ s $ n))
    1.20 -                 (dms as (divs,mods)) =
    1.21 -      if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
    1.22 -  | coll_div_mod (Const(@{const_name Groups.times},_) $ (Const(d,_) $ s $ n) $ m)
    1.23 -                 (dms as (divs,mods)) =
    1.24 -      if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
    1.25 -  | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
    1.26 -      if m = Data.mod_name then (divs,(s,n)::mods) else dms
    1.27 +  | coll_div_mod (Const (@{const_name Groups.times}, _) $ m $ (Const (d, _) $ s $ n))
    1.28 +                 (dms as (divs, mods)) =
    1.29 +      if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms
    1.30 +  | coll_div_mod (Const (@{const_name Groups.times}, _) $ (Const (d, _) $ s $ n) $ m)
    1.31 +                 (dms as (divs, mods)) =
    1.32 +      if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms
    1.33 +  | coll_div_mod (Const (m, _) $ s $ n) (dms as (divs, mods)) =
    1.34 +      if m = Data.mod_name then (divs, (s, n) :: mods) else dms
    1.35    | coll_div_mod _ dms = dms;
    1.36  
    1.37  
    1.38 @@ -58,16 +58,18 @@
    1.39  val mk_plus = Data.mk_binop @{const_name Groups.plus};
    1.40  val mk_times = Data.mk_binop @{const_name Groups.times};
    1.41  
    1.42 -fun rearrange t pq =
    1.43 -  let val ts = Data.dest_sum t;
    1.44 -      val dpq = Data.mk_binop Data.div_name pq
    1.45 -      val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
    1.46 -      val d = if member (op =) ts d1 then d1 else d2
    1.47 -      val m = Data.mk_binop Data.mod_name pq
    1.48 -  in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end
    1.49 +fun rearrange T t pq =
    1.50 +  let
    1.51 +    val ts = Data.dest_sum t;
    1.52 +    val dpq = Data.mk_binop Data.div_name pq;
    1.53 +    val d1 = mk_times (snd pq, dpq) and d2 = mk_times (dpq, snd pq);
    1.54 +    val d = if member (op =) ts d1 then d1 else d2;
    1.55 +    val m = Data.mk_binop Data.mod_name pq;
    1.56 +  in mk_plus (mk_plus (d, m), Data.mk_sum T (ts |> remove (op =) d |> remove (op =) m)) end
    1.57  
    1.58  fun cancel ctxt t pq =
    1.59 -  let val teqt' = Data.prove_eq_sums ctxt (t, rearrange t pq)
    1.60 +  let
    1.61 +    val teqt' = Data.prove_eq_sums ctxt (t, rearrange (fastype_of t) t pq);
    1.62    in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
    1.63  
    1.64  fun proc ctxt ct =