--- 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 \<in> 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 \<union> 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 "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)"
hence I_prime: "\<And> a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> 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 {\<zero>} 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 ["{\<zero>}" "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 "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
--- 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 \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
and compatible_one: "h \<one> = \<one>\<^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
--- 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"
--- 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 "\<exists> (p,n,s) \<in> set (rsplit0 t). Ifm (x#bs) p" (is "\<exists> (p,n,s) \<in> ?SS t. ?I p")
proof(induct t rule: rsplit0.induct)
case (2 a b)
- from prems have "\<exists> (pa,na,sa) \<in> ?SS a. ?I pa" by simp
+ from prems have "\<exists> (pa,na,sa) \<in> ?SS a. ?I pa" by auto
then obtain "pa" "na" "sa" where pa: "(pa,na,sa)\<in> ?SS a \<and> ?I pa" by blast
- from prems have "\<exists> (pb,nb,sb) \<in> ?SS b. ?I pb" by simp
+ from prems have "\<exists> (pb,nb,sb) \<in> ?SS b. ?I pb" by auto
then obtain "pb" "nb" "sb" where pb: "(pb,nb,sb)\<in> ?SS b \<and> ?I pb" by blast
from pa pb have th: "((pa,na,sa),(pb,nb,sb)) \<in> set (allpairs Pair (rsplit0 a) (rsplit0 b))"
by (auto simp add: allpairs_set)
@@ -3763,7 +3763,7 @@
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast
- from prems have "\<exists> (p,n,s) \<in> ?SS a. ?I p" by simp
+ from prems have "\<exists> (p,n,s) \<in> ?SS a. ?I p" by auto
then obtain "p" "n" "s" where pns: "(p,n,s) \<in> ?SS a \<and> ?I p" by blast
let ?N = "\<lambda> t. Inum (x#bs) t"
from rsplit0_cs[rule_format] pns have ans:"(?N a = ?N (CN 0 n s)) \<and> numbound0 s \<and> isrlfm p"
@@ -3824,9 +3824,9 @@
then obtain "j" where j_def: "j\<in> {n .. 0} \<and> ?I (?p (p,n,s) j)" by blast
hence "\<exists>x \<in> {?p (p,n,s) j |j. n\<le> j \<and> j \<le> 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)
--- 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 = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
\<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> 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"
--- 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
--- 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 \<Longrightarrow> r y x \<Longrightarrow> R"
and "!!zs. ys = x # zs \<Longrightarrow> step1 r zs xs \<Longrightarrow> R"
shows R
- using prems
+ using assms
apply (cases ys)
apply (simp add: step1_def)
apply blast
--- 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 \<degree> 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 \<degree> Var 0)" by (rule app_Var_IT)
show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
proof (rule typing.App)
@@ -230,13 +230,13 @@
with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'"
by (rule subject_reduction)
hence "IT ((r[a/0] \<degree>\<degree> as)[u/i])"
- by (rule SI1)
+ using uIT uT by (rule SI1)
thus "IT (r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)"
by (simp del: subst_map add: subst_subst subst_map [symmetric])
from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a : U"
by (rule list_app_typeE) fast
then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> 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 \<degree> a \<degree>\<degree> as)[u/i])" by simp
}
@@ -249,18 +249,18 @@
lemma type_implies_IT:
assumes "e \<turnstile> 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 \<degree> 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 \<degree>\<degree> [lift t 0])" by (rule IT.Var)
also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
@@ -268,9 +268,11 @@
have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
by (rule typing.Var) simp
moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
- by (rule lift_type)
+ by (rule lift_type) (rule App.hyps)
ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
by (rule typing.App)
+ show "IT s" by fact
+ show "e \<turnstile> s : T \<Rightarrow> U" by fact
qed
thus ?case by simp
qed
--- 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
--- 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\<langle>i:T\<rangle> \<tturnstile> bs @ [b] : Us" .
+ have "e\<langle>i:T\<rangle> \<tturnstile> bs @ [b] : Us" by fact
then obtain Vs W where Us: "Us = Vs @ [W]"
and bs: "e\<langle>i:T\<rangle> \<tturnstile> bs : Vs" and bT: "e\<langle>i:T\<rangle> \<turnstile> 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 "\<And>j. NF (Var j \<degree>\<degree> 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\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
by simp
from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto
@@ -287,6 +287,7 @@
qed
with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction')
from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')
+ show "NF a'" by fact
qed
then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "NF ua"
by iprover
@@ -297,7 +298,7 @@
also note uared
finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" .
hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp
- from T have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> NF r"
+ from T asNF _ uaNF have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> NF r"
proof (rule MI2)
have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>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\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle> \<turnstile> r : S" by (rule abs_typeE) simp
- moreover have "NF (lift u 0)" by (rule lift_NF)
- moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" by (rule lift_type)
+ moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF)
+ moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type)
ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)
thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
@@ -377,7 +378,7 @@
theorem type_NF:
assumes "e \<turnstile>\<^sub>R t : T"
- shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" using prems
+ shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> 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 \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "NF s'"
+ sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and "NF s'"
and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "NF t'" by iprover
have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> 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 \<degree>\<degree> [lift t' 0])" by (rule NF.App)
thus "NF (Var 0 \<degree> lift t' 0)" by simp
@@ -400,12 +401,13 @@
show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
by (rule typing.Var) simp
from tred have "e \<turnstile> t' : T"
- by (rule subject_reduction') (rule rtyping_imp_typing)
+ by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
thus "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t' 0 : T"
by (rule lift_type)
qed
from sred show "e \<turnstile> s' : T \<Rightarrow> 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' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" by simp iprover
from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
--- 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
--- 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) \<subseteq> A" by auto
- with x have "?sum ss1 \<in> A" by (auto intro!: plusplus_closed)
+ with x have "?sum ss1 \<in> A" by (auto intro!: plusplus_closed semilat)
with sum have "?s1 \<in> A" by simp
moreover
have mapD: "\<And>x ss. x \<in> set (?map ss) \<Longrightarrow> \<exists>p. (p,x) \<in> set ss \<and> p=pc+1" by auto
@@ -133,9 +133,9 @@
assumes s2: "s2 \<in> 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 \<in> A" by - (rule cert_okD3)
+ from cert B_A pc have "c!Suc pc \<in> A" by (rule cert_okD3)
moreover
from pres s1 pc
have "snd`set (step pc s1) \<subseteq> 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 = \<bottom>")
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: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def)
- from cert pc
- have cert_suc: "c!Suc pc \<in> A" by - (rule cert_okD3)
+ from cert B_A pc
+ have cert_suc: "c!Suc pc \<in> A" by (rule cert_okD3)
moreover
from phi pc have "\<phi>!pc \<in> A" by simp
- with pres pc
- have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2)
+ from pres this pc
+ have stepA: "snd`set ?step \<subseteq> A" by (rule pres_typeD2)
ultimately
have "merge c pc ?step (c!Suc pc) =
(if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
@@ -255,7 +255,7 @@
have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def)
from suc_pc have pc: "pc < length \<phi>" by simp
- with cert have cert_suc: "c!Suc pc \<in> A" by - (rule cert_okD3)
+ with cert B_A have cert_suc: "c!Suc pc \<in> A" by (rule cert_okD3)
moreover
from phi pc have "\<phi>!pc \<in> A" by simp
with pres pc have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2)
@@ -287,7 +287,7 @@
assumes pc: "pc < length \<phi>"
shows "wtc c pc (\<phi>!pc) \<noteq> \<top>"
proof -
- have wti: "wti c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wti)
+ from stable pc have wti: "wti c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wti)
show ?thesis
proof (cases "c!pc = \<bottom>")
case True with wti show ?thesis by (simp add: wtc)
@@ -304,17 +304,18 @@
shows "wtc c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wtc <=_r _")
proof (cases "c!pc = \<bottom>")
case True
- moreover have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)
+ moreover from stable suc_pc have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc"
+ by (rule wti_less)
ultimately show ?thesis by (simp add: wtc)
next
case False
from suc_pc have pc: "pc < length \<phi>" by simp
- hence "?wtc \<noteq> \<top>" by - (rule stable_wtc)
+ with stable have "?wtc \<noteq> \<top>" 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 = \<phi>!pc" ..
finally have "?wtc = wti c pc (\<phi>!pc)" .
- also have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)
+ also from stable suc_pc have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)
finally show ?thesis .
qed
@@ -338,16 +339,11 @@
from pc_l obtain pc: "pc < length \<phi>" by simp
with wt_step have stable: "stable r step \<phi> pc" by (simp add: wt_step_def)
- moreover
+ from this pc have wt_phi: "wtc c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wtc)
assume s_phi: "s <=_r \<phi>!pc"
- ultimately
- have wt_phi: "wtc c pc (\<phi>!pc) \<noteq> \<top>" by - (rule stable_wtc)
-
from phi pc have phi_pc: "\<phi>!pc \<in> A" by simp
- moreover
assume s: "s \<in> A"
- ultimately
- have wt_s_phi: "wtc c pc s <=_r wtc c pc (\<phi>!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 (\<phi>!pc)" by (rule wtc_mono)
with wt_phi have wt_s: "wtc c pc s \<noteq> \<top>" by simp
moreover
assume s: "s \<noteq> \<top>"
--- 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 \<noteq> \<top>" (is "?s1 \<noteq> _") by (rule wtl_take)
- have s2: "wtl (take (pc+1) ins) c 0 s0 \<noteq> \<top>" (is "?s2 \<noteq> _") by (rule wtl_take)
+ from wtl have tkpc: "wtl (take pc ins) c 0 s0 \<noteq> \<top>" (is "?s1 \<noteq> _") by (rule wtl_take)
+ from wtl have s2: "wtl (take (pc+1) ins) c 0 s0 \<noteq> \<top>" (is "?s2 \<noteq> _") by (rule wtl_take)
from wtl pc have wt_s1: "wtc c pc ?s1 \<noteq> \<top>" by (rule wtl_all)
have c_Some: "\<forall>pc t. pc < length ins \<longrightarrow> c!pc \<noteq> \<bottom> \<longrightarrow> \<phi>!pc = c!pc"
by (simp add: phi_def)
- have c_None: "c!pc = \<bottom> \<Longrightarrow> \<phi>!pc = ?s1" ..
+ from pc have c_None: "c!pc = \<bottom> \<Longrightarrow> \<phi>!pc = ?s1" ..
from wt_s1 pc c_None c_Some
have inst: "wtc c pc ?s1 = wti c pc (\<phi>!pc)"
by (simp add: wtc split: split_if_asm)
- have "?s1 \<in> A" by (rule wtl_pres)
+ from pres cert s0 wtl pc have "?s1 \<in> A" by (rule wtl_pres)
with pc c_Some cert c_None
have "\<phi>!pc \<in> A" by (cases "c!pc = \<bottom>") (auto dest: cert_okD1)
with pc pres
@@ -145,7 +145,7 @@
then obtain pc where pc: "pc < length \<phi>" and x: "\<phi>!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 \<in> 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 \<noteq> \<top>" by (rule wtl_take)
+ from wtl have "wtl (take 1 ins) c 0 s0 \<noteq> \<top>" 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 \<noteq> \<top>"
- assumes "s0 \<in> A"
+ assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
+ assumes s0: "s0 \<in> A"
shows "\<exists>ts. wt_step r \<top> step ts"
proof -
have "wt_step r \<top> step \<phi>"
proof (unfold wt_step_def, intro strip conjI)
fix pc assume "pc < length \<phi>"
- then obtain "pc < length ins" by simp
- show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
- show "stable r step \<phi> pc" by (rule wtl_stable)
+ then have pc: "pc < length ins" by simp
+ with wtl show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
+ from wtl s0 pc show "stable r step \<phi> pc" by (rule wtl_stable)
qed
thus ?thesis ..
qed
theorem (in lbvs) wtl_sound_strong:
- assumes "wtl ins c 0 s0 \<noteq> \<top>"
- assumes "s0 \<in> A"
- assumes "0 < length ins"
+ assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
+ assumes s0: "s0 \<in> A"
+ assumes nz: "0 < length ins"
shows "\<exists>ts \<in> list (length ins) A. wt_step r \<top> step ts \<and> s0 <=_r ts!0"
proof -
- have "\<phi> \<in> list (length ins) A" by (rule phi_in_A)
+ from wtl s0 have "\<phi> \<in> list (length ins) A" by (rule phi_in_A)
moreover
have "wt_step r \<top> step \<phi>"
proof (unfold wt_step_def, intro strip conjI)
fix pc assume "pc < length \<phi>"
- then obtain "pc < length ins" by simp
- show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
- show "stable r step \<phi> pc" by (rule wtl_stable)
+ then have pc: "pc < length ins" by simp
+ with wtl show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
+ from wtl s0 pc show "stable r step \<phi> pc" by (rule wtl_stable)
qed
moreover
- have "s0 <=_r \<phi>!0" by (rule phi0)
+ from wtl nz have "s0 <=_r \<phi>!0" by (rule phi0)
ultimately
show ?thesis by fast
qed
-end
\ No newline at end of file
+end
--- 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 \<top> = \<top>"
proof -
from top have "x +_f \<top> <=_r \<top>" ..
- moreover from x have "\<top> <=_r x +_f \<top>" ..
+ moreover from x T_A have "\<top> <=_r x +_f \<top>" ..
ultimately show ?thesis ..
qed
@@ -163,15 +163,15 @@
assume "?set (l#ls)" then obtain set: "snd`set ls \<subseteq> 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 "\<And>x. ?set ls \<Longrightarrow> ?merge ls x \<Longrightarrow> ?P ls" hence "?P ls" .
+ obtain x' where merge': "?merge ls x'" by simp
+ assume "\<And>x. ?set ls \<Longrightarrow> ?merge ls x \<Longrightarrow> ?P ls" hence "?P ls" using set merge' .
moreover
from merge set
- have "pc' \<noteq> pc+1 \<longrightarrow> s' <=_r (c!pc')" by (simp split: split_if_asm)
+ have "pc' \<noteq> pc+1 \<longrightarrow> 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) \<subseteq> A"
then obtain l: "snd l \<in> A" and ls: "snd`set ls \<subseteq> A" by auto
assume "\<And>x. x \<in> A \<Longrightarrow> snd`set ls \<subseteq> A \<Longrightarrow> ?P ls x"
- hence IH: "\<And>x. x \<in> A \<Longrightarrow> ?P ls x" .
+ hence IH: "\<And>x. x \<in> A \<Longrightarrow> ?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 \<top>)"
@@ -201,7 +201,7 @@
proof -
from l have "s' \<in> A" by simp
with x have "s' +_f x \<in> A" by simp
- with x have "?if' \<in> A" by auto
+ with x T_A have "?if' \<in> A" by auto
hence "?P ls ?if'" by (rule IH) thus ?thesis by simp
qed
also have "\<dots> = ?if (l#ls) x"
@@ -317,7 +317,7 @@
proof -
from s0 have "set (map snd [(p', t')\<leftarrow>ss . p'=pc+1]) \<subseteq> A" by auto
with x have "(map snd [(p', t')\<leftarrow>ss . p'=pc+1] ++_f x) \<in> 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 \<in> A" and "c!(pc+1) \<in> A"
- assumes "s \<in> A" and "pc < n"
+ assumes pres: "pres_type step n A"
+ assumes cert: "c!pc \<in> A" and cert': "c!(pc+1) \<in> A"
+ assumes s: "s \<in> A" and pc: "pc < n"
shows "wtc c pc s \<in> A"
proof -
- have "wti c pc s \<in> A" ..
- moreover have "wti c pc (c!pc) \<in> A" ..
+ have "wti c pc s \<in> A" using pres cert' s pc ..
+ moreover have "wti c pc (c!pc) \<in> 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 \<in> A" by simp
next
- fix n assume "Suc n < length is"
- then obtain n: "n < length is" by simp
- assume "n < length is \<Longrightarrow> ?wtl n \<in> A"
- hence "?wtl n \<in> A" .
- moreover
- from cert have "c!n \<in> A" by (rule cert_okD1)
- moreover
- have n1: "n+1 < length is" by simp
- with cert have "c!(n+1) \<in> A" by (rule cert_okD1)
- ultimately
- have "wtc c n (?wtl n) \<in> 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 \<Longrightarrow> ?wtl n \<in> A"
+ have "wtc c n (?wtl n) \<in> A"
+ using pres _ _ _ n
+ proof (rule wtc_pres)
+ from prem n show "?wtl n \<in> A" .
+ from cert n show "c!n \<in> A" by (rule cert_okD1)
+ from cert n1 show "c!(n+1) \<in> A" by (rule cert_okD1)
+ qed
also
from all n have "?wtl n \<noteq> \<top>" 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) \<in> A" by simp
qed
-
end
--- 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 \<in> A" and "ls@b \<in> list n' A" by fastsimp
+ then obtain n' where n: "n = Suc n'" "l \<in> A" and list_n': "ls@b \<in> list n' A" by fastsimp
assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
- hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" .
+ hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" by this (rule list_n')
then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
with n have "?P (l#ls) n (n1+1) n2" by simp
thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
--- 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 \<in> A" and xs: "set (x#xs) \<subseteq> A"
assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
- from xs obtain x: "x \<in> A" and "set xs \<subseteq> A" by simp
+ from xs obtain x: "x \<in> A" and xs': "set xs \<subseteq> A" by simp
from x y have "(x +_f y) \<in> A" ..
- with xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
+ with xs' have "xs ++_f (x +_f y) \<in> A" by (rule IH)
thus "(x#xs) ++_f y \<in> A" by simp
qed
@@ -85,7 +85,7 @@
assume "set (a#l) \<subseteq> A"
then obtain a: "a \<in> A" and x: "set l \<subseteq> A" by simp
assume "\<And>y. \<lbrakk>set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
- hence IH: "\<And>y. y \<in> A \<Longrightarrow> y <=_r l ++_f y" .
+ hence IH: "\<And>y. y \<in> A \<Longrightarrow> y <=_r l ++_f y" using x .
from a y have "y <=_r a +_f y" ..
also from a y have "a +_f y \<in> A" ..
@@ -107,7 +107,7 @@
assume
"\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
- hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" .
+ hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" using ls .
assume "x \<in> set (s#ls)"
then obtain xls: "x = s \<or> x \<in> set ls" by simp
@@ -132,7 +132,7 @@
lemma (in semilat) pp_lub:
- assumes "z \<in> A"
+ assumes z: "z \<in> A"
shows
"\<And>y. y \<in> A \<Longrightarrow> set xs \<subseteq> A \<Longrightarrow> \<forall>x \<in> set xs. x <=_r z \<Longrightarrow> y <=_r z \<Longrightarrow> xs ++_f y <=_r z"
proof (induct xs)
@@ -141,8 +141,8 @@
fix y l ls assume y: "y \<in> A" and "set (l#ls) \<subseteq> A"
then obtain l: "l \<in> A" and ls: "set ls \<subseteq> A" by auto
assume "\<forall>x \<in> set (l#ls). x <=_r z"
- then obtain "l <=_r z" and lsz: "\<forall>x \<in> 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: "\<forall>x \<in> 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 \<in> A" ..
moreover
@@ -171,14 +171,10 @@
show ?thesis by - (rule pp_ub1)
qed
-
lemma plusplus_empty:
"\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
(map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q"
-apply (induct S)
-apply auto
-done
-
+ by (induct S) auto
end
--- 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 \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption
+ with prems NR have "isnorm (R \<oplus> 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 \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption
+ with prems NR have "isnorm (R \<oplus> 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
--- 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
--- 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
--- 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 *}