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;
```