21 val dest_sum: term -> term list |
21 val dest_sum: term -> term list |
22 val mk_bal: term * term -> term |
22 val mk_bal: term * term -> term |
23 val dest_bal: term -> term * term |
23 val dest_bal: term -> term * term |
24 val find_first: term -> term list -> term list |
24 val find_first: term -> term list -> term list |
25 (*proof tools*) |
25 (*proof tools*) |
26 val prove_conv: tactic list -> Sign.sg -> |
26 val prove_conv: tactic list -> theory -> |
27 thm list -> string list -> term * term -> thm option |
27 thm list -> string list -> term * term -> thm option |
28 val norm_tac: tactic (*proves the result*) |
28 val norm_tac: simpset -> tactic (*proves the result*) |
29 val simplify_meta_eq: thm -> thm (*simplifies the result*) |
29 val simplify_meta_eq: simpset -> thm -> thm (*simplifies the result*) |
30 end; |
30 end; |
31 |
31 |
32 |
32 |
33 functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA): |
33 functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA): |
34 sig |
34 sig |
35 val proc: Sign.sg -> simpset -> term -> thm option |
35 val proc: theory -> simpset -> term -> thm option |
36 end |
36 end |
37 = |
37 = |
38 struct |
38 struct |
39 |
39 |
40 (*Store the term t in the table*) |
40 (*Store the term t in the table*) |
41 fun update_by_coeff (tab, t) = Termtab.update ((t, ()), tab); |
41 fun update_by_coeff t tab = Termtab.update ((t, ()), tab); |
42 |
42 |
43 (*a left-to-right scan of terms1, seeking a term u that is also in terms2*) |
43 (*a left-to-right scan of terms1, seeking a term u that is also in terms2*) |
44 fun find_common (terms1,terms2) = |
44 fun find_common (terms1,terms2) = |
45 let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2) |
45 let val tab2 = fold update_by_coeff terms2 Termtab.empty |
46 fun seek [] = raise TERM("find_common", []) |
46 fun seek [] = raise TERM("find_common", []) |
47 | seek (u::terms) = |
47 | seek (u::terms) = |
48 if isSome (Termtab.lookup (tab2, u)) then u |
48 if Termtab.defined tab2 u then u |
49 else seek terms |
49 else seek terms |
50 in seek terms1 end; |
50 in seek terms1 end; |
51 |
51 |
52 (*the simplification procedure*) |
52 (*the simplification procedure*) |
53 fun proc sg ss t = |
53 fun proc thy ss t = |
54 let |
54 let |
55 val hyps = prems_of_ss ss; |
55 val hyps = prems_of_ss ss; |
56 (*first freeze any Vars in the term to prevent flex-flex problems*) |
56 (*first freeze any Vars in the term to prevent flex-flex problems*) |
57 val (t', xs) = Term.adhoc_freeze_vars t; |
57 val (t', xs) = Term.adhoc_freeze_vars t; |
58 val (t1,t2) = Data.dest_bal t' |
58 val (t1,t2) = Data.dest_bal t' |
61 val u = find_common (terms1,terms2) |
61 val u = find_common (terms1,terms2) |
62 val terms1' = Data.find_first u terms1 |
62 val terms1' = Data.find_first u terms1 |
63 and terms2' = Data.find_first u terms2 |
63 and terms2' = Data.find_first u terms2 |
64 and T = Term.fastype_of u |
64 and T = Term.fastype_of u |
65 val reshape = |
65 val reshape = |
66 Data.prove_conv [Data.norm_tac] sg hyps xs |
66 Data.prove_conv [Data.norm_tac ss] thy hyps xs |
67 (t', |
67 (t', |
68 Data.mk_bal (Data.mk_sum T (u::terms1'), |
68 Data.mk_bal (Data.mk_sum T (u::terms1'), |
69 Data.mk_sum T (u::terms2'))) |
69 Data.mk_sum T (u::terms2'))) |
70 in |
70 in |
71 Option.map Data.simplify_meta_eq reshape |
71 Option.map (Data.simplify_meta_eq ss) reshape |
72 end |
72 end |
73 handle TERM _ => NONE |
73 handle TERM _ => NONE |
74 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
74 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
75 Undeclared type constructor "Numeral.bin"*) |
75 Undeclared type constructor "Numeral.bin"*) |
76 |
76 |