1(* Title: Provers/Arith/cancel_div_mod.ML 2 Author: Tobias Nipkow, TU Muenchen 3 4Cancel div and mod terms: 5 6 A + n*(m div n) + B + (m mod n) + C == A + B + C + m 7 8FIXME: Is parameterized but assumes for simplicity that + and * are named 9as in HOL 10*) 11 12signature CANCEL_DIV_MOD_DATA = 13sig 14 (*abstract syntax*) 15 val div_name: string 16 val mod_name: string 17 val mk_binop: string -> term * term -> term 18 val mk_sum: typ -> term list -> term 19 val dest_sum: term -> term list 20 (*logic*) 21 val div_mod_eqs: thm list 22 (* (n*(m div n) + m mod n) + k == m + k and 23 ((m div n)*n + m mod n) + k == m + k *) 24 val prove_eq_sums: Proof.context -> term * term -> thm 25 (* must prove ac0-equivalence of sums *) 26end; 27 28signature CANCEL_DIV_MOD = 29sig 30 val proc: Proof.context -> cterm -> thm option 31end; 32 33 34functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD = 35struct 36 37fun coll_div_mod (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ s $ t) dms = 38 coll_div_mod t (coll_div_mod s dms) 39 | coll_div_mod (Const (\<^const_name>\<open>Groups.times\<close>, _) $ m $ (Const (d, _) $ s $ n)) 40 (dms as (divs, mods)) = 41 if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms 42 | coll_div_mod (Const (\<^const_name>\<open>Groups.times\<close>, _) $ (Const (d, _) $ s $ n) $ m) 43 (dms as (divs, mods)) = 44 if d = Data.div_name andalso m = n then ((s, n) :: divs, mods) else dms 45 | coll_div_mod (Const (m, _) $ s $ n) (dms as (divs, mods)) = 46 if m = Data.mod_name then (divs, (s, n) :: mods) else dms 47 | coll_div_mod _ dms = dms; 48 49 50(* Proof principle: 51 1. (...div...)+(...mod...) == (div + mod) + rest 52 in function rearrange 53 2. (div + mod) + ?x = d + ?x 54 Data.div_mod_eq 55 ==> thesis by transitivity 56*) 57 58val mk_plus = Data.mk_binop \<^const_name>\<open>Groups.plus\<close>; 59val mk_times = Data.mk_binop \<^const_name>\<open>Groups.times\<close>; 60 61fun rearrange T t pq = 62 let 63 val ts = Data.dest_sum t; 64 val dpq = Data.mk_binop Data.div_name pq; 65 val d1 = mk_times (snd pq, dpq) and d2 = mk_times (dpq, snd pq); 66 val d = if member (op =) ts d1 then d1 else d2; 67 val m = Data.mk_binop Data.mod_name pq; 68 in mk_plus (mk_plus (d, m), Data.mk_sum T (ts |> remove (op =) d |> remove (op =) m)) end 69 70fun cancel ctxt t pq = 71 let 72 val teqt' = Data.prove_eq_sums ctxt (t, rearrange (fastype_of t) t pq); 73 in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end; 74 75fun proc ctxt ct = 76 let 77 val t = Thm.term_of ct; 78 val (divs, mods) = coll_div_mod t ([], []); 79 in 80 if null divs orelse null mods then NONE 81 else 82 (case inter (op =) mods divs of 83 pq :: _ => SOME (cancel ctxt t pq) 84 | [] => NONE) 85 end; 86 87end 88