# 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 \" proof (unfold wt_step_def, intro strip conjI) fix pc assume "pc < length \" - then obtain "pc < length ins" by simp - show "\!pc \ \" by (rule phi_not_top) - show "stable r step \ pc" by (rule wtl_stable) + then have pc: "pc < length ins" by simp + with wtl show "\!pc \ \" by (rule phi_not_top) + from wtl s0 pc show "stable r step \ pc" by (rule wtl_stable) qed thus ?thesis .. qed theorem (in lbvs) wtl_sound_strong: - assumes "wtl ins c 0 s0 \ \" - assumes "s0 \ A" - assumes "0 < length ins" + assumes wtl: "wtl ins c 0 s0 \ \" + assumes s0: "s0 \ A" + assumes nz: "0 < length ins" shows "\ts \ list (length ins) A. wt_step r \ step ts \ s0 <=_r ts!0" proof - - have "\ \ list (length ins) A" by (rule phi_in_A) + from wtl s0 have "\ \ list (length ins) A" by (rule phi_in_A) moreover have "wt_step r \ step \" proof (unfold wt_step_def, intro strip conjI) fix pc assume "pc < length \" - then obtain "pc < length ins" by simp - show "\!pc \ \" by (rule phi_not_top) - show "stable r step \ pc" by (rule wtl_stable) + then have pc: "pc < length ins" by simp + with wtl show "\!pc \ \" by (rule phi_not_top) + from wtl s0 pc show "stable r step \ pc" by (rule wtl_stable) qed moreover - have "s0 <=_r \!0" by (rule phi0) + from wtl nz have "s0 <=_r \!0" by (rule phi0) ultimately show ?thesis by fast qed -end \ No newline at end of file +end diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/MicroJava/BV/LBVSpec.thy --- a/src/HOL/MicroJava/BV/LBVSpec.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy Thu Jun 21 20:07:26 2007 +0200 @@ -108,7 +108,7 @@ shows "x +_f \ = \" proof - from top have "x +_f \ <=_r \" .. - moreover from x have "\ <=_r x +_f \" .. + moreover from x T_A have "\ <=_r x +_f \" .. ultimately show ?thesis .. qed @@ -163,15 +163,15 @@ assume "?set (l#ls)" then obtain set: "snd`set ls \ A" by simp assume merge: "?merge (l#ls) x" moreover - obtain pc' s' where [simp]: "l = (pc',s')" by (cases l) + obtain pc' s' where l: "l = (pc',s')" by (cases l) ultimately - obtain x' where "?merge ls x'" by simp - assume "\x. ?set ls \ ?merge ls x \ ?P ls" hence "?P ls" . + obtain x' where merge': "?merge ls x'" by simp + assume "\x. ?set ls \ ?merge ls x \ ?P ls" hence "?P ls" using set merge' . moreover from merge set - have "pc' \ pc+1 \ s' <=_r (c!pc')" by (simp split: split_if_asm) + have "pc' \ pc+1 \ s' <=_r (c!pc')" by (simp add: l split: split_if_asm) ultimately - show "?P (l#ls)" by simp + show "?P (l#ls)" by (simp add: l) qed @@ -191,7 +191,7 @@ assume "snd`set (l#ls) \ A" then obtain l: "snd l \ A" and ls: "snd`set ls \ A" by auto assume "\x. x \ A \ snd`set ls \ A \ ?P ls x" - hence IH: "\x. x \ A \ ?P ls x" . + hence IH: "\x. x \ A \ ?P ls x" using ls by iprover obtain pc' s' where [simp]: "l = (pc',s')" by (cases l) hence "?merge (l#ls) x = ?merge ls (if pc'=pc+1 then s' +_f x else if s' <=_r c!pc' then x else \)" @@ -201,7 +201,7 @@ proof - from l have "s' \ A" by simp with x have "s' +_f x \ A" by simp - with x have "?if' \ A" by auto + with x T_A have "?if' \ A" by auto hence "?P ls ?if'" by (rule IH) thus ?thesis by simp qed also have "\ = ?if (l#ls) x" @@ -317,7 +317,7 @@ proof - from s0 have "set (map snd [(p', t')\ss . p'=pc+1]) \ A" by auto with x have "(map snd [(p', t')\ss . p'=pc+1] ++_f x) \ A" - by (auto intro!: plusplus_closed) + by (auto intro!: plusplus_closed semilat) with s0 x show ?thesis by (simp add: merge_def T_A) qed @@ -339,13 +339,13 @@ lemma (in lbv) wtc_pres: - assumes "pres_type step n A" - assumes "c!pc \ A" and "c!(pc+1) \ A" - assumes "s \ A" and "pc < n" + assumes pres: "pres_type step n A" + assumes cert: "c!pc \ A" and cert': "c!(pc+1) \ A" + assumes s: "s \ A" and pc: "pc < n" shows "wtc c pc s \ A" proof - - have "wti c pc s \ A" .. - moreover have "wti c pc (c!pc) \ A" .. + have "wti c pc s \ A" using pres cert' s pc .. + moreover have "wti c pc (c!pc) \ A" using pres cert' cert pc .. ultimately show ?thesis using T_A by (simp add: wtc) qed @@ -360,22 +360,21 @@ proof (induct pc) from s show "?wtl 0 \ A" by simp next - fix n assume "Suc n < length is" - then obtain n: "n < length is" by simp - assume "n < length is \ ?wtl n \ A" - hence "?wtl n \ A" . - moreover - from cert have "c!n \ A" by (rule cert_okD1) - moreover - have n1: "n+1 < length is" by simp - with cert have "c!(n+1) \ A" by (rule cert_okD1) - ultimately - have "wtc c n (?wtl n) \ A" by - (rule wtc_pres) + fix n assume IH: "Suc n < length is" + then have n: "n < length is" by simp + from IH have n1: "n+1 < length is" by simp + assume prem: "n < length is \ ?wtl n \ A" + have "wtc c n (?wtl n) \ A" + using pres _ _ _ n + proof (rule wtc_pres) + from prem n show "?wtl n \ A" . + from cert n show "c!n \ A" by (rule cert_okD1) + from cert n1 show "c!(n+1) \ A" by (rule cert_okD1) + qed also from all n have "?wtl n \ \" by - (rule wtl_take) with n1 have "wtc c n (?wtl n) = ?wtl (n+1)" by (rule wtl_Suc [symmetric]) finally show "?wtl (Suc n) \ A" by simp qed - end diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/MicroJava/BV/Listn.thy --- a/src/HOL/MicroJava/BV/Listn.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/MicroJava/BV/Listn.thy Thu Jun 21 20:07:26 2007 +0200 @@ -233,9 +233,9 @@ next fix n l ls assume "?list (l#ls) n" - then obtain n' where n: "n = Suc n'" "l \ A" and "ls@b \ list n' A" by fastsimp + then obtain n' where n: "n = Suc n'" "l \ A" and list_n': "ls@b \ list n' A" by fastsimp assume "\n. ls @ b \ list n A \ \n1 n2. n = n1 + n2 \ ls \ list n1 A \ b \ list n2 A" - hence "\n1 n2. n' = n1 + n2 \ ls \ list n1 A \ b \ list n2 A" . + hence "\n1 n2. n' = n1 + n2 \ ls \ list n1 A \ b \ list n2 A" by this (rule list_n') then obtain n1 n2 where "n' = n1 + n2" "ls \ list n1 A" "b \ list n2 A" by fast with n have "?P (l#ls) n (n1+1) n2" by simp thus "\n1 n2. ?P (l#ls) n n1 n2" by fastsimp diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/MicroJava/BV/SemilatAlg.thy --- a/src/HOL/MicroJava/BV/SemilatAlg.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Thu Jun 21 20:07:26 2007 +0200 @@ -69,9 +69,9 @@ fix y x xs assume y: "y \ A" and xs: "set (x#xs) \ A" assume IH: "\y. \ set xs \ A; y \ A\ \ xs ++_f y \ A" - from xs obtain x: "x \ A" and "set xs \ A" by simp + from xs obtain x: "x \ A" and xs': "set xs \ A" by simp from x y have "(x +_f y) \ A" .. - with xs have "xs ++_f (x +_f y) \ A" by - (rule IH) + with xs' have "xs ++_f (x +_f y) \ A" by (rule IH) thus "(x#xs) ++_f y \ A" by simp qed @@ -85,7 +85,7 @@ assume "set (a#l) \ A" then obtain a: "a \ A" and x: "set l \ A" by simp assume "\y. \set l \ A; y \ A\ \ y <=_r l ++_f y" - hence IH: "\y. y \ A \ y <=_r l ++_f y" . + hence IH: "\y. y \ A \ y <=_r l ++_f y" using x . from a y have "y <=_r a +_f y" .. also from a y have "a +_f y \ A" .. @@ -107,7 +107,7 @@ assume "\y. \set ls \ A; y \ A; x \ set ls\ \ x <=_r ls ++_f y" - hence IH: "\y. x \ set ls \ y \ A \ x <=_r ls ++_f y" . + hence IH: "\y. x \ set ls \ y \ A \ x <=_r ls ++_f y" using ls . assume "x \ set (s#ls)" then obtain xls: "x = s \ x \ set ls" by simp @@ -132,7 +132,7 @@ lemma (in semilat) pp_lub: - assumes "z \ A" + assumes z: "z \ A" shows "\y. y \ A \ set xs \ A \ \x \ set xs. x <=_r z \ y <=_r z \ xs ++_f y <=_r z" proof (induct xs) @@ -141,8 +141,8 @@ fix y l ls assume y: "y \ A" and "set (l#ls) \ A" then obtain l: "l \ A" and ls: "set ls \ A" by auto assume "\x \ set (l#ls). x <=_r z" - then obtain "l <=_r z" and lsz: "\x \ set ls. x <=_r z" by auto - assume "y <=_r z" have "l +_f y <=_r z" .. + then obtain lz: "l <=_r z" and lsz: "\x \ set ls. x <=_r z" by auto + assume "y <=_r z" with lz have "l +_f y <=_r z" using l y z .. moreover from l y have "l +_f y \ A" .. moreover @@ -171,14 +171,10 @@ show ?thesis by - (rule pp_ub1) qed - lemma plusplus_empty: "\s'. (q, s') \ set S \ s' +_f ss ! q = ss ! q \ (map snd [(p', t') \ S. p' = q] ++_f ss ! q) = ss ! q" -apply (induct S) -apply auto -done - + by (induct S) auto end diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/ex/Commutative_Ring_Complete.thy --- a/src/HOL/ex/Commutative_Ring_Complete.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/HOL/ex/Commutative_Ring_Complete.thy Thu Jun 21 20:07:26 2007 +0200 @@ -150,7 +150,7 @@ then obtain d where X:"x=Suc (Suc d)" .. from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) - with prems NR have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption + with prems NR have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } ultimately show ?case by blast next @@ -168,7 +168,7 @@ then obtain d where X:"x=Suc (Suc d)" .. from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto) - with prems NR have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption + with prems NR have "isnorm (R \ Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp fact with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } ultimately show ?case by blast next diff -r 9953ff53cc64 -r bc2563c37b1a src/ZF/Constructible/Reflection.thy --- a/src/ZF/Constructible/Reflection.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/ZF/Constructible/Reflection.thy Thu Jun 21 20:07:26 2007 +0200 @@ -200,7 +200,7 @@ ==> Closed_Unbounded(ClEx(P))" apply (unfold ClEx_eq FF_def F0_def M_def) apply (rule ex_reflection.ZF_Closed_Unbounded_ClEx [of Mset _ _ Cl]) -apply (rule ex_reflection.intro, assumption) +apply (rule ex_reflection.intro, rule reflection_axioms) apply (blast intro: ex_reflection_axioms.intro) done diff -r 9953ff53cc64 -r bc2563c37b1a src/ZF/Constructible/Satisfies_absolute.thy --- a/src/ZF/Constructible/Satisfies_absolute.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/ZF/Constructible/Satisfies_absolute.thy Thu Jun 21 20:07:26 2007 +0200 @@ -485,7 +485,7 @@ satisfies_c(A), satisfies_is_c(M,A), satisfies_d(A), satisfies_is_d(M,A))" apply (rule Formula_Rec.intro) - apply (rule M_satisfies.axioms) apply assumption + apply (rule M_satisfies.axioms, rule M_satisfies_axioms) apply (erule Formula_Rec_axioms_M) done diff -r 9953ff53cc64 -r bc2563c37b1a src/ZF/Induct/Brouwer.thy --- a/src/ZF/Induct/Brouwer.thy Thu Jun 21 17:28:53 2007 +0200 +++ b/src/ZF/Induct/Brouwer.thy Thu Jun 21 20:07:26 2007 +0200 @@ -32,10 +32,12 @@ -- {* A nicer induction rule than the standard one. *} using b apply induct - apply (assumption | rule cases)+ - apply (fast elim: fun_weaken_type) - apply (fast dest: apply_type) - done + apply (rule cases(1)) + apply (erule (1) cases(2)) + apply (rule cases(3)) + apply (fast elim: fun_weaken_type) + apply (fast dest: apply_type) + done subsection {* The Martin-Löf wellordering type *}