Menu
▾
▴
[Hol-checkins] CVS: hol98/src/num/arith/src GenPolyCanon.sig,NONE,1.1 GenPolyCanon.sml,NONE,1.1 numSimps.sig,1.6,1.7 numSimps.sml,1.31,1.32
|
From: Michael N. <mic...@us...> - 2006-02-22 02:53:46
|
Update of /cvsroot/hol/hol98/src/num/arith/src In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv18588/num/arith/src Modified Files: numSimps.sig numSimps.sml Added Files: GenPolyCanon.sig GenPolyCanon.sml Log Message: New generic code to normalise arithmetic expressions. Will handle integers and reals too, but this check-in just slots the new code into ARITH_ss. (The broken proofs in integerScript make me wonder how they ever worked. As they fiddle about with dangerous BIT1, BIT2 and NUMERAL constants, I'm not too bothered by their failure). --- NEW FILE: GenPolyCanon.sig --- signature GenPolyCanon = sig include Abbrev datatype assoc_mode = L | R | L_Cflipped datatype gci = GCI of {dest : term -> term * term, is_literal : term -> bool, assoc_mode : assoc_mode, assoc : thm, symassoc : thm , comm : thm, l_asscomm : thm , r_asscomm : thm , non_coeff : term -> term, merge : term -> thm, postnorm : term -> thm, left_id : thm, right_id : thm , reducer : term -> thm} val gencanon : gci -> term -> thm val derive_l_asscomm : thm -> thm -> thm val derive_r_asscomm : thm -> thm -> thm end; (* The gci type stores sufficient information about a type and operators over it to allow normalisation of "polynomials" over that type, collecting up coefficients etc. The required fields of the record are dest : pulls apart a term (e.g., x + y -> (x,y)) is_literal : returns true iff a term is a numeric literal - in L & R modes literals are shunted to the right end of the term. In L_Cflipped they appear on the front. assoc_mode : how the term should be associated when built. L & R are obvious. L_Cflipped has non-literals left-associated, but possibly prepended by a literal to the left. This is appropriate for multiplication, e.g., c((xy)z) assoc : associativity theorem (e.g., |- x + (y + z) = (x + y) + z) symassoc : associativity theorem with equality flipped comm : commutativity theorem (e.g., |- x + y = y + x) l_asscomm : right-commutativity theorem (letter 'l' indicates that terms are left-associated) (e.g., |- (x + y) + z = (x + z) + y) r_asscomm : left-commutativity theorem (terms are right-associated) (e.g., |- x + (y + z) = y + (x + z)) non_coeff : returns the "base" of a term, ignoring the coefficient. (e.g., x -> x, 2 * x -> x, ~y -> y, 3 -> 1) merge : takes a term of the form t1 op t2, where t1 and t2 have equal base, and merges them into one by summing coefficients. The result will be subjected to post-normalisation (see below) postnorm : conversion to normalise certain coeff-term pairs. Must include the analogue of 0 * x -> |- 0 * x = 0 and might reasonably include x ** 1 -> |- x ** 1 = x ~1 * x -> |- ~1 * x = ~x 3 * 1 -> |- 3 * 1 = 3 left_id : theorem stating left-identity for the base operator (e.g., |- 0 + x = x and |- 1 * x = x) right_id : theorem stating right-identity for the base operator reducer : conversion for doing ground arithmetic on coefficients To handle literals, get non_coeff to return a base of 1 for them, and then handle their merging separately in the merge function. [gencanon g t] returns a theorem of the form |- t = t', where t' is a normal form. The polynomial will be right-associated (for backwards compatibility reasons). [derive_l_asscomm ass comm] derives an l_asscomm theorem from assoc and comm theorems. [derive_r_asscomm ass comm] derives an r_asscomm theorem from assoc and comm theorems. *) --- NEW FILE: GenPolyCanon.sml --- structure GenPolyCanon :> GenPolyCanon = struct open HolKernel boolLib datatype assoc_mode = L | R | L_Cflipped datatype gci = GCI of {dest : term -> term * term, is_literal : term -> bool, assoc : thm (* right to left *), symassoc : thm (* left to right *), comm : thm, assoc_mode : assoc_mode, r_asscomm : thm (* swaps 1 and 2 in r-associated triple *), l_asscomm : thm (* swaps 2 and 3 in l-associated triple *), non_coeff : term -> term, merge : term -> thm, postnorm : term -> thm, left_id : thm (* id on left can be rewritten away *), right_id : thm (* id on right can be rewritten away *), reducer : term -> thm} fun gencanon (gci as GCI g) = let val {dest,non_coeff,comm,assoc,symassoc,merge,postnorm,is_literal,...} = g val REDUCE_CONV = #reducer g fun ra_swapmerge t = let val (l,r) = dest t val (r',merge_conval,post_conval,swapper) = let val (l',_) = dest r in (l', (fn c => REWR_CONV assoc THENC LAND_CONV c), LAND_CONV, REWR_CONV (#r_asscomm g)) end handle HOL_ERR _ => (r,I,I,REWR_CONV comm) val swap_action = swapper THENC RAND_CONV ra_swapmerge THENC TRY_CONV (REWR_CONV (#right_id g)) val eq_action = merge_conval merge THENC post_conval postnorm val non_action = LAND_CONV postnorm in case (is_literal l, is_literal r', Term.compare (non_coeff l, non_coeff r')) of (true, false, _) => swap_action | (true, true, _) => eq_action | (false, true, _) => non_action | (false, false, LESS) => non_action | (false, false, EQUAL) => eq_action | (false, false, GREATER) => swap_action end t handle HOL_ERR _ => postnorm t fun la_swapmerge t = let val (l,r) = dest t val (l', merge_conval, post_conval, swapper) = let val (_, r') = dest l in (r', (fn c => REWR_CONV symassoc THENC RAND_CONV c), RAND_CONV, REWR_CONV (#l_asscomm g)) end handle HOL_ERR _ => (l,I,I,REWR_CONV comm) val non_action = RAND_CONV postnorm val eq_action = merge_conval merge THENC post_conval postnorm val swap_action = swapper THENC LAND_CONV la_swapmerge THENC TRY_CONV (REWR_CONV (#left_id g)) in case (is_literal l', is_literal r, Term.compare (non_coeff l', non_coeff r)) of (true, false, _) => swap_action | (true, true, _) => eq_action | (false, true, _) => non_action | (false, false, LESS) => non_action | (false, false, EQUAL) => eq_action | (false, false, GREATER) => swap_action end t handle HOL_ERR _ => postnorm t fun ra_recurse t = let val (l,r) = dest t in if can dest l then REWR_CONV symassoc THENC ra_recurse else RAND_CONV ra_recurse THENC ra_swapmerge THENC TRY_CONV (REWR_CONV (#left_id g)) end t handle HOL_ERR _ => postnorm t fun la_recurse t = let val (l,r) = dest t in if can dest r then REWR_CONV assoc THENC la_recurse else LAND_CONV la_recurse THENC la_swapmerge THENC TRY_CONV (REWR_CONV (#right_id g)) end t handle HOL_ERR _ => postnorm t fun lcflipped t = let val (l,r) = dest t fun finish_have_left_lit t = let val r = rand t in if can dest r then if is_literal (rand r) then RAND_CONV (REWR_CONV comm) THENC REWR_CONV assoc THENC LAND_CONV REDUCE_CONV else ALL_CONV else if is_literal r then REDUCE_CONV else ALL_CONV end t fun finish_no_left_lit t = let val (l,r) = dest t in if is_literal r then REWR_CONV comm else ALL_CONV end t handle HOL_ERR _ => ALL_CONV t in if is_literal l then RAND_CONV la_recurse THENC finish_have_left_lit else la_recurse THENC finish_no_left_lit end t handle HOL_ERR _ => postnorm t in case #assoc_mode g of L => la_recurse | R => ra_recurse | L_Cflipped => lcflipped end fun derive_l_asscomm assoc0 comm0 = let val assoc = SPEC_ALL assoc0 val comm = SPEC_ALL comm0 in SYM (CONV_RULE (LAND_CONV (RAND_CONV (REWR_CONV comm) THENC REWR_CONV assoc)) assoc) end fun derive_r_asscomm assoc0 comm0 = let val assoc = SPEC_ALL assoc0 val comm = SPEC_ALL comm0 in CONV_RULE (RAND_CONV (LAND_CONV (REWR_CONV comm) THENC REWR_CONV (SYM assoc))) assoc end end (* struct *) (* val intadd_gci = let open intSyntax integerTheory intLib val assoc = SPEC_ALL INT_ADD_ASSOC val comm = SPEC_ALL INT_ADD_COMM fun is_good t = let val (l,r) = dest_mult t in is_int_literal l end handle HOL_ERR _ => false fun non_coeff t = if is_good t then rand t else if is_negated t then rand t else t fun add_coeff t = if is_good t then ALL_CONV t else if is_negated t then REWR_CONV INT_NEG_MINUS1 t else REWR_CONV (GSYM INT_MUL_LID) t in GCI { dest = dest_plus, assoc = assoc, symassoc = SYM assoc, comm = comm, asscomm = derive_asscomm assoc comm, non_coeff = non_coeff, distrib = GSYM INT_RDISTRIB, distrib_left = true, add_coeff = add_coeff, postnorm = REWR_CONV INT_MUL_LZERO ORELSEC REWR_CONV INT_MUL_LID ORELSEC TRY_CONV (REWR_CONV (GSYM INT_NEG_MINUS1)), left_id = INT_ADD_LID, right_id = INT_ADD_RID, reducer = REDUCE_CONV } end val realadd_gci = let open realTheory realSyntax val assoc = SPEC_ALL REAL_ADD_ASSOC val comm = SPEC_ALL REAL_ADD_COMM val asscomm = derive_asscomm assoc comm fun is_good t = let val (l,r) = dest_mult t in is_real_literal l orelse (is_div l andalso is_real_literal (rand l) andalso is_real_literal (rand (rator l))) end handle HOL_ERR _ => false fun add_coeff t = if is_good t then ALL_CONV t else if is_negated t then REWR_CONV REAL_NEG_MINUS1 t else REWR_CONV (GSYM REAL_MUL_LID) t fun non_coeff t = if is_good t orelse is_negated t then rand t else t in GCI { dest = dest_plus, assoc = assoc, symassoc = SYM assoc, comm = comm, asscomm = derive_asscomm assoc comm, non_coeff = non_coeff, distrib = GSYM REAL_RDISTRIB, distrib_left = true, add_coeff = add_coeff, postnorm = REWR_CONV REAL_MUL_LZERO ORELSEC REWR_CONV REAL_MUL_LID ORELSEC TRY_CONV (REWR_CONV (GSYM REAL_NEG_MINUS1)), left_id = REAL_ADD_LID, right_id = REAL_ADD_RID, reducer = computeLib.CBV_CONV (realSimps.real_compset())} end *) Index: numSimps.sig =================================================================== RCS file: /cvsroot/hol/hol98/src/num/arith/src/numSimps.sig,v retrieving revision 1.6 retrieving revision 1.7 diff -b -C2 -d -r1.6 -r1.7 *** numSimps.sig 17 Feb 2006 04:35:10 -0000 1.6 --- numSimps.sig 22 Feb 2006 02:53:40 -0000 1.7 *************** *** 17,20 **** --- 17,25 ---- val arith_cache : Cache.cache + val ADDL_CANON_CONV : conv + val ADDR_CANON_CONV : conv + val MUL_CANON_CONV : conv + + (* deprecated *) val old_ARITH_ss : simpLib.ssfrag *************** *** 52,55 **** --- 57,75 ---- [arith_cache] is the cache on which ARITH_ss relies. + [ADDR_CANON_CONV t] normalises additive term t, collecting up terms with + common bases and summing coefficients. Additions are right-associated with + constants appearing to the right. + + [ADDL_CANON_CONV t] normalises additive term t, collecting up terms with + common bases and summing coefficients. Additions are left-associated with + constants appearing to the right. + + [MUL_CANON_CONV t] normalises multiplicative term t, collecting up terms + with common bases and summing exponents. Multiplications are left- + associated, except that constants appear separately to the left (thus + making such terms appropriate coefficient-base pairs). + + + [old_ARITH_ss] is an old version of ARITH_ss that does less normalisation of arithmetic expressions. Here for some backwards Index: numSimps.sml =================================================================== RCS file: /cvsroot/hol/hol98/src/num/arith/src/numSimps.sml,v retrieving revision 1.31 retrieving revision 1.32 diff -b -C2 -d -r1.31 -r1.32 *** numSimps.sml 17 Feb 2006 04:35:10 -0000 1.31 --- numSimps.sml 22 Feb 2006 02:53:40 -0000 1.32 *************** *** 141,144 **** --- 141,252 ---- val _ = BasicProvers.augment_srw_ss [REDUCE_ss, ARITH_RWTS_ss] + (* ---------------------------------------------------------------------- + basic canonisers + ---------------------------------------------------------------------- *) + + (* first define the records containing the necessary information for the + generic canoniser *) + + (* for addition - right-associated for backwards compatibility *) + local + open numSyntax arithmeticTheory GenPolyCanon + fun is_good t = let + val (l,r) = dest_mult t + in + is_numeral l + end handle HOL_ERR _ => false + fun non_coeff t = if is_good t then rand t + else if is_numeral t then mk_var(" ", num) + else t + fun add_coeff (t:term) : thm = if is_good t then ALL_CONV t + else REWR_CONV (GSYM MULT_LEFT_1) t + val distrib = GSYM RIGHT_ADD_DISTRIB + fun merge t = let + val (l,r) = dest_plus t + in + if is_numeral l andalso is_numeral r then + reduceLib.REDUCE_CONV + else + Conv.BINOP_CONV add_coeff THENC + REWR_CONV distrib THENC LAND_CONV reduceLib.REDUCE_CONV + end t + in + val rnatadd_gci = + GCI { dest = dest_plus, + assoc_mode = R, + assoc = ADD_ASSOC, + symassoc = GSYM ADD_ASSOC, + comm = ADD_COMM, + r_asscomm = derive_r_asscomm ADD_ASSOC ADD_COMM, + l_asscomm = derive_l_asscomm ADD_ASSOC ADD_COMM, + is_literal = is_numeral, + non_coeff = non_coeff, merge = merge, + postnorm = REWR_CONV (CONJUNCT1 (SPEC_ALL MULT)) ORELSEC + TRY_CONV (REWR_CONV MULT_LEFT_1), + left_id = CONJUNCT1 ADD, + right_id = ADD_0, + reducer = reduceLib.REDUCE_CONV} + val lnatadd_gci = + GCI { dest = dest_plus, + assoc_mode = L, + assoc = ADD_ASSOC, + symassoc = GSYM ADD_ASSOC, + comm = ADD_COMM, + r_asscomm = derive_r_asscomm ADD_ASSOC ADD_COMM, + l_asscomm = derive_l_asscomm ADD_ASSOC ADD_COMM, + is_literal = is_numeral, + non_coeff = non_coeff, merge = merge, + postnorm = REWR_CONV (CONJUNCT1 (SPEC_ALL MULT)) ORELSEC + TRY_CONV (REWR_CONV MULT_LEFT_1), + left_id = CONJUNCT1 ADD, + right_id = ADD_0, + reducer = reduceLib.REDUCE_CONV} + end + + val ADDL_CANON_CONV = GenPolyCanon.gencanon lnatadd_gci + val ADDR_CANON_CONV = GenPolyCanon.gencanon rnatadd_gci + + (* multiplication *) + val lcnatmult_gci = let + open GenPolyCanon numSyntax arithmeticTheory + fun is_good t = let + val (l,r) = dest_exp t + in + is_numeral r + end handle HOL_ERR _ => false + fun non_coeff t = if is_good t then rand (rator t) + else if is_numeral t then mk_numeral Arbnum.one + else t + fun add_coeff t = if is_good t then ALL_CONV t + else REWR_CONV (GSYM (CONJUNCT2 (SPEC_ALL EXP_1))) t + val distrib = GSYM EXP_ADD + fun merge t = let + val (l,r) = dest_mult t + in + if is_numeral l andalso is_numeral r then reduceLib.REDUCE_CONV + else Conv.BINOP_CONV add_coeff THENC REWR_CONV distrib THENC + reduceLib.REDUCE_CONV + end t + in + GCI { dest = dest_mult, + is_literal = is_numeral, + assoc_mode = L_Cflipped, + assoc = MULT_ASSOC, + symassoc = GSYM MULT_ASSOC, + comm = MULT_COMM, + r_asscomm = derive_r_asscomm MULT_ASSOC MULT_COMM, + l_asscomm = derive_l_asscomm MULT_ASSOC MULT_COMM, + non_coeff = non_coeff, + merge = merge, + postnorm = REWR_CONV (CONJUNCT1 (SPEC_ALL EXP)) ORELSEC + TRY_CONV (REWR_CONV (CONJUNCT2 (SPEC_ALL EXP_1))), + right_id = MULT_RIGHT_1, + left_id = MULT_LEFT_1, + reducer = reduceLib.REDUCE_CONV} + end + + val MUL_CANON_CONV = GenPolyCanon.gencanon lcnatmult_gci + + (* ---------------------------------------------------------------------* * LIN: Linear arithmetic expressions * *************** *** 261,313 **** val linear_reduction = term_of_lin o lin_of_term; - (* ---------------------------------------------------------------------- - normalising multiplication terms - - This is at least the third time I have written this code, but the first - time for use in the simplifier, where you need to be careful that it will - raise UNCHANGED rather than just an instance of reflexivity. - - ---------------------------------------------------------------------- *) - - fun ok_noncoeff t = let - open numSyntax - fun ok t = not (is_mult t) andalso not (is_numeral t) - val (l,r) = dest_mult t - fun recurse last t = let - val (l,r) = dest_mult t - in - ok r andalso Term.compare(r,last) <> GREATER andalso recurse r l - end handle HOL_ERR _ => ok t andalso Term.compare(t,last) <> GREATER - in - ok r andalso recurse r l - end handle HOL_ERR _ => not (numSyntax.is_numeral t) - - fun bad_mult t = let - open numSyntax - val (l,r) = dest_mult t - in - if is_numeral l then not (ok_noncoeff r) - else not (ok_noncoeff t) - end handle HOL_ERR _ => false - - fun fix_bad_mult t = let - open numSyntax arithmeticTheory - val args = strip_mult t - val (nums,others) = partition is_numeral args - fun AC new old = EQT_ELIM (AC_CONV (MULT_ASSOC, MULT_COMM) (mk_eq(old,new))) - val others' = Listsort.sort Term.compare others - in - if null nums then AC (list_mk_mult others') - else if null others then REDUCE_CONV - else - AC (mk_mult(list_mk_mult nums, list_mk_mult others')) THENC - LAND_CONV REDUCE_CONV - end t - - fun NORM_MULT_CONV t = - if bad_mult t then fix_bad_mult t - else ALL_CONV t - - (* --------------------------------------------------------------------- * is_arith --- 369,372 ---- *************** *** 390,393 **** --- 449,453 ---- type ctxt = thm list; + fun contains_minus t = List.exists numSyntax.is_minus (numSyntax.strip_plus t) fun CTXT_ARITH thms tm = *************** *** 411,415 **** end else ! if (type_of tm = num_ty) then let val _ = trace(5, LZ_TEXT (fn () => "Linear reduction on "^ term_to_string tm)) --- 471,475 ---- end else ! if type_of tm = num_ty then let val _ = trace(5, LZ_TEXT (fn () => "Linear reduction on "^ term_to_string tm)) *************** *** 419,423 **** (trace (5, TEXT ("No reduction possible")); failwith "CTXT_ARITH: no reduction possible") ! else let val context = map concl thms val gl = list_mk_imp(context,mk_eq(tm,reduction)) --- 479,483 ---- (trace (5, TEXT ("No reduction possible")); failwith "CTXT_ARITH: no reduction possible") ! else if contains_minus tm then let val context = map concl thms val gl = list_mk_imp(context,mk_eq(tm,reduction)) *************** *** 428,431 **** --- 488,492 ---- trace(1,PRODUCE(tm,"ARITH",thm)); thm end + else ADDR_CANON_CONV tm end else failwith "CTXT_ARITH: not applicable"; *************** *** 529,540 **** val ARITH_DP_ss = ! SSFRAG { convs = [{conv = K (K NORM_MULT_CONV), key = SOME([], ``x * y``), ! name = "NORM_MULT_CONV", trace = 2}], rewrs = [], congs = [], filter = NONE, ac = [], dprocs = [ARITH_REDUCER]}; ! val old_dp_ss = SSFRAG { convs = [], rewrs = [], congs = [], ! filter = NONE, ac = [], dprocs = [ARITH_REDUCER]}; (*---------------------------------------------------------------------------*) --- 590,602 ---- val ARITH_DP_ss = ! SSFRAG { convs = [{conv = K (K MUL_CANON_CONV), key = SOME([], ``x * y``), ! name = "MUL_CANON_CONV", trace = 2}], rewrs = [], congs = [], filter = NONE, ac = [], dprocs = [ARITH_REDUCER]}; ! val old_dp_ss = ! SSFRAG { convs = [], rewrs = [], congs = [], filter = NONE, ac = [], ! dprocs = [ARITH_REDUCER]}; (*---------------------------------------------------------------------------*) |