--- a/src/Provers/Arith/cancel_numeral_factor.ML Wed Jul 12 21:19:14 2006 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Wed Jul 12 21:19:17 2006 +0200
@@ -29,8 +29,7 @@
val neg_exchanges: bool (*true if a negative coeff swaps the two operands,
as with < and <= but not = and div*)
(*proof tools*)
- val prove_conv: tactic list -> Proof.context ->
- thm list -> string list -> term * term -> thm option
+ val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: simpset -> tactic (*proves the initial lemma*)
val numeral_simp_tac: simpset -> tactic (*proves the final theorem*)
@@ -41,43 +40,45 @@
functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
sig
val proc: simpset -> term -> thm option
- end
+ end
=
struct
(*the simplification procedure*)
fun proc ss t =
let
- val ctxt = Simplifier.the_context ss;
- val hyps = prems_of_ss ss;
- (*first freeze any Vars in the term to prevent flex-flex problems*)
- val (t', xs) = Term.adhoc_freeze_vars t;
- val (t1,t2) = Data.dest_bal t'
- val (m1, t1') = Data.dest_coeff t1
- and (m2, t2') = Data.dest_coeff t2
- val d = (*if both are negative, also divide through by ~1*)
- if (m1<0 andalso m2<=0) orelse
- (m1<=0 andalso m2<0) then ~ (abs(gcd(m1,m2))) else abs (gcd(m1,m2))
- val _ = if d=1 then (*trivial, so do nothing*)
- raise TERM("cancel_numeral_factor", [])
- else ()
- fun newshape (i,t) = Data.mk_coeff(d, Data.mk_coeff(i,t))
- val n1 = m1 div d and n2 = m2 div d
- val rhs = if d<0 andalso Data.neg_exchanges
- then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1'))
- else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2'))
- val reshape = (*Move d to the front and put the rest into standard form
- i * #m * j == #d * (#n * (j * k)) *)
- Data.prove_conv [Data.norm_tac ss] ctxt hyps xs
- (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
+ val ctxt = Simplifier.the_context ss;
+ val prems = prems_of_ss ss;
+ val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+ val export = singleton (Variable.export ctxt' ctxt)
+
+ val (t1,t2) = Data.dest_bal t'
+ val (m1, t1') = Data.dest_coeff t1
+ and (m2, t2') = Data.dest_coeff t2
+ val d = (*if both are negative, also divide through by ~1*)
+ if (m1<0 andalso m2<=0) orelse
+ (m1<=0 andalso m2<0) then ~ (abs(gcd(m1,m2))) else abs (gcd(m1,m2))
+ val _ = if d=1 then (*trivial, so do nothing*)
+ raise TERM("cancel_numeral_factor", [])
+ else ()
+ fun newshape (i,t) = Data.mk_coeff(d, Data.mk_coeff(i,t))
+ val n1 = m1 div d and n2 = m2 div d
+ val rhs = if d<0 andalso Data.neg_exchanges
+ then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1'))
+ else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2'))
+ val reshape = (*Move d to the front and put the rest into standard form
+ i * #m * j == #d * (#n * (j * k)) *)
+ Data.prove_conv [Data.norm_tac ss] ctxt prems
+ (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
in
- Option.map (Data.simplify_meta_eq ss)
- (Data.prove_conv
- [Data.trans_tac ss reshape, rtac Data.cancel 1,
- Data.numeral_simp_tac ss] ctxt hyps xs (t', rhs))
+ Option.map (export o Data.simplify_meta_eq ss)
+ (Data.prove_conv
+ [Data.trans_tac ss reshape, rtac Data.cancel 1,
+ Data.numeral_simp_tac ss] ctxt prems (t', rhs))
end
+ (* FIXME avoid handling of generic exceptions *)
handle TERM _ => NONE
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral)
- Undeclared type constructor "Numeral.bin"*)
+ Undeclared type constructor "Numeral.bin"*)
end;
--- a/src/Provers/Arith/cancel_numerals.ML Wed Jul 12 21:19:14 2006 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Wed Jul 12 21:19:17 2006 +0200
@@ -36,8 +36,7 @@
val bal_add1: thm
val bal_add2: thm
(*proof tools*)
- val prove_conv: tactic list -> Proof.context ->
- thm list -> string list -> term * term -> thm option
+ val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: simpset -> tactic (*proves the initial lemma*)
val numeral_simp_tac: simpset -> tactic (*proves the final theorem*)
@@ -69,41 +68,41 @@
(*the simplification procedure*)
fun proc ss t =
let
- val ctxt = Simplifier.the_context ss;
- val hyps = prems_of_ss ss;
- (*first freeze any Vars in the term to prevent flex-flex problems*)
- val (t', xs) = Term.adhoc_freeze_vars t;
- val (t1,t2) = Data.dest_bal t'
- val terms1 = Data.dest_sum t1
- and terms2 = Data.dest_sum t2
- val u = find_common (terms1,terms2)
- val (n1, terms1') = Data.find_first_coeff u terms1
- and (n2, terms2') = Data.find_first_coeff u terms2
- and T = Term.fastype_of u
- fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms)
- val reshape = (*Move i*u to the front and put j*u into standard form
+ val ctxt = Simplifier.the_context ss
+ val prems = prems_of_ss ss
+ val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+ val export = singleton (Variable.export ctxt' ctxt)
+
+ val (t1,t2) = Data.dest_bal t'
+ val terms1 = Data.dest_sum t1
+ and terms2 = Data.dest_sum t2
+
+ val u = find_common (terms1, terms2)
+ val (n1, terms1') = Data.find_first_coeff u terms1
+ and (n2, terms2') = Data.find_first_coeff u terms2
+ and T = Term.fastype_of u
+
+ fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms)
+ val reshape = (*Move i*u to the front and put j*u into standard form
i + #m + j + k == #m + i + (j + k) *)
- if n1=0 orelse n2=0 then (*trivial, so do nothing*)
- raise TERM("cancel_numerals", [])
- else Data.prove_conv [Data.norm_tac ss] ctxt hyps xs
- (t',
- Data.mk_bal (newshape(n1,terms1'),
- newshape(n2,terms2')))
+ if n1=0 orelse n2=0 then (*trivial, so do nothing*)
+ raise TERM("cancel_numerals", [])
+ else Data.prove_conv [Data.norm_tac ss] ctxt prems
+ (t', Data.mk_bal (newshape(n1,terms1'), newshape(n2,terms2')))
in
- Option.map (Data.simplify_meta_eq ss)
- (if n2<=n1 then
- Data.prove_conv
- [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
- Data.numeral_simp_tac ss] ctxt hyps xs
- (t', Data.mk_bal (newshape(n1-n2,terms1'),
- Data.mk_sum T terms2'))
- else
- Data.prove_conv
- [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
- Data.numeral_simp_tac ss] ctxt hyps xs
- (t', Data.mk_bal (Data.mk_sum T terms1',
- newshape(n2-n1,terms2'))))
+ Option.map (export o Data.simplify_meta_eq ss)
+ (if n2 <= n1 then
+ Data.prove_conv
+ [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
+ Data.numeral_simp_tac ss] ctxt prems
+ (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
+ else
+ Data.prove_conv
+ [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
+ Data.numeral_simp_tac ss] ctxt prems
+ (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
end
+ (* FIXME avoid handling of generic exceptions *)
handle TERM _ => NONE
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral)
Undeclared type constructor "Numeral.bin"*)
--- a/src/Provers/Arith/combine_numerals.ML Wed Jul 12 21:19:14 2006 +0200
+++ b/src/Provers/Arith/combine_numerals.ML Wed Jul 12 21:19:17 2006 +0200
@@ -27,7 +27,7 @@
(*rules*)
val left_distrib: thm
(*proof tools*)
- val prove_conv: tactic list -> Proof.context -> string list -> term * term -> thm option
+ val prove_conv: tactic list -> Proof.context -> term * term -> thm option
val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: simpset -> tactic (*proves the initial lemma*)
val numeral_simp_tac: simpset -> tactic (*proves the final theorem*)
@@ -38,56 +38,57 @@
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
sig
val proc: simpset -> term -> thm option
- end
+ end
=
struct
(*Remove the first occurrence of #m*u from the term list*)
fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
- raise TERM("combine_numerals: remove", [])
+ raise TERM("combine_numerals: remove", [])
| remove (m, u, t::terms) =
case try Data.dest_coeff t of
- SOME(n,v) => if m=n andalso u aconv v then terms
- else t :: remove (m, u, terms)
- | NONE => t :: remove (m, u, terms);
+ SOME(n,v) => if m=n andalso u aconv v then terms
+ else t :: remove (m, u, terms)
+ | NONE => t :: remove (m, u, terms);
(*a left-to-right scan of terms, seeking another term of the form #n*u, where
#m*u is already in terms for some m*)
-fun find_repeated (tab, _, []) = raise TERM("find_repeated", [])
+fun find_repeated (tab, _, []) = raise TERM("find_repeated", [])
| find_repeated (tab, past, t::terms) =
case try Data.dest_coeff t of
- SOME(n,u) =>
- (case Termtab.lookup tab u of
- SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
- | NONE => find_repeated (Termtab.update (u, n) tab,
- t::past, terms))
- | NONE => find_repeated (tab, t::past, terms);
+ SOME(n,u) =>
+ (case Termtab.lookup tab u of
+ SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
+ | NONE => find_repeated (Termtab.update (u, n) tab,
+ t::past, terms))
+ | NONE => find_repeated (tab, t::past, terms);
(*the simplification procedure*)
fun proc ss t =
let
- val ctxt = Simplifier.the_context ss;
- (*first freeze any Vars in the term to prevent flex-flex problems*)
- val (t', xs) = Term.adhoc_freeze_vars t
- val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
- val T = Term.fastype_of u
- val reshape = (*Move i*u to the front and put j*u into standard form
- i + #m + j + k == #m + i + (j + k) *)
- if m=0 orelse n=0 then (*trivial, so do nothing*)
- raise TERM("combine_numerals", [])
- else Data.prove_conv [Data.norm_tac ss] ctxt xs
- (t',
- Data.mk_sum T ([Data.mk_coeff(m,u),
- Data.mk_coeff(n,u)] @ terms))
+ val ctxt = Simplifier.the_context ss;
+ val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+ val export = singleton (Variable.export ctxt' ctxt)
+
+ val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
+ val T = Term.fastype_of u
+
+ val reshape = (*Move i*u to the front and put j*u into standard form
+ i + #m + j + k == #m + i + (j + k) *)
+ if m=0 orelse n=0 then (*trivial, so do nothing*)
+ raise TERM("combine_numerals", [])
+ else Data.prove_conv [Data.norm_tac ss] ctxt
+ (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))
in
- Option.map (Data.simplify_meta_eq ss)
- (Data.prove_conv
- [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
- Data.numeral_simp_tac ss] ctxt xs
- (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
+ Option.map (export o Data.simplify_meta_eq ss)
+ (Data.prove_conv
+ [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
+ Data.numeral_simp_tac ss] ctxt
+ (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
end
+ (* FIXME avoid handling of generic exceptions *)
handle TERM _ => NONE
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral)
- Undeclared type constructor "Numeral.bin"*)
+ Undeclared type constructor "Numeral.bin"*)
end;
--- a/src/Provers/Arith/extract_common_term.ML Wed Jul 12 21:19:14 2006 +0200
+++ b/src/Provers/Arith/extract_common_term.ML Wed Jul 12 21:19:17 2006 +0200
@@ -8,7 +8,7 @@
i + u + j ~~ i' + u + j' == u + (i + j) ~~ u + (i' + j')
i + u ~~ u == u + i ~~ u + 0
-where ~~ is an appropriate balancing operation (e.g. =, <=, <, -) and 0 is a
+where ~~ is an appropriate balancing operation (e.g. =, <=, <, -) and 0 is a
suitable identity for +.
This massaged formula is then simplified in a user-specified way.
@@ -23,8 +23,7 @@
val dest_bal: term -> term * term
val find_first: term -> term list -> term list
(*proof tools*)
- val prove_conv: tactic list -> Proof.context ->
- thm list -> string list -> term * term -> thm option
+ val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
val norm_tac: simpset -> tactic (*proves the result*)
val simplify_meta_eq: simpset -> thm -> thm (*simplifies the result*)
end;
@@ -33,43 +32,45 @@
functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
sig
val proc: simpset -> term -> thm option
- end
+ end
=
struct
(*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
fun find_common (terms1,terms2) =
let val tab2 = fold (Termtab.update o rpair ()) terms2 Termtab.empty
- fun seek [] = raise TERM("find_common", [])
- | seek (u::terms) =
- if Termtab.defined tab2 u then u
- else seek terms
+ fun seek [] = raise TERM("find_common", [])
+ | seek (u::terms) =
+ if Termtab.defined tab2 u then u
+ else seek terms
in seek terms1 end;
(*the simplification procedure*)
fun proc ss t =
let
- val ctxt = Simplifier.the_context ss;
- val hyps = prems_of_ss ss;
- (*first freeze any Vars in the term to prevent flex-flex problems*)
- val (t', xs) = Term.adhoc_freeze_vars t;
- val (t1,t2) = Data.dest_bal t'
- val terms1 = Data.dest_sum t1
- and terms2 = Data.dest_sum t2
- val u = find_common (terms1,terms2)
- val terms1' = Data.find_first u terms1
- and terms2' = Data.find_first u terms2
- and T = Term.fastype_of u
- val reshape =
- Data.prove_conv [Data.norm_tac ss] ctxt hyps xs
- (t',
- Data.mk_bal (Data.mk_sum T (u::terms1'),
- Data.mk_sum T (u::terms2')))
+ val ctxt = Simplifier.the_context ss;
+ val prems = prems_of_ss ss;
+ val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+ val export = singleton (Variable.export ctxt' ctxt)
+
+ val (t1,t2) = Data.dest_bal t'
+ val terms1 = Data.dest_sum t1
+ and terms2 = Data.dest_sum t2
+
+ val u = find_common (terms1,terms2)
+ val terms1' = Data.find_first u terms1
+ and terms2' = Data.find_first u terms2
+ and T = Term.fastype_of u
+
+ val reshape =
+ Data.prove_conv [Data.norm_tac ss] ctxt prems
+ (t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')))
in
- Option.map (Data.simplify_meta_eq ss) reshape
+ Option.map (export o Data.simplify_meta_eq ss) reshape
end
+ (* FIXME avoid handling of generic exceptions *)
handle TERM _ => NONE
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral)
- Undeclared type constructor "Numeral.bin"*)
+ Undeclared type constructor "Numeral.bin"*)
end;