# HG changeset patch # User wenzelm # Date 1427276697 -3600 # Node ID 22bc39064290e9f55c27c04703644dbd3a3b30e5 # Parent d3d4ec6c21efb45d073a205924b9e1eda050a0ed prefer local fixes; diff -r d3d4ec6c21ef -r 22bc39064290 src/CCL/ex/Stream.thy --- 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 \ map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))" - apply (rule_tac P = "\x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst]) + apply (rule_tac P = "\x. lhs(x) = rhs" for lhs rhs in iter2B [THEN ssubst]) apply (simp add: nmapBcons) done diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Algebra/Sylow.thy --- 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 diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Auth/KerberosIV_Gets.thy --- 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 \ set ?evs" in thin_rl) +apply (erule_tac V = "Says Aa Tgs X \ 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! *} diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Auth/Yahalom.thy --- 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 = "\KK. ?P KK" in thin_rl, clarify) +apply (erule_tac V = "\KK. P KK" for P in thin_rl, clarify) txt{*If @{prop "A \ bad"} then @{term NBa} is known, therefore @{prop "NBa \ NB"}. Previous two steps make the next step faster.*} diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Bali/AxCompl.thy --- 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) diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Bali/AxExample.thy --- 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 (\Y s Z. arr_inv (snd s))" in conseq1) prefer 2 apply clarsimp -apply (rule_tac Q' = "(\Y s Z. ?Q Y s Z)\=False\=\" in conseq2) +apply (rule_tac Q' = "(\Y s Z. Q Y s Z)\=False\=\" 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'" "\b Y ba Z vf. \Y (x,s) Z. x=None \ 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") diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Bali/AxSem.thy --- 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 \ ?Q" in thin_rl) +apply (erule_tac V = "P \ 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 diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Bali/Example.thy --- 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 *)) diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Bali/State.thy --- 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: "\Z. Z = (s::state) \ 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)) \ 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 - diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Bali/WellType.thy --- 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\e0\-PrimT Boolean" [], - Rule_Insts.thin_tac @{context} "?E,dt\e1\-?T1" [], - Rule_Insts.thin_tac @{context} "?E,dt\e2\-?T2" []] i - else Rule_Insts.thin_tac @{context} "All ?P" [] i) *}) + [Rule_Insts.thin_tac @{context} "E,dt\e0\-PrimT Boolean" [(@{binding E}, NONE, NoSyn)], + Rule_Insts.thin_tac @{context} "E,dt\e1\-T1" [(@{binding E}, NONE, NoSyn), (@{binding T1}, NONE, NoSyn)], + Rule_Insts.thin_tac @{context} "E,dt\e2\-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 diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Decision_Procs/Polynomial_List.thy --- 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))) = diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Divides.thy --- 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 P(n div k :: int)(n mod k) = (\i j. 0\j & 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) = (\i j. k0 & 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) diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/GCD.thy --- 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 \ 0" and a: "a = a' * gcd a b" and diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/HOLCF/IOA/meta_theory/Automata.thy --- 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 diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Hoare_Parallel/Graph.thy --- 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 = "\i. i < nata \ ?P i" and x = "nat" in allE) + apply(erule_tac P = "\i. i < nata \ P i" and x = "nat" for P in allE) apply simp apply clarify - apply(erule_tac P = "\i. i < Suc nat \ ?P i" and x = "nat" in allE) + apply(erule_tac P = "\i. i < Suc nat \ P i" and x = "nat" for P in allE) apply simp apply(case_tac "jR") apply(drule le_imp_less_or_eq [of _ R]) diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Hoare_Parallel/OG_Hoare.thy --- 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 = "\i. ?P i" in thin_rl) + apply(erule_tac V = "\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) diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Hoare_Parallel/RG_Hoare.thy --- 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="\j. ?H j \ (?J j) \ ctran" in allE,simp) +apply(erule_tac x="0" and P="\j. H j \ (J j) \ 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="\j. (0\j) \ (?J j)" in allE,simp) + apply(erule_tac x="nat" and P="\j. (0\j) \ (J j)" for J in allE,simp) apply(subgoal_tac "t\p") apply(subgoal_tac "(\i. i < length xs \ ((P, t) # xs) ! i -e\ xs ! i \ (snd (((P, t) # xs) ! i), snd (xs ! i)) \ rely)") apply clarify - apply(erule_tac x="Suc i" and P="\j. (?H j) \ (?J j)\etran" in allE,simp) + apply(erule_tac x="Suc i" and P="\j. (H j) \ (J j)\etran" for H J in allE,simp) apply clarify - apply(erule_tac x="Suc i" and P="\j. (?H j) \ (?J j) \ (?T j)\rely" in allE,simp) - apply(erule_tac x=0 and P="\j. (?H j) \ (?J j)\etran \ ?T j" in allE,simp) + apply(erule_tac x="Suc i" and P="\j. (H j) \ (J j) \ (T j)\rely" for H J T in allE,simp) + apply(erule_tac x=0 and P="\j. (H j) \ (J j)\etran \ 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="\j. (?s\j) \ (?J j)" in allE,simp) + apply(erule_tac x="nat" and P="\j. (s\j) \ (J j)" for s J in allE,simp) apply(subgoal_tac "(\i. i < length xs \ ((P, t) # xs) ! i -e\ xs ! i \ (snd (((P, t) # xs) ! i), snd (xs ! i)) \ rely)") apply clarify - apply(erule_tac x="Suc i" and P="\j. (?H j) \ (?J j)\etran" in allE,simp) + apply(erule_tac x="Suc i" and P="\j. (H j) \ (J j)\etran" for H J in allE,simp) apply clarify - apply(erule_tac x="Suc i" and P="\j. (?H j) \ (?J j) \ (?T j)\rely" in allE,simp) + apply(erule_tac x="Suc i" and P="\j. (H j) \ (J j) \ (T j)\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="\j. (?H j) \ (?J j)\etran" in allE,simp) + apply(erule_tac x=0 and P="\j. (H j) \ (J j)\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="\j. (?s\j) \ (?J j)" in allE,simp) +apply(erule_tac x="nat" and P="\j. (s\j) \ (J j)" for s J in allE,simp) apply(subgoal_tac "(\i. i < length xs \ ((Q, t) # xs) ! i -e\ xs ! i \ (snd (((Q, t) # xs) ! i), snd (xs ! i)) \ rely)") apply clarify - apply(erule_tac x="Suc i" and P="\j. (?H j) \ (?J j)\etran" in allE,simp) + apply(erule_tac x="Suc i" and P="\j. (H j) \ (J j)\etran" for H J in allE,simp) apply clarify -apply(erule_tac x="Suc i" and P="\j. (?H j) \ (?J j) \ (?T j)\rely" in allE,simp) +apply(erule_tac x="Suc i" and P="\j. (H j) \ (J j) \ (T j)\rely" for H J T in allE,simp) done subsection \Soundness of the System for Component Programs\ @@ -341,7 +341,7 @@ apply(case_tac "x!i") apply clarify apply(drule_tac s="Some (Basic f)" in sym,simp) - apply(thin_tac "\j. ?H j") + apply(thin_tac "\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="\i. ?H i \ (?J i,?I i)\ctran" in allE,simp) + apply(erule_tac x=ia and P="\i. H i \ (J i, I i)\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="\i. ?H i \ (?J i,?I i)\ctran" in allE,simp) + apply(erule_tac x=i and P="\i. H i \ (J i, I i)\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="\i. ?H i \ (?J i,?I i)\ ctran" in Ex_first_occurrence) +apply(drule_tac n=i and P="\i. H i \ (J i, I i) \ 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="\j. ?H j \ ?J j \ (?I j)\guar" in allE) + apply(erule_tac x="i - (Suc m)" and P="\j. H j \ J j \ (I j)\guar" for H J I in allE) apply(subgoal_tac "(Suc m)+(i - Suc m) \ length x") apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \ 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="\j. ?H j \ ?J j \ (?I j)\guar" in allE) +apply(erule_tac x="i - (Suc m)" and P="\j. H j \ J j \ (I j)\guar" for H J I in allE) apply(subgoal_tac "(Suc m)+(i - Suc m) \ length x") apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \ 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="\j. ?H j \ ?J j \ ?I j" in allE,erule impE, assumption) + apply(erule_tac P="\j. H j \ J j \ 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="\j. ?H j \ ?J j \ ?I j" in allE,erule impE, assumption) + apply(erule_tac P="\j. H j \ J j \ 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) --\WhileOne\ -apply(thin_tac "P = While b P \ ?Q") +apply(thin_tac "P = While b P \ 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 --\WhileMore\ -apply(thin_tac "P = While b P \ ?Q") +apply(thin_tac "P = While b P \ Q" for Q) apply(rule ctran_in_comm,simp del:last.simps) --\metiendo la hipotesis antes de dividir la conclusion.\ apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \ assum (pre, rely)") @@ -979,7 +979,7 @@ apply simp apply simp apply(simp add:snd_lift del:list.map last.simps) - apply(thin_tac " \i. i < length ys \ ?P i") + apply(thin_tac " \i. i < length ys \ 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) --\the first c-tran that does not satisfy the guarantee-condition is from @{text "\_i"} at step @{text "m"}.\ -apply(drule_tac n=j and P="\j. \i. ?H i j" in Ex_first_occurrence) +apply(drule_tac n=j and P="\j. \i. H i j" for H in Ex_first_occurrence) apply(erule exE) apply clarify --\@{text "\_i \ A(pre, rely_1)"}\ apply(subgoal_tac "take (Suc (Suc m)) (clist!i) \ assum(Pre(xs!i), Rely(xs!i))") --\but this contradicts @{text "\ \_i sat [pre_i,rely_i,guar_i,post_i]"}\ - apply(erule_tac x=i and P="\i. ?H i \ \ (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption) + apply(erule_tac x=i and P="\i. H i \ \ (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="\j. ?I j \ ?J j \ ?H j" in allE) + apply(erule_tac x=m and P="\j. I j \ J j \ 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="\j. ?H j \ ?I j \cp (?K j) (?J j)" in allE) + apply(erule_tac x=i and P="\j. H j \ I j \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="\j. ?H j \ ?M \ UNION (?S j) (?T j) \ (?L j)" in allE) +apply(erule_tac x=i and P="\j. H j \ M \ UNION (S j) (T j) \ (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="\j. ?H j \ (?P j) \ ?Q j" in allE,simp) +apply(erule_tac x=ia and P="\j. H j \ (P j) \ Q j" for H P Q in allE,simp) --\each etran in @{text "\_1[0\m]"} corresponds to\ apply(erule disjE) --\a c-tran in some @{text "\_{ib}"}\ apply clarify apply(case_tac "i=ib",simp) apply(erule etranE,simp) - apply(erule_tac x="ib" and P="\i. ?H i \ (?I i) \ (?J i)" in allE) + apply(erule_tac x="ib" and P="\i. H i \ (I i) \ (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="\j. ?H j \ (\ i. ?P i j)" in allE) + apply(erule_tac x=ia and P="\j. H j \ (\i. P i j)" for H P in allE) apply(subgoal_tac "iaor an e-tran in @{text "\"}, therefore it satisfies @{text "rely \ guar_{ib}"}\ 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="\j. ?H j \ (?J j \ (\i. ?P i j)) \ ?I j" in allE,simp) +apply(erule_tac x=j and P="\j. H j \ (J j \ (\i. P i j)) \ 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="\i. ?H i \ (?I i) \ (?J i)" in allE,simp) -apply(erule_tac x=j and P="\j. \i. ?S j i \ (?I j i, ?H j i)\ ctran \ (?P i j)" in allE) -apply(erule_tac x=ia and P="\j. ?S j \ (?I j, ?H j)\ ctran \ (?P j)" in allE) +apply(erule_tac x="ia" and P="\i. H i \ (I i) \ (J i)" for H I J in allE,simp) +apply(erule_tac x=j and P="\j. \i. S j i \ (I j i, H j i) \ ctran \ P i j" for S I H P in allE) +apply(erule_tac x=ia and P="\j. S j \ (I j, H j) \ ctran \ P j" for S I H P in allE) apply(simp add:same_state_def) -apply(erule_tac x=i and P="\j. (?T j) \ (\i. (?H j i) \ (snd (?d j i))=(snd (?e j i)))" in all_dupE) -apply(erule_tac x=ia and P="\j. (?T j) \ (\i. (?H j i) \ (snd (?d j i))=(snd (?e j i)))" in allE,simp) +apply(erule_tac x=i and P="\j. T j \ (\i. H j i \ (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE) +apply(erule_tac x=ia and P="\j. T j \ (\i. H j i \ (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="\j. ?H j \ fst(?I j)=(?J j)" in all_dupE) -apply(erule_tac x="Suc i" and P="\j. ?H j \ fst(?I j)=(?J j)" in allE) +apply(erule_tac x=i and P="\j. H j \ fst(I j)=(J j)" for H I J in all_dupE) +apply(erule_tac x="Suc i" and P="\j. H j \ fst(I j)=(J j)" for H I J in allE) apply(erule par_ctranE,simp) -apply(erule_tac x=i and P="\j. \i. ?S j i \ (?I j i, ?H j i)\ ctran \ (?P i j)" in allE) -apply(erule_tac x=ia and P="\j. ?S j \ (?I j, ?H j)\ ctran \ (?P j)" in allE) +apply(erule_tac x=i and P="\j. \i. S j i \ (I j i, H j i) \ ctran \ P i j" for S I H P in allE) +apply(erule_tac x=ia and P="\j. S j \ (I j, H j) \ ctran \ 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="\j. (?T j) \ (\i. (?H j i) \ (snd (?d j i))=(snd (?e j i)))" in all_dupE,simp) -apply(erule_tac x=ia and P="\j. (?T j) \ (\i. (?H j i) \ (snd (?d j i))=(snd (?e j i)))" in allE,simp) -apply(erule_tac x=i and P="\j. ?H j \ (snd (?d j))=(snd (?e j))" in all_dupE) -apply(erule_tac x=i and P="\j. ?H j \ (snd (?d j))=(snd (?e j))" in all_dupE,simp) -apply(erule_tac x="Suc i" and P="\j. ?H j \ (snd (?d j))=(snd (?e j))" in allE,simp) +apply(erule_tac x=ia and P="\j. T j \ (\i. H j i \ (snd (d j i))=(snd (e j i)))" for T H d e in all_dupE,simp) +apply(erule_tac x=ia and P="\j. T j \ (\i. H j i \ (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp) +apply(erule_tac x=i and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in all_dupE) +apply(erule_tac x=i and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in all_dupE,simp) +apply(erule_tac x="Suc i" and P="\j. H j \ (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 "\iassum(Pre(xs!i), Rely(xs!i))") - apply(erule_tac x=i and P="\i. ?H i \ \