--- a/src/Provers/Arith/cancel_numeral_factor.ML Thu Aug 08 23:48:31 2002 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Thu Aug 08 23:49:44 2002 +0200
@@ -30,7 +30,7 @@
as with < and <= but not = and div*)
(*proof tools*)
val prove_conv: tactic list -> Sign.sg ->
- thm list -> term * term -> thm option
+ thm list -> string list -> term * term -> thm option
val trans_tac: thm option -> tactic (*applies the initial lemma*)
val norm_tac: tactic (*proves the initial lemma*)
val numeral_simp_tac: tactic (*proves the final theorem*)
@@ -53,10 +53,7 @@
(*the simplification procedure*)
fun proc sg hyps t =
let (*first freeze any Vars in the term to prevent flex-flex problems*)
- val rand_s = gensym"_"
- fun mk_inst (var as Var((a,i),T)) =
- (var, Free((a ^ rand_s ^ string_of_int i), T))
- val t' = subst_atomic (map mk_inst (term_vars t)) t
+ 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
@@ -73,13 +70,13 @@
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] sg hyps
+ Data.prove_conv [Data.norm_tac] sg hyps xs
(t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
in
apsome Data.simplify_meta_eq
(Data.prove_conv
[Data.trans_tac reshape, rtac Data.cancel 1,
- Data.numeral_simp_tac] sg hyps (t', rhs))
+ Data.numeral_simp_tac] sg hyps xs (t', rhs))
end
handle TERM _ => None
| TYPE _ => None; (*Typically (if thy doesn't include Numeral)
--- a/src/Provers/Arith/cancel_numerals.ML Thu Aug 08 23:48:31 2002 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Thu Aug 08 23:49:44 2002 +0200
@@ -37,7 +37,7 @@
val bal_add2: thm
(*proof tools*)
val prove_conv: tactic list -> Sign.sg ->
- thm list -> term * term -> thm option
+ thm list -> string list -> term * term -> thm option
val trans_tac: thm option -> tactic (*applies the initial lemma*)
val norm_tac: tactic (*proves the initial lemma*)
val numeral_simp_tac: tactic (*proves the final theorem*)
@@ -71,10 +71,7 @@
(*the simplification procedure*)
fun proc sg hyps t =
let (*first freeze any Vars in the term to prevent flex-flex problems*)
- val rand_s = gensym"_"
- fun mk_inst (var as Var((a,i),T)) =
- (var, Free((a ^ rand_s ^ string_of_int i), T))
- val t' = subst_atomic (map mk_inst (term_vars t)) t
+ 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
@@ -86,7 +83,7 @@
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] sg hyps
+ else Data.prove_conv [Data.norm_tac] sg hyps xs
(t',
Data.mk_bal (newshape(n1,terms1'),
newshape(n2,terms2')))
@@ -95,13 +92,13 @@
(if n2<=n1 then
Data.prove_conv
[Data.trans_tac reshape, rtac Data.bal_add1 1,
- Data.numeral_simp_tac] sg hyps
+ Data.numeral_simp_tac] sg hyps xs
(t', Data.mk_bal (newshape(n1-n2,terms1'),
Data.mk_sum terms2'))
else
Data.prove_conv
[Data.trans_tac reshape, rtac Data.bal_add2 1,
- Data.numeral_simp_tac] sg hyps
+ Data.numeral_simp_tac] sg hyps xs
(t', Data.mk_bal (Data.mk_sum terms1',
newshape(n2-n1,terms2'))))
end
--- a/src/Provers/Arith/combine_numerals.ML Thu Aug 08 23:48:31 2002 +0200
+++ b/src/Provers/Arith/combine_numerals.ML Thu Aug 08 23:49:44 2002 +0200
@@ -27,7 +27,7 @@
(*rules*)
val left_distrib: thm
(*proof tools*)
- val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
+ val prove_conv: tactic list -> Sign.sg -> string list -> term * term -> thm option
val trans_tac: thm option -> tactic (*applies the initial lemma*)
val norm_tac: tactic (*proves the initial lemma*)
val numeral_simp_tac: tactic (*proves the final theorem*)
@@ -66,16 +66,13 @@
(*the simplification procedure*)
fun proc sg _ t =
let (*first freeze any Vars in the term to prevent flex-flex problems*)
- val rand_s = gensym"_"
- fun mk_inst (var as Var((a,i),T)) =
- (var, Free((a ^ rand_s ^ string_of_int i), T))
- val t' = subst_atomic (map mk_inst (term_vars t)) t
+ val (t', xs) = Term.adhoc_freeze_vars t;
val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
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] sg
+ else Data.prove_conv [Data.norm_tac] sg xs
(t',
Data.mk_sum ([Data.mk_coeff(m,u),
Data.mk_coeff(n,u)] @ terms))
@@ -83,7 +80,7 @@
apsome Data.simplify_meta_eq
(Data.prove_conv
[Data.trans_tac reshape, rtac Data.left_distrib 1,
- Data.numeral_simp_tac] sg
+ Data.numeral_simp_tac] sg xs
(t', Data.mk_sum (Data.mk_coeff(Data.add(m,n), u) :: terms)))
end
handle TERM _ => None
--- a/src/Provers/Arith/extract_common_term.ML Thu Aug 08 23:48:31 2002 +0200
+++ b/src/Provers/Arith/extract_common_term.ML Thu Aug 08 23:49:44 2002 +0200
@@ -24,7 +24,7 @@
val find_first: term -> term list -> term list
(*proof tools*)
val prove_conv: tactic list -> Sign.sg ->
- thm list -> term * term -> thm option
+ thm list -> string list -> term * term -> thm option
val norm_tac: tactic (*proves the result*)
val simplify_meta_eq: thm -> thm (*simplifies the result*)
end;
@@ -52,10 +52,7 @@
(*the simplification procedure*)
fun proc sg hyps t =
let (*first freeze any Vars in the term to prevent flex-flex problems*)
- val rand_s = gensym"_"
- fun mk_inst (var as Var((a,i),T)) =
- (var, Free((a ^ rand_s ^ string_of_int i), T))
- val t' = subst_atomic (map mk_inst (term_vars t)) t
+ 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
@@ -63,7 +60,7 @@
val terms1' = Data.find_first u terms1
and terms2' = Data.find_first u terms2
val reshape =
- Data.prove_conv [Data.norm_tac] sg hyps
+ Data.prove_conv [Data.norm_tac] sg hyps xs
(t',
Data.mk_bal (Data.mk_sum (u::terms1'),
Data.mk_sum (u::terms2')))
--- a/src/Pure/term.ML Thu Aug 08 23:48:31 2002 +0200
+++ b/src/Pure/term.ML Thu Aug 08 23:49:44 2002 +0200
@@ -195,6 +195,7 @@
val no_dummy_patterns: term -> term
val replace_dummy_patterns: int * term -> int * term
val is_replaced_dummy_pattern: indexname -> bool
+ val adhoc_freeze_vars: term -> term * string list
end;
structure Term: TERM =
@@ -1100,6 +1101,18 @@
fun is_replaced_dummy_pattern ("_dummy_", _) = true
| is_replaced_dummy_pattern _ = false;
+
+(* adhoc freezing *)
+
+fun adhoc_freeze_vars tm =
+ let
+ fun mk_inst (var as Var ((a, i), T)) =
+ let val x = a ^ Library.gensym "_" ^ string_of_int i
+ in ((var, Free(x, T)), x) end;
+ val (insts, xs) = split_list (map mk_inst (term_vars tm));
+ in (subst_atomic insts tm, xs) end;
+
+
end;