# HG changeset patch # User wenzelm # Date 1028843384 -7200 # Node ID d8f5d339176605007c4076a6c38e318797e656cf # Parent 0e6adce08fb0346b938f3186d4d8eaf97114ca06 adhoc_freeze_vars; diff -r 0e6adce08fb0 -r d8f5d3391766 src/Provers/Arith/cancel_numeral_factor.ML --- 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) diff -r 0e6adce08fb0 -r d8f5d3391766 src/Provers/Arith/cancel_numerals.ML --- 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 diff -r 0e6adce08fb0 -r d8f5d3391766 src/Provers/Arith/combine_numerals.ML --- 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 diff -r 0e6adce08fb0 -r d8f5d3391766 src/Provers/Arith/extract_common_term.ML --- 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'))) diff -r 0e6adce08fb0 -r d8f5d3391766 src/Pure/term.ML --- 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;