# HG changeset patch # User wenzelm # Date 1425760351 -3600 # Node ID c6f413b660cfbc105d9ec99c81fb3da72a52ff5e # Parent 48d400469bcbaaaee29e5bc204d563f104b15aee clarified Drule.gen_all: observe context more carefully; diff -r 48d400469bcb -r c6f413b660cf src/FOL/simpdata.ML --- 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 **) diff -r 48d400469bcb -r c6f413b660cf src/HOL/Multivariate_Analysis/Integration.thy --- 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 (\(x, k)\p \ ?A. content k *\<^sub>R f' x - (f ((Sup k)) - f ((Inf k)))) \ e * (b - a) / 2" - apply (rule *[where t="p \ {t. fst t \ {a, b} \ content(snd t) \ 0}"]) + apply (rule *[where t1="p \ {t. fst t \ {a, b} \ content(snd t) \ 0}"]) apply (rule setsum.mono_neutral_right[OF pA(2)]) defer apply rule diff -r 48d400469bcb -r c6f413b660cf src/HOL/Partial_Function.thy --- 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 \ 'c" and - U :: "'c \ 'b \ 'a" and - C :: "('b \ 'a) \ 'c" and - P :: "('b \ 'a) \ bool" + fixes F :: "'c \ 'c" + and U :: "'c \ 'b \ 'a" + and C :: "('b \ 'a) \ 'c" + and P :: "('b \ 'a) \ bool" assumes mono: "\x. mono_body (\f. U (F (C f)) x)" - assumes eq: "f \ C (fixp_fun (\f. U (F (C f))))" - assumes inverse: "\f. U (C f) = f" - assumes adm: "ccpo.admissible lub_fun le_fun P" - and bot: "P (\_. lub {})" - assumes step: "\f. P (U f) \ P (U (F f))" + and eq: "f \ C (fixp_fun (\f. U (F (C f))))" + and inverse: "\f. U (C f) = f" + and adm: "ccpo.admissible lub_fun le_fun P" + and bot: "P (\_. lub {})" + and step: "\f. P (U f) \ 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}: *} diff -r 48d400469bcb -r c6f413b660cf src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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; diff -r 48d400469bcb -r c6f413b660cf src/HOL/Tools/simpdata.ML --- 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) diff -r 48d400469bcb -r c6f413b660cf src/HOL/Transcendental.thy --- 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 < \x\" and "- \x\ < \x\" by auto have "suminf (?c (-\x\)) - arctan (-\x\) = suminf (?c 0) - arctan 0" - by (rule suminf_eq_arctan_bounded[where x="0" and a="-\x\" and b="\x\", symmetric]) + thm suminf_eq_arctan_bounded + by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\x\" and b1="\x\", symmetric]) (simp_all only: `\x\ < r` `-\x\ < \x\` neg_less_iff_less) moreover have "suminf (?c x) - arctan x = suminf (?c (-\x\)) - arctan (-\x\)" - by (rule suminf_eq_arctan_bounded[where x="x" and a="-\x\" and b="\x\"]) + by (rule suminf_eq_arctan_bounded[where x1="x" and a1="-\x\" and b1="\x\"]) (simp_all only: `\x\ < r` `-\x\ < \x\` neg_less_iff_less) ultimately show ?thesis using suminf_arctan_zero by auto diff -r 48d400469bcb -r c6f413b660cf src/Pure/Isar/local_defs.ML --- 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; diff -r 48d400469bcb -r c6f413b660cf src/Pure/Isar/object_logic.ML --- 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; diff -r 48d400469bcb -r c6f413b660cf src/Pure/drule.ML --- 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 diff -r 48d400469bcb -r c6f413b660cf src/Pure/raw_simplifier.ML --- 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 ())) diff -r 48d400469bcb -r c6f413b660cf src/Sequents/simpdata.ML --- 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; diff -r 48d400469bcb -r c6f413b660cf src/ZF/Main_ZF.thy --- 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 diff -r 48d400469bcb -r c6f413b660cf src/ZF/OrdQuant.thy --- 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 *} diff -r 48d400469bcb -r c6f413b660cf src/ZF/Tools/inductive_package.ML --- 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 diff -r 48d400469bcb -r c6f413b660cf src/ZF/pair.thy --- 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}) *}