prefer local fixes;
authorwenzelm
Mon Mar 23 21:05:17 2015 +0100 (2015-03-23)
changeset 597886f7b6adac439
parent 59787 6e2a20486897
child 59789 4c9b3513dfa6
prefer local fixes;
src/ZF/AC/AC16_WO4.thy
src/ZF/AC/HH.thy
src/ZF/AC/WO2_AC16.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/Cardinal.thy
src/ZF/Coind/Map.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Induct/Multiset.thy
src/ZF/Induct/Mutil.thy
src/ZF/Induct/Primrec.thy
src/ZF/Int_ZF.thy
src/ZF/Order.thy
src/ZF/Resid/Residuals.thy
src/ZF/Tools/induct_tacs.ML
src/ZF/UNITY/AllocImpl.thy
src/ZF/UNITY/Comp.thy
src/ZF/UNITY/Distributor.thy
src/ZF/UNITY/Follows.thy
src/ZF/UNITY/GenPrefix.thy
src/ZF/UNITY/Increasing.thy
src/ZF/UNITY/Merge.thy
src/ZF/UNITY/WFair.thy
src/ZF/WF.thy
src/ZF/Zorn.thy
src/ZF/ex/Limit.thy
src/ZF/ex/Primes.thy
     1.1 --- a/src/ZF/AC/AC16_WO4.thy	Mon Mar 23 19:43:03 2015 +0100
     1.2 +++ b/src/ZF/AC/AC16_WO4.thy	Mon Mar 23 21:05:17 2015 +0100
     1.3 @@ -295,7 +295,7 @@
     1.4  apply (rule lam_type)
     1.5  apply (frule ex1_superset_a [THEN theI], fast+, clarify)
     1.6  apply (rule cons_eqE [of _ a])
     1.7 -apply (drule_tac A = "THE c. ?P (c) " and C = y in eq_imp_Int_eq)
     1.8 +apply (drule_tac A = "THE c. P (c)" and C = y for P in eq_imp_Int_eq)
     1.9  apply (simp_all add: the_eq_cons)
    1.10  done
    1.11  
     2.1 --- a/src/ZF/AC/HH.thy	Mon Mar 23 19:43:03 2015 +0100
     2.2 +++ b/src/ZF/AC/HH.thy	Mon Mar 23 21:05:17 2015 +0100
     2.3 @@ -57,7 +57,7 @@
     2.4  prefer 2 apply assumption+
     2.5  apply (rule leI [THEN le_imp_subset, THEN subset_imp_Diff_eq, THEN ssubst], 
     2.6         assumption)
     2.7 -apply (rule_tac t = "%z. z-?X" in subst_context)
     2.8 +apply (rule_tac t = "%z. z-X" for X in subst_context)
     2.9  apply (rule Diff_UN_eq_self)
    2.10  apply (drule Ord_DiffE, assumption) 
    2.11  apply (fast elim: ltE, auto) 
    2.12 @@ -162,7 +162,7 @@
    2.13  lemma f_subsets_imp_UN_HH_eq_x:
    2.14       "\<forall>z \<in> Pow(x)-{0}. f`z \<in> Pow(z)-{0}
    2.15        ==> x - (\<Union>j \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"
    2.16 -apply (case_tac "?P \<in> {0}", fast)
    2.17 +apply (case_tac "P \<in> {0}" for P, fast)
    2.18  apply (drule Diff_subset [THEN PowI, THEN DiffI])
    2.19  apply (drule bspec, assumption) 
    2.20  apply (drule f_subset_imp_HH_subset) 
     3.1 --- a/src/ZF/AC/WO2_AC16.thy	Mon Mar 23 19:43:03 2015 +0100
     3.2 +++ b/src/ZF/AC/WO2_AC16.thy	Mon Mar 23 21:05:17 2015 +0100
     3.3 @@ -563,7 +563,7 @@
     3.4  apply (elim exE)
     3.5  apply (rename_tac h)
     3.6  apply (rule_tac x = "\<Union>j<a. recfunAC16 (h,f,j,a) " in exI)
     3.7 -apply (rule_tac P="%z. ?Y & (\<forall>x \<in> z. ?Z (x))" 
     3.8 +apply (rule_tac P="%z. Y & (\<forall>x \<in> z. Z(x))"  for Y Z
     3.9         in bij_is_surj [THEN surj_image_eq, THEN subst], assumption)
    3.10  apply (rule lemma_simp_induct)
    3.11  apply (blast del: conjI notI
     4.1 --- a/src/ZF/AC/WO6_WO1.thy	Mon Mar 23 19:43:03 2015 +0100
     4.2 +++ b/src/ZF/AC/WO6_WO1.thy	Mon Mar 23 21:05:17 2015 +0100
     4.3 @@ -390,7 +390,7 @@
     4.4  apply (fast intro!: Ord_oadd domain_gg1 UN_gg1_eq gg1_lepoll_m)
     4.5  (* case 2 *)
     4.6  apply (elim oexE conjE)
     4.7 -apply (rule_tac A = "f`?B" in not_emptyE, assumption)
     4.8 +apply (rule_tac A = "f`B" for B in not_emptyE, assumption)
     4.9  apply (rule CollectI)
    4.10  apply (erule succ_natD)
    4.11  apply (rule_tac x = "a++a" in exI)
     5.1 --- a/src/ZF/Cardinal.thy	Mon Mar 23 19:43:03 2015 +0100
     5.2 +++ b/src/ZF/Cardinal.thy	Mon Mar 23 21:05:17 2015 +0100
     5.3 @@ -59,7 +59,7 @@
     5.4      "g \<in> Y->X
     5.5       ==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =
     5.6           X - lfp(X, %W. X - g``(Y - f``W))"
     5.7 -apply (rule_tac P = "%u. ?v = X-u"
     5.8 +apply (rule_tac P = "%u. v = X-u" for v
     5.9         in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
    5.10  apply (simp add: double_complement  fun_is_rel [THEN image_subset])
    5.11  done
    5.12 @@ -1079,7 +1079,7 @@
    5.13   prefer 2 apply (blast del: allE elim: equalityE, clarify)
    5.14  apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
    5.15   apply (blast intro: Diff_sing_Finite)
    5.16 -apply (thin_tac "\<forall>A. ?P(A) \<longrightarrow> Finite(A)")
    5.17 +apply (thin_tac "\<forall>A. P(A) \<longrightarrow> Finite(A)" for P)
    5.18  apply (rule equalityI)
    5.19   apply (blast intro: elim: equalityE)
    5.20  apply (blast intro: elim: equalityCE)
     6.1 --- a/src/ZF/Coind/Map.thy	Mon Mar 23 19:43:03 2015 +0100
     6.2 +++ b/src/ZF/Coind/Map.thy	Mon Mar 23 21:05:17 2015 +0100
     6.3 @@ -111,7 +111,7 @@
     6.4  (*Remaining subgoal*)
     6.5  apply (rule excluded_middle [THEN disjE])
     6.6  apply (erule image_Sigma1)
     6.7 -apply (drule_tac psi = "?uu \<notin> B" in asm_rl)
     6.8 +apply (drule_tac psi = "uu \<notin> B" for uu in asm_rl)
     6.9  apply (auto simp add: qbeta)
    6.10  done
    6.11  
     7.1 --- a/src/ZF/Constructible/Normal.thy	Mon Mar 23 19:43:03 2015 +0100
     7.2 +++ b/src/ZF/Constructible/Normal.thy	Mon Mar 23 21:05:17 2015 +0100
     7.3 @@ -284,7 +284,7 @@
     7.4        ==> F(\<Union>(X)) = (\<Union>y\<in>X. F(y))"
     7.5  apply (frule Ord_set_cases)
     7.6  apply (erule disjE, force) 
     7.7 -apply (thin_tac "X=0 \<longrightarrow> ?Q", auto)
     7.8 +apply (thin_tac "X=0 \<longrightarrow> Q" for Q, auto)
     7.9   txt{*The trival case of @{term "\<Union>X \<in> X"}*}
    7.10   apply (rule equalityI, blast intro: Ord_Union_eq_succD) 
    7.11   apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff) 
     8.1 --- a/src/ZF/Constructible/Relative.thy	Mon Mar 23 19:43:03 2015 +0100
     8.2 +++ b/src/ZF/Constructible/Relative.thy	Mon Mar 23 21:05:17 2015 +0100
     8.3 @@ -1024,9 +1024,9 @@
     8.4   apply blast
     8.5  txt{*Final, difficult case: the left-to-right direction of the theorem.*}
     8.6  apply (insert power_ax, simp add: power_ax_def)
     8.7 -apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
     8.8 +apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
     8.9  apply (blast, clarify)
    8.10 -apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
    8.11 +apply (drule_tac x=z and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
    8.12  apply assumption
    8.13  apply (blast intro: cartprod_iff_lemma)
    8.14  done
    8.15 @@ -1035,9 +1035,9 @@
    8.16       "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
    8.17  apply (simp del: cartprod_abs add: cartprod_iff)
    8.18  apply (insert power_ax, simp add: power_ax_def)
    8.19 -apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
    8.20 +apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
    8.21  apply (blast, clarify)
    8.22 -apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec, auto)
    8.23 +apply (drule_tac x=z and P="\<lambda>x. rex(M,Q(x))" for Q in rspec, auto)
    8.24  apply (intro rexI conjI, simp+)
    8.25  apply (insert cartprod_separation [of A B], simp)
    8.26  done
     9.1 --- a/src/ZF/Constructible/WFrec.thy	Mon Mar 23 19:43:03 2015 +0100
     9.2 +++ b/src/ZF/Constructible/WFrec.thy	Mon Mar 23 21:05:17 2015 +0100
     9.3 @@ -180,7 +180,7 @@
     9.4         ==> restrict(Y, r -`` {x}) = f"
     9.5  apply (subgoal_tac "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y \<longleftrightarrow> <y,z>:f") 
     9.6   apply (simp (no_asm_simp) add: restrict_def) 
     9.7 - apply (thin_tac "rall(M,?P)")+  --{*essential for efficiency*}
     9.8 + apply (thin_tac "rall(M,P)" for P)+  --{*essential for efficiency*}
     9.9   apply (frule is_recfun_type [THEN fun_is_rel], blast)
    9.10  apply (frule pair_components_in_M, assumption, clarify) 
    9.11  apply (rule iffI)
    10.1 --- a/src/ZF/Induct/Multiset.thy	Mon Mar 23 19:43:03 2015 +0100
    10.2 +++ b/src/ZF/Induct/Multiset.thy	Mon Mar 23 21:05:17 2015 +0100
    10.3 @@ -363,7 +363,7 @@
    10.4  
    10.5  lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 \<longleftrightarrow> M=0"
    10.6  apply (simp add: msize_def, auto)
    10.7 -apply (rule_tac P = "setsum (?u,?v) \<noteq> #0" in swap)
    10.8 +apply (rule_tac P = "setsum (u,v) \<noteq> #0" for u v in swap)
    10.9  apply blast
   10.10  apply (drule not_empty_multiset_imp_exist, assumption, clarify)
   10.11  apply (subgoal_tac "Finite (mset_of (M) - {a}) ")
   10.12 @@ -571,7 +571,7 @@
   10.13   apply (simp add: multiset_def multiset_fun_iff)
   10.14   apply (rule_tac x = A in exI, force)
   10.15  apply (simp_all add: mset_of_def)
   10.16 -apply (drule_tac psi = "\<forall>x \<in> A. ?u (x) " in asm_rl)
   10.17 +apply (drule_tac psi = "\<forall>x \<in> A. u(x)" for u in asm_rl)
   10.18  apply (drule_tac x = a in bspec)
   10.19  apply (simp (no_asm_simp))
   10.20  apply (subgoal_tac "cons (a, A) = A")
   10.21 @@ -596,7 +596,7 @@
   10.22  apply (simp (no_asm_simp) add: multiset_def multiset_fun_iff)
   10.23  apply blast
   10.24  apply (simp (no_asm_simp) add: mset_of_def)
   10.25 -apply (drule_tac b = "if ?u then ?v else ?w" in sym, simp_all)
   10.26 +apply (drule_tac b = "if u then v else w" for u v w in sym, simp_all)
   10.27  apply (subgoal_tac "{x \<in> A - {a} . 0 < funrestrict (M, A - {x}) ` x} = A - {a}")
   10.28  apply (auto intro!: setsum_cong simp add: zdiff_eq_iff zadd_commute multiset_def multiset_fun_iff mset_of_def)
   10.29  done
   10.30 @@ -815,7 +815,7 @@
   10.31  apply (subgoal_tac "aa \<in> A")
   10.32  prefer 2 apply blast
   10.33  apply (drule_tac x = "M0 +# M" and P =
   10.34 -       "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> ?Q(x)" in spec)
   10.35 +       "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> Q(x)" for Q in spec)
   10.36  apply (simp add: munion_assoc [symmetric])
   10.37  (* subgoal 3 \<in> additional conditions *)
   10.38  apply (auto intro!: multirel1_base [THEN fieldI2] simp add: Mult_iff_multiset)
   10.39 @@ -942,7 +942,7 @@
   10.40  apply (simp add: mdiff_union_single_conv melem_diff_single, clarify)
   10.41  apply (erule disjE, simp)
   10.42  apply (erule disjE, simp)
   10.43 -apply (drule_tac x = a and P = "%x. x :# Ka \<longrightarrow> ?Q(x)" in spec)
   10.44 +apply (drule_tac x = a and P = "%x. x :# Ka \<longrightarrow> Q(x)" for Q in spec)
   10.45  apply clarify
   10.46  apply (rule_tac x = xa in exI)
   10.47  apply (simp (no_asm_simp))
   10.48 @@ -1005,7 +1005,7 @@
   10.49  apply (drule sym, rotate_tac -1, simp)
   10.50  apply (erule_tac V = "$# x = msize (J') " in thin_rl)
   10.51  apply (frule_tac M = K and P = "%x. <x,a> \<in> r" in multiset_partition)
   10.52 -apply (erule_tac P = "\<forall>k \<in> mset_of (K) . ?P (k) " in rev_mp)
   10.53 +apply (erule_tac P = "\<forall>k \<in> mset_of (K) . P(k)" for P in rev_mp)
   10.54  apply (erule ssubst)
   10.55  apply (simp add: Ball_def, auto)
   10.56  apply (subgoal_tac "< (I +# {# x \<in> K. <x, a> \<in> r#}) +# {# x \<in> K. <x, a> \<notin> r#}, (I +# {# x \<in> K. <x, a> \<in> r#}) +# J'> \<in> multirel(A, r) ")
   10.57 @@ -1119,7 +1119,7 @@
   10.58  lemma munion_multirel_mono1:
   10.59       "[|<M, N> \<in> multirel(A, r); K \<in> Mult(A)|] ==> <M +# K, N +# K> \<in> multirel(A, r)"
   10.60  apply (frule multirel_type [THEN subsetD])
   10.61 -apply (rule_tac P = "%x. <x,?u> \<in> multirel(A, r) " in munion_commute [THEN subst])
   10.62 +apply (rule_tac P = "%x. <x,u> \<in> multirel(A, r)" for u in munion_commute [THEN subst])
   10.63  apply (subst munion_commute [of N])
   10.64  apply (rule munion_multirel_mono2)
   10.65  apply (auto simp add: Mult_iff_multiset)
    11.1 --- a/src/ZF/Induct/Mutil.thy	Mon Mar 23 19:43:03 2015 +0100
    11.2 +++ b/src/ZF/Induct/Mutil.thy	Mon Mar 23 21:05:17 2015 +0100
    11.3 @@ -147,7 +147,7 @@
    11.4        ==> t' \<notin> tiling(domino)"
    11.5    apply (rule notI)
    11.6    apply (drule tiling_domino_0_1)
    11.7 -  apply (erule_tac x = "|?A|" in eq_lt_E)
    11.8 +  apply (erule_tac x = "|A|" for A in eq_lt_E)
    11.9    apply (subgoal_tac "t \<in> tiling (domino)")
   11.10     prefer 2 (*Requires a small simpset that won't move the succ applications*)
   11.11     apply (simp only: nat_succI add_type dominoes_tile_matrix)
    12.1 --- a/src/ZF/Induct/Primrec.thy	Mon Mar 23 19:43:03 2015 +0100
    12.2 +++ b/src/ZF/Induct/Primrec.thy	Mon Mar 23 21:05:17 2015 +0100
    12.3 @@ -334,7 +334,7 @@
    12.4     apply (simp add: add_le_self [THEN ack_lt_mono1])
    12.5    txt {* ind step *}
    12.6    apply (rule succ_leI [THEN lt_trans1])
    12.7 -   apply (rule_tac j = "g ` ?ll #+ ?mm" in lt_trans1)
    12.8 +   apply (rule_tac j = "g ` ll #+ mm" for ll mm in lt_trans1)
    12.9      apply (erule_tac [2] bspec)
   12.10      apply (rule nat_le_refl [THEN add_le_mono])
   12.11         apply typecheck
    13.1 --- a/src/ZF/Int_ZF.thy	Mon Mar 23 19:43:03 2015 +0100
    13.2 +++ b/src/ZF/Int_ZF.thy	Mon Mar 23 21:05:17 2015 +0100
    13.3 @@ -661,7 +661,7 @@
    13.4  apply (simp add: zless_def znegative_def zdiff_def int_def)
    13.5  apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def)
    13.6  apply (rule_tac x = k in bexI)
    13.7 -apply (erule_tac i="succ (?v)" in add_left_cancel, auto)
    13.8 +apply (erule_tac i="succ (v)" for v in add_left_cancel, auto)
    13.9  done
   13.10  
   13.11  lemma zless_imp_succ_zadd:
    14.1 --- a/src/ZF/Order.thy	Mon Mar 23 19:43:03 2015 +0100
    14.2 +++ b/src/ZF/Order.thy	Mon Mar 23 21:05:17 2015 +0100
    14.3 @@ -670,8 +670,8 @@
    14.4    apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
    14.5     apply blast
    14.6    unfolding trans_on_def
    14.7 -  apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(?r).
    14.8 -          \<forall>z\<in>field(?r). \<langle>x, y\<rangle> \<in> ?r \<longrightarrow> \<langle>y, z\<rangle> \<in> ?r \<longrightarrow> \<langle>x, z\<rangle> \<in> ?r)" in rev_ballE)
    14.9 +  apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(r).
   14.10 +          \<forall>z\<in>field(r). \<langle>x, y\<rangle> \<in> r \<longrightarrow> \<langle>y, z\<rangle> \<in> r \<longrightarrow> \<langle>x, z\<rangle> \<in> r)" for r in rev_ballE)
   14.11      (* instance obtained from proof term generated by best *)
   14.12     apply best
   14.13    apply blast
    15.1 --- a/src/ZF/Resid/Residuals.thy	Mon Mar 23 19:43:03 2015 +0100
    15.2 +++ b/src/ZF/Resid/Residuals.thy	Mon Mar 23 21:05:17 2015 +0100
    15.3 @@ -129,7 +129,7 @@
    15.4                      subst_rec(v1 |> v2, u1 |> u2,n))"
    15.5  apply (erule Scomp.induct, safe)
    15.6  apply (simp_all add: lift_rec_Var subst_Var residuals_lift_rec)
    15.7 -apply (drule_tac psi = "\<forall>x.?P (x) " in asm_rl)
    15.8 +apply (drule_tac psi = "\<forall>x. P(x)" for P in asm_rl)
    15.9  apply (simp add: substitution)
   15.10  done
   15.11  
   15.12 @@ -159,7 +159,7 @@
   15.13  lemma preservation [rule_format]:
   15.14       "u ~ v ==> regular(v) \<longrightarrow> u|>v = (u un v)|>v"
   15.15  apply (erule Scomp.induct, safe)
   15.16 -apply (drule_tac [3] psi = "Fun (?u) |> ?v = ?w" in asm_rl)
   15.17 +apply (drule_tac [3] psi = "Fun (u) |> v = w" for u v w in asm_rl)
   15.18  apply (auto simp add: union_preserve_comp comp_sym_iff)
   15.19  done
   15.20  
    16.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Mar 23 19:43:03 2015 +0100
    16.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Mar 23 21:05:17 2015 +0100
    16.3 @@ -9,8 +9,10 @@
    16.4  
    16.5  signature DATATYPE_TACTICS =
    16.6  sig
    16.7 -  val induct_tac: Proof.context -> string -> int -> tactic
    16.8 -  val exhaust_tac: Proof.context -> string -> int -> tactic
    16.9 +  val exhaust_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
   16.10 +    int -> tactic
   16.11 +  val induct_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
   16.12 +    int -> tactic
   16.13    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
   16.14    val rep_datatype: Facts.ref * Token.src list -> Facts.ref * Token.src list ->
   16.15      (Facts.ref * Token.src list) list -> (Facts.ref * Token.src list) list -> theory -> theory
   16.16 @@ -88,7 +90,7 @@
   16.17        (2) exhaustion works for VARIABLES in the premises, not general terms
   16.18  **)
   16.19  
   16.20 -fun exhaust_induct_tac exh ctxt var i state = SUBGOAL (fn _ =>
   16.21 +fun exhaust_induct_tac exh ctxt var fixes i state = SUBGOAL (fn _ =>
   16.22    let
   16.23      val thy = Proof_Context.theory_of ctxt
   16.24      val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
   16.25 @@ -101,11 +103,11 @@
   16.26               [] => error "induction is not available for this datatype"
   16.27             | major::_ => FOLogic.dest_Trueprop major)
   16.28    in
   16.29 -    Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] [] rule i
   16.30 +    Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] fixes rule i
   16.31    end
   16.32    handle Find_tname msg =>
   16.33              if exh then (*try boolean case analysis instead*)
   16.34 -                case_tac ctxt var [] i
   16.35 +                case_tac ctxt var fixes i
   16.36              else error msg) i state;
   16.37  
   16.38  val exhaust_tac = exhaust_induct_tac true;
   16.39 @@ -177,12 +179,12 @@
   16.40  val _ =
   16.41    Theory.setup
   16.42      (Method.setup @{binding induct_tac}
   16.43 -      (Args.goal_spec -- Scan.lift Args.name >>
   16.44 -        (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
   16.45 +      (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
   16.46 +        (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s xs)))
   16.47        "induct_tac emulation (dynamic instantiation!)" #>
   16.48      Method.setup @{binding case_tac}
   16.49 -     (Args.goal_spec -- Scan.lift Args.name >>
   16.50 -        (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
   16.51 +     (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
   16.52 +        (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s xs)))
   16.53        "datatype case_tac emulation (dynamic instantiation!)");
   16.54  
   16.55  
    17.1 --- a/src/ZF/UNITY/AllocImpl.thy	Mon Mar 23 19:43:03 2015 +0100
    17.2 +++ b/src/ZF/UNITY/AllocImpl.thy	Mon Mar 23 21:05:17 2015 +0100
    17.3 @@ -167,8 +167,8 @@
    17.4  apply (drule_tac f = "lift (rel) " in preserves_imp_eq)
    17.5  apply assumption+
    17.6  apply (force dest: ActsD)
    17.7 -apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) \<union> Acts (G). ?P(x)" in thin_rl)
    17.8 -apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl)
    17.9 +apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) \<union> Acts (G). P(x)" for P in thin_rl)
   17.10 +apply (erule_tac V = "alloc_prog \<in> stable (u)" for u in thin_rl)
   17.11  apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable)
   17.12  apply (auto simp add: Stable_def Constrains_def constrains_def)
   17.13  apply (drule bspec, force)
   17.14 @@ -219,7 +219,7 @@
   17.15               transient({s\<in>state. k \<le> length(s`rel)} \<inter>
   17.16               {s\<in>state. succ(s`NbR) = k})"
   17.17  apply auto
   17.18 -apply (erule_tac V = "G\<notin>?u" in thin_rl)
   17.19 +apply (erule_tac V = "G\<notin>u" for u in thin_rl)
   17.20  apply (rule_tac act = alloc_rel_act in transientI)
   17.21  apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts])
   17.22  apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset])
   17.23 @@ -329,7 +329,7 @@
   17.24    {s\<in>state.  k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k}
   17.25    Ensures {s\<in>state. ~ k <length(s`ask)} \<union> {s\<in>state. length(s`giv) \<noteq> k}"
   17.26  apply (rule EnsuresI, auto)
   17.27 -apply (erule_tac [2] V = "G\<notin>?u" in thin_rl)
   17.28 +apply (erule_tac [2] V = "G\<notin>u" for u in thin_rl)
   17.29  apply (rule_tac [2] act = alloc_giv_act in transientI)
   17.30   prefer 2
   17.31   apply (simp add: alloc_prog_def [THEN def_prg_Acts])
   17.32 @@ -573,7 +573,7 @@
   17.33  apply (rule LeadsTo_weaken_R)
   17.34  apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify)
   17.35  apply (simp add: INT_iff)
   17.36 -apply (drule_tac x = "length(x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
   17.37 +apply (drule_tac x = "length(x ` giv)" and P = "%x. f (x) \<le> NbT" for f in bspec)
   17.38  apply simp
   17.39  apply (blast intro: le_trans)
   17.40  done
    18.1 --- a/src/ZF/UNITY/Comp.thy	Mon Mar 23 19:43:03 2015 +0100
    18.2 +++ b/src/ZF/UNITY/Comp.thy	Mon Mar 23 21:05:17 2015 +0100
    18.3 @@ -305,8 +305,8 @@
    18.4  (*The G case remains*)
    18.5  apply (auto dest: ActsD simp add: preserves_def stable_def constrains_def ball_conj_distrib all_conj_distrib)
    18.6  (*We have a G-action, so delete assumptions about F-actions*)
    18.7 -apply (erule_tac V = "\<forall>act \<in> Acts (F) . ?P (act)" in thin_rl)
    18.8 -apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . ?P (k,act)" in thin_rl)
    18.9 +apply (erule_tac V = "\<forall>act \<in> Acts (F). P (act)" for P in thin_rl)
   18.10 +apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . P (k,act)" for P in thin_rl)
   18.11  apply (subgoal_tac "f (x) = f (xa) ")
   18.12  apply (auto dest!: bspec)
   18.13  done
    19.1 --- a/src/ZF/UNITY/Distributor.thy	Mon Mar 23 19:43:03 2015 +0100
    19.2 +++ b/src/ZF/UNITY/Distributor.thy	Mon Mar 23 21:05:17 2015 +0100
    19.3 @@ -131,7 +131,7 @@
    19.4  apply (subgoal_tac "length (s ` iIn) \<in> nat")
    19.5  apply typecheck
    19.6  apply (subgoal_tac "m \<in> nat")
    19.7 -apply (drule_tac x = "nth(m, s`iIn) " and P = "%elt. ?X (elt) \<longrightarrow> elt<Nclients" in bspec)
    19.8 +apply (drule_tac x = "nth(m, s`iIn) " and P = "%elt. X (elt) \<longrightarrow> elt<Nclients" for X in bspec)
    19.9  apply (simp add: ltI)
   19.10  apply (simp_all add: Ord_mem_iff_lt)
   19.11  apply (blast dest: ltD)
    20.1 --- a/src/ZF/UNITY/Follows.thy	Mon Mar 23 19:43:03 2015 +0100
    20.2 +++ b/src/ZF/UNITY/Follows.thy	Mon Mar 23 21:05:17 2015 +0100
    20.3 @@ -114,14 +114,14 @@
    20.4  apply (rule single_LeadsTo_I, auto)
    20.5  apply (drule_tac x = "g (sa) " and A = B in bspec)
    20.6  apply auto
    20.7 -apply (drule_tac x = "f (sa) " and P = "%j. F \<in> ?X (j) \<longmapsto>w ?Y (j) " in bspec)
    20.8 +apply (drule_tac x = "f (sa) " and P = "%j. F \<in> X(j) \<longmapsto>w Y(j)" for X Y in bspec)
    20.9  apply auto
   20.10  apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast)
   20.11  apply auto
   20.12  apply (force simp add: part_order_def refl_def)
   20.13  apply (force simp add: part_order_def refl_def)
   20.14 -apply (drule_tac x = "f1 (x) " and x1 = "f (sa) " and P2 = "%x y. \<forall>u\<in>B. ?P (x,y,u) " in bspec [THEN bspec])
   20.15 -apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) \<longrightarrow> ?d (x,y) \<in> t" in bspec [THEN bspec])
   20.16 +apply (drule_tac x = "f1 (x)" and x1 = "f (sa) " and P2 = "%x y. \<forall>u\<in>B. P (x,y,u)" for P in bspec [THEN bspec])
   20.17 +apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. P (x,y) \<longrightarrow> d (x,y) \<in> t" for P d in bspec [THEN bspec])
   20.18  apply auto
   20.19  apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
   20.20  apply (auto simp add: part_order_def)
   20.21 @@ -135,7 +135,7 @@
   20.22    F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f(x), g1(x))> \<in> t}"
   20.23  apply (unfold mono2_def Increasing_def)
   20.24  apply (rule single_LeadsTo_I, auto)
   20.25 -apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (?X (k))" in bspec)
   20.26 +apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (X (k))" for X in bspec)
   20.27  apply auto
   20.28  apply (drule_tac x = "g (sa) " in bspec)
   20.29  apply auto
   20.30 @@ -144,7 +144,7 @@
   20.31  apply (force simp add: part_order_def refl_def)
   20.32  apply (force simp add: part_order_def refl_def)
   20.33  apply (drule_tac x = "f (x) " and x1 = "f (sa) " in bspec [THEN bspec])
   20.34 -apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) \<longrightarrow> ?d (x,y) \<in> t" in bspec [THEN bspec])
   20.35 +apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. P (x,y) \<longrightarrow> d (x,y) \<in> t" for P d in bspec [THEN bspec])
   20.36  apply auto
   20.37  apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
   20.38  apply (auto simp add: part_order_def)
    21.1 --- a/src/ZF/UNITY/GenPrefix.thy	Mon Mar 23 19:43:03 2015 +0100
    21.2 +++ b/src/ZF/UNITY/GenPrefix.thy	Mon Mar 23 21:05:17 2015 +0100
    21.3 @@ -281,9 +281,9 @@
    21.4  apply (simp_all add: nth_append length_type length_app)
    21.5  apply (rule conjI)
    21.6  apply (blast intro: gen_prefix.append)
    21.7 -apply (erule_tac V = "length (xs) < length (ys) \<longrightarrow>?u" in thin_rl)
    21.8 +apply (erule_tac V = "length (xs) < length (ys) \<longrightarrow>u" for u in thin_rl)
    21.9  apply (erule_tac a = zs in list.cases, auto)
   21.10 -apply (rule_tac P1 = "%x. <?u (x), ?v>:?w" in nat_diff_split [THEN iffD2])
   21.11 +apply (rule_tac P1 = "%x. <u(x), v>:w" for u v w in nat_diff_split [THEN iffD2])
   21.12  apply auto
   21.13  apply (simplesubst append_cons_conv)
   21.14  apply (rule_tac [2] gen_prefix.append)
   21.15 @@ -407,7 +407,7 @@
   21.16  declare same_prefix_prefix [simp]
   21.17  
   21.18  lemma same_prefix_prefix_Nil: "xs \<in> list(A) ==> <xs@ys,xs> \<in> prefix(A) \<longleftrightarrow> (<ys,[]> \<in> prefix(A))"
   21.19 -apply (rule_tac P = "%x. <?u, x>:?v \<longleftrightarrow> ?w (x) " in app_right_Nil [THEN subst])
   21.20 +apply (rule_tac P = "%x. <u, x>:v \<longleftrightarrow> w(x)" for u v w in app_right_Nil [THEN subst])
   21.21  apply (rule_tac [2] same_prefix_prefix, auto)
   21.22  done
   21.23  declare same_prefix_prefix_Nil [simp]
    22.1 --- a/src/ZF/UNITY/Increasing.thy	Mon Mar 23 19:43:03 2015 +0100
    22.2 +++ b/src/ZF/UNITY/Increasing.thy	Mon Mar 23 21:05:17 2015 +0100
    22.3 @@ -67,8 +67,8 @@
    22.4  apply (drule_tac x = "f (xb) " in bspec)
    22.5  apply (rotate_tac [2] -1)
    22.6  apply (drule_tac [2] x = act in bspec, simp_all)
    22.7 -apply (drule_tac A = "act``?u" and c = xa in subsetD, blast)
    22.8 -apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
    22.9 +apply (drule_tac A = "act``u" and c = xa for u in subsetD, blast)
   22.10 +apply (drule_tac x = "f(xa) " and x1 = "f(xb)" in bspec [THEN bspec])
   22.11  apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
   22.12  apply simp_all
   22.13  done
   22.14 @@ -137,8 +137,8 @@
   22.15  apply clarify
   22.16  apply (rotate_tac -2)
   22.17  apply (drule_tac x = act in bspec)
   22.18 -apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, simp_all, blast)
   22.19 -apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
   22.20 +apply (drule_tac [2] A = "act``u" and c = xa for u in subsetD, simp_all, blast)
   22.21 +apply (drule_tac x = "f(xa)" and x1 = "f(xb)" in bspec [THEN bspec])
   22.22  apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
   22.23  apply simp_all
   22.24  done
   22.25 @@ -181,8 +181,8 @@
   22.26  apply (drule_tac x = act in bspec)
   22.27  apply (rotate_tac [2] -3)
   22.28  apply (drule_tac [2] x = act in bspec, simp_all)
   22.29 -apply (drule_tac A = "act``?u" and c = xa in subsetD)
   22.30 -apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, blast, blast)
   22.31 +apply (drule_tac A = "act``u" and c = xa for u in subsetD)
   22.32 +apply (drule_tac [2] A = "act``u" and c = xa for u in subsetD, blast, blast)
   22.33  apply (rotate_tac -4)
   22.34  apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
   22.35  apply (rotate_tac [3] -1)
   22.36 @@ -213,8 +213,8 @@
   22.37  apply (drule_tac x = act in bspec)
   22.38  apply (rotate_tac [2] -3)
   22.39  apply (drule_tac [2] x = act in bspec, simp_all)
   22.40 -apply (drule_tac A = "act``?u" and c = x in subsetD)
   22.41 -apply (drule_tac [2] A = "act``?u" and c = x in subsetD, blast, blast)
   22.42 +apply (drule_tac A = "act``u" and c = x for u in subsetD)
   22.43 +apply (drule_tac [2] A = "act``u" and c = x for u in subsetD, blast, blast)
   22.44  apply (rotate_tac -9)
   22.45  apply (drule_tac x = "f (x) " and x1 = "f (xa) " in bspec [THEN bspec])
   22.46  apply (rotate_tac [3] -1)
    23.1 --- a/src/ZF/UNITY/Merge.thy	Mon Mar 23 19:43:03 2015 +0100
    23.2 +++ b/src/ZF/UNITY/Merge.thy	Mon Mar 23 21:05:17 2015 +0100
    23.3 @@ -166,7 +166,7 @@
    23.4  apply (subgoal_tac "xa \<in> nat")
    23.5  apply (simp_all add: Ord_mem_iff_lt)
    23.6  prefer 2 apply (blast intro: lt_trans)
    23.7 -apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. ?X (elt) \<longrightarrow> elt<Nclients" in bspec)
    23.8 +apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. X (elt) \<longrightarrow> elt<Nclients" for X in bspec)
    23.9  apply (simp add: ltI nat_into_Ord)
   23.10  apply (blast dest: ltD)
   23.11  done
    24.1 --- a/src/ZF/UNITY/WFair.thy	Mon Mar 23 19:43:03 2015 +0100
    24.2 +++ b/src/ZF/UNITY/WFair.thy	Mon Mar 23 21:05:17 2015 +0100
    24.3 @@ -517,7 +517,7 @@
    24.4  apply (unfold field_def)
    24.5  apply (simp add: measure_def)
    24.6  apply (rule equalityI, force, clarify)
    24.7 -apply (erule_tac V = "x\<notin>range (?y) " in thin_rl)
    24.8 +apply (erule_tac V = "x\<notin>range (y)" for y in thin_rl)
    24.9  apply (erule nat_induct)
   24.10  apply (rule_tac [2] b = "succ (succ (xa))" in domainI)
   24.11  apply (rule_tac b = "succ (0) " in domainI)
    25.1 --- a/src/ZF/WF.thy	Mon Mar 23 19:43:03 2015 +0100
    25.2 +++ b/src/ZF/WF.thy	Mon Mar 23 21:05:17 2015 +0100
    25.3 @@ -230,7 +230,7 @@
    25.4      "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
    25.5  apply (unfold is_recfun_def)
    25.6    txt{*replace f only on the left-hand side*}
    25.7 -apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
    25.8 +apply (erule_tac P = "%x. t(x) = u" for t u in ssubst)
    25.9  apply (simp add: underI)
   25.10  done
   25.11  
   25.12 @@ -244,7 +244,7 @@
   25.13  apply (intro impI)
   25.14  apply (elim ssubst)
   25.15  apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
   25.16 -apply (rule_tac t = "%z. H (?x,z) " in subst_context)
   25.17 +apply (rule_tac t = "%z. H (x, z)" for x in subst_context)
   25.18  apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f \<longleftrightarrow> <y,z>:g")
   25.19   apply (blast dest: transD)
   25.20  apply (simp add: apply_iff)
   25.21 @@ -291,7 +291,7 @@
   25.22  apply (rule lam_cong [OF refl])
   25.23  apply (drule underD)
   25.24  apply (fold is_recfun_def)
   25.25 -apply (rule_tac t = "%z. H(?x,z)" in subst_context)
   25.26 +apply (rule_tac t = "%z. H(x, z)" for x in subst_context)
   25.27  apply (rule fun_extension)
   25.28    apply (blast intro: is_recfun_type)
   25.29   apply (rule lam_type [THEN restrict_type2])
    26.1 --- a/src/ZF/Zorn.thy	Mon Mar 23 19:43:03 2015 +0100
    26.2 +++ b/src/ZF/Zorn.thy	Mon Mar 23 21:05:17 2015 +0100
    26.3 @@ -469,7 +469,7 @@
    26.4        apply (erule lamE) apply simp
    26.5        apply assumption
    26.6  
    26.7 -      apply (thin_tac "C \<subseteq> ?X")
    26.8 +      apply (thin_tac "C \<subseteq> X" for X)
    26.9        apply (fast elim: lamE)
   26.10        done
   26.11      have "?A \<in> Chain(r)"
    27.1 --- a/src/ZF/ex/Limit.thy	Mon Mar 23 19:43:03 2015 +0100
    27.2 +++ b/src/ZF/ex/Limit.thy	Mon Mar 23 21:05:17 2015 +0100
    27.3 @@ -1833,8 +1833,8 @@
    27.4  apply (rename_tac [5] y)
    27.5  apply (rule_tac [5] P =
    27.6           "%z. rel(DD`succ(y),
    27.7 -                  (ee`y O Rp(?DD(y)`y,?DD(y)`succ(y),?ee(y)`y)) ` (x`succ(y)),
    27.8 -                  z)"
    27.9 +                  (ee`y O Rp(DD'(y)`y,DD'(y)`succ(y),ee'(y)`y)) ` (x`succ(y)),
   27.10 +                  z)" for DD' ee'
   27.11         in id_conv [THEN subst])
   27.12  apply (rule_tac [6] rel_cf)
   27.13  (* Dinf and cont_fun doesn't go well together, both Pi(_,%x._). *)
    28.1 --- a/src/ZF/ex/Primes.thy	Mon Mar 23 19:43:03 2015 +0100
    28.2 +++ b/src/ZF/ex/Primes.thy	Mon Mar 23 21:05:17 2015 +0100
    28.3 @@ -93,7 +93,7 @@
    28.4  lemma gcd_non_0_raw: 
    28.5      "[| 0<n;  n \<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)"
    28.6  apply (simp add: gcd_def)
    28.7 -apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst])
    28.8 +apply (rule_tac P = "%z. left (z) = right" for left right in transrec [THEN ssubst])
    28.9  apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym] 
   28.10                   mod_less_divisor [THEN ltD])
   28.11  done