1(* Title: Provers/Arith/combine_numerals.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 2000 University of Cambridge 4 5Combine coefficients in expressions: 6 7 i + #m*u + j ... + #n*u + k == #(m+n)*u + (i + (j + k)) 8 9It works by (a) massaging the sum to bring the selected terms to the front: 10 11 #m*u + (#n*u + (i + (j + k))) 12 13(b) then using left_distrib to reach 14 15 #(m+n)*u + (i + (j + k)) 16*) 17 18signature COMBINE_NUMERALS_DATA = 19sig 20 (*abstract syntax*) 21 eqtype coeff 22 val iszero: coeff -> bool 23 val add: coeff * coeff -> coeff (*addition (or multiplication) *) 24 val mk_sum: typ -> term list -> term 25 val dest_sum: term -> term list 26 val mk_coeff: coeff * term -> term 27 val dest_coeff: term -> coeff * term 28 (*rules*) 29 val left_distrib: thm 30 (*proof tools*) 31 val prove_conv: tactic list -> Proof.context -> term * term -> thm option 32 val trans_tac: Proof.context -> thm option -> tactic (*applies the initial lemma*) 33 val norm_tac: Proof.context -> tactic (*proves the initial lemma*) 34 val numeral_simp_tac: Proof.context -> tactic (*proves the final theorem*) 35 val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*) 36end; 37 38 39functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): 40 sig 41 val proc: Proof.context -> cterm -> thm option 42 end 43= 44struct 45 46(*Remove the first occurrence of #m*u from the term list*) 47fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*) 48 raise TERM("combine_numerals: remove", []) 49 | remove (m, u, t::terms) = 50 case try Data.dest_coeff t of 51 SOME(n,v) => if m=n andalso u aconv v then terms 52 else t :: remove (m, u, terms) 53 | NONE => t :: remove (m, u, terms); 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*) 57fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) 58 | find_repeated (tab, past, t::terms) = 59 case try Data.dest_coeff t of 60 SOME(n,u) => 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 | NONE => find_repeated (tab, t::past, terms); 66 67(*the simplification procedure*) 68fun proc ctxt ct = 69 let 70 val t = Thm.term_of ct 71 val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt 72 73 val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') 74 val T = Term.fastype_of u 75 76 val reshape = (*Move i*u to the front and put j*u into standard form 77 i + #m + j + k == #m + i + (j + k) *) 78 if Data.iszero m orelse Data.iszero n then (*trivial, so do nothing*) 79 raise TERM("combine_numerals", []) 80 else Data.prove_conv [Data.norm_tac ctxt'] ctxt' 81 (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms)) 82 in 83 Data.prove_conv 84 [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.left_distrib] 1, 85 Data.numeral_simp_tac ctxt'] ctxt' 86 (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)) 87 |> Option.map 88 (Data.simplify_meta_eq ctxt' #> 89 singleton (Variable.export ctxt' ctxt)) 90 end 91 (* FIXME avoid handling of generic exceptions *) 92 handle TERM _ => NONE 93 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) 94 Undeclared type constructor "Numeral.bin"*) 95 96end; 97