prefer local fixes;
authorwenzelm
Wed Mar 25 10:44:57 2015 +0100 (2015-03-25)
changeset 5980722bc39064290
parent 59806 d3d4ec6c21ef
child 59808 3b6ad54b04fc
prefer local fixes;
src/CCL/ex/Stream.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Auth/KerberosIV_Gets.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxExample.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/State.thy
src/HOL/Bali/WellType.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/HOLCF/IOA/meta_theory/Automata.thy
src/HOL/Hoare_Parallel/Graph.thy
src/HOL/Hoare_Parallel/OG_Hoare.thy
src/HOL/Hoare_Parallel/RG_Hoare.thy
src/HOL/Hoare_Parallel/RG_Tran.thy
src/HOL/IMPP/EvenOdd.thy
src/HOL/IMPP/Hoare.thy
src/HOL/IMPP/Natural.thy
src/HOL/Induct/Com.thy
src/HOL/Library/Multiset.thy
src/HOL/MicroJava/DFA/Listn.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/Nominal/Examples/Standardization.thy
src/HOL/SET_Protocol/Cardholder_Registration.thy
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/Project.thy
src/HOL/UNITY/Transformers.thy
src/HOL/Wellfounded.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Misc_Typedef.thy
src/HOL/Word/Word.thy
     1.1 --- a/src/CCL/ex/Stream.thy	Wed Mar 25 10:41:53 2015 +0100
     1.2 +++ b/src/CCL/ex/Stream.thy	Wed Mar 25 10:44:57 2015 +0100
     1.3 @@ -120,7 +120,7 @@
     1.4  lemma iter2Blemma:
     1.5    "n:Nat \<Longrightarrow>  
     1.6      map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))"
     1.7 -  apply (rule_tac P = "\<lambda>x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst])
     1.8 +  apply (rule_tac P = "\<lambda>x. lhs(x) = rhs" for lhs rhs in iter2B [THEN ssubst])
     1.9    apply (simp add: nmapBcons)
    1.10    done
    1.11  
     2.1 --- a/src/HOL/Algebra/Sylow.thy	Wed Mar 25 10:41:53 2015 +0100
     2.2 +++ b/src/HOL/Algebra/Sylow.thy	Wed Mar 25 10:44:57 2015 +0100
     2.3 @@ -182,7 +182,7 @@
     2.4  apply (erule H_into_carrier_G)
     2.5  apply (rule H_not_empty)
     2.6  apply (simp add: H_def, clarify)
     2.7 -apply (erule_tac P = "%z. ?lhs(z) = M1" in subst)
     2.8 +apply (erule_tac P = "%z. lhs(z) = M1" for lhs in subst)
     2.9  apply (simp add: coset_mult_assoc )
    2.10  apply (blast intro: H_m_closed)
    2.11  done
     3.1 --- a/src/HOL/Auth/KerberosIV_Gets.thy	Wed Mar 25 10:41:53 2015 +0100
     3.2 +++ b/src/HOL/Auth/KerberosIV_Gets.thy	Wed Mar 25 10:44:57 2015 +0100
     3.3 @@ -1238,11 +1238,12 @@
     3.4  txt{*K5. Not clear how this step could be integrated with the main
     3.5         simplification step. Done in KerberosV.thy*}
     3.6  apply clarify
     3.7 -apply (erule_tac V = "Says Aa Tgs ?X \<in> set ?evs" in thin_rl)
     3.8 +apply (erule_tac V = "Says Aa Tgs X \<in> set evs" for X evs in thin_rl)
     3.9  apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN servK_notin_authKeysD])
    3.10  apply (assumption, assumption, blast, assumption)
    3.11  apply (simp add: analz_insert_freshK2)
    3.12 -by (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
    3.13 +apply (blast dest: Key_unique_SesKey intro: less_SucI)
    3.14 +done
    3.15  
    3.16  
    3.17  text{* In the real world Tgs can't check wheter authK is secure! *}
     4.1 --- a/src/HOL/Auth/Yahalom.thy	Wed Mar 25 10:41:53 2015 +0100
     4.2 +++ b/src/HOL/Auth/Yahalom.thy	Wed Mar 25 10:44:57 2015 +0100
     4.3 @@ -403,7 +403,7 @@
     4.4  txt{*YM3*}
     4.5  apply blast
     4.6  txt{*YM4*}
     4.7 -apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
     4.8 +apply (erule_tac V = "\<forall>KK. P KK" for P in thin_rl, clarify)
     4.9  txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore
    4.10    @{prop "NBa \<noteq> NB"}.  Previous two steps make the next step
    4.11    faster.*}
     5.1 --- a/src/HOL/Bali/AxCompl.thy	Wed Mar 25 10:41:53 2015 +0100
     5.2 +++ b/src/HOL/Bali/AxCompl.thy	Wed Mar 25 10:44:57 2015 +0100
     5.3 @@ -71,7 +71,7 @@
     5.4  apply (subgoal_tac 
     5.5          "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
     5.6  apply  clarsimp
     5.7 -apply  (erule_tac V="nyinitcls G (x, s) = ?rhs" in thin_rl)
     5.8 +apply  (erule_tac V="nyinitcls G (x, s) = rhs" for rhs in thin_rl)
     5.9  apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
    5.10  apply   (auto dest!: not_initedD elim!: 
    5.11                simp add: nyinitcls_def inited_def split add: split_if_asm)
     6.1 --- a/src/HOL/Bali/AxExample.thy	Wed Mar 25 10:41:53 2015 +0100
     6.2 +++ b/src/HOL/Bali/AxExample.thy	Wed Mar 25 10:44:57 2015 +0100
     6.3 @@ -71,13 +71,13 @@
     6.4  apply   (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
     6.5  prefer 2
     6.6  apply    clarsimp
     6.7 -apply   (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2)
     6.8 +apply   (rule_tac Q' = "(\<lambda>Y s Z. Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" and Q = Q for Q in conseq2)
     6.9  prefer 2
    6.10  apply    simp
    6.11  apply   (tactic "ax_tac @{context} 1" (* While *))
    6.12  prefer 2
    6.13  apply    (rule ax_impossible [THEN conseq1], clarsimp)
    6.14 -apply   (rule_tac P' = "Normal ?P" in conseq1)
    6.15 +apply   (rule_tac P' = "Normal P" and P = P for P in conseq1)
    6.16  prefer 2
    6.17  apply    clarsimp
    6.18  apply   (tactic "ax_tac @{context} 1")
    6.19 @@ -106,7 +106,7 @@
    6.20  apply     (unfold DynT_prop_def)
    6.21  apply     (simp (no_asm))
    6.22  apply    (intro strip)
    6.23 -apply    (rule_tac P' = "Normal ?P" in conseq1)
    6.24 +apply    (rule_tac P' = "Normal P" and P = P for P in conseq1)
    6.25  apply     (tactic "ax_tac @{context} 1" (* Methd *))
    6.26  apply     (rule ax_thin [OF _ empty_subsetI])
    6.27  apply     (simp (no_asm) add: body_def2)
    6.28 @@ -185,7 +185,7 @@
    6.29  apply     (simp (no_asm))
    6.30  apply    (unfold arr_viewed_from_def)
    6.31  apply    (rule allI)
    6.32 -apply    (rule_tac P' = "Normal ?P" in conseq1)
    6.33 +apply    (rule_tac P' = "Normal P" and P = P for P in conseq1)
    6.34  apply     (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
    6.35  apply     (tactic "ax_tac @{context} 1")
    6.36  apply     (tactic "ax_tac @{context} 1")
    6.37 @@ -268,7 +268,7 @@
    6.38  apply   (rule ax_subst_Var_allI)
    6.39  apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" [] *})
    6.40  apply   (rule allI)
    6.41 -apply   (rule_tac P' = "Normal ?P" in conseq1)
    6.42 +apply   (rule_tac P' = "Normal P" and P = P for P in conseq1)
    6.43  prefer 2
    6.44  apply    clarsimp
    6.45  apply   (tactic "ax_tac @{context} 1")
     7.1 --- a/src/HOL/Bali/AxSem.thy	Wed Mar 25 10:41:53 2015 +0100
     7.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Mar 25 10:44:57 2015 +0100
     7.3 @@ -1055,7 +1055,7 @@
     7.4  apply  safe
     7.5  apply  (erule spec)
     7.6  apply (rule ax_escape, clarsimp)
     7.7 -apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)
     7.8 +apply (erule_tac V = "P \<longrightarrow> Q" for P Q in thin_rl)
     7.9  apply (drule spec,drule spec,drule spec, erule conseq12)
    7.10  apply (force simp add: init_lvars_def Let_def)
    7.11  done
     8.1 --- a/src/HOL/Bali/Example.thy	Wed Mar 25 10:41:53 2015 +0100
     8.2 +++ b/src/HOL/Bali/Example.thy	Wed Mar 25 10:44:57 2015 +0100
     8.3 @@ -1259,18 +1259,18 @@
     8.4  apply (simp (no_asm_use))
     8.5  apply (drule (1) alloc_one,clarsimp)
     8.6  apply (rule eval_Is (* ;; *))
     8.7 -apply  (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
     8.8 -apply  (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
     8.9 -apply  (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
    8.10 +apply  (erule_tac V = "the (new_Addr _) = c" in thin_rl)
    8.11 +apply  (erule_tac [2] V = "new_Addr _ = Some a" in thin_rl)
    8.12 +apply  (erule_tac [2] V = "atleast_free _ four" in thin_rl)
    8.13  apply  (rule eval_Is (* Expr *))
    8.14  apply  (rule eval_Is (* Ass *))
    8.15  apply   (rule eval_Is (* LVar *))
    8.16  apply  (rule eval_Is (* NewC *))
    8.17        (* begin init Ext *)
    8.18 -apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
    8.19 -apply   (erule_tac V = "atleast_free ?h three" in thin_rl)
    8.20 -apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
    8.21 -apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
    8.22 +apply   (erule_tac V = "the (new_Addr _) = b" in thin_rl)
    8.23 +apply   (erule_tac V = "atleast_free _ three" in thin_rl)
    8.24 +apply   (erule_tac [2] V = "atleast_free _ four" in thin_rl)
    8.25 +apply   (erule_tac [2] V = "new_Addr _ = Some a" in thin_rl)
    8.26  apply   (rule eval_Is (* Init Ext *))
    8.27  apply   (simp)
    8.28  apply   (rule conjI)
    8.29 @@ -1309,7 +1309,7 @@
    8.30  apply (drule alloc_one)
    8.31  apply  (simp (no_asm_simp))
    8.32  apply clarsimp
    8.33 -apply (erule_tac V = "atleast_free ?h three" in thin_rl)
    8.34 +apply (erule_tac V = "atleast_free _ three" in thin_rl)
    8.35  apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
    8.36  apply (simp (no_asm_use))
    8.37  apply (rule eval_Is (* Try *))
    8.38 @@ -1361,7 +1361,7 @@
    8.39  apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
    8.40  apply (drule alloc_one [THEN conjunct1])
    8.41  apply  (simp (no_asm_simp))
    8.42 -apply (erule_tac V = "atleast_free ?h two" in thin_rl)
    8.43 +apply (erule_tac V = "atleast_free _ two" in thin_rl)
    8.44  apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
    8.45  apply simp
    8.46  apply (rule eval_Is (* While *))
     9.1 --- a/src/HOL/Bali/State.thy	Wed Mar 25 10:41:53 2015 +0100
     9.2 +++ b/src/HOL/Bali/State.thy	Wed Mar 25 10:44:57 2015 +0100
     9.3 @@ -599,13 +599,13 @@
     9.4    where "store == snd"
     9.5  
     9.6  lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False"
     9.7 -apply (erule_tac x = "(Some k,y)" in all_dupE)
     9.8 -apply (erule_tac x = "(None,y)" in allE)
     9.9 +apply (erule_tac x = "(Some k,y)" for k y in all_dupE)
    9.10 +apply (erule_tac x = "(None,y)" for y in allE)
    9.11  apply clarify
    9.12  done
    9.13  
    9.14  lemma state_not_single: "All (op = (x::state)) \<Longrightarrow> R"
    9.15 -apply (drule_tac x = "(if abrupt x = None then Some ?x else None,?y)" in spec)
    9.16 +apply (drule_tac x = "(if abrupt x = None then Some x' else None, y)" for x' y in spec)
    9.17  apply clarsimp
    9.18  done
    9.19  
    9.20 @@ -823,4 +823,3 @@
    9.21  
    9.22  
    9.23  end
    9.24 -
    10.1 --- a/src/HOL/Bali/WellType.thy	Wed Mar 25 10:41:53 2015 +0100
    10.2 +++ b/src/HOL/Bali/WellType.thy	Wed Mar 25 10:44:57 2015 +0100
    10.3 @@ -660,14 +660,14 @@
    10.4  (* 17 subgoals *)
    10.5  apply (tactic {* ALLGOALS (fn i =>
    10.6    if i = 11 then EVERY'
    10.7 -   [Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean" [],
    10.8 -    Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1" [],
    10.9 -    Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2" []] i
   10.10 -  else Rule_Insts.thin_tac @{context} "All ?P" [] i) *})
   10.11 +   [Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e0\<Colon>-PrimT Boolean" [(@{binding E}, NONE, NoSyn)],
   10.12 +    Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e1\<Colon>-T1" [(@{binding E}, NONE, NoSyn), (@{binding T1}, NONE, NoSyn)],
   10.13 +    Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e2\<Colon>-T2" [(@{binding E}, NONE, NoSyn), (@{binding T2}, NONE, NoSyn)]] i
   10.14 +  else Rule_Insts.thin_tac @{context} "All P" [(@{binding P}, NONE, NoSyn)] i) *})
   10.15  (*apply (safe del: disjE elim!: wt_elim_cases)*)
   10.16  apply (tactic {*ALLGOALS (eresolve_tac @{context} @{thms wt_elim_cases})*})
   10.17  apply (simp_all (no_asm_use) split del: split_if_asm)
   10.18 -apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
   10.19 +apply (erule_tac [12] V = "All P" for P in thin_rl) (* Call *)
   10.20  apply (blast del: equalityCE dest: sym [THEN trans])+
   10.21  done
   10.22  
    11.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Mar 25 10:41:53 2015 +0100
    11.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Mar 25 10:44:57 2015 +0100
    11.3 @@ -787,7 +787,7 @@
    11.4    apply (auto simp add: divides_def simp del: pmult_Cons)
    11.5    apply (rule_tac x = qb in exI)
    11.6    apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa)) =
    11.7 -    poly (pmult (pexp [uminus a, one] (?order a p)) (pmult [uminus a, one] qb))")
    11.8 +    poly (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb))")
    11.9    apply (drule poly_mult_left_cancel [THEN iffD1], force)
   11.10    apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a q))
   11.11        (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa))) =
    12.1 --- a/src/HOL/Divides.thy	Wed Mar 25 10:41:53 2015 +0100
    12.2 +++ b/src/HOL/Divides.thy	Wed Mar 25 10:44:57 2015 +0100
    12.3 @@ -1195,7 +1195,7 @@
    12.4  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
    12.5    apply (cut_tac m = q and n = c in mod_less_divisor)
    12.6    apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
    12.7 -  apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
    12.8 +  apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
    12.9    apply (simp add: add_mult_distrib2)
   12.10    done
   12.11  
   12.12 @@ -2408,7 +2408,7 @@
   12.13   "0<k ==> 
   12.14      P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
   12.15  apply (rule iffI, clarify)
   12.16 - apply (erule_tac P="P ?x ?y" in rev_mp)  
   12.17 + apply (erule_tac P="P x y" for x y in rev_mp)  
   12.18   apply (subst mod_add_eq) 
   12.19   apply (subst zdiv_zadd1_eq) 
   12.20   apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)  
   12.21 @@ -2421,7 +2421,7 @@
   12.22   "k<0 ==>
   12.23      P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
   12.24  apply (rule iffI, clarify)
   12.25 - apply (erule_tac P="P ?x ?y" in rev_mp)  
   12.26 + apply (erule_tac P="P x y" for x y in rev_mp)  
   12.27   apply (subst mod_add_eq) 
   12.28   apply (subst zdiv_zadd1_eq) 
   12.29   apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)  
    13.1 --- a/src/HOL/GCD.thy	Wed Mar 25 10:41:53 2015 +0100
    13.2 +++ b/src/HOL/GCD.thy	Wed Mar 25 10:44:57 2015 +0100
    13.3 @@ -626,11 +626,11 @@
    13.4    apply (erule subst)
    13.5    apply (rule iffI)
    13.6    apply force
    13.7 -  apply (drule_tac x = "abs ?e" in exI)
    13.8 -  apply (case_tac "(?e::int) >= 0")
    13.9 +  apply (drule_tac x = "abs e" for e in exI)
   13.10 +  apply (case_tac "e >= 0" for e :: int)
   13.11    apply force
   13.12    apply force
   13.13 -done
   13.14 +  done
   13.15  
   13.16  lemma gcd_coprime_nat:
   13.17    assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
    14.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Wed Mar 25 10:41:53 2015 +0100
    14.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Wed Mar 25 10:44:57 2015 +0100
    14.3 @@ -654,7 +654,7 @@
    14.4  apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def
    14.5    asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def)
    14.6  apply auto
    14.7 -apply (drule_tac [!] s = "Some ?x" in sym)
    14.8 +apply (drule_tac [!] s = "Some _" in sym)
    14.9  apply auto
   14.10  done
   14.11  
    15.1 --- a/src/HOL/Hoare_Parallel/Graph.thy	Wed Mar 25 10:41:53 2015 +0100
    15.2 +++ b/src/HOL/Hoare_Parallel/Graph.thy	Wed Mar 25 10:44:57 2015 +0100
    15.3 @@ -287,10 +287,10 @@
    15.4   apply(case_tac "length path")
    15.5    apply force
    15.6   apply simp
    15.7 - apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE)
    15.8 + apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> P i" and x = "nat" for P in allE)
    15.9   apply simp
   15.10   apply clarify
   15.11 - apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
   15.12 + apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> P i" and x = "nat" for P in allE)
   15.13   apply simp
   15.14   apply(case_tac "j<I")
   15.15    apply(erule_tac x = "j" in allE)
   15.16 @@ -329,10 +329,10 @@
   15.17   apply(case_tac "length path")
   15.18    apply force
   15.19   apply simp
   15.20 - apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE)
   15.21 + apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> P i" and x = "nat" for P in allE)
   15.22   apply simp
   15.23   apply clarify
   15.24 - apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
   15.25 + apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> P i" and x = "nat" for P in allE)
   15.26   apply simp
   15.27   apply(case_tac "j\<le>R")
   15.28    apply(drule le_imp_less_or_eq [of _ R])
    16.1 --- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Mar 25 10:41:53 2015 +0100
    16.2 +++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Mar 25 10:44:57 2015 +0100
    16.3 @@ -441,7 +441,7 @@
    16.4          apply simp
    16.5         apply force
    16.6        apply simp
    16.7 -      apply(erule_tac V = "\<forall>i. ?P i" in thin_rl)
    16.8 +      apply(erule_tac V = "\<forall>i. P i" for P in thin_rl)
    16.9        apply(drule_tac s = "length Rs" in sym)
   16.10        apply(erule allE, erule impE, assumption)
   16.11        apply(force dest: nth_mem simp add: All_None_def)
    17.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Mar 25 10:41:53 2015 +0100
    17.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Mar 25 10:44:57 2015 +0100
    17.3 @@ -186,7 +186,7 @@
    17.4    apply force
    17.5   apply clarify
    17.6   apply(erule_tac x="Suc ia" in allE,simp)
    17.7 -apply(erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (?J j) \<notin> ctran" in allE,simp)
    17.8 +apply(erule_tac x="0" and P="\<lambda>j. H j \<longrightarrow> (J j) \<notin> ctran" for H J in allE,simp)
    17.9  done
   17.10  
   17.11  lemma etran_or_ctran2 [rule_format]:
   17.12 @@ -241,14 +241,14 @@
   17.13   apply(case_tac k,simp,simp)
   17.14   apply(case_tac j,simp)
   17.15    apply(erule_tac x=0 in allE)
   17.16 -  apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (?J j)" in allE,simp)
   17.17 +  apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (J j)" for J in allE,simp)
   17.18    apply(subgoal_tac "t\<in>p")
   17.19     apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((P, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((P, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
   17.20      apply clarify
   17.21 -    apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
   17.22 +    apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
   17.23     apply clarify
   17.24 -   apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
   17.25 -  apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran \<longrightarrow> ?T j" in allE,simp)
   17.26 +   apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j) \<longrightarrow> (T j)\<in>rely" for H J T in allE,simp)
   17.27 +  apply(erule_tac x=0 and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran \<longrightarrow> T j" for H J T in allE,simp)
   17.28    apply(simp(no_asm_use) only:stable_def)
   17.29    apply(erule_tac x=s in allE)
   17.30    apply(erule_tac x=t in allE)
   17.31 @@ -258,23 +258,23 @@
   17.32    apply(rule Env)
   17.33   apply simp
   17.34   apply(erule_tac x="nata" in allE)
   17.35 - apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
   17.36 + apply(erule_tac x="nat" and P="\<lambda>j. (s\<le>j) \<longrightarrow> (J j)" for s J in allE,simp)
   17.37   apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((P, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((P, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
   17.38    apply clarify
   17.39 -  apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
   17.40 +  apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
   17.41   apply clarify
   17.42 - apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
   17.43 + apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j) \<longrightarrow> (T j)\<in>rely" for H J T in allE,simp)
   17.44  apply(case_tac k,simp,simp)
   17.45  apply(case_tac j)
   17.46 - apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
   17.47 + apply(erule_tac x=0 and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
   17.48   apply(erule etran.cases,simp)
   17.49  apply(erule_tac x="nata" in allE)
   17.50 -apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
   17.51 +apply(erule_tac x="nat" and P="\<lambda>j. (s\<le>j) \<longrightarrow> (J j)" for s J in allE,simp)
   17.52  apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((Q, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((Q, t) # xs) ! i), snd (xs ! i)) \<in> rely)")
   17.53   apply clarify
   17.54 - apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
   17.55 + apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
   17.56  apply clarify
   17.57 -apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
   17.58 +apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j) \<longrightarrow> (T j)\<in>rely" for H J T in allE,simp)
   17.59  done
   17.60  
   17.61  subsection \<open>Soundness of the System for Component Programs\<close>
   17.62 @@ -341,7 +341,7 @@
   17.63   apply(case_tac "x!i")
   17.64   apply clarify
   17.65   apply(drule_tac s="Some (Basic f)" in sym,simp)
   17.66 - apply(thin_tac "\<forall>j. ?H j")
   17.67 + apply(thin_tac "\<forall>j. H j" for H)
   17.68   apply(force elim:ctran.cases)
   17.69  apply clarify
   17.70  apply(simp add:cp_def)
   17.71 @@ -468,7 +468,7 @@
   17.72   apply(drule_tac c=l in subsetD)
   17.73    apply (simp add:cp_def)
   17.74    apply clarify
   17.75 -  apply(erule_tac x=ia and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
   17.76 +  apply(erule_tac x=ia and P="\<lambda>i. H i \<longrightarrow> (J i, I i)\<in>ctran" for H J I in allE,simp)
   17.77    apply(erule etranE,simp)
   17.78   apply simp
   17.79  apply clarify
   17.80 @@ -499,7 +499,7 @@
   17.81  apply(drule_tac c=l in subsetD)
   17.82   apply (simp add:cp_def)
   17.83   apply clarify
   17.84 - apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
   17.85 + apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> (J i, I i)\<in>ctran" for H J I in allE,simp)
   17.86   apply(erule etranE,simp)
   17.87  apply simp
   17.88  apply clarify
   17.89 @@ -532,7 +532,7 @@
   17.90    apply(erule_tac m="length x" in etran_or_ctran,simp+)
   17.91   apply(case_tac x, (simp add:last_length)+)
   17.92  apply(erule exE)
   17.93 -apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
   17.94 +apply(drule_tac n=i and P="\<lambda>i. H i \<and> (J i, I i) \<in> ctran" for H J I in Ex_first_occurrence)
   17.95  apply clarify
   17.96  apply (simp add:assum_def)
   17.97  apply(frule_tac j=0 and k="m" and p=pre in stability,simp+)
   17.98 @@ -549,7 +549,7 @@
   17.99    apply(erule disjE)
  17.100     apply(erule_tac x=i in allE, erule impE, assumption)
  17.101     apply simp+
  17.102 - apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
  17.103 + apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> (I j)\<in>guar" for H J I in allE)
  17.104   apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
  17.105    apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
  17.106     apply(rotate_tac -2)
  17.107 @@ -569,7 +569,7 @@
  17.108    apply(erule_tac x=i in allE, erule impE, assumption)
  17.109    apply simp
  17.110   apply simp
  17.111 -apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
  17.112 +apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> (I j)\<in>guar" for H J I in allE)
  17.113  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
  17.114   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
  17.115    apply(rotate_tac -2)
  17.116 @@ -713,14 +713,14 @@
  17.117   apply(drule_tac c=xs in subsetD,simp add:cp_def cptn_iff_cptn_mod)
  17.118    apply(simp add:assum_def)
  17.119    apply clarify
  17.120 -  apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
  17.121 +  apply(erule_tac P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> I j" for H J I in allE,erule impE, assumption)
  17.122    apply(simp add:snd_lift)
  17.123    apply(erule mp)
  17.124    apply(force elim:etranE intro:Env simp add:lift_def)
  17.125   apply(simp add:comm_def)
  17.126   apply(rule conjI)
  17.127    apply clarify
  17.128 -  apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
  17.129 +  apply(erule_tac P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> I j" for H J I in allE,erule impE, assumption)
  17.130    apply(simp add:snd_lift)
  17.131    apply(erule mp)
  17.132    apply(case_tac "(xs!i)")
  17.133 @@ -914,7 +914,7 @@
  17.134  apply clarify
  17.135  apply (simp add:last_length)
  17.136  --\<open>WhileOne\<close>
  17.137 -apply(thin_tac "P = While b P \<longrightarrow> ?Q")
  17.138 +apply(thin_tac "P = While b P \<longrightarrow> Q" for Q)
  17.139  apply(rule ctran_in_comm,simp)
  17.140  apply(simp add:Cons_lift del:list.map)
  17.141  apply(simp add:comm_def del:list.map)
  17.142 @@ -957,7 +957,7 @@
  17.143   apply(simp only:last_lift_not_None)
  17.144  apply simp
  17.145  --\<open>WhileMore\<close>
  17.146 -apply(thin_tac "P = While b P \<longrightarrow> ?Q")
  17.147 +apply(thin_tac "P = While b P \<longrightarrow> Q" for Q)
  17.148  apply(rule ctran_in_comm,simp del:last.simps)
  17.149  --\<open>metiendo la hipotesis antes de dividir la conclusion.\<close>
  17.150  apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \<in> assum (pre, rely)")
  17.151 @@ -979,7 +979,7 @@
  17.152      apply simp
  17.153     apply simp
  17.154    apply(simp add:snd_lift del:list.map last.simps)
  17.155 -  apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> ?P i")
  17.156 +  apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> P i" for P)
  17.157    apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
  17.158    apply(erule_tac x=sa in allE)
  17.159    apply(drule_tac c="(Some P, sa) # xs" in subsetD)
  17.160 @@ -1111,13 +1111,13 @@
  17.161  apply simp
  17.162  apply(erule exE)
  17.163  --\<open>the first c-tran that does not satisfy the guarantee-condition is from @{text "\<sigma>_i"} at step @{text "m"}.\<close>
  17.164 -apply(drule_tac n=j and P="\<lambda>j. \<exists>i. ?H i j" in Ex_first_occurrence)
  17.165 +apply(drule_tac n=j and P="\<lambda>j. \<exists>i. H i j" for H in Ex_first_occurrence)
  17.166  apply(erule exE)
  17.167  apply clarify
  17.168  --\<open>@{text "\<sigma>_i \<in> A(pre, rely_1)"}\<close>
  17.169  apply(subgoal_tac "take (Suc (Suc m)) (clist!i) \<in> assum(Pre(xs!i), Rely(xs!i))")
  17.170  --\<open>but this contradicts @{text "\<Turnstile> \<sigma>_i sat [pre_i,rely_i,guar_i,post_i]"}\<close>
  17.171 - apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> \<Turnstile> (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption)
  17.172 + apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
  17.173   apply(simp add:com_validity_def)
  17.174   apply(erule_tac x=s in allE)
  17.175   apply(simp add:cp_def comm_def)
  17.176 @@ -1126,40 +1126,40 @@
  17.177    apply (blast intro: takecptn_is_cptn)
  17.178   apply simp
  17.179   apply clarify
  17.180 - apply(erule_tac x=m and P="\<lambda>j. ?I j \<and> ?J j \<longrightarrow> ?H j" in allE)
  17.181 + apply(erule_tac x=m and P="\<lambda>j. I j \<and> J j \<longrightarrow> H j" for I J H in allE)
  17.182   apply (simp add:conjoin_def same_length_def)
  17.183  apply(simp add:assum_def)
  17.184  apply(rule conjI)
  17.185 - apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow>  ?I j \<in>cp (?K j) (?J j)" in allE)
  17.186 + apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> I j \<in>cp (K j) (J j)" for H I K J in allE)
  17.187   apply(simp add:cp_def par_assum_def)
  17.188   apply(drule_tac c="s" in subsetD,simp)
  17.189   apply simp
  17.190  apply clarify
  17.191 -apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?M \<union> UNION (?S j) (?T j) \<subseteq>  (?L j)" in allE)
  17.192 +apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> M \<union> UNION (S j) (T j) \<subseteq> (L j)" for H M S T L in allE)
  17.193  apply simp
  17.194  apply(erule subsetD)
  17.195  apply simp
  17.196  apply(simp add:conjoin_def compat_label_def)
  17.197  apply clarify
  17.198 -apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?P j) \<or> ?Q j" in allE,simp)
  17.199 +apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (P j) \<or> Q j" for H P Q in allE,simp)
  17.200  --\<open>each etran in @{text "\<sigma>_1[0\<dots>m]"} corresponds to\<close>
  17.201  apply(erule disjE)
  17.202  --\<open>a c-tran in some @{text "\<sigma>_{ib}"}\<close>
  17.203   apply clarify
  17.204   apply(case_tac "i=ib",simp)
  17.205    apply(erule etranE,simp)
  17.206 - apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE)
  17.207 + apply(erule_tac x="ib" and P="\<lambda>i. H i \<longrightarrow> (I i) \<or> (J i)" for H I J in allE)
  17.208   apply (erule etranE)
  17.209   apply(case_tac "ia=m",simp)
  17.210   apply simp
  17.211 - apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE)
  17.212 + apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (\<forall>i. P i j)" for H P in allE)
  17.213   apply(subgoal_tac "ia<m",simp)
  17.214    prefer 2
  17.215    apply arith
  17.216 - apply(erule_tac x=ib and P="\<lambda>j. (?I j, ?H j)\<in> ctran \<longrightarrow> (?P i j)" in allE,simp)
  17.217 + apply(erule_tac x=ib and P="\<lambda>j. (I j, H j) \<in> ctran \<longrightarrow> P i j" for I H P in allE,simp)
  17.218   apply(simp add:same_state_def)
  17.219 - apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE)
  17.220 - apply(erule_tac x=ib and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
  17.221 + apply(erule_tac x=i and P="\<lambda>j. (T j) \<longrightarrow> (\<forall>i. (H j i) \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE)
  17.222 + apply(erule_tac x=ib and P="\<lambda>j. (T j) \<longrightarrow> (\<forall>i. (H j i) \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
  17.223  --\<open>or an e-tran in @{text "\<sigma>"},
  17.224  therefore it satisfies @{text "rely \<or> guar_{ib}"}\<close>
  17.225  apply (force simp add:par_assum_def same_state_def)
  17.226 @@ -1181,19 +1181,19 @@
  17.227  apply clarify
  17.228  apply(simp add:conjoin_def compat_label_def)
  17.229  apply clarify
  17.230 -apply(erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (?J j \<and> (\<exists>i. ?P i j)) \<or> ?I j" in allE,simp)
  17.231 +apply(erule_tac x=j and P="\<lambda>j. H j \<longrightarrow> (J j \<and> (\<exists>i. P i j)) \<or> I j" for H J P I in allE,simp)
  17.232  apply(erule disjE)
  17.233   prefer 2
  17.234   apply(force simp add:same_state_def par_assum_def)
  17.235  apply clarify
  17.236  apply(case_tac "i=ia",simp)
  17.237   apply(erule etranE,simp)
  17.238 -apply(erule_tac x="ia" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp)
  17.239 -apply(erule_tac x=j and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
  17.240 -apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
  17.241 +apply(erule_tac x="ia" and P="\<lambda>i. H i \<longrightarrow> (I i) \<or> (J i)" for H I J in allE,simp)
  17.242 +apply(erule_tac x=j and P="\<lambda>j. \<forall>i. S j i \<longrightarrow> (I j i, H j i) \<in> ctran \<longrightarrow> P i j" for S I H P in allE)
  17.243 +apply(erule_tac x=ia and P="\<lambda>j. S j \<longrightarrow> (I j, H j) \<in> ctran \<longrightarrow> P j" for S I H P in allE)
  17.244  apply(simp add:same_state_def)
  17.245 -apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE)
  17.246 -apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
  17.247 +apply(erule_tac x=i and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE)
  17.248 +apply(erule_tac x=ia and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
  17.249  done
  17.250  
  17.251  lemma four:
  17.252 @@ -1224,18 +1224,18 @@
  17.253   apply assumption
  17.254  apply(simp add:conjoin_def same_program_def)
  17.255  apply clarify
  17.256 -apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in all_dupE)
  17.257 -apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE)
  17.258 +apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in all_dupE)
  17.259 +apply(erule_tac x="Suc i" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE)
  17.260  apply(erule par_ctranE,simp)
  17.261 -apply(erule_tac x=i and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
  17.262 -apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
  17.263 +apply(erule_tac x=i and P="\<lambda>j. \<forall>i. S j i \<longrightarrow> (I j i, H j i) \<in> ctran \<longrightarrow> P i j" for S I H P in allE)
  17.264 +apply(erule_tac x=ia and P="\<lambda>j. S j \<longrightarrow> (I j, H j) \<in> ctran \<longrightarrow> P j" for S I H P in allE)
  17.265  apply(rule_tac x=ia in exI)
  17.266  apply(simp add:same_state_def)
  17.267 -apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE,simp)
  17.268 -apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
  17.269 -apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
  17.270 -apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE,simp)
  17.271 -apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
  17.272 +apply(erule_tac x=ia and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE,simp)
  17.273 +apply(erule_tac x=ia and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
  17.274 +apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in all_dupE)
  17.275 +apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in all_dupE,simp)
  17.276 +apply(erule_tac x="Suc i" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
  17.277  apply(erule mp)
  17.278  apply(subgoal_tac "r=fst(clist ! ia ! Suc i)",simp)
  17.279  apply(drule_tac i=ia in list_eq_if)
  17.280 @@ -1266,17 +1266,17 @@
  17.281  apply simp
  17.282  apply clarify
  17.283  apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))")
  17.284 - apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> \<Turnstile> (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption)
  17.285 + apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
  17.286   apply(simp add:com_validity_def)
  17.287   apply(erule_tac x=s in allE)
  17.288 - apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?I j) \<in> cp (?J j) s" in allE,simp)
  17.289 + apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (I j) \<in> cp (J j) s" for H I J in allE,simp)
  17.290   apply(drule_tac c="clist!i" in subsetD)
  17.291    apply (force simp add:Com_def)
  17.292   apply(simp add:comm_def conjoin_def same_program_def del:last.simps)
  17.293   apply clarify
  17.294 - apply(erule_tac x="length x - 1" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE)
  17.295 + apply(erule_tac x="length x - 1" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE)
  17.296   apply (simp add:All_None_def same_length_def)
  17.297 - apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> length(?J j)=(?K j)" in allE)
  17.298 + apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> length(J j)=(K j)" for H J K in allE)
  17.299   apply(subgoal_tac "length x - 1 < length x",simp)
  17.300    apply(case_tac "x\<noteq>[]")
  17.301     apply(simp add: last_conv_nth)
  17.302 @@ -1297,8 +1297,8 @@
  17.303  apply(rule conjI)
  17.304   apply(simp add:conjoin_def same_state_def par_cp_def)
  17.305   apply clarify
  17.306 - apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
  17.307 - apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
  17.308 + apply(erule_tac x=ia and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
  17.309 + apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
  17.310   apply(case_tac x,simp+)
  17.311   apply (simp add:par_assum_def)
  17.312   apply clarify
    18.1 --- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Mar 25 10:41:53 2015 +0100
    18.2 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Mar 25 10:44:57 2015 +0100
    18.3 @@ -494,7 +494,7 @@
    18.4  apply(clarify)
    18.5  apply(simp add:conjoin_def compat_label_def)
    18.6  apply clarify
    18.7 -apply(erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (?P j \<or> ?Q j)" in all_dupE,simp)
    18.8 +apply(erule_tac x="0" and P="\<lambda>j. H j \<longrightarrow> (P j \<or> Q j)" for H P Q in all_dupE, simp)
    18.9  apply(erule disjE)
   18.10  --\<open>first step is a Component step\<close>
   18.11   apply clarify 
   18.12 @@ -504,14 +504,14 @@
   18.13     prefer 2
   18.14     apply(simp add: same_state_def)
   18.15     apply(erule_tac x=i in allE,erule impE,assumption, 
   18.16 -         erule_tac x=1 and P="\<lambda>j. (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   18.17 +         erule_tac x=1 and P="\<lambda>j. (H j) \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE, simp)
   18.18    prefer 2
   18.19    apply(simp add:same_program_def)
   18.20 -  apply(erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp)
   18.21 +  apply(erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (fst (s j))=(t j)" for H s t in allE,simp)
   18.22    apply(rule nth_equalityI,simp)
   18.23    apply clarify
   18.24    apply(case_tac "i=ia",simp,simp)
   18.25 -  apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   18.26 +  apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
   18.27    apply(drule_tac t=i in not_sym,simp)
   18.28    apply(erule etranE,simp)
   18.29   apply(rule ParCptnComp)
   18.30 @@ -532,8 +532,8 @@
   18.31      apply(force simp add:same_length_def length_Suc_conv)
   18.32     apply(simp add:same_state_def)
   18.33     apply(erule_tac x=ia in allE, erule impE, assumption, 
   18.34 -     erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   18.35 -   apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   18.36 +     erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
   18.37 +   apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
   18.38     apply(drule_tac t=i  in not_sym,simp)
   18.39     apply(erule etranE,simp)
   18.40    apply(erule allE,erule impE,assumption,erule tl_in_cptn)
   18.41 @@ -543,7 +543,7 @@
   18.42    apply clarify
   18.43    apply(case_tac j,simp,simp)
   18.44    apply(erule_tac x=ia in allE, erule impE, assumption,
   18.45 -        erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   18.46 +        erule_tac x="Suc(Suc nat)" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
   18.47    apply(force simp add:same_length_def length_Suc_conv)
   18.48   apply(rule conjI)
   18.49    apply(simp add:same_program_def)
   18.50 @@ -552,11 +552,11 @@
   18.51     apply(rule nth_equalityI,simp)
   18.52     apply clarify
   18.53     apply(case_tac "i=ia",simp,simp)
   18.54 -  apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp)
   18.55 +  apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. H j \<longrightarrow> (fst (s j))=(t j)" for H s t in allE,simp)
   18.56    apply(rule nth_equalityI,simp,simp)
   18.57    apply(force simp add:length_Suc_conv)
   18.58   apply(rule allI,rule impI)
   18.59 - apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<or> ?J j)" in allE,simp)
   18.60 + apply(erule_tac x="Suc j" and P="\<lambda>j. H j \<longrightarrow> (I j \<or> J j)" for H I J in allE,simp)
   18.61   apply(erule disjE) 
   18.62    apply clarify
   18.63    apply(rule_tac x=ia in exI,simp)
   18.64 @@ -564,13 +564,13 @@
   18.65     apply(rule conjI)
   18.66      apply(force simp add: length_Suc_conv)
   18.67     apply clarify
   18.68 -   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption)
   18.69 -   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption)
   18.70 +   apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE,erule impE,assumption)
   18.71 +   apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE,erule impE,assumption)
   18.72     apply simp
   18.73     apply(case_tac j,simp)
   18.74      apply(rule tl_zero)
   18.75        apply(erule_tac x=l in allE, erule impE, assumption, 
   18.76 -            erule_tac x=1 and P="\<lambda>j.  (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   18.77 +            erule_tac x=1 and P="\<lambda>j.  (H j) \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
   18.78        apply(force elim:etranE intro:Env)
   18.79       apply force
   18.80      apply force
   18.81 @@ -585,8 +585,8 @@
   18.82     apply(rule nth_tl_if)
   18.83       apply force
   18.84      apply(erule_tac x=ia  in allE, erule impE, assumption,
   18.85 -          erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   18.86 -    apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   18.87 +          erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
   18.88 +    apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
   18.89      apply(drule_tac t=i  in not_sym,simp)
   18.90      apply(erule etranE,simp)
   18.91     apply(erule tl_zero)
   18.92 @@ -595,41 +595,41 @@
   18.93    apply clarify
   18.94    apply(case_tac "i=l",simp)
   18.95     apply(rule nth_tl_if)
   18.96 -     apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   18.97 +     apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   18.98      apply simp
   18.99 -   apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption,erule impE,assumption)
  18.100 +   apply(erule_tac P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE,erule impE,assumption,erule impE,assumption)
  18.101     apply(erule tl_zero,force)
  18.102 -   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.103 +   apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.104     apply(rule nth_tl_if)
  18.105 -     apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.106 +     apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.107      apply(erule_tac x=l  in allE, erule impE, assumption,
  18.108 -          erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
  18.109 -    apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp)
  18.110 +          erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
  18.111 +    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE,erule impE, assumption,simp)
  18.112      apply(erule etranE,simp)
  18.113     apply(rule tl_zero)
  18.114      apply force
  18.115     apply force
  18.116 -  apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.117 +  apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.118   apply(rule disjI2)
  18.119   apply(case_tac j,simp)
  18.120    apply clarify
  18.121    apply(rule tl_zero)
  18.122 -    apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j\<in>etran" in allE,erule impE, assumption)
  18.123 +    apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j\<in>etran" for H I in allE,erule impE, assumption)
  18.124      apply(case_tac "i=ia",simp,simp)
  18.125      apply(erule_tac x=ia  in allE, erule impE, assumption,
  18.126 -    erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
  18.127 -    apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp)
  18.128 +    erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
  18.129 +    apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE,erule impE, assumption,simp)
  18.130      apply(force elim:etranE intro:Env)
  18.131     apply force
  18.132 -  apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.133 +  apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.134   apply simp
  18.135   apply clarify
  18.136   apply(rule tl_zero)
  18.137     apply(rule tl_zero,force)
  18.138      apply force
  18.139 -   apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.140 +   apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.141    apply force
  18.142 - apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.143 + apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.144  --\<open>first step is an environmental step\<close>
  18.145  apply clarify
  18.146  apply(erule par_etran.cases)
  18.147 @@ -641,24 +641,24 @@
  18.148  apply(rule_tac x="map tl clist" in exI,simp)
  18.149  apply(rule conjI)
  18.150   apply clarify
  18.151 - apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?I ?s j) \<in> cptn" in allE,simp)
  18.152 + apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> I j \<in> cptn" for H I in allE,simp)
  18.153   apply(erule cptn.cases)
  18.154     apply(simp add:same_length_def)
  18.155 -   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.156 +   apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.157    apply(simp add:same_state_def)
  18.158    apply(erule_tac x=i  in allE, erule impE, assumption,
  18.159 -   erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
  18.160 - apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<in>etran" in allE,simp)
  18.161 +   erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
  18.162 + apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> J j \<in>etran" for H J in allE,simp)
  18.163   apply(erule etranE,simp)
  18.164  apply(simp add:same_state_def same_length_def)
  18.165  apply(rule conjI,clarify)
  18.166   apply(case_tac j,simp,simp)
  18.167   apply(erule_tac x=i  in allE, erule impE, assumption,
  18.168 -       erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
  18.169 +       erule_tac x="Suc(Suc nat)" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
  18.170   apply(rule tl_zero)
  18.171     apply(simp)
  18.172    apply force
  18.173 - apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.174 + apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.175  apply(rule conjI)
  18.176   apply(simp add:same_program_def)
  18.177   apply clarify
  18.178 @@ -666,52 +666,52 @@
  18.179    apply(rule nth_equalityI,simp)
  18.180    apply clarify
  18.181    apply simp
  18.182 - apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp)
  18.183 + apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. H j \<longrightarrow> (fst (s j))=(t j)" for H s t in allE,simp)
  18.184   apply(rule nth_equalityI,simp,simp)
  18.185   apply(force simp add:length_Suc_conv)
  18.186  apply(rule allI,rule impI)
  18.187 -apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<or> ?J j)" in allE,simp)
  18.188 +apply(erule_tac x="Suc j" and P="\<lambda>j. H j \<longrightarrow> (I j \<or> J j)" for H I J in allE,simp)
  18.189  apply(erule disjE) 
  18.190   apply clarify
  18.191   apply(rule_tac x=i in exI,simp)
  18.192   apply(rule conjI)
  18.193 -  apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
  18.194 +  apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
  18.195    apply(erule etranE,simp)
  18.196    apply(erule_tac x=i  in allE, erule impE, assumption,
  18.197 -        erule_tac x=1 and P="\<lambda>j.  (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
  18.198 +        erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
  18.199    apply(rule nth_tl_if)
  18.200 -   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.201 +   apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.202    apply simp
  18.203   apply(erule tl_zero,force) 
  18.204 -  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.205 +  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.206   apply clarify
  18.207 - apply(erule_tac x=l and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
  18.208 + apply(erule_tac x=l and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
  18.209   apply(erule etranE,simp)
  18.210   apply(erule_tac x=l  in allE, erule impE, assumption,
  18.211 -       erule_tac x=1 and P="\<lambda>j.  (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
  18.212 +       erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
  18.213   apply(rule nth_tl_if)
  18.214 -   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.215 +   apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.216    apply simp
  18.217    apply(rule tl_zero,force)
  18.218    apply force
  18.219 - apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.220 + apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.221  apply(rule disjI2)
  18.222  apply simp
  18.223  apply clarify
  18.224  apply(case_tac j,simp)
  18.225   apply(rule tl_zero)
  18.226 -   apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
  18.227 -   apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
  18.228 +   apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
  18.229 +   apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
  18.230     apply(force elim:etranE intro:Env)
  18.231    apply force
  18.232 - apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.233 + apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.234  apply simp
  18.235  apply(rule tl_zero)
  18.236    apply(rule tl_zero,force)
  18.237     apply force
  18.238 -  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.239 +  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.240   apply force
  18.241 -apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.242 +apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.243  done
  18.244  
  18.245  lemma aux_onlyif [rule_format]: "\<forall>xs s. (xs, s)#ys \<in> par_cptn \<longrightarrow> 
  18.246 @@ -769,7 +769,7 @@
  18.247   apply clarify
  18.248   apply(case_tac "i=ia",simp)
  18.249    apply(erule CptnComp)
  18.250 -  apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<in> cptn)" in allE,simp)
  18.251 +  apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (I j \<in> cptn)" for H I in allE,simp)
  18.252   apply simp
  18.253   apply(erule_tac x=ia in allE)
  18.254   apply(rule CptnEnv,simp)
  18.255 @@ -790,7 +790,7 @@
  18.256    apply(rule nth_equalityI,simp,simp)
  18.257   apply simp
  18.258   apply(rule nth_equalityI,simp,simp)
  18.259 - apply(erule_tac x=nat and P="\<lambda>j. ?H j \<longrightarrow> (fst (?a j))=((?b j))" in allE)
  18.260 + apply(erule_tac x=nat and P="\<lambda>j. H j \<longrightarrow> (fst (a j))=((b j))" for H a b in allE)
  18.261   apply(case_tac nat)
  18.262    apply clarify
  18.263    apply(case_tac "i=ia",simp,simp)
  18.264 @@ -806,7 +806,7 @@
  18.265   apply clarify
  18.266   apply(rule Env)
  18.267  apply simp
  18.268 -apply(erule_tac x=nat and P="\<lambda>j. ?H j \<longrightarrow> (?P j \<or> ?Q j)" in allE,simp)
  18.269 +apply(erule_tac x=nat and P="\<lambda>j. H j \<longrightarrow> (P j \<or> Q j)" for H P Q in allE,simp)
  18.270  apply(erule disjE)
  18.271   apply clarify
  18.272   apply(rule_tac x=ia in exI,simp)
  18.273 @@ -819,7 +819,7 @@
  18.274   apply simp
  18.275   apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp)
  18.276  apply clarify
  18.277 -apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?P j)\<in>etran" in allE, erule impE, assumption)
  18.278 +apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (P j)\<in>etran" for H P in allE, erule impE, assumption)
  18.279  apply(case_tac "i=ia",simp,simp)
  18.280  done
  18.281  
  18.282 @@ -851,28 +851,28 @@
  18.283    apply(erule cptn.cases,force,force,force)
  18.284   apply(simp add:par_cp_def conjoin_def  same_length_def same_program_def same_state_def compat_label_def)
  18.285   apply clarify
  18.286 - apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in all_dupE)
  18.287 + apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in all_dupE)
  18.288   apply(subgoal_tac "a = xs")
  18.289    apply(subgoal_tac "b = s",simp)
  18.290     prefer 3
  18.291 -   apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=((?t j))" in allE)
  18.292 +   apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (fst (s j))=((t j))" for H s t in allE)
  18.293     apply (simp add:cp_def)
  18.294     apply(rule nth_equalityI,simp,simp)
  18.295    prefer 2
  18.296    apply(erule_tac x=0 in allE)
  18.297    apply (simp add:cp_def)
  18.298 -  apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (\<forall>i. ?T i \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
  18.299 -  apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
  18.300 +  apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (\<forall>i. T i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for H T d e in allE,simp)
  18.301 +  apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
  18.302   apply(erule_tac x=list in allE)
  18.303   apply(rule_tac x="map tl clist" in exI,simp) 
  18.304   apply(rule conjI)
  18.305    apply clarify
  18.306    apply(case_tac j,simp)
  18.307     apply(erule_tac x=i  in allE, erule impE, assumption,
  18.308 -        erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
  18.309 +        erule_tac x="0" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
  18.310    apply(erule_tac x=i  in allE, erule impE, assumption,
  18.311 -        erule_tac x="Suc nat" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
  18.312 -  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.313 +        erule_tac x="Suc nat" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
  18.314 +  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.315    apply(case_tac "clist!i",simp,simp)
  18.316   apply(rule conjI)
  18.317    apply clarify
  18.318 @@ -883,9 +883,9 @@
  18.319     apply(simp add:cp_def)
  18.320    apply clarify
  18.321    apply simp
  18.322 -  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.323 +  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.324    apply(case_tac "clist!i",simp,simp)
  18.325 - apply(thin_tac "?H = (\<exists>i. ?J i)")
  18.326 + apply(thin_tac "H = (\<exists>i. J i)" for H J)
  18.327   apply(rule conjI)
  18.328    apply clarify
  18.329    apply(erule_tac x=j in allE,erule impE, assumption,erule disjE)
  18.330 @@ -895,34 +895,34 @@
  18.331      apply(rule conjI)
  18.332       apply(erule_tac x=i in allE)
  18.333       apply(simp add:cp_def)
  18.334 -     apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.335 +     apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.336       apply(case_tac "clist!i",simp,simp)
  18.337      apply clarify
  18.338      apply(erule_tac x=l in allE)
  18.339 -    apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
  18.340 +    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
  18.341      apply clarify
  18.342      apply(simp add:cp_def)
  18.343 -    apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.344 +    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.345      apply(case_tac "clist!l",simp,simp)
  18.346     apply simp
  18.347     apply(rule conjI)
  18.348 -    apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.349 +    apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.350      apply(case_tac "clist!i",simp,simp)
  18.351     apply clarify
  18.352 -   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
  18.353 -   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.354 +   apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
  18.355 +   apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.356     apply(case_tac "clist!l",simp,simp)
  18.357    apply clarify
  18.358    apply(erule_tac x=i in allE)
  18.359    apply(simp add:cp_def)
  18.360 -  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.361 +  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.362    apply(case_tac "clist!i",simp)
  18.363    apply(rule nth_tl_if,simp,simp)
  18.364 -  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?P j)\<in>etran" in allE, erule impE, assumption,simp)
  18.365 +  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (P j)\<in>etran" for H P in allE, erule impE, assumption,simp)
  18.366    apply(simp add:cp_def)
  18.367    apply clarify
  18.368    apply(rule nth_tl_if)
  18.369 -   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.370 +   apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.371     apply(case_tac "clist!i",simp,simp)
  18.372    apply force
  18.373   apply force
  18.374 @@ -940,14 +940,14 @@
  18.375      apply clarify
  18.376      apply(unfold same_length_def)
  18.377      apply clarify
  18.378 -    apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,simp)
  18.379 +    apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,simp)
  18.380     apply(rule conjI)
  18.381      apply(simp add:same_state_def)
  18.382      apply clarify
  18.383      apply(erule_tac x=i in allE, erule impE, assumption,
  18.384 -       erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
  18.385 +       erule_tac x=j and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
  18.386      apply(case_tac j,simp)
  18.387 -    apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.388 +    apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.389      apply(case_tac "clist!i",simp,simp)
  18.390     apply(rule conjI)
  18.391      apply(simp add:same_program_def)
  18.392 @@ -955,7 +955,7 @@
  18.393      apply(rule nth_equalityI,simp,simp)
  18.394      apply(case_tac j,simp)
  18.395      apply clarify
  18.396 -    apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.397 +    apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.398      apply(case_tac "clist!i",simp,simp)
  18.399     apply clarify
  18.400     apply(simp add:compat_label_def)
  18.401 @@ -967,13 +967,13 @@
  18.402      apply(rule conjI)
  18.403       apply(erule_tac x=i in allE)
  18.404       apply(case_tac j,simp)
  18.405 -      apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.406 +      apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.407        apply(case_tac "clist!i",simp,simp)
  18.408 -     apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.409 +     apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.410       apply(case_tac "clist!i",simp,simp)
  18.411      apply clarify
  18.412 -    apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
  18.413 -    apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  18.414 +    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
  18.415 +    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
  18.416      apply(case_tac "clist!l",simp,simp)
  18.417      apply(erule_tac x=l in allE,simp)
  18.418     apply(rule disjI2)
  18.419 @@ -982,9 +982,9 @@
  18.420       apply(case_tac j,simp,simp)
  18.421       apply(rule tl_zero,force)   
  18.422        apply force
  18.423 -     apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.424 +     apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.425      apply force
  18.426 -   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  18.427 +   apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
  18.428    apply clarify
  18.429    apply(erule_tac x=i in allE)
  18.430    apply(simp add:cp_def)
    19.1 --- a/src/HOL/IMPP/EvenOdd.thy	Wed Mar 25 10:41:53 2015 +0100
    19.2 +++ b/src/HOL/IMPP/EvenOdd.thy	Wed Mar 25 10:44:57 2015 +0100
    19.3 @@ -91,7 +91,7 @@
    19.4  apply (rule hoare_derivs.Comp)
    19.5  apply (rule_tac [2] hoare_derivs.Ass)
    19.6  apply clarsimp
    19.7 -apply (rule_tac Q = "%Z s. ?P Z s & Res_ok Z s" in hoare_derivs.Comp)
    19.8 +apply (rule_tac Q = "%Z s. P Z s & Res_ok Z s" and P = P for P in hoare_derivs.Comp)
    19.9  apply (rule export_s)
   19.10  apply  (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12])
   19.11  apply (rule single_asm [THEN conseq2])
    20.1 --- a/src/HOL/IMPP/Hoare.thy	Wed Mar 25 10:41:53 2015 +0100
    20.2 +++ b/src/HOL/IMPP/Hoare.thy	Wed Mar 25 10:44:57 2015 +0100
    20.3 @@ -286,7 +286,7 @@
    20.4  apply         (blast) (* cut *)
    20.5  apply        (blast) (* weaken *)
    20.6  apply       (tactic {* ALLGOALS (EVERY'
    20.7 -  [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs ?x ?y" [],
    20.8 +  [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs _ _" [],
    20.9     simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *})
   20.10  apply       (simp_all (no_asm_use) add: triple_valid_def2)
   20.11  apply       (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *)
   20.12 @@ -315,7 +315,7 @@
   20.13  apply (unfold MGT_def)
   20.14  apply (erule conseq12)
   20.15  apply auto
   20.16 -apply (case_tac "? t. <c,?s> -c-> t")
   20.17 +apply (case_tac "\<exists>t. <c,s> -c-> t" for s)
   20.18  apply  (fast elim: com_det)
   20.19  apply clarsimp
   20.20  apply (drule single_stateE)
    21.1 --- a/src/HOL/IMPP/Natural.thy	Wed Mar 25 10:41:53 2015 +0100
    21.2 +++ b/src/HOL/IMPP/Natural.thy	Wed Mar 25 10:44:57 2015 +0100
    21.3 @@ -105,7 +105,7 @@
    21.4  (* evaluation of com is deterministic *)
    21.5  lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"
    21.6  apply (erule evalc.induct)
    21.7 -apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl)
    21.8 +apply (erule_tac [8] V = "<c,s1> -c-> s2" for c in thin_rl)
    21.9  apply (blast elim: evalc_WHILE_case)+
   21.10  done
   21.11  
    22.1 --- a/src/HOL/Induct/Com.thy	Wed Mar 25 10:41:53 2015 +0100
    22.2 +++ b/src/HOL/Induct/Com.thy	Wed Mar 25 10:44:57 2015 +0100
    22.3 @@ -184,7 +184,7 @@
    22.4     apply blast
    22.5    apply blast
    22.6   apply (blast elim: exec_WHILE_case)
    22.7 -apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
    22.8 +apply (erule_tac V = "(c,s2) -[ev]-> s3" for c ev in thin_rl)
    22.9  apply clarify
   22.10  apply (erule exec_WHILE_case, blast+)
   22.11  done
    23.1 --- a/src/HOL/Library/Multiset.thy	Wed Mar 25 10:41:53 2015 +0100
    23.2 +++ b/src/HOL/Library/Multiset.thy	Wed Mar 25 10:44:57 2015 +0100
    23.3 @@ -1658,7 +1658,7 @@
    23.4   apply (simp (no_asm))
    23.5   apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
    23.6   apply (simp (no_asm_simp) add: add.assoc [symmetric])
    23.7 - apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong)
    23.8 + apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong)
    23.9   apply (simp add: diff_union_single_conv)
   23.10   apply (simp (no_asm_use) add: trans_def)
   23.11   apply blast
   23.12 @@ -1669,7 +1669,7 @@
   23.13   apply (rule conjI)
   23.14    apply (simp add: multiset_eq_iff split: nat_diff_split)
   23.15   apply (rule conjI)
   23.16 -  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong, simp)
   23.17 +  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong, simp)
   23.18    apply (simp add: multiset_eq_iff split: nat_diff_split)
   23.19   apply (simp (no_asm_use) add: trans_def)
   23.20   apply blast
   23.21 @@ -1692,7 +1692,7 @@
   23.22   apply (simp add: mult1_def set_of_def, blast)
   23.23  txt {* Now we know @{term "J' \<noteq> {#}"}. *}
   23.24  apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
   23.25 -apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
   23.26 +apply (erule_tac P = "\<forall>k \<in> set_of K. P k" for P in rev_mp)
   23.27  apply (erule ssubst)
   23.28  apply (simp add: Ball_def, auto)
   23.29  apply (subgoal_tac
    24.1 --- a/src/HOL/MicroJava/DFA/Listn.thy	Wed Mar 25 10:41:53 2015 +0100
    24.2 +++ b/src/HOL/MicroJava/DFA/Listn.thy	Wed Mar 25 10:44:57 2015 +0100
    24.3 @@ -345,7 +345,7 @@
    24.4  apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs:M}" in allE)
    24.5  apply (erule impE)
    24.6   apply blast
    24.7 -apply (thin_tac "\<exists>x xs. ?P x xs")
    24.8 +apply (thin_tac "\<exists>x xs. P x xs" for P)
    24.9  apply clarify
   24.10  apply (rename_tac maxA xs)
   24.11  apply (erule_tac x = "{ys. size ys = size xs \<and> maxA#ys \<in> M}" in allE)
    25.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Mar 25 10:41:53 2015 +0100
    25.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Mar 25 10:44:57 2015 +0100
    25.3 @@ -137,20 +137,20 @@
    25.4  apply( clarsimp)
    25.5  apply( drule (3) Call_lemma)
    25.6  apply( clarsimp simp add: wf_java_mdecl_def)
    25.7 -apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
    25.8 +apply( erule_tac V = "method sig x = y" for sig x y in thin_rl)
    25.9  apply( drule spec, erule impE,  erule_tac [2] notE impE, tactic "assume_tac @{context} 2")
   25.10  apply(  rule conformsI)
   25.11  apply(   erule conforms_heapD)
   25.12  apply(  rule lconf_ext)
   25.13  apply(   force elim!: Call_lemma2)
   25.14  apply(  erule conf_hext, erule (1) conf_obj_AddrI)
   25.15 -apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl) 
   25.16 +apply( erule_tac V = "E\<turnstile>blk\<surd>" for E blk in thin_rl) 
   25.17  apply (simp add: conforms_def)
   25.18  
   25.19  apply( erule conjE)
   25.20  apply( drule spec, erule (1) impE)
   25.21  apply( drule spec, erule (1) impE)
   25.22 -apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl)
   25.23 +apply( erule_tac V = "E\<turnstile>res::rT" for E rT in thin_rl)
   25.24  apply( clarify)
   25.25  apply( rule conjI)
   25.26  apply(  fast intro: hext_trans)
   25.27 @@ -291,7 +291,7 @@
   25.28  
   25.29  -- "5 While"
   25.30  prefer 5
   25.31 -apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
   25.32 +apply(erule_tac V = "a \<longrightarrow> b" for a b in thin_rl)
   25.33  apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
   25.34  apply(force elim: hext_trans)
   25.35  
    26.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Wed Mar 25 10:41:53 2015 +0100
    26.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Mar 25 10:44:57 2015 +0100
    26.3 @@ -419,7 +419,7 @@
    26.4  apply( simp)
    26.5  apply( drule map_add_SomeD)
    26.6  apply( erule disjE)
    26.7 -apply(  erule_tac V = "?P --> ?Q" in thin_rl)
    26.8 +apply(  erule_tac V = "P --> Q" for P Q in thin_rl)
    26.9  apply (frule map_of_SomeD)
   26.10  apply (clarsimp simp add: wf_cdecl_def)
   26.11  apply( clarify)
   26.12 @@ -454,7 +454,7 @@
   26.13  apply( simp)
   26.14  apply( drule map_add_SomeD)
   26.15  apply( erule disjE)
   26.16 -apply(  erule_tac V = "?P --> ?Q" in thin_rl)
   26.17 +apply(  erule_tac V = "P --> Q" for P Q in thin_rl)
   26.18  apply (frule map_of_SomeD)
   26.19  apply (clarsimp simp add: ws_cdecl_def)
   26.20  apply blast
   26.21 @@ -486,7 +486,7 @@
   26.22  apply(  assumption)
   26.23  apply( unfold map_add_def)
   26.24  apply( simp (no_asm_simp) add: wf_prog_ws_prog del: split_paired_Ex)
   26.25 -apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
   26.26 +apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, C, m)) ms) sig = Some z" for C)
   26.27  apply(  erule exE)
   26.28  apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
   26.29  prefer 2
    27.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Mar 25 10:41:53 2015 +0100
    27.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Mar 25 10:44:57 2015 +0100
    27.3 @@ -6703,7 +6703,7 @@
    27.4    moreover have "?d > 0"
    27.5      using as(2) by (auto simp: Suc_le_eq DIM_positive)
    27.6    ultimately show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> setsum (op \<bullet> y) Basis \<le> 1"
    27.7 -    apply (rule_tac x="min (Min ((op \<bullet> x) ` Basis)) ?D" in exI)
    27.8 +    apply (rule_tac x="min (Min ((op \<bullet> x) ` Basis)) D" for D in exI)
    27.9      apply rule
   27.10      defer
   27.11      apply (rule, rule)
    28.1 --- a/src/HOL/NanoJava/Equivalence.thy	Wed Mar 25 10:41:53 2015 +0100
    28.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Wed Mar 25 10:44:57 2015 +0100
    28.3 @@ -105,8 +105,8 @@
    28.4  apply (rule hoare_ehoare.induct)
    28.5  (*18*)
    28.6  apply (tactic {* ALLGOALS (REPEAT o dresolve_tac @{context} [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
    28.7 -apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare ?x ?y" []) *})
    28.8 -apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare ?x ?y" []) *})
    28.9 +apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare _ _" []) *})
   28.10 +apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare _ _" []) *})
   28.11  apply (simp_all only: cnvalid1_eq cenvalid_def2)
   28.12                   apply fast
   28.13                  apply fast
    29.1 --- a/src/HOL/Nominal/Examples/Standardization.thy	Wed Mar 25 10:41:53 2015 +0100
    29.2 +++ b/src/HOL/Nominal/Examples/Standardization.thy	Wed Mar 25 10:44:57 2015 +0100
    29.3 @@ -384,7 +384,7 @@
    29.4      apply (subgoal_tac "r = (Lam [xa]. [(xa, x)] \<bullet> s)")
    29.5      prefer 2
    29.6      apply (simp add: calc_atm)
    29.7 -    apply (thin_tac "r = ?t")
    29.8 +    apply (thin_tac "r = _")
    29.9      apply simp
   29.10      apply (rule exI)
   29.11      apply (rule conjI)
    30.1 --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Wed Mar 25 10:41:53 2015 +0100
    30.2 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Wed Mar 25 10:44:57 2015 +0100
    30.3 @@ -771,7 +771,7 @@
    30.4    ==> Nonce N \<notin> analz (knows Spy evs) -->
    30.5        (\<exists>k i W. Says (Cardholder k) (CA i) {|U,W|} \<in> set evs & 
    30.6                 Cardholder k \<notin> bad & CA i \<notin> bad)"
    30.7 -apply (erule_tac P = "U \<in> ?H" in rev_mp)
    30.8 +apply (erule_tac P = "U \<in> H" for H in rev_mp)
    30.9  apply (erule set_cr.induct)
   30.10  apply (valid_certificate_tac [8])  --{*for message 5*}
   30.11  apply (simp_all del: image_insert image_Un imp_disjL
    31.1 --- a/src/HOL/UNITY/Comp.thy	Wed Mar 25 10:41:53 2015 +0100
    31.2 +++ b/src/HOL/UNITY/Comp.thy	Wed Mar 25 10:44:57 2015 +0100
    31.3 @@ -186,7 +186,7 @@
    31.4  apply simp
    31.5  apply (subgoal_tac "G \<in> preserves (funPair v w) ")
    31.6   prefer 2 apply simp
    31.7 -apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], 
    31.8 +apply (drule_tac P1 = "split Q" for Q in preserves_subset_stable [THEN subsetD], 
    31.9         auto)
   31.10  done
   31.11  
   31.12 @@ -198,8 +198,8 @@
   31.13  (*The G case remains*)
   31.14  apply (auto simp add: preserves_def stable_def constrains_def)
   31.15  (*We have a G-action, so delete assumptions about F-actions*)
   31.16 -apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
   31.17 -apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)
   31.18 +apply (erule_tac V = "\<forall>act \<in> Acts F. P act" for P in thin_rl)
   31.19 +apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. P z act" for P in thin_rl)
   31.20  apply (subgoal_tac "v x = v xa")
   31.21   apply auto
   31.22  apply (erule order_trans, blast)
    32.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Wed Mar 25 10:41:53 2015 +0100
    32.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Wed Mar 25 10:44:57 2015 +0100
    32.3 @@ -1080,7 +1080,7 @@
    32.4  text{*Could go to Extend.ML*}
    32.5  lemma bij_fst_inv_inv_eq: "bij f ==> fst (inv (%(x, u). inv f x) z) = f z"
    32.6    apply (rule fst_inv_equalityI)
    32.7 -   apply (rule_tac f = "%z. (f z, ?h z) " in surjI)
    32.8 +   apply (rule_tac f = "%z. (f z, h z)" for h in surjI)
    32.9     apply (simp add: bij_is_inj inv_f_f)
   32.10    apply (simp add: bij_is_surj surj_f_inv_f)
   32.11    done
    33.1 --- a/src/HOL/UNITY/ELT.thy	Wed Mar 25 10:41:53 2015 +0100
    33.2 +++ b/src/HOL/UNITY/ELT.thy	Wed Mar 25 10:44:57 2015 +0100
    33.3 @@ -63,7 +63,7 @@
    33.4  
    33.5  lemma givenBy_eq_all: "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}"
    33.6  apply (unfold givenBy_def, safe)
    33.7 -apply (rule_tac [2] x = "v ` ?u" in image_eqI, auto)
    33.8 +apply (rule_tac [2] x = "v ` _" in image_eqI, auto)
    33.9  done
   33.10  
   33.11  lemma givenByI: "(!!x y. [| x:A;  v x = v y |] ==> y: A) ==> A: givenBy v"
   33.12 @@ -101,7 +101,7 @@
   33.13       "[| A : givenBy v;  B : givenBy v |] ==> A-B : givenBy v"
   33.14  apply (simp (no_asm_use) add: givenBy_eq_Collect)
   33.15  apply safe
   33.16 -apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI)
   33.17 +apply (rule_tac x = "%z. R z & ~ Q z" for R Q in exI)
   33.18  unfolding set_diff_eq
   33.19  apply auto
   33.20  done
    34.1 --- a/src/HOL/UNITY/Guar.thy	Wed Mar 25 10:41:53 2015 +0100
    34.2 +++ b/src/HOL/UNITY/Guar.thy	Wed Mar 25 10:44:57 2015 +0100
    34.3 @@ -349,7 +349,7 @@
    34.4        ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =  
    34.5            (F \<in> welldef \<inter> X --> G \<in> X)"
    34.6  apply (unfold strict_ex_prop_def, safe)
    34.7 -apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
    34.8 +apply (erule_tac x = SKIP and P = "%H. PP H --> RR H" for PP RR in allE)
    34.9  apply (auto dest: Join_welldef_D1 Join_welldef_D2)
   34.10  done
   34.11  
   34.12 @@ -372,7 +372,7 @@
   34.13        ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =  
   34.14            (F \<in> welldef \<inter> X --> G \<in> X)"
   34.15  apply (unfold strict_uv_prop_def, safe)
   34.16 -apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
   34.17 +apply (erule_tac x = SKIP and P = "%H. PP H --> RR H" for PP RR in allE)
   34.18  apply (auto dest: Join_welldef_D1 Join_welldef_D2)
   34.19  done
   34.20  
    35.1 --- a/src/HOL/UNITY/ProgressSets.thy	Wed Mar 25 10:41:53 2015 +0100
    35.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Wed Mar 25 10:44:57 2015 +0100
    35.3 @@ -383,7 +383,7 @@
    35.4  apply (drule equalityD1)   
    35.5  apply (rule subset_trans) 
    35.6   prefer 2 apply assumption
    35.7 -apply (thin_tac "?U \<subseteq> X") 
    35.8 +apply (thin_tac "_ \<subseteq> X") 
    35.9  apply (cut_tac A=X in UN_singleton) 
   35.10  apply (erule subst) 
   35.11  apply (simp only: cl_UN lattice_latticeof 
    36.1 --- a/src/HOL/UNITY/Project.thy	Wed Mar 25 10:41:53 2015 +0100
    36.2 +++ b/src/HOL/UNITY/Project.thy	Wed Mar 25 10:44:57 2015 +0100
    36.3 @@ -410,7 +410,7 @@
    36.4   prefer 2
    36.5   apply (simp add: stable_def constrains_def, blast) 
    36.6  (*back to main goal*)
    36.7 -apply (erule_tac V = "?AA \<subseteq> -C \<union> ?BB" in thin_rl)
    36.8 +apply (erule_tac V = "AA \<subseteq> -C \<union> BB" for AA BB in thin_rl)
    36.9  apply (drule bspec, assumption) 
   36.10  apply (simp add: extend_set_def project_act_def, blast)
   36.11  done
    37.1 --- a/src/HOL/UNITY/Transformers.thy	Wed Mar 25 10:41:53 2015 +0100
    37.2 +++ b/src/HOL/UNITY/Transformers.thy	Wed Mar 25 10:44:57 2015 +0100
    37.3 @@ -139,7 +139,7 @@
    37.4        "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
    37.5         ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
    37.6  apply (rule subset_wens) 
    37.7 -apply (rule_tac P="\<lambda>x. ?f x \<subseteq> ?b" in ssubst [OF wens_unfold])
    37.8 +apply (rule_tac P="\<lambda>x. f x \<subseteq> b" for f b in ssubst [OF wens_unfold])
    37.9  apply (simp add: wp_def awp_def, blast)
   37.10  done
   37.11  
    38.1 --- a/src/HOL/Wellfounded.thy	Wed Mar 25 10:41:53 2015 +0100
    38.2 +++ b/src/HOL/Wellfounded.thy	Wed Mar 25 10:44:57 2015 +0100
    38.3 @@ -232,7 +232,7 @@
    38.4   prefer 2 apply blast
    38.5  apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
    38.6   apply assumption
    38.7 -apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) 
    38.8 +apply (erule_tac V = "ALL Q. (EX x. x : Q) --> P Q" for P in thin_rl) 
    38.9    --{*essential for speed*}
   38.10  txt{*Blast with new substOccur fails*}
   38.11  apply (fast intro: converse_rtrancl_into_rtrancl)
    39.1 --- a/src/HOL/Word/Bit_Representation.thy	Wed Mar 25 10:41:53 2015 +0100
    39.2 +++ b/src/HOL/Word/Bit_Representation.thy	Wed Mar 25 10:44:57 2015 +0100
    39.3 @@ -224,7 +224,7 @@
    39.4       apply (erule conjI)
    39.5       apply (drule_tac x=0 in fun_cong, force)
    39.6      apply (rule ext)
    39.7 -    apply (drule_tac x="Suc ?x" in fun_cong, force)
    39.8 +    apply (drule_tac x="Suc x" for x in fun_cong, force)
    39.9      done
   39.10    show ?thesis
   39.11    by (auto elim: bin_nth_lem)
    40.1 --- a/src/HOL/Word/Misc_Typedef.thy	Wed Mar 25 10:41:53 2015 +0100
    40.2 +++ b/src/HOL/Word/Misc_Typedef.thy	Wed Mar 25 10:44:57 2015 +0100
    40.3 @@ -194,7 +194,7 @@
    40.4     prefer 2
    40.5     apply (simp add: comp_assoc)
    40.6    apply (rule ext)
    40.7 -  apply (drule_tac f="?a o ?b" in fun_cong)
    40.8 +  apply (drule_tac f="a o b" for a b in fun_cong)
    40.9    apply simp
   40.10    done
   40.11  
    41.1 --- a/src/HOL/Word/Word.thy	Wed Mar 25 10:41:53 2015 +0100
    41.2 +++ b/src/HOL/Word/Word.thy	Wed Mar 25 10:44:57 2015 +0100
    41.3 @@ -3190,7 +3190,7 @@
    41.4    apply clarsimp
    41.5    apply (case_tac x, force)
    41.6    apply (case_tac m, auto)
    41.7 -  apply (drule_tac t="length ?xs" in sym)
    41.8 +  apply (drule_tac t="length xs" for xs in sym)
    41.9    apply (clarsimp simp: map2_def zip_replicate o_def)
   41.10    done
   41.11  
   41.12 @@ -3203,7 +3203,7 @@
   41.13    apply clarsimp
   41.14    apply (case_tac x, force)
   41.15    apply (case_tac m, auto)
   41.16 -  apply (drule_tac t="length ?xs" in sym)
   41.17 +  apply (drule_tac t="length xs" for xs in sym)
   41.18    apply (clarsimp simp: map2_def zip_replicate o_def map_replicate_const)
   41.19    done
   41.20  
   41.21 @@ -3811,7 +3811,7 @@
   41.22  
   41.23  lemma word_split_cat_alt:
   41.24    "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
   41.25 -  apply (case_tac "word_split ?w")
   41.26 +  apply (case_tac "word_split w")
   41.27    apply (rule trans, assumption)
   41.28    apply (drule test_bit_split)
   41.29    apply safe
   41.30 @@ -4694,7 +4694,7 @@
   41.31   apply simp
   41.32  apply (case_tac "1 + (n - m) = 0")
   41.33   apply (simp add: word_rec_0)
   41.34 - apply (rule_tac f = "word_rec ?a ?b" in arg_cong)
   41.35 + apply (rule_tac f = "word_rec a b" for a b in arg_cong)
   41.36   apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
   41.37    apply simp
   41.38   apply (simp (no_asm_use))