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