author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41051  2ed1b971fc20 
parent 35762  af3ff2ba4c54 
child 43597  b4a093e755db 
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*) 

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

25 
val prove_conv: tactic list > Proof.context > thm list > term * term > thm option 
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; 
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset

52 
val prems = prems_of_ss ss; 
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 

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

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

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

70 
(t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2'))) 
10694  71 
in 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
20114
diff
changeset

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

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

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

79 
end; 