author  wenzelm 
Sun, 15 Oct 2000 19:50:35 +0200  
changeset 10220  2a726de6e124 
parent 9546  be095014e72f 
child 13484  d8f5d3391766 
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*) 
9546
be095014e72f
prove_conv gets an extra argument, so the ZF instantiation can use hyps
paulson
parents:
9191
diff
changeset

39 
val prove_conv: tactic list > Sign.sg > 
be095014e72f
prove_conv gets an extra argument, so the ZF instantiation can use hyps
paulson
parents:
9191
diff
changeset

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

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

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

8736  45 
end; 
46 

47 

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

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

51 
end 

52 
= 

8736  53 
struct 
54 

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

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

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

61 
fun find_common (terms1,terms2) = 

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

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

64 
 seek (t::terms) = 

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

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

67 
else seek terms 

68 
end 

69 
in seek terms1 end; 

8736  70 

71 
(*the simplification procedure*) 

9546
be095014e72f
prove_conv gets an extra argument, so the ZF instantiation can use hyps
paulson
parents:
9191
diff
changeset

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

73 
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

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

75 
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

76 
(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

77 
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

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

81 
val u = find_common (terms1,terms2) 

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

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

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

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

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

9546
be095014e72f
prove_conv gets an extra argument, so the ZF instantiation can use hyps
paulson
parents:
9191
diff
changeset

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

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

96 
Data.prove_conv 

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

9546
be095014e72f
prove_conv gets an extra argument, so the ZF instantiation can use hyps
paulson
parents:
9191
diff
changeset

98 
Data.numeral_simp_tac] sg hyps 
9191
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8799
diff
changeset

99 
(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

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

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

9546
be095014e72f
prove_conv gets an extra argument, so the ZF instantiation can use hyps
paulson
parents:
9191
diff
changeset

104 
Data.numeral_simp_tac] sg hyps 
9191
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8799
diff
changeset

105 
(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

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

110 
Undeclared type constructor "Numeral.bin"*) 

8736  111 

112 
end; 