author  paulson 
Thu, 29 Jun 2000 16:50:52 +0200  
changeset 9191  300bd596d696 
parent 8816  31b4fb3d8d60 
child 9571  c869d1886a32 
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 
ID: $Id$ 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

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

5 

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

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

7 

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

8 
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

9 

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

10 
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

11 

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

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

13 

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

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

15 

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

16 
#(m+n)*u + (i + (j + k)) 
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 

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

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

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

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

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

23 
val dest_sum: term > term list 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

24 
val mk_coeff: int * term > term 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

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

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

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

29 
val prove_conv: tactic list > Sign.sg > term * term > thm option 
8799  30 
val trans_tac: thm option > tactic (*applies the initial lemma*) 
31 
val norm_tac: tactic (*proves the initial lemma*) 

32 
val numeral_simp_tac: tactic (*proves the final theorem*) 

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

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

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

35 

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

36 

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

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

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

39 
val proc: Sign.sg > thm list > term > thm option 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

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

42 
struct 
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 
(*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

45 
fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

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

48 
let val (n,v) = Data.dest_coeff t 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

49 
in if m=n andalso u aconv v then terms 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

50 
else t :: remove (m, u, terms) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

52 

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

53 
(*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

54 
#m*u is already in terms for some m*) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

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

57 
let val (n,u) = Data.dest_coeff t 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

59 
case Termtab.lookup (tab, u) of 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

60 
Some m => (u, m, n, rev (remove (m,u,past)) @ terms) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

61 
 None => find_repeated (Termtab.update ((u,n), tab), 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

62 
t::past, terms) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

64 

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

65 
(*the simplification procedure*) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

66 
fun proc sg _ t = 
9191
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8816
diff
changeset

67 
let (*first freeze any Vars in the term to prevent flexflex problems*) 
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8816
diff
changeset

68 
val rand_s = gensym"_" 
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8816
diff
changeset

69 
fun mk_inst (var as Var((a,i),T)) = 
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8816
diff
changeset

70 
(var, Free((a ^ rand_s ^ string_of_int i), T)) 
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8816
diff
changeset

71 
val t' = subst_atomic (map mk_inst (term_vars t)) t 
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8816
diff
changeset

72 
val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') 
8774
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

73 
val reshape = (*Move i*u to the front and put j*u into standard form 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

75 
if m=0 orelse n=0 then (*trivial, so do nothing*) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

77 
else Data.prove_conv [Data.norm_tac] sg 
9191
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8816
diff
changeset

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

79 
Data.mk_sum ([Data.mk_coeff(m,u), 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

80 
Data.mk_coeff(n,u)] @ terms)) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

81 
in 
8799  82 
apsome Data.simplify_meta_eq 
83 
(Data.prove_conv 

84 
[Data.trans_tac reshape, rtac Data.left_distrib 1, 

85 
Data.numeral_simp_tac] sg 

9191
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8816
diff
changeset

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

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

88 
handle TERM _ => None 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

89 
 TYPE _ => None; (*Typically (if thy doesn't include Numeral) 
ad5026ff0c16
new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff
changeset

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

91 

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

92 
end; 