author  blanchet 
Mon, 26 Nov 2012 13:35:05 +0100  
changeset 50222  40e3c3be6bca 
parent 45306  1e380c50a183 
child 51717  9e7d1c139569 
permissions  rwrr 
10694  1 
(* Title: Provers/Arith/extract_common_term.ML 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
Copyright 2000 University of Cambridge 

4 

5 
Extract common terms in balanced expressions: 

6 

7 
i + u + j ~~ i' + u + j' == u + (i + j) ~~ u + (i' + j') 

8 
i + u ~~ u == u + i ~~ u + 0 

9 

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

10 
where ~~ is an appropriate balancing operation (e.g. =, <=, <, ) and 0 is a 
10694  11 
suitable identity for +. 
12 

13 
This massaged formula is then simplified in a userspecified way. 

14 
*) 

15 

16 
signature EXTRACT_COMMON_TERM_DATA = 

17 
sig 

18 
(*abstract syntax*) 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13484
diff
changeset

19 
val mk_sum: typ > term list > term 
10694  20 
val dest_sum: term > term list 
21 
val mk_bal: term * term > term 

22 
val dest_bal: term > term * term 

23 
val find_first: term > term list > term list 

24 
(*proof tools*) 

45270
d5b5c9259afd
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
huffman
parents:
43597
diff
changeset

25 
val mk_eq: term * term > term 
16973  26 
val norm_tac: simpset > tactic (*proves the result*) 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
20114
diff
changeset

27 
val simplify_meta_eq: simpset > thm > thm > thm (*simplifies the result*) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
20114
diff
changeset

28 
val simp_conv: simpset > term > thm option (*proves simp thm*) 
10694  29 
end; 
30 

31 

32 
functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA): 

33 
sig 

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

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

35 
end 
10694  36 
= 
37 
struct 

38 

39 
(*a lefttoright scan of terms1, seeking a term u that is also in terms2*) 

40 
fun find_common (terms1,terms2) = 

17412  41 
let val tab2 = fold (Termtab.update o rpair ()) terms2 Termtab.empty 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

42 
fun seek [] = raise TERM("find_common", []) 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

43 
 seek (u::terms) = 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

44 
if Termtab.defined tab2 u then u 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

45 
else seek terms 
16973  46 
in seek terms1 end; 
10694  47 

48 
(*the simplification procedure*) 

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

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

51 
val ctxt = Simplifier.the_context ss; 
43597  52 
val prems = Simplifier.prems_of ss; 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

53 
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

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

55 

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

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

57 
val terms1 = Data.dest_sum t1 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

58 
and terms2 = Data.dest_sum t2 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

59 

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

60 
val u = find_common (terms1,terms2) 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
20114
diff
changeset

61 
val simp_th = 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
20114
diff
changeset

62 
case Data.simp_conv ss u of NONE => raise TERM("no simp", []) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
20114
diff
changeset

63 
 SOME th => th 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

64 
val terms1' = Data.find_first u terms1 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

65 
and terms2' = Data.find_first u terms2 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

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

67 

45270
d5b5c9259afd
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
huffman
parents:
43597
diff
changeset

68 
val t'' = Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')) 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

69 
val reshape = 
45270
d5b5c9259afd
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
huffman
parents:
43597
diff
changeset

70 
Goal.prove ctxt [] [] (Data.mk_eq (t', t'')) (K (Data.norm_tac ss)) 
d5b5c9259afd
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
huffman
parents:
43597
diff
changeset

71 

10694  72 
in 
45270
d5b5c9259afd
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
huffman
parents:
43597
diff
changeset

73 
SOME (export (Data.simplify_meta_eq ss simp_th reshape)) 
10694  74 
end 
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

75 
(* FIXME avoid handling of generic exceptions *) 
15531  76 
handle TERM _ => NONE 
77 
 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

78 
Undeclared type constructor "Numeral.bin"*) 
10694  79 

80 
end; 