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;
paulson@10694
     1
(*  Title:      Provers/Arith/extract_common_term.ML
paulson@10694
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@10694
     3
    Copyright   2000  University of Cambridge
paulson@10694
     4
paulson@10694
     5
Extract common terms in balanced expressions:
paulson@10694
     6
paulson@10694
     7
     i + u + j ~~ i' + u + j'  ==  u + (i + j) ~~ u + (i' + j')
paulson@10694
     8
     i + u     ~~ u            ==  u + i       ~~ u + 0
paulson@10694
     9
wenzelm@20114
    10
where ~~ is an appropriate balancing operation (e.g. =, <=, <, -) and 0 is a
paulson@10694
    11
suitable identity for +.
paulson@10694
    12
paulson@10694
    13
This massaged formula is then simplified in a user-specified way.
paulson@10694
    14
*)
paulson@10694
    15
paulson@10694
    16
signature EXTRACT_COMMON_TERM_DATA =
paulson@10694
    17
sig
paulson@10694
    18
  (*abstract syntax*)
paulson@14387
    19
  val mk_sum: typ -> term list -> term
paulson@10694
    20
  val dest_sum: term -> term list
paulson@10694
    21
  val mk_bal: term * term -> term
paulson@10694
    22
  val dest_bal: term -> term * term
paulson@10694
    23
  val find_first: term -> term list -> term list
paulson@10694
    24
  (*proof tools*)
huffman@45270
    25
  val mk_eq: term * term -> term
wenzelm@51717
    26
  val norm_tac: Proof.context -> tactic                (*proves the result*)
wenzelm@51717
    27
  val simplify_meta_eq: Proof.context -> thm -> thm -> thm (*simplifies the result*)
wenzelm@51717
    28
  val simp_conv: Proof.context -> term -> thm option  (*proves simp thm*)
paulson@10694
    29
end;
paulson@10694
    30
paulson@10694
    31
paulson@10694
    32
functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
paulson@10694
    33
  sig
wenzelm@51717
    34
  val proc: Proof.context -> term -> thm option
wenzelm@20114
    35
  end
paulson@10694
    36
=
paulson@10694
    37
struct
paulson@10694
    38
paulson@10694
    39
(*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
paulson@10694
    40
fun find_common (terms1,terms2) =
wenzelm@17412
    41
  let val tab2 = fold (Termtab.update o rpair ()) terms2 Termtab.empty
wenzelm@20114
    42
      fun seek [] = raise TERM("find_common", [])
wenzelm@20114
    43
        | seek (u::terms) =
wenzelm@20114
    44
              if Termtab.defined tab2 u then u
wenzelm@20114
    45
              else seek terms
wenzelm@16973
    46
  in seek terms1 end;
paulson@10694
    47
paulson@10694
    48
(*the simplification procedure*)
wenzelm@51717
    49
fun proc ctxt t =
wenzelm@15027
    50
  let
wenzelm@51717
    51
    val prems = Simplifier.prems_of ctxt;
wenzelm@20114
    52
    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
wenzelm@20114
    53
    val export = singleton (Variable.export ctxt' ctxt)
wenzelm@51717
    54
    (* FIXME ctxt vs. ctxt' (!?) *)
wenzelm@20114
    55
wenzelm@20114
    56
    val (t1,t2) = Data.dest_bal t'
wenzelm@20114
    57
    val terms1 = Data.dest_sum t1
wenzelm@20114
    58
    and terms2 = Data.dest_sum t2
wenzelm@20114
    59
wenzelm@20114
    60
    val u = find_common (terms1,terms2)
nipkow@30649
    61
    val simp_th =
wenzelm@51717
    62
          case Data.simp_conv ctxt u of NONE => raise TERM("no simp", [])
nipkow@30649
    63
          | SOME th => th
wenzelm@20114
    64
    val terms1' = Data.find_first u terms1
wenzelm@20114
    65
    and terms2' = Data.find_first u terms2
wenzelm@20114
    66
    and T = Term.fastype_of u
wenzelm@20114
    67
huffman@45270
    68
    val t'' = Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2'))
wenzelm@20114
    69
    val reshape =
wenzelm@51717
    70
      Goal.prove ctxt [] [] (Data.mk_eq (t', t'')) (K (Data.norm_tac ctxt))
huffman@45270
    71
paulson@10694
    72
  in
wenzelm@51717
    73
    SOME (export (Data.simplify_meta_eq ctxt 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;