--- a/src/FOL/simpdata.ML Sat Mar 07 15:40:36 2015 +0100
+++ b/src/FOL/simpdata.ML Sat Mar 07 21:32:31 2015 +0100
@@ -50,7 +50,8 @@
| _ => [th])
in atoms end;
-fun mksimps pairs (_: Proof.context) = map mk_eq o mk_atomize pairs o gen_all;
+fun mksimps pairs ctxt =
+ map mk_eq o mk_atomize pairs o Drule.gen_all (Variable.maxidx_of ctxt);
(** make simplification procedures for quantifier elimination **)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Sat Mar 07 15:40:36 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Sat Mar 07 21:32:31 2015 +0100
@@ -8058,7 +8058,7 @@
by auto
show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x -
(f ((Sup k)) - f ((Inf k)))) \<le> e * (b - a) / 2"
- apply (rule *[where t="p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0}"])
+ apply (rule *[where t1="p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0}"])
apply (rule setsum.mono_neutral_right[OF pA(2)])
defer
apply rule
--- a/src/HOL/Partial_Function.thy Sat Mar 07 15:40:36 2015 +0100
+++ b/src/HOL/Partial_Function.thy Sat Mar 07 21:32:31 2015 +0100
@@ -168,21 +168,23 @@
text {* Fixpoint induction rule *}
lemma fixp_induct_uc:
- fixes F :: "'c \<Rightarrow> 'c" and
- U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
- C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
- P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
+ fixes F :: "'c \<Rightarrow> 'c"
+ and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a"
+ and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
+ and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
- assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
- assumes inverse: "\<And>f. U (C f) = f"
- assumes adm: "ccpo.admissible lub_fun le_fun P"
- and bot: "P (\<lambda>_. lub {})"
- assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
+ and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
+ and inverse: "\<And>f. U (C f) = f"
+ and adm: "ccpo.admissible lub_fun le_fun P"
+ and bot: "P (\<lambda>_. lub {})"
+ and step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
shows "P (U f)"
unfolding eq inverse
apply (rule ccpo.fixp_induct[OF ccpo adm])
apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
-by (rule_tac f="C x" in step, simp add: inverse)
+apply (rule_tac f5="C x" in step)
+apply (simp add: inverse)
+done
text {* Rules for @{term mono_body}: *}
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sat Mar 07 15:40:36 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sat Mar 07 21:32:31 2015 +0100
@@ -789,8 +789,11 @@
val vselss = map (map (rapp v)) selss;
fun make_sel_thm xs' case_thm sel_def =
- zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
- (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
+ zero_var_indexes
+ (Drule.gen_all (Variable.maxidx_of lthy)
+ (Drule.rename_bvars'
+ (map (SOME o fst) xs')
+ (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
val sel_thmss = @{map 3} (map oo make_sel_thm) xss' case_thms sel_defss;
--- a/src/HOL/Tools/simpdata.ML Sat Mar 07 15:40:36 2015 +0100
+++ b/src/HOL/Tools/simpdata.ML Sat Mar 07 21:32:31 2015 +0100
@@ -113,7 +113,7 @@
in atoms end;
fun mksimps pairs ctxt =
- map_filter (try mk_eq) o mk_atomize ctxt pairs o gen_all;
+ map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt);
val simp_legacy_precond =
Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false)
--- a/src/HOL/Transcendental.thy Sat Mar 07 15:40:36 2015 +0100
+++ b/src/HOL/Transcendental.thy Sat Mar 07 21:32:31 2015 +0100
@@ -4028,11 +4028,12 @@
case False
hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
- by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
+ thm suminf_eq_arctan_bounded
+ by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
(simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
moreover
have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
- by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
+ by (rule suminf_eq_arctan_bounded[where x1="x" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>"])
(simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
ultimately
show ?thesis using suminf_arctan_zero by auto
--- a/src/Pure/Isar/local_defs.ML Sat Mar 07 15:40:36 2015 +0100
+++ b/src/Pure/Isar/local_defs.ML Sat Mar 07 21:32:31 2015 +0100
@@ -147,7 +147,7 @@
NONE => (asm, false)
| SOME u =>
if t aconv u then (asm, false)
- else (Drule.abs_def (Drule.gen_all asm), true))
+ else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true))
end)));
in (apply2 (map #1) (List.partition #2 defs_asms), th') end
end;
--- a/src/Pure/Isar/object_logic.ML Sat Mar 07 15:40:36 2015 +0100
+++ b/src/Pure/Isar/object_logic.ML Sat Mar 07 21:32:31 2015 +0100
@@ -201,7 +201,9 @@
fun gen_rulify full ctxt =
Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
- #> Drule.gen_all #> Thm.strip_shyps #> Drule.zero_var_indexes;
+ #> Drule.gen_all (Variable.maxidx_of ctxt)
+ #> Thm.strip_shyps
+ #> Drule.zero_var_indexes;
val rulify = gen_rulify true;
val rulify_no_asm = gen_rulify false;
--- a/src/Pure/drule.ML Sat Mar 07 15:40:36 2015 +0100
+++ b/src/Pure/drule.ML Sat Mar 07 21:32:31 2015 +0100
@@ -18,7 +18,7 @@
val forall_intr_list: cterm list -> thm -> thm
val forall_intr_vars: thm -> thm
val forall_elim_list: cterm list -> thm -> thm
- val gen_all: thm -> thm
+ val gen_all: int -> thm -> thm
val lift_all: cterm -> thm -> thm
val implies_elim_list: thm -> thm list -> thm
val implies_intr_list: cterm list -> thm -> thm
@@ -208,10 +208,13 @@
in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
(*generalize outermost parameters*)
-fun gen_all th =
+fun gen_all maxidx0 th =
let
- val {thy, prop, maxidx, ...} = Thm.rep_thm th;
- fun elim (x, T) = Thm.forall_elim (Thm.global_cterm_of thy (Var ((x, maxidx + 1), T)));
+ val thy = Thm.theory_of_thm th;
+ val maxidx = Thm.maxidx_thm th maxidx0;
+ val prop = Thm.prop_of th;
+ fun elim (x, T) =
+ Thm.forall_elim (Thm.global_cterm_of thy (Var ((x, maxidx + 1), T)));
in fold elim (outer_params prop) th end;
(*lift vars wrt. outermost goal parameters
--- a/src/Pure/raw_simplifier.ML Sat Mar 07 15:40:36 2015 +0100
+++ b/src/Pure/raw_simplifier.ML Sat Mar 07 21:32:31 2015 +0100
@@ -1382,7 +1382,7 @@
Conv.fconv_rule
(rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th)
|> Thm.adjust_maxidx_thm ~1
- |> Drule.gen_all;
+ |> Drule.gen_all (Variable.maxidx_of ctxt);
val hhf_ss =
simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
--- a/src/Sequents/simpdata.ML Sat Mar 07 15:40:36 2015 +0100
+++ b/src/Sequents/simpdata.ML Sat Mar 07 21:32:31 2015 +0100
@@ -71,7 +71,8 @@
setSSolver (mk_solver "safe" safe_solver)
setSolver (mk_solver "unsafe" unsafe_solver)
|> Simplifier.set_subgoaler asm_simp_tac
- |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o gen_all)
+ |> Simplifier.set_mksimps (fn ctxt =>
+ map (mk_meta_eq ctxt) o atomize o Drule.gen_all (Variable.maxidx_of ctxt))
|> Simplifier.set_mkcong mk_meta_cong
|> simpset_of;
--- a/src/ZF/Main_ZF.thy Sat Mar 07 15:40:36 2015 +0100
+++ b/src/ZF/Main_ZF.thy Sat Mar 07 21:32:31 2015 +0100
@@ -71,7 +71,8 @@
declaration {* fn _ =>
- Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
+ Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
+ map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
*}
end
--- a/src/ZF/OrdQuant.thy Sat Mar 07 15:40:36 2015 +0100
+++ b/src/ZF/OrdQuant.thy Sat Mar 07 21:32:31 2015 +0100
@@ -361,7 +361,8 @@
ZF_conn_pairs, ZF_mem_pairs);
*}
declaration {* fn _ =>
- Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
+ Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
+ map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
*}
text {* Setting up the one-point-rule simproc *}
--- a/src/ZF/Tools/inductive_package.ML Sat Mar 07 15:40:36 2015 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sat Mar 07 21:32:31 2015 +0100
@@ -327,7 +327,8 @@
If the premises get simplified, then the proofs could fail.*)
val min_ss =
(empty_simpset (Proof_Context.init_global thy)
- |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)))
+ |> Simplifier.set_mksimps (fn ctxt =>
+ map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
setSolver (mk_solver "minimal"
(fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt)
ORELSE' assume_tac ctxt
--- a/src/ZF/pair.thy Sat Mar 07 15:40:36 2015 +0100
+++ b/src/ZF/pair.thy Sat Mar 07 21:32:31 2015 +0100
@@ -12,7 +12,8 @@
setup {*
map_theory_simpset
- (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))
+ (Simplifier.set_mksimps (fn ctxt =>
+ map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt))
#> Simplifier.add_cong @{thm if_weak_cong})
*}