author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41051  2ed1b971fc20 
parent 36692  54b64d4ad524 
child 43594  ef1ddc59b825 
permissions  rwrr 
13516  1 
(* Title: Provers/Arith/cancel_div_mod.ML 
2 
Author: Tobias Nipkow, TU Muenchen 

3 

4 
Cancel div and mod terms: 

5 

6 
A + n*(m div n) + B + (m mod n) + C == A + B + C + m 

7 

22997  8 
FIXME: Is parameterized but assumes for simplicity that + and * are named 
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
33049
diff
changeset

9 
as in HOL 
13516  10 
*) 
11 

12 
signature CANCEL_DIV_MOD_DATA = 

13 
sig 

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: 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 *) 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

24 
val prove_eq_sums: simpset > term * term > thm 
13516  25 
(* must prove ac0equivalence of sums *) 
26 
end; 

27 

28 
signature CANCEL_DIV_MOD = 

29 
sig 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

30 
val proc: simpset > term > thm option 
13516  31 
end; 
32 

33 

34 
functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD = 

35 
struct 

36 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset

37 
fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms = 
13516  38 
coll_div_mod t (coll_div_mod s dms) 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset

39 
 coll_div_mod (Const(@{const_name Groups.times},_) $ m $ (Const(d,_) $ s $ n)) 
13516  40 
(dms as (divs,mods)) = 
41 
if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset

42 
 coll_div_mod (Const(@{const_name Groups.times},_) $ (Const(d,_) $ s $ n) $ m) 
13516  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 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset

58 
val mk_plus = Data.mk_binop @{const_name Groups.plus}; 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
34974
diff
changeset

59 
val mk_times = Data.mk_binop @{const_name Groups.times}; 
13516  60 

61 
fun rearrange t pq = 

62 
let val ts = Data.dest_sum t; 

63 
val dpq = Data.mk_binop Data.div_name pq 

64 
val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq) 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
35267
diff
changeset

65 
val d = if member (op =) ts d1 then d1 else d2 
13516  66 
val m = Data.mk_binop Data.mod_name pq 
33040  67 
in mk_plus(mk_plus(d,m),Data.mk_sum(ts > remove (op =) d > remove (op =) m)) end 
13516  68 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

69 
fun cancel ss t pq = 
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

70 
let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq) 
30937  71 
in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end; 
13516  72 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

73 
fun proc ss t = 
13516  74 
let val (divs,mods) = coll_div_mod t ([],[]) 
15531  75 
in if null divs orelse null mods then NONE 
33049
c38f02fdf35d
curried inter as canonical list operation (beware of argument order)
haftmann
parents:
33040
diff
changeset

76 
else case inter (op =) mods divs of 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19233
diff
changeset

77 
pq :: _ => SOME (cancel ss t pq) 
15531  78 
 [] => NONE 
13516  79 
end 
80 

17613  81 
end 