# HG changeset patch # User wenzelm # Date 1182449246 -7200 # Node ID bc2563c37b1aef9d5d831989f1dffb87f62753bc # Parent 9953ff53cc648d052ff488b4fbabd7b52405da72 tuned proofs -- avoid implicit prems; diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Algebra/Ideal.thy --- a/src/HOL/Algebra/Ideal.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/Algebra/Ideal.thy Thu Jun 21 20:07:26 2007 +0200 @@ -542,7 +542,7 @@ assumes icarr: "i \ carrier R" shows "principalideal (PIdl i) R" apply (rule principalidealI) -apply (rule cgenideal_ideal, assumption) +apply (rule cgenideal_ideal [OF icarr]) proof - from icarr have "PIdl i = Idl {i}" by (rule cgenideal_eq_genideal) @@ -559,7 +559,7 @@ shows "Idl (I \ J) = I <+> J" apply rule apply (rule ring.genideal_minimal) - apply assumption + apply (rule R.is_ring) apply (rule add_ideals[OF idealI idealJ]) apply (rule) apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1 @@ -675,8 +675,11 @@ and "\a. a \ carrier R \ (\b. a \ b \ I \ b \ carrier R \ a \ I \ b \ I)" hence I_prime: "\ a b. \a \ carrier R; b \ carrier R; a \ b \ I\ \ a \ I \ b \ I" by simp have "primeideal I R" - apply (rule primeideal.intro, assumption+) - by (rule primeideal_axioms.intro, rule InR, erule I_prime) + apply (rule primeideal.intro [OF is_ideal is_cring]) + apply (rule primeideal_axioms.intro) + apply (rule InR) + apply (erule (2) I_prime) + done from this and notprime show "False" by simp qed @@ -692,7 +695,7 @@ lemma (in cring) zeroprimeideal_domainI: assumes pi: "primeideal {\} R" shows "domain R" -apply (rule domain.intro, assumption+) +apply (rule domain.intro, rule is_cring) apply (rule domain_axioms.intro) proof (rule ccontr, simp) interpret primeideal ["{\}" "R"] by (rule pi) @@ -779,7 +782,8 @@ shows "primeideal I R" apply (rule ccontr) apply (rule primeidealCE) - apply assumption+ + apply (rule is_cring) + apply assumption apply (simp add: I_notcarr) proof - assume "\a b. a \ carrier R \ b \ carrier R \ a \ b \ I \ a \ I \ b \ I" diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Algebra/RingHom.thy --- a/src/HOL/Algebra/RingHom.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/Algebra/RingHom.thy Thu Jun 21 20:07:26 2007 +0200 @@ -8,7 +8,6 @@ imports Ideal begin - section {* Homomorphisms of Non-Commutative Rings *} text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *} @@ -67,7 +66,7 @@ assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \ y) = h x \\<^bsub>S\<^esub> h y" and compatible_one: "h \ = \\<^bsub>S\<^esub>" shows "ring_hom_ring R S h" -apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+) +apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring) apply (insert group_hom.homh[OF a_group_hom]) apply (unfold hom_def ring_hom_def, simp) apply safe diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Complex/ex/HarmonicSeries.thy --- a/src/HOL/Complex/ex/HarmonicSeries.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/Complex/ex/HarmonicSeries.thy Thu Jun 21 20:07:26 2007 +0200 @@ -137,7 +137,7 @@ case 0 show ?case by simp next case (Suc M) - have ant: "0 < Suc M" . + have ant: "0 < Suc M" by fact { have suc: "?LHS (Suc M) = ?RHS (Suc M)" proof cases -- "show that LHS = c and RHS = c, and thus LHS = RHS" diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Complex/ex/MIR.thy --- a/src/HOL/Complex/ex/MIR.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/Complex/ex/MIR.thy Thu Jun 21 20:07:26 2007 +0200 @@ -3699,9 +3699,9 @@ shows "\ (p,n,s) \ set (rsplit0 t). Ifm (x#bs) p" (is "\ (p,n,s) \ ?SS t. ?I p") proof(induct t rule: rsplit0.induct) case (2 a b) - from prems have "\ (pa,na,sa) \ ?SS a. ?I pa" by simp + from prems have "\ (pa,na,sa) \ ?SS a. ?I pa" by auto then obtain "pa" "na" "sa" where pa: "(pa,na,sa)\ ?SS a \ ?I pa" by blast - from prems have "\ (pb,nb,sb) \ ?SS b. ?I pb" by simp + from prems have "\ (pb,nb,sb) \ ?SS b. ?I pb" by auto then obtain "pb" "nb" "sb" where pb: "(pb,nb,sb)\ ?SS b \ ?I pb" by blast from pa pb have th: "((pa,na,sa),(pb,nb,sb)) \ set (allpairs Pair (rsplit0 a) (rsplit0 b))" by (auto simp add: allpairs_set) @@ -3763,7 +3763,7 @@ ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). {(p,0,Floor s)})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {0 .. n}})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {n .. 0}})))" by blast - from prems have "\ (p,n,s) \ ?SS a. ?I p" by simp + from prems have "\ (p,n,s) \ ?SS a. ?I p" by auto then obtain "p" "n" "s" where pns: "(p,n,s) \ ?SS a \ ?I p" by blast let ?N = "\ t. Inum (x#bs) t" from rsplit0_cs[rule_format] pns have ans:"(?N a = ?N (CN 0 n s)) \ numbound0 s \ isrlfm p" @@ -3824,9 +3824,9 @@ then obtain "j" where j_def: "j\ {n .. 0} \ ?I (?p (p,n,s) j)" by blast hence "\x \ {?p (p,n,s) j |j. n\ j \ j \ 0 }. ?I x" by auto hence ?case using pns - by (simp only: FS,simp add: bex_Un) + by (simp only: FS,simp add: bex_Un) (rule disjI2, rule disjI2,rule exI [where x="p"], - rule exI [where x="n"],rule exI [where x="s"],simp_all add: np) + rule exI [where x="n"],rule exI [where x="s"],simp_all add: nn) } ultimately show ?case by blast qed (auto simp add: Let_def split_def) diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Lambda/Commutation.thy --- a/src/HOL/Lambda/Commutation.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/Lambda/Commutation.thy Thu Jun 21 20:07:26 2007 +0200 @@ -150,8 +150,8 @@ using wf proof induct case (less x b c) - have xc: "R\<^sup>*\<^sup>* x c" . - have xb: "R\<^sup>*\<^sup>* x b" . thus ?case + have xc: "R\<^sup>*\<^sup>* x c" by fact + have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case proof (rule converse_rtranclE') assume "x = b" with xc have "R\<^sup>*\<^sup>* b c" by simp @@ -203,8 +203,8 @@ case (less x b c) note IH = `\y b c. \R\\ y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\ \ \d. R\<^sup>*\<^sup>* b d \ R\<^sup>*\<^sup>* c d` - have xc: "R\<^sup>*\<^sup>* x c" . - have xb: "R\<^sup>*\<^sup>* x b" . + have xc: "R\<^sup>*\<^sup>* x c" by fact + have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case proof (rule converse_rtranclE') assume "x = b" diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Lambda/ListApplication.thy --- a/src/HOL/Lambda/ListApplication.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/Lambda/ListApplication.thy Thu Jun 21 20:07:26 2007 +0200 @@ -105,7 +105,7 @@ apply clarify apply (erule disjE) apply clarify - apply (rule prems) + apply (rule assms) apply clarify apply (erule allE, erule impE) prefer 2 @@ -116,7 +116,7 @@ apply (rule elem_le_sum) apply force apply clarify - apply (rule prems) + apply (rule assms) apply (erule allE, erule impE) prefer 2 apply (erule allE, erule mp, rule refl) @@ -140,7 +140,7 @@ apply (rule_tac t = t in lem) prefer 3 apply (rule refl) - apply (assumption | rule prems)+ + using assms apply iprover+ done end diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Lambda/ListOrder.thy --- a/src/HOL/Lambda/ListOrder.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/Lambda/ListOrder.thy Thu Jun 21 20:07:26 2007 +0200 @@ -68,7 +68,7 @@ and "!!y. ys = y # xs \ r y x \ R" and "!!zs. ys = x # zs \ step1 r zs xs \ R" shows R - using prems + using assms apply (cases ys) apply (simp add: step1_def) apply blast diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Lambda/StrongNorm.thy --- a/src/HOL/Lambda/StrongNorm.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/Lambda/StrongNorm.thy Thu Jun 21 20:07:26 2007 +0200 @@ -136,7 +136,7 @@ proof (rule MI2) from T have "IT ((lift u 0 \ Var 0)[a[u/i]/0])" proof (rule MI1) - have "IT (lift u 0)" by (rule lift_IT) + have "IT (lift u 0)" by (rule lift_IT [OF uIT]) thus "IT (lift u 0 \ Var 0)" by (rule app_Var_IT) show "e\0:T''\ \ lift u 0 \ Var 0 : Ts \ T'" proof (rule typing.App) @@ -230,13 +230,13 @@ with T have "e\i:T\ \ r[a/0] \\ as : T'" by (rule subject_reduction) hence "IT ((r[a/0] \\ as)[u/i])" - by (rule SI1) + using uIT uT by (rule SI1) thus "IT (r[lift u 0/Suc i][a[u/i]/0] \\ map (\t. t[u/i]) as)" by (simp del: subst_map add: subst_subst subst_map [symmetric]) from T obtain U where "e\i:T\ \ Abs r \ a : U" by (rule list_app_typeE) fast then obtain T'' where "e\i:T\ \ a : T''" by cases simp_all - thus "IT (a[u/i])" by (rule SI2) + thus "IT (a[u/i])" using uIT uT by (rule SI2) qed thus "IT ((Abs r \ a \\ as)[u/i])" by simp } @@ -249,18 +249,18 @@ lemma type_implies_IT: assumes "e \ t : T" shows "IT t" - using prems + using assms proof induct case Var show ?case by (rule Var_IT) next case Abs - show ?case by (rule IT.Lambda) + show ?case by (rule IT.Lambda) (rule Abs) next case (App e s T U t) have "IT ((Var 0 \ lift t 0)[s/0])" proof (rule subst_type_IT) - have "IT (lift t 0)" by (rule lift_IT) + have "IT (lift t 0)" using `IT t` by (rule lift_IT) hence "listsp IT [lift t 0]" by (rule listsp.Cons) (rule listsp.Nil) hence "IT (Var 0 \\ [lift t 0])" by (rule IT.Var) also have "Var 0 \\ [lift t 0] = Var 0 \ lift t 0" by simp @@ -268,9 +268,11 @@ have "e\0:T \ U\ \ Var 0 : T \ U" by (rule typing.Var) simp moreover have "e\0:T \ U\ \ lift t 0 : T" - by (rule lift_type) + by (rule lift_type) (rule App.hyps) ultimately show "e\0:T \ U\ \ Var 0 \ lift t 0 : U" by (rule typing.App) + show "IT s" by fact + show "e \ s : T \ U" by fact qed thus ?case by simp qed diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Lambda/Type.thy --- a/src/HOL/Lambda/Type.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/Lambda/Type.thy Thu Jun 21 20:07:26 2007 +0200 @@ -356,10 +356,10 @@ shows "P T" proof (induct T) case Atom - show ?case by (rule prems) simp_all + show ?case by (rule assms) simp_all next case Fun - show ?case by (rule prems) (insert Fun, simp_all) + show ?case by (rule assms) (insert Fun, simp_all) qed end diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Lambda/WeakNorm.thy --- a/src/HOL/Lambda/WeakNorm.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/Lambda/WeakNorm.thy Thu Jun 21 20:07:26 2007 +0200 @@ -193,7 +193,7 @@ thus ?case .. next case (snoc b bs Us) - have "e\i:T\ \ bs @ [b] : Us" . + have "e\i:T\ \ bs @ [b] : Us" by fact then obtain Vs W where Us: "Us = Vs @ [W]" and bs: "e\i:T\ \ bs : Vs" and bT: "e\i:T\ \ b : W" by (rule types_snocE) @@ -209,7 +209,7 @@ by iprover from bsNF [of 0] have "listall NF (map f bs')" by (rule App_NF_D) - moreover have "NF (f b')" by (rule f_NF) + moreover have "NF (f b')" using bNF by (rule f_NF) ultimately have "listall NF (map f (bs' @ [b']))" by simp hence "\j. NF (Var j \\ map f (bs' @ [b']))" by (rule NF.App) @@ -253,7 +253,7 @@ next case (Cons a as) with argsT obtain T'' Ts where Us: "Us = T'' # Ts" - by (cases Us) (rule FalseE, simp+) + by (cases Us) (rule FalseE, simp+, erule that) from varT and Us have varT: "e\i:T\ \ Var x : T'' \ Ts \ T'" by simp from varT eq have T: "T = T'' \ Ts \ T'" by cases auto @@ -287,6 +287,7 @@ qed with ured show "e\0:T''\ \ u' : Ts \ T'" by (rule subject_reduction') from ared aT show "e \ a' : T''" by (rule subject_reduction') + show "NF a'" by fact qed then obtain ua where uared: "u'[a'/0] \\<^sub>\\<^sup>* ua" and uaNF: "NF ua" by iprover @@ -297,7 +298,7 @@ also note uared finally have "(lift u 0 \ Var 0)[a[u/i]/0] \\<^sub>\\<^sup>* ua" . hence uared': "u \ a[u/i] \\<^sub>\\<^sup>* ua" by simp - from T have "\r. (Var 0 \\ map (\t. lift t 0) as')[ua/0] \\<^sub>\\<^sup>* r \ NF r" + from T asNF _ uaNF have "\r. (Var 0 \\ map (\t. lift t 0) as')[ua/0] \\<^sub>\\<^sup>* r \ NF r" proof (rule MI2) have "e\0:Ts \ T'\ \ Var 0 \\ map (\t. lift (t[u/i]) 0) as : T'" proof (rule list_app_typeI) @@ -349,8 +350,8 @@ case (Abs r e_ T'_ u_ i_) assume absT: "e\i:T\ \ Abs r : T'" then obtain R S where "e\0:R\\Suc i:T\ \ r : S" by (rule abs_typeE) simp - moreover have "NF (lift u 0)" by (rule lift_NF) - moreover have "e\0:R\ \ lift u 0 : T" by (rule lift_type) + moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF) + moreover have "e\0:R\ \ lift u 0 : T" using uT by (rule lift_type) ultimately have "\t'. r[lift u 0/Suc i] \\<^sub>\\<^sup>* t' \ NF t'" by (rule Abs) thus "\t'. Abs r[u/i] \\<^sub>\\<^sup>* t' \ NF t'" by simp (iprover intro: rtrancl_beta_Abs NF.Abs) @@ -377,7 +378,7 @@ theorem type_NF: assumes "e \\<^sub>R t : T" - shows "\t'. t \\<^sub>\\<^sup>* t' \ NF t'" using prems + shows "\t'. t \\<^sub>\\<^sup>* t' \ NF t'" using assms proof induct case Var show ?case by (iprover intro: Var_NF) @@ -387,11 +388,11 @@ next case (App e s T U t) from App obtain s' t' where - sred: "s \\<^sub>\\<^sup>* s'" and sNF: "NF s'" + sred: "s \\<^sub>\\<^sup>* s'" and "NF s'" and tred: "t \\<^sub>\\<^sup>* t'" and tNF: "NF t'" by iprover have "\u. (Var 0 \ lift t' 0)[s'/0] \\<^sub>\\<^sup>* u \ NF u" proof (rule subst_type_NF) - have "NF (lift t' 0)" by (rule lift_NF) + have "NF (lift t' 0)" using tNF by (rule lift_NF) hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil) hence "NF (Var 0 \\ [lift t' 0])" by (rule NF.App) thus "NF (Var 0 \ lift t' 0)" by simp @@ -400,12 +401,13 @@ show "e\0:T \ U\ \ Var 0 : T \ U" by (rule typing.Var) simp from tred have "e \ t' : T" - by (rule subject_reduction') (rule rtyping_imp_typing) + by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps) thus "e\0:T \ U\ \ lift t' 0 : T" by (rule lift_type) qed from sred show "e \ s' : T \ U" - by (rule subject_reduction') (rule rtyping_imp_typing) + by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps) + show "NF s'" by fact qed then obtain u where ured: "s' \ t' \\<^sub>\\<^sup>* u" and unf: "NF u" by simp iprover from sred tred have "s \ t \\<^sub>\\<^sup>* s' \ t'" by (rule rtrancl_beta_App) diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/MetisExamples/BigO.thy --- a/src/HOL/MetisExamples/BigO.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/MetisExamples/BigO.thy Thu Jun 21 20:07:26 2007 +0200 @@ -848,7 +848,7 @@ apply (rule bigo_abs) done also have "... <= O(h)" - by (rule bigo_elt_subset) + using a by (rule bigo_elt_subset) finally show "(%x. abs (f x) - abs (g x)) : O(h)". qed diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/MicroJava/BV/LBVComplete.thy --- a/src/HOL/MicroJava/BV/LBVComplete.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy Thu Jun 21 20:07:26 2007 +0200 @@ -95,7 +95,7 @@ have "?app ss2" by (blast dest: trans_r lesub_step_typeD) moreover { from ss1 have map1: "set (?map ss1) \ A" by auto - with x have "?sum ss1 \ A" by (auto intro!: plusplus_closed) + with x have "?sum ss1 \ A" by (auto intro!: plusplus_closed semilat) with sum have "?s1 \ A" by simp moreover have mapD: "\x ss. x \ set (?map ss) \ \p. (p,x) \ set ss \ p=pc+1" by auto @@ -133,9 +133,9 @@ assumes s2: "s2 \ A" shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'") proof - - from mono s2 have "step pc s2 <=|r| step pc s1" by - (rule monoD) + from mono pc s2 less have "step pc s2 <=|r| step pc s1" by (rule monoD) moreover - from pc cert have "c!Suc pc \ A" by - (rule cert_okD3) + from cert B_A pc have "c!Suc pc \ A" by (rule cert_okD3) moreover from pres s1 pc have "snd`set (step pc s1) \ A" by (rule pres_typeD2) @@ -154,7 +154,7 @@ shows "wtc c pc s2 <=_r wtc c pc s1" (is "?s2' <=_r ?s1'") proof (cases "c!pc = \") case True - moreover have "wti c pc s2 <=_r wti c pc s1" by (rule wti_mono) + moreover from less pc s1 s2 have "wti c pc s2 <=_r wti c pc s1" by (rule wti_mono) ultimately show ?thesis by (simp add: wtc) next case False @@ -187,12 +187,12 @@ from stable have less: "\(q,s')\set ?step. s' <=_r \!q" by (simp add: stable_def) - from cert pc - have cert_suc: "c!Suc pc \ A" by - (rule cert_okD3) + from cert B_A pc + have cert_suc: "c!Suc pc \ A" by (rule cert_okD3) moreover from phi pc have "\!pc \ A" by simp - with pres pc - have stepA: "snd`set ?step \ A" by - (rule pres_typeD2) + from pres this pc + have stepA: "snd`set ?step \ A" by (rule pres_typeD2) ultimately have "merge c pc ?step (c!Suc pc) = (if \(pc',s')\set ?step. pc'\pc+1 \ s' <=_r c!pc' @@ -255,7 +255,7 @@ have less: "\(q,s')\set ?step. s' <=_r \!q" by (simp add: stable_def) from suc_pc have pc: "pc < length \" by simp - with cert have cert_suc: "c!Suc pc \ A" by - (rule cert_okD3) + with cert B_A have cert_suc: "c!Suc pc \ A" by (rule cert_okD3) moreover from phi pc have "\!pc \ A" by simp with pres pc have stepA: "snd`set ?step \ A" by - (rule pres_typeD2) @@ -287,7 +287,7 @@ assumes pc: "pc < length \" shows "wtc c pc (\!pc) \ \" proof - - have wti: "wti c pc (\!pc) \ \" by (rule stable_wti) + from stable pc have wti: "wti c pc (\!pc) \ \" by (rule stable_wti) show ?thesis proof (cases "c!pc = \") case True with wti show ?thesis by (simp add: wtc) @@ -304,17 +304,18 @@ shows "wtc c pc (\!pc) <=_r \!Suc pc" (is "?wtc <=_r _") proof (cases "c!pc = \") case True - moreover have "wti c pc (\!pc) <=_r \!Suc pc" by (rule wti_less) + moreover from stable suc_pc have "wti c pc (\!pc) <=_r \!Suc pc" + by (rule wti_less) ultimately show ?thesis by (simp add: wtc) next case False from suc_pc have pc: "pc < length \" by simp - hence "?wtc \ \" by - (rule stable_wtc) + with stable have "?wtc \ \" by (rule stable_wtc) with False have "?wtc = wti c pc (c!pc)" by (unfold wtc) (simp split: split_if_asm) also from pc False have "c!pc = \!pc" .. finally have "?wtc = wti c pc (\!pc)" . - also have "wti c pc (\!pc) <=_r \!Suc pc" by (rule wti_less) + also from stable suc_pc have "wti c pc (\!pc) <=_r \!Suc pc" by (rule wti_less) finally show ?thesis . qed @@ -338,16 +339,11 @@ from pc_l obtain pc: "pc < length \" by simp with wt_step have stable: "stable r step \ pc" by (simp add: wt_step_def) - moreover + from this pc have wt_phi: "wtc c pc (\!pc) \ \" by (rule stable_wtc) assume s_phi: "s <=_r \!pc" - ultimately - have wt_phi: "wtc c pc (\!pc) \ \" by - (rule stable_wtc) - from phi pc have phi_pc: "\!pc \ A" by simp - moreover assume s: "s \ A" - ultimately - have wt_s_phi: "wtc c pc s <=_r wtc c pc (\!pc)" using s_phi by - (rule wtc_mono) + with s_phi pc phi_pc have wt_s_phi: "wtc c pc s <=_r wtc c pc (\!pc)" by (rule wtc_mono) with wt_phi have wt_s: "wtc c pc s \ \" by simp moreover assume s: "s \ \" diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/MicroJava/BV/LBVCorrect.thy --- a/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Jun 21 20:07:26 2007 +0200 @@ -57,20 +57,20 @@ from bounded pc step have pc': "pc' < length ins" by (rule boundedD) - have tkpc: "wtl (take pc ins) c 0 s0 \ \" (is "?s1 \ _") by (rule wtl_take) - have s2: "wtl (take (pc+1) ins) c 0 s0 \ \" (is "?s2 \ _") by (rule wtl_take) + from wtl have tkpc: "wtl (take pc ins) c 0 s0 \ \" (is "?s1 \ _") by (rule wtl_take) + from wtl have s2: "wtl (take (pc+1) ins) c 0 s0 \ \" (is "?s2 \ _") by (rule wtl_take) from wtl pc have wt_s1: "wtc c pc ?s1 \ \" by (rule wtl_all) have c_Some: "\pc t. pc < length ins \ c!pc \ \ \ \!pc = c!pc" by (simp add: phi_def) - have c_None: "c!pc = \ \ \!pc = ?s1" .. + from pc have c_None: "c!pc = \ \ \!pc = ?s1" .. from wt_s1 pc c_None c_Some have inst: "wtc c pc ?s1 = wti c pc (\!pc)" by (simp add: wtc split: split_if_asm) - have "?s1 \ A" by (rule wtl_pres) + from pres cert s0 wtl pc have "?s1 \ A" by (rule wtl_pres) with pc c_Some cert c_None have "\!pc \ A" by (cases "c!pc = \") (auto dest: cert_okD1) with pc pres @@ -145,7 +145,7 @@ then obtain pc where pc: "pc < length \" and x: "\!pc = x" by (simp add: that [of "length xs"] nth_append) - from wtl s0 pc + from pres cert wtl s0 pc have "wtl (take pc ins) c 0 s0 \ A" by (auto intro!: wtl_pres) moreover from pc have "pc < length ins" by simp @@ -173,7 +173,7 @@ case False with 0 have "phi!0 = c!0" .. moreover - have "wtl (take 1 ins) c 0 s0 \ \" by (rule wtl_take) + from wtl have "wtl (take 1 ins) c 0 s0 \ \" by (rule wtl_take) with 0 False have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm) ultimately @@ -182,40 +182,40 @@ theorem (in lbvs) wtl_sound: - assumes "wtl ins c 0 s0 \ \" - assumes "s0 \ A" + assumes wtl: "wtl ins c 0 s0 \ \" + assumes s0: "s0 \ A" shows "\ts. wt_step r \ step ts" proof - have "wt_step r \ step \