author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41051  2ed1b971fc20 
parent 35762  af3ff2ba4c54 
child 44947  8ae418dfe561 
permissions  rwrr 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

1 
(* Title: Provers/Arith/combine_numerals.ML 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

3 
Copyright 2000 University of Cambridge 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

4 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

5 
Combine coefficients in expressions: 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

6 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

7 
i + #m*u + j ... + #n*u + k == #(m+n)*u + (i + (j + k)) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

8 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

9 
It works by (a) massaging the sum to bring the selected terms to the front: 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

10 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

11 
#m*u + (#n*u + (i + (j + k))) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

12 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

13 
(b) then using left_distrib to reach 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

14 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

15 
#(m+n)*u + (i + (j + k)) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

16 
*) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

17 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

18 
signature COMBINE_NUMERALS_DATA = 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

19 
sig 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

20 
(*abstract syntax*) 
23058
c722004c5a22
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents:
20114
diff
changeset

21 
eqtype coeff 
c722004c5a22
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents:
20114
diff
changeset

22 
val iszero: coeff > bool 
c722004c5a22
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents:
20114
diff
changeset

23 
val add: coeff * coeff > coeff (*addition (or multiplication) *) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13484
diff
changeset

24 
val mk_sum: typ > term list > term 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

25 
val dest_sum: term > term list 
23058
c722004c5a22
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents:
20114
diff
changeset

26 
val mk_coeff: coeff * term > term 
c722004c5a22
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents:
20114
diff
changeset

27 
val dest_coeff: term > coeff * term 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

28 
(*rules*) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

29 
val left_distrib: thm 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
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 > 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*) 

8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

36 
end; 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

37 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

38 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

39 
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

40 
sig 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
17412
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 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

43 
= 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

44 
struct 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

45 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

46 
(*Remove the first occurrence of #m*u from the term list*) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

47 
fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*) 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

48 
raise TERM("combine_numerals: remove", []) 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

49 
 remove (m, u, t::terms) = 
9646  50 
case try Data.dest_coeff t of 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

51 
SOME(n,v) => if m=n andalso u aconv v then terms 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

52 
else t :: remove (m, u, terms) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

53 
 NONE => t :: remove (m, u, terms); 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

54 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

55 
(*a lefttoright scan of terms, seeking another term of the form #n*u, where 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

56 
#m*u is already in terms for some m*) 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

57 
fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

58 
 find_repeated (tab, past, t::terms) = 
9646  59 
case try Data.dest_coeff t of 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

60 
SOME(n,u) => 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

61 
(case Termtab.lookup tab u of 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

62 
SOME m => (u, m, n, rev (remove (m,u,past)) @ terms) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

63 
 NONE => find_repeated (Termtab.update (u, n) tab, 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

64 
t::past, terms)) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

65 
 NONE => find_repeated (tab, t::past, terms); 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

66 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

68 
fun proc ss t = 
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
17412
diff
changeset

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

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

71 
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

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

73 

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

74 
val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

75 
val T = Term.fastype_of u 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

76 

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

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

78 
i + #m + j + k == #m + i + (j + k) *) 
23058
c722004c5a22
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents:
20114
diff
changeset

79 
if Data.iszero m orelse Data.iszero n then (*trivial, so do nothing*) 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

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

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

82 
(t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms)) 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

84 
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

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

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

87 
Data.numeral_simp_tac ss] ctxt 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

88 
(t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

90 
(* FIXME avoid handling of generic exceptions *) 
15531  91 
handle TERM _ => NONE 
92 
 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

93 
Undeclared type constructor "Numeral.bin"*) 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

94 

ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

95 
end; 