clarified Drule.gen_all: observe context more carefully;
authorwenzelm
Sat Mar 07 21:32:31 2015 +0100 (2015-03-07)
changeset 59647c6f413b660cf
parent 59646 48d400469bcb
child 59648 d1148f0baef5
clarified Drule.gen_all: observe context more carefully;
src/FOL/simpdata.ML
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Partial_Function.thy
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/simpdata.ML
src/HOL/Transcendental.thy
src/Pure/Isar/local_defs.ML
src/Pure/Isar/object_logic.ML
src/Pure/drule.ML
src/Pure/raw_simplifier.ML
src/Sequents/simpdata.ML
src/ZF/Main_ZF.thy
src/ZF/OrdQuant.thy
src/ZF/Tools/inductive_package.ML
src/ZF/pair.thy
     1.1 --- a/src/FOL/simpdata.ML	Sat Mar 07 15:40:36 2015 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Sat Mar 07 21:32:31 2015 +0100
     1.3 @@ -50,7 +50,8 @@
     1.4         | _ => [th])
     1.5    in atoms end;
     1.6  
     1.7 -fun mksimps pairs (_: Proof.context) = map mk_eq o mk_atomize pairs o gen_all;
     1.8 +fun mksimps pairs ctxt =
     1.9 +  map mk_eq o mk_atomize pairs o Drule.gen_all (Variable.maxidx_of ctxt);
    1.10  
    1.11  
    1.12  (** make simplification procedures for quantifier elimination **)
     2.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sat Mar 07 15:40:36 2015 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sat Mar 07 21:32:31 2015 +0100
     2.3 @@ -8058,7 +8058,7 @@
     2.4            by auto
     2.5          show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x -
     2.6            (f ((Sup k)) - f ((Inf k)))) \<le> e * (b - a) / 2"
     2.7 -          apply (rule *[where t="p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0}"])
     2.8 +          apply (rule *[where t1="p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0}"])
     2.9            apply (rule setsum.mono_neutral_right[OF pA(2)])
    2.10            defer
    2.11            apply rule
     3.1 --- a/src/HOL/Partial_Function.thy	Sat Mar 07 15:40:36 2015 +0100
     3.2 +++ b/src/HOL/Partial_Function.thy	Sat Mar 07 21:32:31 2015 +0100
     3.3 @@ -168,21 +168,23 @@
     3.4  text {* Fixpoint induction rule *}
     3.5  
     3.6  lemma fixp_induct_uc:
     3.7 -  fixes F :: "'c \<Rightarrow> 'c" and
     3.8 -    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
     3.9 -    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
    3.10 -    P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
    3.11 +  fixes F :: "'c \<Rightarrow> 'c"
    3.12 +    and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a"
    3.13 +    and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
    3.14 +    and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
    3.15    assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
    3.16 -  assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
    3.17 -  assumes inverse: "\<And>f. U (C f) = f"
    3.18 -  assumes adm: "ccpo.admissible lub_fun le_fun P"
    3.19 -  and bot: "P (\<lambda>_. lub {})"
    3.20 -  assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
    3.21 +    and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
    3.22 +    and inverse: "\<And>f. U (C f) = f"
    3.23 +    and adm: "ccpo.admissible lub_fun le_fun P"
    3.24 +    and bot: "P (\<lambda>_. lub {})"
    3.25 +    and step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
    3.26    shows "P (U f)"
    3.27  unfolding eq inverse
    3.28  apply (rule ccpo.fixp_induct[OF ccpo adm])
    3.29  apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
    3.30 -by (rule_tac f="C x" in step, simp add: inverse)
    3.31 +apply (rule_tac f5="C x" in step)
    3.32 +apply (simp add: inverse)
    3.33 +done
    3.34  
    3.35  
    3.36  text {* Rules for @{term mono_body}: *}
     4.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat Mar 07 15:40:36 2015 +0100
     4.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat Mar 07 21:32:31 2015 +0100
     4.3 @@ -789,8 +789,11 @@
     4.4                val vselss = map (map (rapp v)) selss;
     4.5  
     4.6                fun make_sel_thm xs' case_thm sel_def =
     4.7 -                zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
     4.8 -                    (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
     4.9 +                zero_var_indexes
    4.10 +                  (Drule.gen_all (Variable.maxidx_of lthy)
    4.11 +                    (Drule.rename_bvars'
    4.12 +                      (map (SOME o fst) xs')
    4.13 +                      (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
    4.14  
    4.15                val sel_thmss = @{map 3} (map oo make_sel_thm) xss' case_thms sel_defss;
    4.16  
     5.1 --- a/src/HOL/Tools/simpdata.ML	Sat Mar 07 15:40:36 2015 +0100
     5.2 +++ b/src/HOL/Tools/simpdata.ML	Sat Mar 07 21:32:31 2015 +0100
     5.3 @@ -113,7 +113,7 @@
     5.4    in atoms end;
     5.5  
     5.6  fun mksimps pairs ctxt =
     5.7 -  map_filter (try mk_eq) o mk_atomize ctxt pairs o gen_all;
     5.8 +  map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt);
     5.9  
    5.10  val simp_legacy_precond =
    5.11    Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false)
     6.1 --- a/src/HOL/Transcendental.thy	Sat Mar 07 15:40:36 2015 +0100
     6.2 +++ b/src/HOL/Transcendental.thy	Sat Mar 07 21:32:31 2015 +0100
     6.3 @@ -4028,11 +4028,12 @@
     6.4          case False
     6.5          hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
     6.6          have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
     6.7 -          by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
     6.8 +        thm suminf_eq_arctan_bounded
     6.9 +          by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
    6.10              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
    6.11          moreover
    6.12          have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
    6.13 -          by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
    6.14 +          by (rule suminf_eq_arctan_bounded[where x1="x" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>"])
    6.15               (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
    6.16          ultimately
    6.17          show ?thesis using suminf_arctan_zero by auto
     7.1 --- a/src/Pure/Isar/local_defs.ML	Sat Mar 07 15:40:36 2015 +0100
     7.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Mar 07 21:32:31 2015 +0100
     7.3 @@ -147,7 +147,7 @@
     7.4                    NONE => (asm, false)
     7.5                  | SOME u =>
     7.6                      if t aconv u then (asm, false)
     7.7 -                    else (Drule.abs_def (Drule.gen_all asm), true))
     7.8 +                    else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true))
     7.9                end)));
    7.10        in (apply2 (map #1) (List.partition #2 defs_asms), th') end
    7.11    end;
     8.1 --- a/src/Pure/Isar/object_logic.ML	Sat Mar 07 15:40:36 2015 +0100
     8.2 +++ b/src/Pure/Isar/object_logic.ML	Sat Mar 07 21:32:31 2015 +0100
     8.3 @@ -201,7 +201,9 @@
     8.4  
     8.5  fun gen_rulify full ctxt =
     8.6    Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
     8.7 -  #> Drule.gen_all #> Thm.strip_shyps #> Drule.zero_var_indexes;
     8.8 +  #> Drule.gen_all (Variable.maxidx_of ctxt)
     8.9 +  #> Thm.strip_shyps
    8.10 +  #> Drule.zero_var_indexes;
    8.11  
    8.12  val rulify = gen_rulify true;
    8.13  val rulify_no_asm = gen_rulify false;
     9.1 --- a/src/Pure/drule.ML	Sat Mar 07 15:40:36 2015 +0100
     9.2 +++ b/src/Pure/drule.ML	Sat Mar 07 21:32:31 2015 +0100
     9.3 @@ -18,7 +18,7 @@
     9.4    val forall_intr_list: cterm list -> thm -> thm
     9.5    val forall_intr_vars: thm -> thm
     9.6    val forall_elim_list: cterm list -> thm -> thm
     9.7 -  val gen_all: thm -> thm
     9.8 +  val gen_all: int -> thm -> thm
     9.9    val lift_all: cterm -> thm -> thm
    9.10    val implies_elim_list: thm -> thm list -> thm
    9.11    val implies_intr_list: cterm list -> thm -> thm
    9.12 @@ -208,10 +208,13 @@
    9.13    in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
    9.14  
    9.15  (*generalize outermost parameters*)
    9.16 -fun gen_all th =
    9.17 +fun gen_all maxidx0 th =
    9.18    let
    9.19 -    val {thy, prop, maxidx, ...} = Thm.rep_thm th;
    9.20 -    fun elim (x, T) = Thm.forall_elim (Thm.global_cterm_of thy (Var ((x, maxidx + 1), T)));
    9.21 +    val thy = Thm.theory_of_thm th;
    9.22 +    val maxidx = Thm.maxidx_thm th maxidx0;
    9.23 +    val prop = Thm.prop_of th;
    9.24 +    fun elim (x, T) =
    9.25 +      Thm.forall_elim (Thm.global_cterm_of thy (Var ((x, maxidx + 1), T)));
    9.26    in fold elim (outer_params prop) th end;
    9.27  
    9.28  (*lift vars wrt. outermost goal parameters
    10.1 --- a/src/Pure/raw_simplifier.ML	Sat Mar 07 15:40:36 2015 +0100
    10.2 +++ b/src/Pure/raw_simplifier.ML	Sat Mar 07 21:32:31 2015 +0100
    10.3 @@ -1382,7 +1382,7 @@
    10.4      Conv.fconv_rule
    10.5        (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th)
    10.6    |> Thm.adjust_maxidx_thm ~1
    10.7 -  |> Drule.gen_all;
    10.8 +  |> Drule.gen_all (Variable.maxidx_of ctxt);
    10.9  
   10.10  val hhf_ss =
   10.11    simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
    11.1 --- a/src/Sequents/simpdata.ML	Sat Mar 07 15:40:36 2015 +0100
    11.2 +++ b/src/Sequents/simpdata.ML	Sat Mar 07 21:32:31 2015 +0100
    11.3 @@ -71,7 +71,8 @@
    11.4    setSSolver (mk_solver "safe" safe_solver)
    11.5    setSolver (mk_solver "unsafe" unsafe_solver)
    11.6    |> Simplifier.set_subgoaler asm_simp_tac
    11.7 -  |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o gen_all)
    11.8 +  |> Simplifier.set_mksimps (fn ctxt =>
    11.9 +      map (mk_meta_eq ctxt) o atomize o Drule.gen_all (Variable.maxidx_of ctxt))
   11.10    |> Simplifier.set_mkcong mk_meta_cong
   11.11    |> simpset_of;
   11.12  
    12.1 --- a/src/ZF/Main_ZF.thy	Sat Mar 07 15:40:36 2015 +0100
    12.2 +++ b/src/ZF/Main_ZF.thy	Sat Mar 07 21:32:31 2015 +0100
    12.3 @@ -71,7 +71,8 @@
    12.4  
    12.5  
    12.6  declaration {* fn _ =>
    12.7 -  Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
    12.8 +  Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
    12.9 +    map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
   12.10  *}
   12.11  
   12.12  end
    13.1 --- a/src/ZF/OrdQuant.thy	Sat Mar 07 15:40:36 2015 +0100
    13.2 +++ b/src/ZF/OrdQuant.thy	Sat Mar 07 21:32:31 2015 +0100
    13.3 @@ -361,7 +361,8 @@
    13.4      ZF_conn_pairs, ZF_mem_pairs);
    13.5  *}
    13.6  declaration {* fn _ =>
    13.7 -  Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
    13.8 +  Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
    13.9 +    map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
   13.10  *}
   13.11  
   13.12  text {* Setting up the one-point-rule simproc *}
    14.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Mar 07 15:40:36 2015 +0100
    14.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Mar 07 21:32:31 2015 +0100
    14.3 @@ -327,7 +327,8 @@
    14.4         If the premises get simplified, then the proofs could fail.*)
    14.5       val min_ss =
    14.6             (empty_simpset (Proof_Context.init_global thy)
    14.7 -             |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)))
    14.8 +             |> Simplifier.set_mksimps (fn ctxt =>
    14.9 +                 map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
   14.10             setSolver (mk_solver "minimal"
   14.11                        (fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt)
   14.12                                     ORELSE' assume_tac ctxt
    15.1 --- a/src/ZF/pair.thy	Sat Mar 07 15:40:36 2015 +0100
    15.2 +++ b/src/ZF/pair.thy	Sat Mar 07 21:32:31 2015 +0100
    15.3 @@ -12,7 +12,8 @@
    15.4  
    15.5  setup {*
    15.6    map_theory_simpset
    15.7 -    (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))
    15.8 +    (Simplifier.set_mksimps (fn ctxt =>
    15.9 +        map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt))
   15.10        #> Simplifier.add_cong @{thm if_weak_cong})
   15.11  *}
   15.12