author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 51717  9e7d1c139569 
child 59582  0fbed69ff081 
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 *) 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset

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

27 

28 
signature CANCEL_DIV_MOD = 

29 
sig 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset

30 
val proc: Proof.context > cterm > thm option 
13516  31 
end; 
32 

33 

43594  34 
functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD = 
13516  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 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset

69 
fun cancel ctxt t pq = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset

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

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset

73 
fun proc ctxt ct = 
43594  74 
let 
75 
val t = term_of ct; 

76 
val (divs, mods) = coll_div_mod t ([], []); 

77 
in 

78 
if null divs orelse null mods then NONE 

79 
else 

80 
(case inter (op =) mods divs of 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
43594
diff
changeset

81 
pq :: _ => SOME (cancel ctxt t pq) 
43594  82 
 [] => NONE) 
83 
end; 

13516  84 

17613  85 
end 