src/Provers/Arith/combine_numerals.ML
author paulson
Fri Jun 16 13:13:55 2000 +0200 (2000-06-16)
changeset 9073 40d8dfac96b8
parent 8816 31b4fb3d8d60
child 9191 300bd596d696
permissions -rw-r--r--
tracing flag for arith_tac
paulson@8774
     1
(*  Title:      Provers/Arith/combine_numerals.ML
paulson@8774
     2
    ID:         $Id$
paulson@8774
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@8774
     4
    Copyright   2000  University of Cambridge
paulson@8774
     5
paulson@8774
     6
Combine coefficients in expressions:
paulson@8774
     7
paulson@8774
     8
     i + #m*u + j ... + #n*u + k  ==  #(m+n)*u + (i + (j + k))
paulson@8774
     9
paulson@8774
    10
It works by (a) massaging the sum to bring the selected terms to the front:
paulson@8774
    11
paulson@8774
    12
     #m*u + (#n*u + (i + (j + k)))
paulson@8774
    13
paulson@8774
    14
(b) then using left_distrib to reach
paulson@8774
    15
paulson@8774
    16
     #(m+n)*u + (i + (j + k))
paulson@8774
    17
*)
paulson@8774
    18
paulson@8774
    19
signature COMBINE_NUMERALS_DATA =
paulson@8774
    20
sig
paulson@8774
    21
  (*abstract syntax*)
paulson@8774
    22
  val mk_sum: term list -> term
paulson@8774
    23
  val dest_sum: term -> term list
paulson@8774
    24
  val mk_coeff: int * term -> term
paulson@8774
    25
  val dest_coeff: term -> int * term
paulson@8774
    26
  (*rules*)
paulson@8774
    27
  val left_distrib: thm
paulson@8774
    28
  (*proof tools*)
paulson@8774
    29
  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
paulson@8799
    30
  val trans_tac: thm option -> tactic (*applies the initial lemma*)
paulson@8799
    31
  val norm_tac: tactic                (*proves the initial lemma*)
paulson@8799
    32
  val numeral_simp_tac: tactic        (*proves the final theorem*)
paulson@8799
    33
  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
paulson@8774
    34
end;
paulson@8774
    35
paulson@8774
    36
paulson@8774
    37
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
paulson@8774
    38
  sig
paulson@8774
    39
  val proc: Sign.sg -> thm list -> term -> thm option
paulson@8774
    40
  end 
paulson@8774
    41
=
paulson@8774
    42
struct
paulson@8774
    43
paulson@8774
    44
(*Remove the first occurrence of #m*u from the term list*)
paulson@8774
    45
fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
paulson@8774
    46
      raise TERM("combine_numerals: remove", [])  
paulson@8774
    47
  | remove (m, u, t::terms) =
paulson@8774
    48
      let val (n,v) = Data.dest_coeff t 
paulson@8774
    49
      in  if m=n andalso u aconv v then terms
paulson@8774
    50
          else t :: remove (m, u, terms)
paulson@8774
    51
      end;
paulson@8774
    52
paulson@8774
    53
(*a left-to-right scan of terms, seeking another term of the form #n*u, where
paulson@8774
    54
  #m*u is already in terms for some m*)
paulson@8774
    55
fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) 
paulson@8774
    56
  | find_repeated (tab, past, t::terms) =
paulson@8774
    57
      let val (n,u) = Data.dest_coeff t 
paulson@8774
    58
      in  
paulson@8774
    59
	  case Termtab.lookup (tab, u) of
paulson@8774
    60
	      Some m => (u, m, n, rev (remove (m,u,past)) @ terms)
paulson@8774
    61
	    | None => find_repeated (Termtab.update ((u,n), tab), 
paulson@8774
    62
				     t::past,  terms)
paulson@8774
    63
      end;
paulson@8774
    64
paulson@8774
    65
(*the simplification procedure*)
paulson@8774
    66
fun proc sg _ t =
paulson@8774
    67
  let val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t)
paulson@8774
    68
      val reshape =  (*Move i*u to the front and put j*u into standard form
paulson@8774
    69
		       i + #m + j + k == #m + i + (j + k) *)
paulson@8774
    70
	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
paulson@8774
    71
		raise TERM("combine_numerals", []) 
paulson@8774
    72
	    else Data.prove_conv [Data.norm_tac] sg 
paulson@8774
    73
			(t, 
paulson@8774
    74
			 Data.mk_sum ([Data.mk_coeff(m,u),
paulson@8774
    75
				       Data.mk_coeff(n,u)] @ terms))
paulson@8774
    76
  in
paulson@8799
    77
      apsome Data.simplify_meta_eq
paulson@8799
    78
	 (Data.prove_conv 
paulson@8799
    79
	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
paulson@8799
    80
	     Data.numeral_simp_tac] sg
paulson@8799
    81
	    (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
paulson@8774
    82
  end
paulson@8774
    83
  handle TERM _ => None
paulson@8774
    84
       | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
paulson@8774
    85
			     Undeclared type constructor "Numeral.bin"*)
paulson@8774
    86
paulson@8774
    87
end;