src/Provers/Arith/combine_numerals.ML
author paulson
Sun, 15 Feb 2004 10:46:37 +0100
changeset 14387 e96d5c42c4b0
parent 13484 d8f5d3391766
child 15027 d23887300b96
permissions -rw-r--r--
Polymorphic treatment of binary arithmetic using axclasses
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
    ID:         $Id$
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     4
    Copyright   2000  University of Cambridge
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     5
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     6
Combine coefficients in expressions:
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     7
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
     8
     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
     9
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    10
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
    11
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    12
     #m*u + (#n*u + (i + (j + k)))
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    13
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    14
(b) then using left_distrib to reach
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    15
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    16
     #(m+n)*u + (i + (j + k))
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
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    19
signature COMBINE_NUMERALS_DATA =
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    20
sig
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    21
  (*abstract syntax*)
9571
c869d1886a32 new structure field "add" for CombineNumerals
paulson
parents: 9191
diff changeset
    22
  val add: int * int -> int          (*addition (or multiplication) *)
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 13484
diff changeset
    23
  val mk_sum: typ -> term list -> term
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    24
  val dest_sum: term -> term list
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    25
  val mk_coeff: int * term -> term
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    26
  val dest_coeff: term -> int * term
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    27
  (*rules*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    28
  val left_distrib: thm
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    29
  (*proof tools*)
13484
d8f5d3391766 adhoc_freeze_vars;
wenzelm
parents: 9646
diff changeset
    30
  val prove_conv: tactic list -> Sign.sg -> string list -> term * term -> thm option
8799
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    31
  val trans_tac: thm option -> tactic (*applies the initial lemma*)
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    32
  val norm_tac: tactic                (*proves the initial lemma*)
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    33
  val numeral_simp_tac: tactic        (*proves the final theorem*)
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    34
  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    35
end;
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    36
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
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    39
  sig
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    40
  val proc: Sign.sg -> thm list -> term -> thm option
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    41
  end 
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    42
=
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    43
struct
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    44
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    45
(*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
    46
fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    47
      raise TERM("combine_numerals: remove", [])  
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    48
  | remove (m, u, t::terms) =
9646
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    49
      case try Data.dest_coeff t of
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    50
	  Some(n,v) => if m=n andalso u aconv v then terms
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    51
		       else t :: remove (m, u, terms)
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    52
	| None      =>  t :: remove (m, u, terms);
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    53
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    54
(*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
    55
  #m*u is already in terms for some m*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    56
fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) 
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    57
  | find_repeated (tab, past, t::terms) =
9646
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    58
      case try Data.dest_coeff t of
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    59
	  Some(n,u) => 
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    60
	      (case Termtab.lookup (tab, u) of
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    61
		  Some m => (u, m, n, rev (remove (m,u,past)) @ terms)
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    62
		| None => find_repeated (Termtab.update ((u,n), tab), 
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    63
					 t::past,  terms))
aa3b82085e07 now allows dest_coeff to fail
paulson
parents: 9571
diff changeset
    64
	| None => find_repeated (tab, t::past, terms);
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    65
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    66
(*the simplification procedure*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    67
fun proc sg _ t =
9191
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    68
  let (*first freeze any Vars in the term to prevent flex-flex problems*)
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 13484
diff changeset
    69
      val (t', xs) = Term.adhoc_freeze_vars t
9191
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    70
      val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 13484
diff changeset
    71
      val T = Term.fastype_of u
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    72
      val reshape =  (*Move i*u to the front and put j*u into standard form
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    73
		       i + #m + j + k == #m + i + (j + k) *)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    74
	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    75
		raise TERM("combine_numerals", []) 
13484
d8f5d3391766 adhoc_freeze_vars;
wenzelm
parents: 9646
diff changeset
    76
	    else Data.prove_conv [Data.norm_tac] sg xs
9191
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    77
			(t', 
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 13484
diff changeset
    78
			 Data.mk_sum T ([Data.mk_coeff(m,u),
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 13484
diff changeset
    79
				         Data.mk_coeff(n,u)] @ terms))
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    80
  in
8799
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    81
      apsome Data.simplify_meta_eq
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    82
	 (Data.prove_conv 
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    83
	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
13484
d8f5d3391766 adhoc_freeze_vars;
wenzelm
parents: 9646
diff changeset
    84
	     Data.numeral_simp_tac] sg xs
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 13484
diff changeset
    85
	    (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
    86
  end
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    87
  handle TERM _ => None
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    88
       | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    89
			     Undeclared type constructor "Numeral.bin"*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    90
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    91
end;