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 -> Proof.context -> thm list -> term * term -> thm option |
26 val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option |
27 val norm_tac: simpset -> tactic (*proves the result*) |
27 val norm_tac: simpset -> tactic (*proves the result*) |
28 val simplify_meta_eq: simpset -> thm -> thm (*simplifies the result*) |
28 val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*) |
|
29 val simp_conv: simpset -> term -> thm option (*proves simp thm*) |
29 end; |
30 end; |
30 |
31 |
31 |
32 |
32 functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA): |
33 functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA): |
33 sig |
34 sig |
56 val (t1,t2) = Data.dest_bal t' |
57 val (t1,t2) = Data.dest_bal t' |
57 val terms1 = Data.dest_sum t1 |
58 val terms1 = Data.dest_sum t1 |
58 and terms2 = Data.dest_sum t2 |
59 and terms2 = Data.dest_sum t2 |
59 |
60 |
60 val u = find_common (terms1,terms2) |
61 val u = find_common (terms1,terms2) |
|
62 val simp_th = |
|
63 case Data.simp_conv ss u of NONE => raise TERM("no simp", []) |
|
64 | SOME th => th |
61 val terms1' = Data.find_first u terms1 |
65 val terms1' = Data.find_first u terms1 |
62 and terms2' = Data.find_first u terms2 |
66 and terms2' = Data.find_first u terms2 |
63 and T = Term.fastype_of u |
67 and T = Term.fastype_of u |
64 |
68 |
65 val reshape = |
69 val reshape = |
66 Data.prove_conv [Data.norm_tac ss] ctxt prems |
70 Data.prove_conv [Data.norm_tac ss] ctxt prems |
67 (t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2'))) |
71 (t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2'))) |
68 in |
72 in |
69 Option.map (export o Data.simplify_meta_eq ss) reshape |
73 Option.map (export o Data.simplify_meta_eq ss simp_th) reshape |
70 end |
74 end |
71 (* FIXME avoid handling of generic exceptions *) |
75 (* FIXME avoid handling of generic exceptions *) |
72 handle TERM _ => NONE |
76 handle TERM _ => NONE |
73 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
77 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
74 Undeclared type constructor "Numeral.bin"*) |
78 Undeclared type constructor "Numeral.bin"*) |