src/Provers/Arith/extract_common_term.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 51717 9e7d1c139569
child 70315 2f9623aa1eeb
permissions -rw-r--r--
more robust sorted_entries;
     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 
    10 where ~~ is an appropriate balancing operation (e.g. =, <=, <, -) and 0 is a
    11 suitable identity for +.
    12 
    13 This massaged formula is then simplified in a user-specified way.
    14 *)
    15 
    16 signature EXTRACT_COMMON_TERM_DATA =
    17 sig
    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*)
    29 end;
    30 
    31 
    32 functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
    33   sig
    34   val proc: Proof.context -> term -> thm option
    35   end
    36 =
    37 struct
    38 
    39 (*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
    40 fun 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*)
    49 fun proc ctxt t =
    50   let
    51     val prems = Simplifier.prems_of ctxt;
    52     val ([t'], ctxt') = Variable.import_terms true [t] ctxt
    53     val export = singleton (Variable.export ctxt' ctxt)
    54     (* FIXME ctxt vs. ctxt' (!?) *)
    55 
    56     val (t1,t2) = Data.dest_bal t'
    57     val terms1 = Data.dest_sum t1
    58     and terms2 = Data.dest_sum t2
    59 
    60     val u = find_common (terms1,terms2)
    61     val simp_th =
    62           case Data.simp_conv ctxt u of NONE => raise TERM("no simp", [])
    63           | SOME th => th
    64     val terms1' = Data.find_first u terms1
    65     and terms2' = Data.find_first u terms2
    66     and T = Term.fastype_of u
    67 
    68     val t'' = Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2'))
    69     val reshape =
    70       Goal.prove ctxt [] [] (Data.mk_eq (t', t'')) (K (Data.norm_tac ctxt))
    71 
    72   in
    73     SOME (export (Data.simplify_meta_eq ctxt simp_th reshape))
    74   end
    75   (* FIXME avoid handling of generic exceptions *)
    76   handle TERM _ => NONE
    77        | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
    78                              Undeclared type constructor "Numeral.bin"*)
    79 
    80 end;