--- a/src/CCL/ex/Stream.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/CCL/ex/Stream.thy Wed Mar 25 10:44:57 2015 +0100
@@ -120,7 +120,7 @@
lemma iter2Blemma:
"n:Nat \<Longrightarrow>
map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))"
- apply (rule_tac P = "\<lambda>x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst])
+ apply (rule_tac P = "\<lambda>x. lhs(x) = rhs" for lhs rhs in iter2B [THEN ssubst])
apply (simp add: nmapBcons)
done
--- a/src/HOL/Algebra/Sylow.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Algebra/Sylow.thy Wed Mar 25 10:44:57 2015 +0100
@@ -182,7 +182,7 @@
apply (erule H_into_carrier_G)
apply (rule H_not_empty)
apply (simp add: H_def, clarify)
-apply (erule_tac P = "%z. ?lhs(z) = M1" in subst)
+apply (erule_tac P = "%z. lhs(z) = M1" for lhs in subst)
apply (simp add: coset_mult_assoc )
apply (blast intro: H_m_closed)
done
--- a/src/HOL/Auth/KerberosIV_Gets.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Auth/KerberosIV_Gets.thy Wed Mar 25 10:44:57 2015 +0100
@@ -1238,11 +1238,12 @@
txt{*K5. Not clear how this step could be integrated with the main
simplification step. Done in KerberosV.thy*}
apply clarify
-apply (erule_tac V = "Says Aa Tgs ?X \<in> set ?evs" in thin_rl)
+apply (erule_tac V = "Says Aa Tgs X \<in> set evs" for X evs in thin_rl)
apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN servK_notin_authKeysD])
apply (assumption, assumption, blast, assumption)
apply (simp add: analz_insert_freshK2)
-by (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
+apply (blast dest: Key_unique_SesKey intro: less_SucI)
+done
text{* In the real world Tgs can't check wheter authK is secure! *}
--- a/src/HOL/Auth/Yahalom.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Auth/Yahalom.thy Wed Mar 25 10:44:57 2015 +0100
@@ -403,7 +403,7 @@
txt{*YM3*}
apply blast
txt{*YM4*}
-apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
+apply (erule_tac V = "\<forall>KK. P KK" for P in thin_rl, clarify)
txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore
@{prop "NBa \<noteq> NB"}. Previous two steps make the next step
faster.*}
--- a/src/HOL/Bali/AxCompl.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Bali/AxCompl.thy Wed Mar 25 10:44:57 2015 +0100
@@ -71,7 +71,7 @@
apply (subgoal_tac
"nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
apply clarsimp
-apply (erule_tac V="nyinitcls G (x, s) = ?rhs" in thin_rl)
+apply (erule_tac V="nyinitcls G (x, s) = rhs" for rhs in thin_rl)
apply (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
apply (auto dest!: not_initedD elim!:
simp add: nyinitcls_def inited_def split add: split_if_asm)
--- a/src/HOL/Bali/AxExample.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Bali/AxExample.thy Wed Mar 25 10:44:57 2015 +0100
@@ -71,13 +71,13 @@
apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
prefer 2
apply clarsimp
-apply (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2)
+apply (rule_tac Q' = "(\<lambda>Y s Z. Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" and Q = Q for Q in conseq2)
prefer 2
apply simp
apply (tactic "ax_tac @{context} 1" (* While *))
prefer 2
apply (rule ax_impossible [THEN conseq1], clarsimp)
-apply (rule_tac P' = "Normal ?P" in conseq1)
+apply (rule_tac P' = "Normal P" and P = P for P in conseq1)
prefer 2
apply clarsimp
apply (tactic "ax_tac @{context} 1")
@@ -106,7 +106,7 @@
apply (unfold DynT_prop_def)
apply (simp (no_asm))
apply (intro strip)
-apply (rule_tac P' = "Normal ?P" in conseq1)
+apply (rule_tac P' = "Normal P" and P = P for P in conseq1)
apply (tactic "ax_tac @{context} 1" (* Methd *))
apply (rule ax_thin [OF _ empty_subsetI])
apply (simp (no_asm) add: body_def2)
@@ -185,7 +185,7 @@
apply (simp (no_asm))
apply (unfold arr_viewed_from_def)
apply (rule allI)
-apply (rule_tac P' = "Normal ?P" in conseq1)
+apply (rule_tac P' = "Normal P" and P = P for P in conseq1)
apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
apply (tactic "ax_tac @{context} 1")
apply (tactic "ax_tac @{context} 1")
@@ -268,7 +268,7 @@
apply (rule ax_subst_Var_allI)
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)" [] *})
apply (rule allI)
-apply (rule_tac P' = "Normal ?P" in conseq1)
+apply (rule_tac P' = "Normal P" and P = P for P in conseq1)
prefer 2
apply clarsimp
apply (tactic "ax_tac @{context} 1")
--- a/src/HOL/Bali/AxSem.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Bali/AxSem.thy Wed Mar 25 10:44:57 2015 +0100
@@ -1055,7 +1055,7 @@
apply safe
apply (erule spec)
apply (rule ax_escape, clarsimp)
-apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)
+apply (erule_tac V = "P \<longrightarrow> Q" for P Q in thin_rl)
apply (drule spec,drule spec,drule spec, erule conseq12)
apply (force simp add: init_lvars_def Let_def)
done
--- a/src/HOL/Bali/Example.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Bali/Example.thy Wed Mar 25 10:44:57 2015 +0100
@@ -1259,18 +1259,18 @@
apply (simp (no_asm_use))
apply (drule (1) alloc_one,clarsimp)
apply (rule eval_Is (* ;; *))
-apply (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
-apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
-apply (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
+apply (erule_tac V = "the (new_Addr _) = c" in thin_rl)
+apply (erule_tac [2] V = "new_Addr _ = Some a" in thin_rl)
+apply (erule_tac [2] V = "atleast_free _ four" in thin_rl)
apply (rule eval_Is (* Expr *))
apply (rule eval_Is (* Ass *))
apply (rule eval_Is (* LVar *))
apply (rule eval_Is (* NewC *))
(* begin init Ext *)
-apply (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
-apply (erule_tac V = "atleast_free ?h three" in thin_rl)
-apply (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
-apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
+apply (erule_tac V = "the (new_Addr _) = b" in thin_rl)
+apply (erule_tac V = "atleast_free _ three" in thin_rl)
+apply (erule_tac [2] V = "atleast_free _ four" in thin_rl)
+apply (erule_tac [2] V = "new_Addr _ = Some a" in thin_rl)
apply (rule eval_Is (* Init Ext *))
apply (simp)
apply (rule conjI)
@@ -1309,7 +1309,7 @@
apply (drule alloc_one)
apply (simp (no_asm_simp))
apply clarsimp
-apply (erule_tac V = "atleast_free ?h three" in thin_rl)
+apply (erule_tac V = "atleast_free _ three" in thin_rl)
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
apply (simp (no_asm_use))
apply (rule eval_Is (* Try *))
@@ -1361,7 +1361,7 @@
apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
apply (drule alloc_one [THEN conjunct1])
apply (simp (no_asm_simp))
-apply (erule_tac V = "atleast_free ?h two" in thin_rl)
+apply (erule_tac V = "atleast_free _ two" in thin_rl)
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
apply simp
apply (rule eval_Is (* While *))
--- a/src/HOL/Bali/State.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Bali/State.thy Wed Mar 25 10:44:57 2015 +0100
@@ -599,13 +599,13 @@
where "store == snd"
lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False"
-apply (erule_tac x = "(Some k,y)" in all_dupE)
-apply (erule_tac x = "(None,y)" in allE)
+apply (erule_tac x = "(Some k,y)" for k y in all_dupE)
+apply (erule_tac x = "(None,y)" for y in allE)
apply clarify
done
lemma state_not_single: "All (op = (x::state)) \<Longrightarrow> R"
-apply (drule_tac x = "(if abrupt x = None then Some ?x else None,?y)" in spec)
+apply (drule_tac x = "(if abrupt x = None then Some x' else None, y)" for x' y in spec)
apply clarsimp
done
@@ -823,4 +823,3 @@
end
-
--- a/src/HOL/Bali/WellType.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Bali/WellType.thy Wed Mar 25 10:44:57 2015 +0100
@@ -660,14 +660,14 @@
(* 17 subgoals *)
apply (tactic {* ALLGOALS (fn i =>
if i = 11 then EVERY'
- [Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean" [],
- Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1" [],
- Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2" []] i
- else Rule_Insts.thin_tac @{context} "All ?P" [] i) *})
+ [Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e0\<Colon>-PrimT Boolean" [(@{binding E}, NONE, NoSyn)],
+ Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e1\<Colon>-T1" [(@{binding E}, NONE, NoSyn), (@{binding T1}, NONE, NoSyn)],
+ Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e2\<Colon>-T2" [(@{binding E}, NONE, NoSyn), (@{binding T2}, NONE, NoSyn)]] i
+ else Rule_Insts.thin_tac @{context} "All P" [(@{binding P}, NONE, NoSyn)] i) *})
(*apply (safe del: disjE elim!: wt_elim_cases)*)
apply (tactic {*ALLGOALS (eresolve_tac @{context} @{thms wt_elim_cases})*})
apply (simp_all (no_asm_use) split del: split_if_asm)
-apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
+apply (erule_tac [12] V = "All P" for P in thin_rl) (* Call *)
apply (blast del: equalityCE dest: sym [THEN trans])+
done
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Wed Mar 25 10:44:57 2015 +0100
@@ -787,7 +787,7 @@
apply (auto simp add: divides_def simp del: pmult_Cons)
apply (rule_tac x = qb in exI)
apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa)) =
- poly (pmult (pexp [uminus a, one] (?order a p)) (pmult [uminus a, one] qb))")
+ poly (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb))")
apply (drule poly_mult_left_cancel [THEN iffD1], force)
apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a q))
(pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa))) =
--- a/src/HOL/Divides.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Divides.thy Wed Mar 25 10:44:57 2015 +0100
@@ -1195,7 +1195,7 @@
lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
apply (cut_tac m = q and n = c in mod_less_divisor)
apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
- apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
+ apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
apply (simp add: add_mult_distrib2)
done
@@ -2408,7 +2408,7 @@
"0<k ==>
P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
apply (rule iffI, clarify)
- apply (erule_tac P="P ?x ?y" in rev_mp)
+ apply (erule_tac P="P x y" for x y in rev_mp)
apply (subst mod_add_eq)
apply (subst zdiv_zadd1_eq)
apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
@@ -2421,7 +2421,7 @@
"k<0 ==>
P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
apply (rule iffI, clarify)
- apply (erule_tac P="P ?x ?y" in rev_mp)
+ apply (erule_tac P="P x y" for x y in rev_mp)
apply (subst mod_add_eq)
apply (subst zdiv_zadd1_eq)
apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
--- a/src/HOL/GCD.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/GCD.thy Wed Mar 25 10:44:57 2015 +0100
@@ -626,11 +626,11 @@
apply (erule subst)
apply (rule iffI)
apply force
- apply (drule_tac x = "abs ?e" in exI)
- apply (case_tac "(?e::int) >= 0")
+ apply (drule_tac x = "abs e" for e in exI)
+ apply (case_tac "e >= 0" for e :: int)
apply force
apply force
-done
+ done
lemma gcd_coprime_nat:
assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Mar 25 10:44:57 2015 +0100
@@ -654,7 +654,7 @@
apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def
asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def)
apply auto
-apply (drule_tac [!] s = "Some ?x" in sym)
+apply (drule_tac [!] s = "Some _" in sym)
apply auto
done
--- a/src/HOL/Hoare_Parallel/Graph.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Hoare_Parallel/Graph.thy Wed Mar 25 10:44:57 2015 +0100
@@ -287,10 +287,10 @@
apply(case_tac "length path")
apply force
apply simp
- apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE)
+ apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> P i" and x = "nat" for P in allE)
apply simp
apply clarify
- apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
+ apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> P i" and x = "nat" for P in allE)
apply simp
apply(case_tac "j<I")
apply(erule_tac x = "j" in allE)
@@ -329,10 +329,10 @@
apply(case_tac "length path")
apply force
apply simp
- apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE)
+ apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> P i" and x = "nat" for P in allE)
apply simp
apply clarify
- apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
+ apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> P i" and x = "nat" for P in allE)
apply simp
apply(case_tac "j\<le>R")
apply(drule le_imp_less_or_eq [of _ R])
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Mar 25 10:44:57 2015 +0100
@@ -441,7 +441,7 @@
apply simp
apply force
apply simp
- apply(erule_tac V = "\<forall>i. ?P i" in thin_rl)
+ apply(erule_tac V = "\<forall>i. P i" for P in thin_rl)
apply(drule_tac s = "length Rs" in sym)
apply(erule allE, erule impE, assumption)
apply(force dest: nth_mem simp add: All_None_def)
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Mar 25 10:44:57 2015 +0100
@@ -186,7 +186,7 @@
apply force
apply clarify
apply(erule_tac x="Suc ia" in allE,simp)
-apply(erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (?J j) \<notin> ctran" in allE,simp)
+apply(erule_tac x="0" and P="\<lambda>j. H j \<longrightarrow> (J j) \<notin> ctran" for H J in allE,simp)
done
lemma etran_or_ctran2 [rule_format]:
@@ -241,14 +241,14 @@
apply(case_tac k,simp,simp)
apply(case_tac j,simp)
apply(erule_tac x=0 in allE)
- apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (?J j)" in allE,simp)
+ apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (J j)" for J in allE,simp)
apply(subgoal_tac "t\<in>p")
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)")
apply clarify
- apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
+ apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
apply clarify
- apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
- apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran \<longrightarrow> ?T j" in allE,simp)
+ 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)
+ 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)
apply(simp(no_asm_use) only:stable_def)
apply(erule_tac x=s in allE)
apply(erule_tac x=t in allE)
@@ -258,23 +258,23 @@
apply(rule Env)
apply simp
apply(erule_tac x="nata" in allE)
- apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
+ apply(erule_tac x="nat" and P="\<lambda>j. (s\<le>j) \<longrightarrow> (J j)" for s J in allE,simp)
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)")
apply clarify
- apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
+ apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
apply clarify
- apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
+ 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)
apply(case_tac k,simp,simp)
apply(case_tac j)
- apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
+ apply(erule_tac x=0 and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
apply(erule etran.cases,simp)
apply(erule_tac x="nata" in allE)
-apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp)
+apply(erule_tac x="nat" and P="\<lambda>j. (s\<le>j) \<longrightarrow> (J j)" for s J in allE,simp)
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)")
apply clarify
- apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp)
+ apply(erule_tac x="Suc i" and P="\<lambda>j. (H j) \<longrightarrow> (J j)\<in>etran" for H J in allE,simp)
apply clarify
-apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp)
+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)
done
subsection \<open>Soundness of the System for Component Programs\<close>
@@ -341,7 +341,7 @@
apply(case_tac "x!i")
apply clarify
apply(drule_tac s="Some (Basic f)" in sym,simp)
- apply(thin_tac "\<forall>j. ?H j")
+ apply(thin_tac "\<forall>j. H j" for H)
apply(force elim:ctran.cases)
apply clarify
apply(simp add:cp_def)
@@ -468,7 +468,7 @@
apply(drule_tac c=l in subsetD)
apply (simp add:cp_def)
apply clarify
- apply(erule_tac x=ia and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
+ 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)
apply(erule etranE,simp)
apply simp
apply clarify
@@ -499,7 +499,7 @@
apply(drule_tac c=l in subsetD)
apply (simp add:cp_def)
apply clarify
- apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp)
+ 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)
apply(erule etranE,simp)
apply simp
apply clarify
@@ -532,7 +532,7 @@
apply(erule_tac m="length x" in etran_or_ctran,simp+)
apply(case_tac x, (simp add:last_length)+)
apply(erule exE)
-apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
+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)
apply clarify
apply (simp add:assum_def)
apply(frule_tac j=0 and k="m" and p=pre in stability,simp+)
@@ -549,7 +549,7 @@
apply(erule disjE)
apply(erule_tac x=i in allE, erule impE, assumption)
apply simp+
- apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
+ 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)
apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
apply(rotate_tac -2)
@@ -569,7 +569,7 @@
apply(erule_tac x=i in allE, erule impE, assumption)
apply simp
apply simp
-apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
+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)
apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
apply(rotate_tac -2)
@@ -713,14 +713,14 @@
apply(drule_tac c=xs in subsetD,simp add:cp_def cptn_iff_cptn_mod)
apply(simp add:assum_def)
apply clarify
- apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
+ apply(erule_tac P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> I j" for H J I in allE,erule impE, assumption)
apply(simp add:snd_lift)
apply(erule mp)
apply(force elim:etranE intro:Env simp add:lift_def)
apply(simp add:comm_def)
apply(rule conjI)
apply clarify
- apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption)
+ apply(erule_tac P="\<lambda>j. H j \<longrightarrow> J j \<longrightarrow> I j" for H J I in allE,erule impE, assumption)
apply(simp add:snd_lift)
apply(erule mp)
apply(case_tac "(xs!i)")
@@ -914,7 +914,7 @@
apply clarify
apply (simp add:last_length)
--\<open>WhileOne\<close>
-apply(thin_tac "P = While b P \<longrightarrow> ?Q")
+apply(thin_tac "P = While b P \<longrightarrow> Q" for Q)
apply(rule ctran_in_comm,simp)
apply(simp add:Cons_lift del:list.map)
apply(simp add:comm_def del:list.map)
@@ -957,7 +957,7 @@
apply(simp only:last_lift_not_None)
apply simp
--\<open>WhileMore\<close>
-apply(thin_tac "P = While b P \<longrightarrow> ?Q")
+apply(thin_tac "P = While b P \<longrightarrow> Q" for Q)
apply(rule ctran_in_comm,simp del:last.simps)
--\<open>metiendo la hipotesis antes de dividir la conclusion.\<close>
apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \<in> assum (pre, rely)")
@@ -979,7 +979,7 @@
apply simp
apply simp
apply(simp add:snd_lift del:list.map last.simps)
- apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> ?P i")
+ apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> P i" for P)
apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod)
apply(erule_tac x=sa in allE)
apply(drule_tac c="(Some P, sa) # xs" in subsetD)
@@ -1111,13 +1111,13 @@
apply simp
apply(erule exE)
--\<open>the first c-tran that does not satisfy the guarantee-condition is from @{text "\<sigma>_i"} at step @{text "m"}.\<close>
-apply(drule_tac n=j and P="\<lambda>j. \<exists>i. ?H i j" in Ex_first_occurrence)
+apply(drule_tac n=j and P="\<lambda>j. \<exists>i. H i j" for H in Ex_first_occurrence)
apply(erule exE)
apply clarify
--\<open>@{text "\<sigma>_i \<in> A(pre, rely_1)"}\<close>
apply(subgoal_tac "take (Suc (Suc m)) (clist!i) \<in> assum(Pre(xs!i), Rely(xs!i))")
--\<open>but this contradicts @{text "\<Turnstile> \<sigma>_i sat [pre_i,rely_i,guar_i,post_i]"}\<close>
- 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)
+ 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)
apply(simp add:com_validity_def)
apply(erule_tac x=s in allE)
apply(simp add:cp_def comm_def)
@@ -1126,40 +1126,40 @@
apply (blast intro: takecptn_is_cptn)
apply simp
apply clarify
- apply(erule_tac x=m and P="\<lambda>j. ?I j \<and> ?J j \<longrightarrow> ?H j" in allE)
+ apply(erule_tac x=m and P="\<lambda>j. I j \<and> J j \<longrightarrow> H j" for I J H in allE)
apply (simp add:conjoin_def same_length_def)
apply(simp add:assum_def)
apply(rule conjI)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<in>cp (?K j) (?J j)" in allE)
+ 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)
apply(simp add:cp_def par_assum_def)
apply(drule_tac c="s" in subsetD,simp)
apply simp
apply clarify
-apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?M \<union> UNION (?S j) (?T j) \<subseteq> (?L j)" in allE)
+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)
apply simp
apply(erule subsetD)
apply simp
apply(simp add:conjoin_def compat_label_def)
apply clarify
-apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?P j) \<or> ?Q j" in allE,simp)
+apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (P j) \<or> Q j" for H P Q in allE,simp)
--\<open>each etran in @{text "\<sigma>_1[0\<dots>m]"} corresponds to\<close>
apply(erule disjE)
--\<open>a c-tran in some @{text "\<sigma>_{ib}"}\<close>
apply clarify
apply(case_tac "i=ib",simp)
apply(erule etranE,simp)
- apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE)
+ apply(erule_tac x="ib" and P="\<lambda>i. H i \<longrightarrow> (I i) \<or> (J i)" for H I J in allE)
apply (erule etranE)
apply(case_tac "ia=m",simp)
apply simp
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE)
+ apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (\<forall>i. P i j)" for H P in allE)
apply(subgoal_tac "ia<m",simp)
prefer 2
apply arith
- apply(erule_tac x=ib and P="\<lambda>j. (?I j, ?H j)\<in> ctran \<longrightarrow> (?P i j)" in allE,simp)
+ 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)
apply(simp add:same_state_def)
- 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)
- 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)
+ 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)
+ 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)
--\<open>or an e-tran in @{text "\<sigma>"},
therefore it satisfies @{text "rely \<or> guar_{ib}"}\<close>
apply (force simp add:par_assum_def same_state_def)
@@ -1181,19 +1181,19 @@
apply clarify
apply(simp add:conjoin_def compat_label_def)
apply clarify
-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)
+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)
apply(erule disjE)
prefer 2
apply(force simp add:same_state_def par_assum_def)
apply clarify
apply(case_tac "i=ia",simp)
apply(erule etranE,simp)
-apply(erule_tac x="ia" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp)
-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)
-apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
+apply(erule_tac x="ia" and P="\<lambda>i. H i \<longrightarrow> (I i) \<or> (J i)" for H I J in allE,simp)
+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)
+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)
apply(simp add:same_state_def)
-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)
-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)
+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)
+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)
done
lemma four:
@@ -1224,18 +1224,18 @@
apply assumption
apply(simp add:conjoin_def same_program_def)
apply clarify
-apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in all_dupE)
-apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE)
+apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in all_dupE)
+apply(erule_tac x="Suc i" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE)
apply(erule par_ctranE,simp)
-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)
-apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
+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)
+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)
apply(rule_tac x=ia in exI)
apply(simp add:same_state_def)
-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)
-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)
-apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
-apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE,simp)
-apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
+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)
+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)
+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)
+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)
+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)
apply(erule mp)
apply(subgoal_tac "r=fst(clist ! ia ! Suc i)",simp)
apply(drule_tac i=ia in list_eq_if)
@@ -1266,17 +1266,17 @@
apply simp
apply clarify
apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))")
- 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)
+ 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)
apply(simp add:com_validity_def)
apply(erule_tac x=s in allE)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?I j) \<in> cp (?J j) s" in allE,simp)
+ 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)
apply(drule_tac c="clist!i" in subsetD)
apply (force simp add:Com_def)
apply(simp add:comm_def conjoin_def same_program_def del:last.simps)
apply clarify
- apply(erule_tac x="length x - 1" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE)
+ 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)
apply (simp add:All_None_def same_length_def)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> length(?J j)=(?K j)" in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> length(J j)=(K j)" for H J K in allE)
apply(subgoal_tac "length x - 1 < length x",simp)
apply(case_tac "x\<noteq>[]")
apply(simp add: last_conv_nth)
@@ -1297,8 +1297,8 @@
apply(rule conjI)
apply(simp add:conjoin_def same_state_def par_cp_def)
apply clarify
- 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)
- apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
+ 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)
+ apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
apply(case_tac x,simp+)
apply (simp add:par_assum_def)
apply clarify
--- a/src/HOL/Hoare_Parallel/RG_Tran.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Wed Mar 25 10:44:57 2015 +0100
@@ -494,7 +494,7 @@
apply(clarify)
apply(simp add:conjoin_def compat_label_def)
apply clarify
-apply(erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (?P j \<or> ?Q j)" in all_dupE,simp)
+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)
apply(erule disjE)
--\<open>first step is a Component step\<close>
apply clarify
@@ -504,14 +504,14 @@
prefer 2
apply(simp add: same_state_def)
apply(erule_tac x=i in allE,erule impE,assumption,
- erule_tac x=1 and P="\<lambda>j. (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
+ erule_tac x=1 and P="\<lambda>j. (H j) \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE, simp)
prefer 2
apply(simp add:same_program_def)
- apply(erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp)
+ apply(erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (fst (s j))=(t j)" for H s t in allE,simp)
apply(rule nth_equalityI,simp)
apply clarify
apply(case_tac "i=ia",simp,simp)
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
+ apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
apply(drule_tac t=i in not_sym,simp)
apply(erule etranE,simp)
apply(rule ParCptnComp)
@@ -532,8 +532,8 @@
apply(force simp add:same_length_def length_Suc_conv)
apply(simp add:same_state_def)
apply(erule_tac x=ia in allE, erule impE, assumption,
- erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
+ erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
+ apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
apply(drule_tac t=i in not_sym,simp)
apply(erule etranE,simp)
apply(erule allE,erule impE,assumption,erule tl_in_cptn)
@@ -543,7 +543,7 @@
apply clarify
apply(case_tac j,simp,simp)
apply(erule_tac x=ia in allE, erule impE, assumption,
- erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
+ 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)
apply(force simp add:same_length_def length_Suc_conv)
apply(rule conjI)
apply(simp add:same_program_def)
@@ -552,11 +552,11 @@
apply(rule nth_equalityI,simp)
apply clarify
apply(case_tac "i=ia",simp,simp)
- apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp)
+ 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)
apply(rule nth_equalityI,simp,simp)
apply(force simp add:length_Suc_conv)
apply(rule allI,rule impI)
- apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<or> ?J j)" in allE,simp)
+ 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)
apply(erule disjE)
apply clarify
apply(rule_tac x=ia in exI,simp)
@@ -564,13 +564,13 @@
apply(rule conjI)
apply(force simp add: length_Suc_conv)
apply clarify
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption)
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption)
+ 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)
+ 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)
apply simp
apply(case_tac j,simp)
apply(rule tl_zero)
apply(erule_tac x=l in allE, erule impE, assumption,
- erule_tac x=1 and P="\<lambda>j. (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
+ erule_tac x=1 and P="\<lambda>j. (H j) \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
apply(force elim:etranE intro:Env)
apply force
apply force
@@ -585,8 +585,8 @@
apply(rule nth_tl_if)
apply force
apply(erule_tac x=ia in allE, erule impE, assumption,
- erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
+ erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
+ apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
apply(drule_tac t=i in not_sym,simp)
apply(erule etranE,simp)
apply(erule tl_zero)
@@ -595,41 +595,41 @@
apply clarify
apply(case_tac "i=l",simp)
apply(rule nth_tl_if)
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply simp
- apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption,erule impE,assumption)
+ 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)
apply(erule tl_zero,force)
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply(rule nth_tl_if)
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply(erule_tac x=l in allE, erule impE, assumption,
- erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp)
+ erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
+ 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)
apply(erule etranE,simp)
apply(rule tl_zero)
apply force
apply force
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply(rule disjI2)
apply(case_tac j,simp)
apply clarify
apply(rule tl_zero)
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j\<in>etran" in allE,erule impE, assumption)
+ apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j\<in>etran" for H I in allE,erule impE, assumption)
apply(case_tac "i=ia",simp,simp)
apply(erule_tac x=ia in allE, erule impE, assumption,
- erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp)
+ erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
+ 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)
apply(force elim:etranE intro:Env)
apply force
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply simp
apply clarify
apply(rule tl_zero)
apply(rule tl_zero,force)
apply force
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply force
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
--\<open>first step is an environmental step\<close>
apply clarify
apply(erule par_etran.cases)
@@ -641,24 +641,24 @@
apply(rule_tac x="map tl clist" in exI,simp)
apply(rule conjI)
apply clarify
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?I ?s j) \<in> cptn" in allE,simp)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> I j \<in> cptn" for H I in allE,simp)
apply(erule cptn.cases)
apply(simp add:same_length_def)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply(simp add:same_state_def)
apply(erule_tac x=i in allE, erule impE, assumption,
- erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<in>etran" in allE,simp)
+ erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> J j \<in>etran" for H J in allE,simp)
apply(erule etranE,simp)
apply(simp add:same_state_def same_length_def)
apply(rule conjI,clarify)
apply(case_tac j,simp,simp)
apply(erule_tac x=i in allE, erule impE, assumption,
- erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
+ 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)
apply(rule tl_zero)
apply(simp)
apply force
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply(rule conjI)
apply(simp add:same_program_def)
apply clarify
@@ -666,52 +666,52 @@
apply(rule nth_equalityI,simp)
apply clarify
apply simp
- apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp)
+ 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)
apply(rule nth_equalityI,simp,simp)
apply(force simp add:length_Suc_conv)
apply(rule allI,rule impI)
-apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<or> ?J j)" in allE,simp)
+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)
apply(erule disjE)
apply clarify
apply(rule_tac x=i in exI,simp)
apply(rule conjI)
- apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
+ apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
apply(erule etranE,simp)
apply(erule_tac x=i in allE, erule impE, assumption,
- erule_tac x=1 and P="\<lambda>j. (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
+ erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
apply(rule nth_tl_if)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply simp
apply(erule tl_zero,force)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply clarify
- apply(erule_tac x=l and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
+ apply(erule_tac x=l and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
apply(erule etranE,simp)
apply(erule_tac x=l in allE, erule impE, assumption,
- erule_tac x=1 and P="\<lambda>j. (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
+ erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
apply(rule nth_tl_if)
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply simp
apply(rule tl_zero,force)
apply force
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply(rule disjI2)
apply simp
apply clarify
apply(case_tac j,simp)
apply(rule tl_zero)
- apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
- apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
+ apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
+ apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
apply(force elim:etranE intro:Env)
apply force
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply simp
apply(rule tl_zero)
apply(rule tl_zero,force)
apply force
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply force
-apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
done
lemma aux_onlyif [rule_format]: "\<forall>xs s. (xs, s)#ys \<in> par_cptn \<longrightarrow>
@@ -769,7 +769,7 @@
apply clarify
apply(case_tac "i=ia",simp)
apply(erule CptnComp)
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<in> cptn)" in allE,simp)
+ apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (I j \<in> cptn)" for H I in allE,simp)
apply simp
apply(erule_tac x=ia in allE)
apply(rule CptnEnv,simp)
@@ -790,7 +790,7 @@
apply(rule nth_equalityI,simp,simp)
apply simp
apply(rule nth_equalityI,simp,simp)
- apply(erule_tac x=nat and P="\<lambda>j. ?H j \<longrightarrow> (fst (?a j))=((?b j))" in allE)
+ apply(erule_tac x=nat and P="\<lambda>j. H j \<longrightarrow> (fst (a j))=((b j))" for H a b in allE)
apply(case_tac nat)
apply clarify
apply(case_tac "i=ia",simp,simp)
@@ -806,7 +806,7 @@
apply clarify
apply(rule Env)
apply simp
-apply(erule_tac x=nat and P="\<lambda>j. ?H j \<longrightarrow> (?P j \<or> ?Q j)" in allE,simp)
+apply(erule_tac x=nat and P="\<lambda>j. H j \<longrightarrow> (P j \<or> Q j)" for H P Q in allE,simp)
apply(erule disjE)
apply clarify
apply(rule_tac x=ia in exI,simp)
@@ -819,7 +819,7 @@
apply simp
apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp)
apply clarify
-apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?P j)\<in>etran" in allE, erule impE, assumption)
+apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (P j)\<in>etran" for H P in allE, erule impE, assumption)
apply(case_tac "i=ia",simp,simp)
done
@@ -851,28 +851,28 @@
apply(erule cptn.cases,force,force,force)
apply(simp add:par_cp_def conjoin_def same_length_def same_program_def same_state_def compat_label_def)
apply clarify
- apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in all_dupE)
+ apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in all_dupE)
apply(subgoal_tac "a = xs")
apply(subgoal_tac "b = s",simp)
prefer 3
- apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=((?t j))" in allE)
+ apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (fst (s j))=((t j))" for H s t in allE)
apply (simp add:cp_def)
apply(rule nth_equalityI,simp,simp)
prefer 2
apply(erule_tac x=0 in allE)
apply (simp add:cp_def)
- 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)
- apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
+ 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)
+ 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)
apply(erule_tac x=list in allE)
apply(rule_tac x="map tl clist" in exI,simp)
apply(rule conjI)
apply clarify
apply(case_tac j,simp)
apply(erule_tac x=i in allE, erule impE, assumption,
- erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
+ erule_tac x="0" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
apply(erule_tac x=i in allE, erule impE, assumption,
- erule_tac x="Suc nat" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ erule_tac x="Suc nat" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!i",simp,simp)
apply(rule conjI)
apply clarify
@@ -883,9 +883,9 @@
apply(simp add:cp_def)
apply clarify
apply simp
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!i",simp,simp)
- apply(thin_tac "?H = (\<exists>i. ?J i)")
+ apply(thin_tac "H = (\<exists>i. J i)" for H J)
apply(rule conjI)
apply clarify
apply(erule_tac x=j in allE,erule impE, assumption,erule disjE)
@@ -895,34 +895,34 @@
apply(rule conjI)
apply(erule_tac x=i in allE)
apply(simp add:cp_def)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!i",simp,simp)
apply clarify
apply(erule_tac x=l in allE)
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
apply clarify
apply(simp add:cp_def)
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!l",simp,simp)
apply simp
apply(rule conjI)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!i",simp,simp)
apply clarify
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!l",simp,simp)
apply clarify
apply(erule_tac x=i in allE)
apply(simp add:cp_def)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!i",simp)
apply(rule nth_tl_if,simp,simp)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?P j)\<in>etran" in allE, erule impE, assumption,simp)
+ 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)
apply(simp add:cp_def)
apply clarify
apply(rule nth_tl_if)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!i",simp,simp)
apply force
apply force
@@ -940,14 +940,14 @@
apply clarify
apply(unfold same_length_def)
apply clarify
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,simp)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,simp)
apply(rule conjI)
apply(simp add:same_state_def)
apply clarify
apply(erule_tac x=i in allE, erule impE, assumption,
- erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
+ erule_tac x=j and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
apply(case_tac j,simp)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!i",simp,simp)
apply(rule conjI)
apply(simp add:same_program_def)
@@ -955,7 +955,7 @@
apply(rule nth_equalityI,simp,simp)
apply(case_tac j,simp)
apply clarify
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!i",simp,simp)
apply clarify
apply(simp add:compat_label_def)
@@ -967,13 +967,13 @@
apply(rule conjI)
apply(erule_tac x=i in allE)
apply(case_tac j,simp)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!i",simp,simp)
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!i",simp,simp)
apply clarify
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
- apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
+ apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
apply(case_tac "clist!l",simp,simp)
apply(erule_tac x=l in allE,simp)
apply(rule disjI2)
@@ -982,9 +982,9 @@
apply(case_tac j,simp,simp)
apply(rule tl_zero,force)
apply force
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply force
- apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
+ apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
apply clarify
apply(erule_tac x=i in allE)
apply(simp add:cp_def)
--- a/src/HOL/IMPP/EvenOdd.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/IMPP/EvenOdd.thy Wed Mar 25 10:44:57 2015 +0100
@@ -91,7 +91,7 @@
apply (rule hoare_derivs.Comp)
apply (rule_tac [2] hoare_derivs.Ass)
apply clarsimp
-apply (rule_tac Q = "%Z s. ?P Z s & Res_ok Z s" in hoare_derivs.Comp)
+apply (rule_tac Q = "%Z s. P Z s & Res_ok Z s" and P = P for P in hoare_derivs.Comp)
apply (rule export_s)
apply (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12])
apply (rule single_asm [THEN conseq2])
--- a/src/HOL/IMPP/Hoare.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/IMPP/Hoare.thy Wed Mar 25 10:44:57 2015 +0100
@@ -286,7 +286,7 @@
apply (blast) (* cut *)
apply (blast) (* weaken *)
apply (tactic {* ALLGOALS (EVERY'
- [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs ?x ?y" [],
+ [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs _ _" [],
simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *})
apply (simp_all (no_asm_use) add: triple_valid_def2)
apply (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *)
@@ -315,7 +315,7 @@
apply (unfold MGT_def)
apply (erule conseq12)
apply auto
-apply (case_tac "? t. <c,?s> -c-> t")
+apply (case_tac "\<exists>t. <c,s> -c-> t" for s)
apply (fast elim: com_det)
apply clarsimp
apply (drule single_stateE)
--- a/src/HOL/IMPP/Natural.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/IMPP/Natural.thy Wed Mar 25 10:44:57 2015 +0100
@@ -105,7 +105,7 @@
(* evaluation of com is deterministic *)
lemma com_det [rule_format (no_asm)]: "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"
apply (erule evalc.induct)
-apply (erule_tac [8] V = "<?c,s1> -c-> s2" in thin_rl)
+apply (erule_tac [8] V = "<c,s1> -c-> s2" for c in thin_rl)
apply (blast elim: evalc_WHILE_case)+
done
--- a/src/HOL/Induct/Com.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Induct/Com.thy Wed Mar 25 10:44:57 2015 +0100
@@ -184,7 +184,7 @@
apply blast
apply blast
apply (blast elim: exec_WHILE_case)
-apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
+apply (erule_tac V = "(c,s2) -[ev]-> s3" for c ev in thin_rl)
apply clarify
apply (erule exec_WHILE_case, blast+)
done
--- a/src/HOL/Library/Multiset.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Mar 25 10:44:57 2015 +0100
@@ -1658,7 +1658,7 @@
apply (simp (no_asm))
apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
apply (simp (no_asm_simp) add: add.assoc [symmetric])
- apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong)
+ apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong)
apply (simp add: diff_union_single_conv)
apply (simp (no_asm_use) add: trans_def)
apply blast
@@ -1669,7 +1669,7 @@
apply (rule conjI)
apply (simp add: multiset_eq_iff split: nat_diff_split)
apply (rule conjI)
- apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong, simp)
+ apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong, simp)
apply (simp add: multiset_eq_iff split: nat_diff_split)
apply (simp (no_asm_use) add: trans_def)
apply blast
@@ -1692,7 +1692,7 @@
apply (simp add: mult1_def set_of_def, blast)
txt {* Now we know @{term "J' \<noteq> {#}"}. *}
apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
-apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
+apply (erule_tac P = "\<forall>k \<in> set_of K. P k" for P in rev_mp)
apply (erule ssubst)
apply (simp add: Ball_def, auto)
apply (subgoal_tac
--- a/src/HOL/MicroJava/DFA/Listn.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy Wed Mar 25 10:44:57 2015 +0100
@@ -345,7 +345,7 @@
apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs:M}" in allE)
apply (erule impE)
apply blast
-apply (thin_tac "\<exists>x xs. ?P x xs")
+apply (thin_tac "\<exists>x xs. P x xs" for P)
apply clarify
apply (rename_tac maxA xs)
apply (erule_tac x = "{ys. size ys = size xs \<and> maxA#ys \<in> M}" in allE)
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Wed Mar 25 10:44:57 2015 +0100
@@ -137,20 +137,20 @@
apply( clarsimp)
apply( drule (3) Call_lemma)
apply( clarsimp simp add: wf_java_mdecl_def)
-apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
+apply( erule_tac V = "method sig x = y" for sig x y in thin_rl)
apply( drule spec, erule impE, erule_tac [2] notE impE, tactic "assume_tac @{context} 2")
apply( rule conformsI)
apply( erule conforms_heapD)
apply( rule lconf_ext)
apply( force elim!: Call_lemma2)
apply( erule conf_hext, erule (1) conf_obj_AddrI)
-apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl)
+apply( erule_tac V = "E\<turnstile>blk\<surd>" for E blk in thin_rl)
apply (simp add: conforms_def)
apply( erule conjE)
apply( drule spec, erule (1) impE)
apply( drule spec, erule (1) impE)
-apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl)
+apply( erule_tac V = "E\<turnstile>res::rT" for E rT in thin_rl)
apply( clarify)
apply( rule conjI)
apply( fast intro: hext_trans)
@@ -291,7 +291,7 @@
-- "5 While"
prefer 5
-apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
+apply(erule_tac V = "a \<longrightarrow> b" for a b in thin_rl)
apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
apply(force elim: hext_trans)
--- a/src/HOL/MicroJava/J/WellForm.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Wed Mar 25 10:44:57 2015 +0100
@@ -419,7 +419,7 @@
apply( simp)
apply( drule map_add_SomeD)
apply( erule disjE)
-apply( erule_tac V = "?P --> ?Q" in thin_rl)
+apply( erule_tac V = "P --> Q" for P Q in thin_rl)
apply (frule map_of_SomeD)
apply (clarsimp simp add: wf_cdecl_def)
apply( clarify)
@@ -454,7 +454,7 @@
apply( simp)
apply( drule map_add_SomeD)
apply( erule disjE)
-apply( erule_tac V = "?P --> ?Q" in thin_rl)
+apply( erule_tac V = "P --> Q" for P Q in thin_rl)
apply (frule map_of_SomeD)
apply (clarsimp simp add: ws_cdecl_def)
apply blast
@@ -486,7 +486,7 @@
apply( assumption)
apply( unfold map_add_def)
apply( simp (no_asm_simp) add: wf_prog_ws_prog del: split_paired_Ex)
-apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
+apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, C, m)) ms) sig = Some z" for C)
apply( erule exE)
apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
prefer 2
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Mar 25 10:44:57 2015 +0100
@@ -6703,7 +6703,7 @@
moreover have "?d > 0"
using as(2) by (auto simp: Suc_le_eq DIM_positive)
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"
- apply (rule_tac x="min (Min ((op \<bullet> x) ` Basis)) ?D" in exI)
+ apply (rule_tac x="min (Min ((op \<bullet> x) ` Basis)) D" for D in exI)
apply rule
defer
apply (rule, rule)
--- a/src/HOL/NanoJava/Equivalence.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy Wed Mar 25 10:44:57 2015 +0100
@@ -105,8 +105,8 @@
apply (rule hoare_ehoare.induct)
(*18*)
apply (tactic {* ALLGOALS (REPEAT o dresolve_tac @{context} [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
-apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare ?x ?y" []) *})
-apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare ?x ?y" []) *})
+apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare _ _" []) *})
+apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare _ _" []) *})
apply (simp_all only: cnvalid1_eq cenvalid_def2)
apply fast
apply fast
--- a/src/HOL/Nominal/Examples/Standardization.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy Wed Mar 25 10:44:57 2015 +0100
@@ -384,7 +384,7 @@
apply (subgoal_tac "r = (Lam [xa]. [(xa, x)] \<bullet> s)")
prefer 2
apply (simp add: calc_atm)
- apply (thin_tac "r = ?t")
+ apply (thin_tac "r = _")
apply simp
apply (rule exI)
apply (rule conjI)
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Mar 25 10:44:57 2015 +0100
@@ -771,7 +771,7 @@
==> Nonce N \<notin> analz (knows Spy evs) -->
(\<exists>k i W. Says (Cardholder k) (CA i) {|U,W|} \<in> set evs &
Cardholder k \<notin> bad & CA i \<notin> bad)"
-apply (erule_tac P = "U \<in> ?H" in rev_mp)
+apply (erule_tac P = "U \<in> H" for H in rev_mp)
apply (erule set_cr.induct)
apply (valid_certificate_tac [8]) --{*for message 5*}
apply (simp_all del: image_insert image_Un imp_disjL
--- a/src/HOL/UNITY/Comp.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/UNITY/Comp.thy Wed Mar 25 10:44:57 2015 +0100
@@ -186,7 +186,7 @@
apply simp
apply (subgoal_tac "G \<in> preserves (funPair v w) ")
prefer 2 apply simp
-apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD],
+apply (drule_tac P1 = "split Q" for Q in preserves_subset_stable [THEN subsetD],
auto)
done
@@ -198,8 +198,8 @@
(*The G case remains*)
apply (auto simp add: preserves_def stable_def constrains_def)
(*We have a G-action, so delete assumptions about F-actions*)
-apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
-apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)
+apply (erule_tac V = "\<forall>act \<in> Acts F. P act" for P in thin_rl)
+apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. P z act" for P in thin_rl)
apply (subgoal_tac "v x = v xa")
apply auto
apply (erule order_trans, blast)
--- a/src/HOL/UNITY/Comp/Alloc.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Wed Mar 25 10:44:57 2015 +0100
@@ -1080,7 +1080,7 @@
text{*Could go to Extend.ML*}
lemma bij_fst_inv_inv_eq: "bij f ==> fst (inv (%(x, u). inv f x) z) = f z"
apply (rule fst_inv_equalityI)
- apply (rule_tac f = "%z. (f z, ?h z) " in surjI)
+ apply (rule_tac f = "%z. (f z, h z)" for h in surjI)
apply (simp add: bij_is_inj inv_f_f)
apply (simp add: bij_is_surj surj_f_inv_f)
done
--- a/src/HOL/UNITY/ELT.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/UNITY/ELT.thy Wed Mar 25 10:44:57 2015 +0100
@@ -63,7 +63,7 @@
lemma givenBy_eq_all: "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}"
apply (unfold givenBy_def, safe)
-apply (rule_tac [2] x = "v ` ?u" in image_eqI, auto)
+apply (rule_tac [2] x = "v ` _" in image_eqI, auto)
done
lemma givenByI: "(!!x y. [| x:A; v x = v y |] ==> y: A) ==> A: givenBy v"
@@ -101,7 +101,7 @@
"[| A : givenBy v; B : givenBy v |] ==> A-B : givenBy v"
apply (simp (no_asm_use) add: givenBy_eq_Collect)
apply safe
-apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI)
+apply (rule_tac x = "%z. R z & ~ Q z" for R Q in exI)
unfolding set_diff_eq
apply auto
done
--- a/src/HOL/UNITY/Guar.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/UNITY/Guar.thy Wed Mar 25 10:44:57 2015 +0100
@@ -349,7 +349,7 @@
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =
(F \<in> welldef \<inter> X --> G \<in> X)"
apply (unfold strict_ex_prop_def, safe)
-apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
+apply (erule_tac x = SKIP and P = "%H. PP H --> RR H" for PP RR in allE)
apply (auto dest: Join_welldef_D1 Join_welldef_D2)
done
@@ -372,7 +372,7 @@
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =
(F \<in> welldef \<inter> X --> G \<in> X)"
apply (unfold strict_uv_prop_def, safe)
-apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
+apply (erule_tac x = SKIP and P = "%H. PP H --> RR H" for PP RR in allE)
apply (auto dest: Join_welldef_D1 Join_welldef_D2)
done
--- a/src/HOL/UNITY/ProgressSets.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy Wed Mar 25 10:44:57 2015 +0100
@@ -383,7 +383,7 @@
apply (drule equalityD1)
apply (rule subset_trans)
prefer 2 apply assumption
-apply (thin_tac "?U \<subseteq> X")
+apply (thin_tac "_ \<subseteq> X")
apply (cut_tac A=X in UN_singleton)
apply (erule subst)
apply (simp only: cl_UN lattice_latticeof
--- a/src/HOL/UNITY/Project.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/UNITY/Project.thy Wed Mar 25 10:44:57 2015 +0100
@@ -410,7 +410,7 @@
prefer 2
apply (simp add: stable_def constrains_def, blast)
(*back to main goal*)
-apply (erule_tac V = "?AA \<subseteq> -C \<union> ?BB" in thin_rl)
+apply (erule_tac V = "AA \<subseteq> -C \<union> BB" for AA BB in thin_rl)
apply (drule bspec, assumption)
apply (simp add: extend_set_def project_act_def, blast)
done
--- a/src/HOL/UNITY/Transformers.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/UNITY/Transformers.thy Wed Mar 25 10:44:57 2015 +0100
@@ -139,7 +139,7 @@
"[|T-B \<subseteq> awp F T; act \<in> Acts F|]
==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
apply (rule subset_wens)
-apply (rule_tac P="\<lambda>x. ?f x \<subseteq> ?b" in ssubst [OF wens_unfold])
+apply (rule_tac P="\<lambda>x. f x \<subseteq> b" for f b in ssubst [OF wens_unfold])
apply (simp add: wp_def awp_def, blast)
done
--- a/src/HOL/Wellfounded.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Wellfounded.thy Wed Mar 25 10:44:57 2015 +0100
@@ -232,7 +232,7 @@
prefer 2 apply blast
apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
apply assumption
-apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl)
+apply (erule_tac V = "ALL Q. (EX x. x : Q) --> P Q" for P in thin_rl)
--{*essential for speed*}
txt{*Blast with new substOccur fails*}
apply (fast intro: converse_rtrancl_into_rtrancl)
--- a/src/HOL/Word/Bit_Representation.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Wed Mar 25 10:44:57 2015 +0100
@@ -224,7 +224,7 @@
apply (erule conjI)
apply (drule_tac x=0 in fun_cong, force)
apply (rule ext)
- apply (drule_tac x="Suc ?x" in fun_cong, force)
+ apply (drule_tac x="Suc x" for x in fun_cong, force)
done
show ?thesis
by (auto elim: bin_nth_lem)
--- a/src/HOL/Word/Misc_Typedef.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Word/Misc_Typedef.thy Wed Mar 25 10:44:57 2015 +0100
@@ -194,7 +194,7 @@
prefer 2
apply (simp add: comp_assoc)
apply (rule ext)
- apply (drule_tac f="?a o ?b" in fun_cong)
+ apply (drule_tac f="a o b" for a b in fun_cong)
apply simp
done
--- a/src/HOL/Word/Word.thy Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Word/Word.thy Wed Mar 25 10:44:57 2015 +0100
@@ -3190,7 +3190,7 @@
apply clarsimp
apply (case_tac x, force)
apply (case_tac m, auto)
- apply (drule_tac t="length ?xs" in sym)
+ apply (drule_tac t="length xs" for xs in sym)
apply (clarsimp simp: map2_def zip_replicate o_def)
done
@@ -3203,7 +3203,7 @@
apply clarsimp
apply (case_tac x, force)
apply (case_tac m, auto)
- apply (drule_tac t="length ?xs" in sym)
+ apply (drule_tac t="length xs" for xs in sym)
apply (clarsimp simp: map2_def zip_replicate o_def map_replicate_const)
done
@@ -3811,7 +3811,7 @@
lemma word_split_cat_alt:
"w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
- apply (case_tac "word_split ?w")
+ apply (case_tac "word_split w")
apply (rule trans, assumption)
apply (drule test_bit_split)
apply safe
@@ -4694,7 +4694,7 @@
apply simp
apply (case_tac "1 + (n - m) = 0")
apply (simp add: word_rec_0)
- apply (rule_tac f = "word_rec ?a ?b" in arg_cong)
+ apply (rule_tac f = "word_rec a b" for a b in arg_cong)
apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
apply simp
apply (simp (no_asm_use))