1(* Title: Provers/Arith/extract_common_term.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 2000 University of Cambridge 4 5Extract 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 10where ~~ is an appropriate balancing operation (e.g. =, <=, <, -) and 0 is a 11suitable identity for +. 12 13This massaged formula is then simplified in a user-specified way. 14*) 15 16signature EXTRACT_COMMON_TERM_DATA = 17sig 18 (*abstract syntax*) 19 val mk_sum: typ -> term list -> term 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*) 25 val mk_eq: term * term -> term 26 val norm_tac: Proof.context -> tactic (*proves the result*) 27 val simplify_meta_eq: Proof.context -> thm -> thm -> thm (*simplifies the result*) 28 val simp_conv: Proof.context -> term -> thm option (*proves simp thm*) 29end; 30 31 32functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA): 33 sig 34 val proc: Proof.context -> term -> thm option 35 end 36= 37struct 38 39(*a left-to-right scan of terms1, seeking a term u that is also in terms2*) 40fun find_common (terms1,terms2) = 41 let val tab2 = fold (Termtab.update o rpair ()) terms2 Termtab.empty 42 fun seek [] = raise TERM("find_common", []) 43 | seek (u::terms) = 44 if Termtab.defined tab2 u then u 45 else seek terms 46 in seek terms1 end; 47 48(*the simplification procedure*) 49fun proc ctxt t = 50 let 51 val prems = Simplifier.prems_of ctxt; 52 val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt 53 54 val (t1,t2) = Data.dest_bal t' 55 val terms1 = Data.dest_sum t1 56 and terms2 = Data.dest_sum t2 57 58 val u = find_common (terms1,terms2) 59 val simp_th = 60 case Data.simp_conv ctxt' u of NONE => raise TERM("no simp", []) 61 | SOME th => th 62 val terms1' = Data.find_first u terms1 63 and terms2' = Data.find_first u terms2 64 and T = Term.fastype_of u 65 66 val t'' = Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')) 67 val reshape = 68 Goal.prove ctxt' [] [] (Data.mk_eq (t', t'')) (K (Data.norm_tac ctxt)) 69 70 in 71 SOME (singleton (Variable.export ctxt' ctxt) (Data.simplify_meta_eq ctxt' simp_th reshape)) 72 end 73 (* FIXME avoid handling of generic exceptions *) 74 handle TERM _ => NONE 75 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) 76 Undeclared type constructor "Numeral.bin"*) 77 78end; 79