--- a/src/Provers/Arith/combine_coeff.ML Tue May 02 18:56:39 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,193 +0,0 @@
-(* Title: Provers/Arith/combine_coeff.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Simplification procedure to combine literal coefficients in sums of products
-
-Example, #3*x + y - (x*#2) goes to x + y
-
-For the relations <, <= and =, the difference is simplified
-
-[COULD BE GENERALIZED to products of exponentials?]
-*)
-
-signature COMBINE_COEFF_DATA =
-sig
- val ss : simpset (*basic simpset of object-logtic*)
- val eq_reflection : thm (*object-equality to meta-equality*)
- val thy : theory (*the theory of the group*)
- val T : typ (*the type of group elements*)
-
- val trans : thm (*transitivity of equals*)
- val add_ac : thm list (*AC-rules for the addition operator*)
- val diff_def : thm (*Defines x-y as x + -y *)
- val minus_add_distrib : thm (* -(x+y) = -x + -y *)
- val minus_minus : thm (* - -x = x *)
- val mult_commute : thm (*commutative law for the product*)
- val mult_1_right : thm (*the law x*1=x *)
- val add_mult_distrib : thm (*law w*(x+y) = w*x + w*y *)
- val diff_mult_distrib : thm (*law w*(x-y) = w*x - w*y *)
- val mult_minus_right : thm (*law x * -y = -(x*y) *)
-
- val rel_iff_rel_0_rls : thm list (*e.g. (x < y) = (x-y < 0) *)
- val dest_eqI : thm -> term (*to get patterns from the rel rules*)
-end;
-
-
-functor Combine_Coeff (Data: COMBINE_COEFF_DATA) =
-struct
-
- local open Data
- in
- val rhs_ss = ss addsimps
- [add_mult_distrib, diff_mult_distrib,
- mult_minus_right, mult_1_right];
-
- val lhs_ss = ss addsimps
- add_ac @
- [diff_def, minus_add_distrib, minus_minus, mult_commute];
- end;
-
- (*prove while suppressing timing information*)
- fun prove name ct tacf =
- setmp Goals.proof_timing false (prove_goalw_cterm [] ct) tacf
- handle ERROR =>
- error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
-
- val plus = Const ("op +", [Data.T,Data.T] ---> Data.T);
- val minus = Const ("op -", [Data.T,Data.T] ---> Data.T);
- val uminus = Const ("uminus", Data.T --> Data.T);
- val times = Const ("op *", [Data.T,Data.T] ---> Data.T);
-
- val number_of = Const ("Numeral.number_of",
- Type ("Numeral.bin", []) --> Data.T);
-
- val zero = number_of $ HOLogic.pls_const;
- val one = number_of $ (HOLogic.bit_const $
- HOLogic.pls_const $
- HOLogic.true_const);
-
- (*We map -t to t and (in other cases) t to -t. No need to check the type of
- uminus, since the simproc is only called on sums of type T.*)
- fun negate (Const("uminus",_) $ t) = t
- | negate t = uminus $ t;
-
- fun mk_sum [] = zero
- | mk_sum tms = foldr1 (fn (x,y) => plus $ x $ y) tms;
-
- fun attach_coeff (Bound ~1,ns) = mk_sum ns (*just a literal*)
- | attach_coeff (x,ns) = times $ x $ (mk_sum ns);
-
- fun add_atom (x, (neg,m)) pairs =
- let val m' = if neg then negate m else m
- in
- case gen_assoc (op aconv) (pairs, x) of
- Some n => gen_overwrite (op aconv) (pairs, (x, m'::n))
- | None => (x,[m']) :: pairs
- end;
-
- (**STILL MISSING: a treatment of nested coeffs, e.g. a*(b*3) **)
- (*Convert a formula built from +, * and - (binary and unary) to a
- (atom, coeff) association list. Handles t+t, t-t, -t, a*n, n*a, n, a
- where n denotes a numeric literal and a is any other term.
- No need to check types PROVIDED they are checked upon entry!*)
- fun add_terms neg (Const("op +", _) $ x $ y, pairs) =
- add_terms neg (x, add_terms neg (y, pairs))
- | add_terms neg (Const("op -", _) $ x $ y, pairs) =
- add_terms neg (x, add_terms (not neg) (y, pairs))
- | add_terms neg (Const("uminus", _) $ x, pairs) =
- add_terms (not neg) (x, pairs)
- | add_terms neg (lit as Const("Numeral.number_of", _) $ _, pairs) =
- (*literal: make it the coefficient of a dummy term*)
- add_atom (Bound ~1, (neg, lit)) pairs
- | add_terms neg (Const("op *", _) $ x
- $ (lit as Const("Numeral.number_of", _) $ _),
- pairs) =
- (*coefficient on the right*)
- add_atom (x, (neg, lit)) pairs
- | add_terms neg (Const("op *", _)
- $ (lit as Const("Numeral.number_of", _) $ _)
- $ x, pairs) =
- (*coefficient on the left*)
- add_atom (x, (neg, lit)) pairs
- | add_terms neg (x, pairs) = add_atom (x, (neg, one)) pairs;
-
- fun terms fml = add_terms false (fml, []);
-
- exception CC_fail;
-
- (*The number of terms in t, assuming no collapsing takes place*)
- fun term_count (Const("op +", _) $ x $ y) = term_count x + term_count y
- | term_count (Const("op -", _) $ x $ y) = term_count x + term_count y
- | term_count (Const("uminus", _) $ x) = term_count x
- | term_count x = 1;
-
-
- val trace = ref false;
-
- (*The simproc for sums*)
- fun sum_proc sg _ lhs =
- let fun show t = string_of_cterm (Thm.cterm_of sg t)
- val _ = if !trace then writeln
- ("combine_coeff sum simproc: LHS = " ^ show lhs)
- else ()
- val ts = terms lhs
- val _ = if term_count lhs = length ts
- then raise CC_fail (*we can't reduce the number of terms*)
- else ()
- val rhs = mk_sum (map attach_coeff ts)
- val _ = if !trace then writeln ("RHS = " ^ show rhs) else ()
- val th = prove "combine_coeff"
- (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
- (fn _ => [rtac Data.eq_reflection 1,
- simp_tac rhs_ss 1,
- IF_UNSOLVED (simp_tac lhs_ss 1)])
- in Some th end
- handle CC_fail => None;
-
- val sum_conv =
- Simplifier.mk_simproc "combine_coeff_sums"
- (map (Thm.read_cterm (Theory.sign_of Data.thy))
- [("x + y", Data.T), ("x - y", Data.T)])
- sum_proc;
-
-
- (*The simproc for relations, which just replaces x<y by x-y<0 and simplifies*)
-
- val trans_eq_reflection = Data.trans RS Data.eq_reflection |> standard;
-
- fun rel_proc sg asms (lhs as (rel$lt$rt)) =
- let val _ = if !trace then writeln
- ("cc_rel simproc: LHS = " ^
- string_of_cterm (cterm_of sg lhs))
- else ()
- val _ = if lt=zero orelse rt=zero then raise CC_fail
- else () (*this simproc can do nothing if either side is zero*)
- val cc_th = the (sum_proc sg asms (minus $ lt $ rt))
- handle OPTION => raise CC_fail
- val _ = if !trace then
- writeln ("cc_th = " ^ string_of_thm cc_th)
- else ()
- val cc_lr = #2 (Logic.dest_equals (concl_of cc_th))
-
- val rhs = rel $ cc_lr $ zero
- val _ = if !trace then
- writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
- else ()
- val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
-
- val th = prove "cc_rel" ct
- (fn _ => [rtac trans_eq_reflection 1,
- resolve_tac Data.rel_iff_rel_0_rls 1,
- simp_tac (Data.ss addsimps [cc_th]) 1])
- in Some th end
- handle CC_fail => None;
-
- val rel_conv =
- Simplifier.mk_simproc "cc_relations"
- (map (Thm.cterm_of (Theory.sign_of Data.thy) o Data.dest_eqI)
- Data.rel_iff_rel_0_rls)
- rel_proc;
-
-end;
--- a/src/Provers/Arith/fold_Suc.ML Tue May 02 18:56:39 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(* Title: Provers/Arith/fold_Suc.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2000 University of Cambridge
-
-Simplifies Suc (i + ... #m + ... j) == #(m+1) + i + ... j
-*)
-
-
-signature FOLD_SUC_DATA =
-sig
- (*abstract syntax*)
- val mk_numeral: int -> term
- val find_first_numeral: term list -> int * term * term list
- val mk_sum: term list -> term
- val dest_sum: term -> term list
- val dest_Suc: term -> term
- (*proof tools*)
- val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
- val add_norm_tac: tactic
- val numeral_simp_tac: tactic
-end;
-
-
-functor FoldSucFun(Data: FOLD_SUC_DATA):
- sig
- val proc: Sign.sg -> thm list -> term -> thm option
- end
-=
-struct
-
-fun listof None = []
- | listof (Some x) = [x];
-
-fun proc sg _ t =
- let val sum = Data.dest_Suc t
- val terms = Data.dest_sum sum
- val (m, lit_m, terms') = Data.find_first_numeral terms
- val assocs = (*If needed, rewrite the literal m to the front:
- i + #m + j + k == #m + i + (j + k) *)
- listof (Data.prove_conv [Data.add_norm_tac] sg
- (sum, Data.mk_sum (lit_m::terms')))
- in
- Data.prove_conv
- [rewrite_goals_tac assocs, Data.numeral_simp_tac] sg
- (t, Data.mk_sum (Data.mk_numeral (m+1) :: terms'))
- end
- handle TERM _ => None;
-
-end;