author  paulson 
Thu, 29 Jun 2000 16:50:52 +0200  
changeset 9191  300bd596d696 
parent 8799  89e9deef4bcb 
child 9546  be095014e72f 
permissions  rwrr 
8760  1 
(* Title: Provers/Arith/cancel_numerals.ML 
8736  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 2000 University of Cambridge 

5 

8760  6 
Cancel common coefficients in balanced expressions: 
8736  7 

8760  8 
i + #m*u + j ~~ i' + #m'*u + j' == #(mm')*u + i + j ~~ i' + j' 
8736  9 

10 
where ~~ is an appropriate balancing operation (e.g. =, <=, <, ). 

8760  11 

12 
It works by (a) massaging both sides to bring the selected term to the front: 

13 

14 
#m*u + (i + j) ~~ #m'*u + (i' + j') 

15 

16 
(b) then using bal_add1 or bal_add2 to reach 

17 

18 
#(mm')*u + i + j ~~ i' + j' (if m'<=m) 

19 

20 
or 

21 

22 
i + j ~~ #(m'm)*u + i' + j' (otherwise) 

8736  23 
*) 
24 

25 
signature CANCEL_NUMERALS_DATA = 

26 
sig 

27 
(*abstract syntax*) 

28 
val mk_sum: term list > term 

29 
val dest_sum: term > term list 

30 
val mk_bal: term * term > term 

31 
val dest_bal: term > term * term 

8760  32 
val mk_coeff: int * term > term 
33 
val dest_coeff: term > int * term 

34 
val find_first_coeff: term > term list > int * term list 

35 
(*rules*) 

36 
val bal_add1: thm 

37 
val bal_add2: thm 

8736  38 
(*proof tools*) 
39 
val prove_conv: tactic list > Sign.sg > term * term > thm option 

8799  40 
val trans_tac: thm option > tactic (*applies the initial lemma*) 
41 
val norm_tac: tactic (*proves the initial lemma*) 

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

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

8736  44 
end; 
45 

46 

8760  47 
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): 
48 
sig 

49 
val proc: Sign.sg > thm list > term > thm option 

50 
end 

51 
= 

8736  52 
struct 
53 

8779  54 
(*For t = #n*u then put u in the table*) 
8760  55 
fun update_by_coeff (tab, t) = 
8779  56 
Termtab.update ((#2 (Data.dest_coeff t), ()), tab); 
8760  57 

58 
(*a lefttoright scan of terms1, seeking a term of the form #n*u, where 

59 
#m*u is in terms2 for some m*) 

60 
fun find_common (terms1,terms2) = 

61 
let val tab2 = foldl update_by_coeff (Termtab.empty, terms2) 

62 
fun seek [] = raise TERM("find_common", []) 

63 
 seek (t::terms) = 

64 
let val (_,u) = Data.dest_coeff t 

65 
in if is_some (Termtab.lookup (tab2, u)) then u 

66 
else seek terms 

67 
end 

68 
in seek terms1 end; 

8736  69 

70 
(*the simplification procedure*) 

71 
fun proc sg _ t = 

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

72 
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:
8799
diff
changeset

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

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

75 
(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:
8799
diff
changeset

76 
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:
8799
diff
changeset

77 
val (t1,t2) = Data.dest_bal t' 
8760  78 
val terms1 = Data.dest_sum t1 
79 
and terms2 = Data.dest_sum t2 

80 
val u = find_common (terms1,terms2) 

81 
val (n1, terms1') = Data.find_first_coeff u terms1 

82 
and (n2, terms2') = Data.find_first_coeff u terms2 

83 
fun newshape (i,terms) = Data.mk_sum (Data.mk_coeff(i,u)::terms) 

8779  84 
val reshape = (*Move i*u to the front and put j*u into standard form 
85 
i + #m + j + k == #m + i + (j + k) *) 

8772  86 
if n1=0 orelse n2=0 then (*trivial, so do nothing*) 
87 
raise TERM("cancel_numerals", []) 

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

89 
(t', 
8772  90 
Data.mk_bal (newshape(n1,terms1'), 
8779  91 
newshape(n2,terms2'))) 
8736  92 
in 
8799  93 
apsome Data.simplify_meta_eq 
94 
(if n2<=n1 then 

95 
Data.prove_conv 

96 
[Data.trans_tac reshape, rtac Data.bal_add1 1, 

97 
Data.numeral_simp_tac] sg 

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

98 
(t', Data.mk_bal (newshape(n1n2,terms1'), 
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8799
diff
changeset

99 
Data.mk_sum terms2')) 
8799  100 
else 
101 
Data.prove_conv 

102 
[Data.trans_tac reshape, rtac Data.bal_add2 1, 

103 
Data.numeral_simp_tac] sg 

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

104 
(t', Data.mk_bal (Data.mk_sum terms1', 
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8799
diff
changeset

105 
newshape(n2n1,terms2')))) 
8736  106 
end 
8779  107 
handle TERM _ => None 
108 
 TYPE _ => None; (*Typically (if thy doesn't include Numeral) 

109 
Undeclared type constructor "Numeral.bin"*) 

8736  110 

111 
end; 