src/Provers/Arith/extract_common_term.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 30649 57753e0ec1d4
child 35762 af3ff2ba4c54
permissions -rw-r--r--
modernized structure Object_Logic;
paulson@10694
     1
(*  Title:      Provers/Arith/extract_common_term.ML
paulson@10694
     2
    ID:         $Id$
paulson@10694
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@10694
     4
    Copyright   2000  University of Cambridge
paulson@10694
     5
paulson@10694
     6
Extract common terms in balanced expressions:
paulson@10694
     7
paulson@10694
     8
     i + u + j ~~ i' + u + j'  ==  u + (i + j) ~~ u + (i' + j')
paulson@10694
     9
     i + u     ~~ u            ==  u + i       ~~ u + 0
paulson@10694
    10
wenzelm@20114
    11
where ~~ is an appropriate balancing operation (e.g. =, <=, <, -) and 0 is a
paulson@10694
    12
suitable identity for +.
paulson@10694
    13
paulson@10694
    14
This massaged formula is then simplified in a user-specified way.
paulson@10694
    15
*)
paulson@10694
    16
paulson@10694
    17
signature EXTRACT_COMMON_TERM_DATA =
paulson@10694
    18
sig
paulson@10694
    19
  (*abstract syntax*)
paulson@14387
    20
  val mk_sum: typ -> term list -> term
paulson@10694
    21
  val dest_sum: term -> term list
paulson@10694
    22
  val mk_bal: term * term -> term
paulson@10694
    23
  val dest_bal: term -> term * term
paulson@10694
    24
  val find_first: term -> term list -> term list
paulson@10694
    25
  (*proof tools*)
wenzelm@20114
    26
  val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
wenzelm@16973
    27
  val norm_tac: simpset -> tactic                (*proves the result*)
nipkow@30649
    28
  val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*)
nipkow@30649
    29
  val simp_conv: simpset -> term -> thm option  (*proves simp thm*)
paulson@10694
    30
end;
paulson@10694
    31
paulson@10694
    32
paulson@10694
    33
functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
paulson@10694
    34
  sig
wenzelm@20044
    35
  val proc: simpset -> term -> thm option
wenzelm@20114
    36
  end
paulson@10694
    37
=
paulson@10694
    38
struct
paulson@10694
    39
paulson@10694
    40
(*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
paulson@10694
    41
fun find_common (terms1,terms2) =
wenzelm@17412
    42
  let val tab2 = fold (Termtab.update o rpair ()) terms2 Termtab.empty
wenzelm@20114
    43
      fun seek [] = raise TERM("find_common", [])
wenzelm@20114
    44
        | seek (u::terms) =
wenzelm@20114
    45
              if Termtab.defined tab2 u then u
wenzelm@20114
    46
              else seek terms
wenzelm@16973
    47
  in seek terms1 end;
paulson@10694
    48
paulson@10694
    49
(*the simplification procedure*)
wenzelm@20044
    50
fun proc ss t =
wenzelm@15027
    51
  let
wenzelm@20114
    52
    val ctxt = Simplifier.the_context ss;
wenzelm@20114
    53
    val prems = prems_of_ss ss;
wenzelm@20114
    54
    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
wenzelm@20114
    55
    val export = singleton (Variable.export ctxt' ctxt)
wenzelm@20114
    56
wenzelm@20114
    57
    val (t1,t2) = Data.dest_bal t'
wenzelm@20114
    58
    val terms1 = Data.dest_sum t1
wenzelm@20114
    59
    and terms2 = Data.dest_sum t2
wenzelm@20114
    60
wenzelm@20114
    61
    val u = find_common (terms1,terms2)
nipkow@30649
    62
    val simp_th =
nipkow@30649
    63
          case Data.simp_conv ss u of NONE => raise TERM("no simp", [])
nipkow@30649
    64
          | SOME th => th
wenzelm@20114
    65
    val terms1' = Data.find_first u terms1
wenzelm@20114
    66
    and terms2' = Data.find_first u terms2
wenzelm@20114
    67
    and T = Term.fastype_of u
wenzelm@20114
    68
wenzelm@20114
    69
    val reshape =
wenzelm@20114
    70
      Data.prove_conv [Data.norm_tac ss] ctxt prems
wenzelm@20114
    71
        (t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')))
paulson@10694
    72
  in
nipkow@30649
    73
    Option.map (export o Data.simplify_meta_eq ss simp_th) reshape
paulson@10694
    74
  end
wenzelm@20114
    75
  (* FIXME avoid handling of generic exceptions *)
skalberg@15531
    76
  handle TERM _ => NONE
skalberg@15531
    77
       | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
wenzelm@20114
    78
                             Undeclared type constructor "Numeral.bin"*)
paulson@10694
    79
paulson@10694
    80
end;