src/Provers/Arith/combine_numerals.ML
author paulson
Thu, 29 Jun 2000 16:50:52 +0200
changeset 9191 300bd596d696
parent 8816 31b4fb3d8d60
child 9571 c869d1886a32
permissions -rw-r--r--
now freezes Vars in order to prevent errors in cases like these: Goal "Suc (x + i + j) + ?q ?ii ?jj + k + x = xxx"; Goal "Suc (x + i + j) = x + f(?q i j) + k"; Goal "Suc (x + i + j) = x + ?q i j + k"; Goal "Suc (?q ?ii ?jj + i + j) + ?rq ?ii ?jj + k + ?q ?ii ?jj = xxx";
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*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    22
  val mk_sum: term list -> term
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    23
  val dest_sum: term -> term list
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    24
  val mk_coeff: int * term -> term
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    25
  val dest_coeff: term -> int * term
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    26
  (*rules*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    27
  val left_distrib: thm
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    28
  (*proof tools*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    29
  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
8799
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    30
  val trans_tac: thm option -> tactic (*applies the initial lemma*)
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    31
  val norm_tac: tactic                (*proves the initial lemma*)
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    32
  val numeral_simp_tac: tactic        (*proves the final theorem*)
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    33
  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
    34
end;
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    35
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
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    38
  sig
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    39
  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
    40
  end 
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    41
=
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    42
struct
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
(*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
    45
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
    46
      raise TERM("combine_numerals: remove", [])  
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    47
  | remove (m, u, t::terms) =
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    48
      let val (n,v) = Data.dest_coeff t 
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    49
      in  if m=n andalso u aconv v then terms
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    50
          else t :: remove (m, u, terms)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    51
      end;
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    52
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    53
(*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
    54
  #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
    55
fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) 
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    56
  | find_repeated (tab, past, t::terms) =
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    57
      let val (n,u) = Data.dest_coeff t 
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    58
      in  
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    59
	  case Termtab.lookup (tab, u) of
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    60
	      Some m => (u, m, n, rev (remove (m,u,past)) @ terms)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    61
	    | None => find_repeated (Termtab.update ((u,n), tab), 
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    62
				     t::past,  terms)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    63
      end;
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    64
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    65
(*the simplification procedure*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    66
fun proc sg _ t =
9191
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    67
  let (*first freeze any Vars in the term to prevent flex-flex problems*)
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    68
      val rand_s = gensym"_"
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    69
      fun mk_inst (var as Var((a,i),T))  = 
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    70
	    (var,  Free((a ^ rand_s ^ string_of_int i), T))
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    71
      val t' = subst_atomic (map mk_inst (term_vars t)) t
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    72
      val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    73
      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
    74
		       i + #m + j + k == #m + i + (j + k) *)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    75
	    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
    76
		raise TERM("combine_numerals", []) 
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    77
	    else Data.prove_conv [Data.norm_tac] sg 
9191
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    78
			(t', 
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    79
			 Data.mk_sum ([Data.mk_coeff(m,u),
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    80
				       Data.mk_coeff(n,u)] @ terms))
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    81
  in
8799
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    82
      apsome Data.simplify_meta_eq
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    83
	 (Data.prove_conv 
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    84
	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
89e9deef4bcb simprocs now simplify the RHS of their result
paulson
parents: 8774
diff changeset
    85
	     Data.numeral_simp_tac] sg
9191
300bd596d696 now freezes Vars in order to prevent errors in cases like these:
paulson
parents: 8816
diff changeset
    86
	    (t', Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
8774
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    87
  end
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    88
  handle TERM _ => None
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    89
       | 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
    90
			     Undeclared type constructor "Numeral.bin"*)
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    91
ad5026ff0c16 new simproc, replacing combine_coeffs and working for nat, int, real
paulson
parents:
diff changeset
    92
end;