src/Provers/Arith/combine_numerals.ML
author blanchet
Tue, 07 Dec 2010 11:56:01 +0100
changeset 41051 2ed1b971fc20
parent 35762 af3ff2ba4c54
child 44947 8ae418dfe561
permissions -rw-r--r--
give the inner timeout mechanism a chance, since it gives more precise information to the user
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     1
(*  Title:      Provers/Arith/combine_numerals.ML
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     3
    Copyright   2000  University of Cambridge
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     4
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     5
Combine coefficients in expressions:
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     6
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     7
     i + #m*u + j ... + #n*u + k  ==  #(m+n)*u + (i + (j + k))
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     8
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     9
It works by (a) massaging the sum to bring the selected terms to the front:
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    10
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    11
     #m*u + (#n*u + (i + (j + k)))
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    12
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    13
(b) then using left_distrib to reach
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    14
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    15
     #(m+n)*u + (i + (j + k))
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    16
*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    17
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    18
signature COMBINE_NUMERALS_DATA =
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    19
sig
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    20
  (*abstract syntax*)
23058
c722004c5a22 generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents: 20114
diff changeset
    21
  eqtype coeff
c722004c5a22 generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents: 20114
diff changeset
    22
  val iszero: coeff -> bool
c722004c5a22 generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents: 20114
diff changeset
    23
  val add: coeff * coeff -> coeff     (*addition (or multiplication) *)
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 13484
diff changeset
    24
  val mk_sum: typ -> term list -> term
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    25
  val dest_sum: term -> term list
23058
c722004c5a22 generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents: 20114
diff changeset
    26
  val mk_coeff: coeff * term -> term
c722004c5a22 generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents: 20114
diff changeset
    27
  val dest_coeff: term -> coeff * term
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    28
  (*rules*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    29
  val left_distrib: thm
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    30
  (*proof tools*)
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    31
  val prove_conv: tactic list -> Proof.context -> term * term -> thm option
16973
b2a894562b8f simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15965
diff changeset
    32
  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
b2a894562b8f simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15965
diff changeset
    33
  val norm_tac: simpset -> tactic                (*proves the initial lemma*)
b2a894562b8f simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15965
diff changeset
    34
  val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
b2a894562b8f simprocs: Simplifier.inherit_bounds;
wenzelm
parents: 15965
diff changeset
    35
  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    36
end;
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    37
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    38
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    39
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    40
  sig
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17412
diff changeset
    41
  val proc: simpset -> term -> thm option
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    42
  end
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    43
=
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    44
struct
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    45
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    46
(*Remove the first occurrence of #m*u from the term list*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    47
fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    48
      raise TERM("combine_numerals: remove", [])
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    49
  | remove (m, u, t::terms) =
9646
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    50
      case try Data.dest_coeff t of
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    51
          SOME(n,v) => if m=n andalso u aconv v then terms
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    52
                       else t :: remove (m, u, terms)
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    53
        | NONE      =>  t :: remove (m, u, terms);
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    54
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    55
(*a left-to-right scan of terms, seeking another term of the form #n*u, where
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    56
  #m*u is already in terms for some m*)
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    57
fun find_repeated (tab, _, []) = raise TERM("find_repeated", [])
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    58
  | find_repeated (tab, past, t::terms) =
9646
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    59
      case try Data.dest_coeff t of
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    60
          SOME(n,u) =>
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    61
              (case Termtab.lookup tab u of
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    62
                  SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    63
                | NONE => find_repeated (Termtab.update (u, n) tab,
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    64
                                         t::past,  terms))
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    65
        | NONE => find_repeated (tab, t::past, terms);
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    66
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    67
(*the simplification procedure*)
20044
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17412
diff changeset
    68
fun proc ss t =
92cc2f4c7335 simprocs: no theory argument -- use simpset context instead;
wenzelm
parents: 17412
diff changeset
    69
  let
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    70
    val ctxt = Simplifier.the_context ss;
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    71
    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    72
    val export = singleton (Variable.export ctxt' ctxt)
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    73
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    74
    val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    75
    val T = Term.fastype_of u
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    76
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    77
    val reshape =  (*Move i*u to the front and put j*u into standard form
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    78
                       i + #m + j + k == #m + i + (j + k) *)
23058
c722004c5a22 generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
huffman
parents: 20114
diff changeset
    79
      if Data.iszero m orelse Data.iszero n then   (*trivial, so do nothing*)
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    80
        raise TERM("combine_numerals", [])
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    81
      else Data.prove_conv [Data.norm_tac ss] ctxt
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    82
        (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    83
  in
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    84
    Option.map (export o Data.simplify_meta_eq ss)
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    85
      (Data.prove_conv
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    86
         [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    87
          Data.numeral_simp_tac ss] ctxt
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    88
         (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    89
  end
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    90
  (* FIXME avoid handling of generic exceptions *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    91
  handle TERM _ => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15027
diff changeset
    92
       | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
20114
a1bb4bc68ff3 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents: 20044
diff changeset
    93
                             Undeclared type constructor "Numeral.bin"*)
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    94
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    95
end;