author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41051  2ed1b971fc20 
parent 35762  af3ff2ba4c54 
child 43597  b4a093e755db 
permissions  rwrr 
10537
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

1 
(* Title: Provers/Arith/cancel_numeral_factor.ML 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

3 
Copyright 2000 University of Cambridge 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

4 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

5 
Cancel common coefficients in balanced expressions: 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

6 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

7 
u*#m ~~ u'*#m' == #n*u ~~ #n'*u' 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

8 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

9 
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

10 
and d = gcd(m,m') and n=m/d and n'=m'/d. 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

11 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

12 
It works by (a) massaging both sides to bring gcd(m,m') to the front: 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

13 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

14 
u*#m ~~ u'*#m' == #d*(#n*u) ~~ #d*(#n'*u') 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

15 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

16 
(b) then using the rule "cancel" to reach #n*u ~~ #n'*u'. 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

17 
*) 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

18 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

19 
signature CANCEL_NUMERAL_FACTOR_DATA = 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

20 
sig 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

21 
(*abstract syntax*) 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

22 
val mk_bal: term * term > term 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

23 
val dest_bal: term > term * term 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23261
diff
changeset

24 
val mk_coeff: int * term > term 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23261
diff
changeset

25 
val dest_coeff: term > int * term 
10537
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

26 
(*rules*) 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

27 
val cancel: thm 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

28 
val neg_exchanges: bool (*true if a negative coeff swaps the two operands, 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

29 
as with < and <= but not = and div*) 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

30 
(*proof tools*) 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

31 
val prove_conv: tactic list > Proof.context > thm list > term * term > thm option 
16973  32 
val trans_tac: simpset > thm option > tactic (*applies the initial lemma*) 
33 
val norm_tac: simpset > tactic (*proves the initial lemma*) 

34 
val numeral_simp_tac: simpset > tactic (*proves the final theorem*) 

35 
val simplify_meta_eq: simpset > thm > thm (*simplifies the final theorem*) 

10537
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

36 
end; 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

37 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

38 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

39 
functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA): 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

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

41 
val proc: simpset > term > thm option 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

42 
end 
10537
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

43 
= 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

44 
struct 
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

45 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

46 
(*the simplification procedure*) 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
16973
diff
changeset

47 
fun proc ss t = 
15027  48 
let 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

49 
val ctxt = Simplifier.the_context ss; 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

50 
val prems = prems_of_ss ss; 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

51 
val ([t'], ctxt') = Variable.import_terms true [t] ctxt 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

52 
val export = singleton (Variable.export ctxt' ctxt) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

53 

a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

54 
val (t1,t2) = Data.dest_bal t' 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

55 
val (m1, t1') = Data.dest_coeff t1 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

56 
and (m2, t2') = Data.dest_coeff t2 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

57 
val d = (*if both are negative, also divide through by ~1*) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

58 
if (m1<0 andalso m2<=0) orelse 
23261  59 
(m1<=0 andalso m2<0) then ~ (abs (Integer.gcd m1 m2)) else abs (Integer.gcd m1 m2) 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

60 
val _ = if d=1 then (*trivial, so do nothing*) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

61 
raise TERM("cancel_numeral_factor", []) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

62 
else () 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

63 
fun newshape (i,t) = Data.mk_coeff(d, Data.mk_coeff(i,t)) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

64 
val n1 = m1 div d and n2 = m2 div d 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

65 
val rhs = if d<0 andalso Data.neg_exchanges 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

66 
then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1')) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

67 
else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2')) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

68 
val reshape = (*Move d to the front and put the rest into standard form 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

69 
i * #m * j == #d * (#n * (j * k)) *) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

70 
Data.prove_conv [Data.norm_tac ss] ctxt prems 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

71 
(t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2'))) 
10537
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

72 
in 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

73 
Option.map (export o Data.simplify_meta_eq ss) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

74 
(Data.prove_conv 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

75 
[Data.trans_tac ss reshape, rtac Data.cancel 1, 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

76 
Data.numeral_simp_tac ss] ctxt prems (t', rhs)) 
10537
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

77 
end 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

78 
(* FIXME avoid handling of generic exceptions *) 
15531  79 
handle TERM _ => NONE 
80 
 TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) 

20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

81 
Undeclared type constructor "Numeral.bin"*) 
10537
1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

82 

1d2f15504d38
simproc for cancelling common factors around = < <= div /
paulson
parents:
diff
changeset

83 
end; 