--- a/src/FOL/IFOL.thy Thu May 10 22:11:38 2007 +0200
+++ b/src/FOL/IFOL.thy Fri May 11 00:43:45 2007 +0200
@@ -676,37 +676,37 @@
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
proof
assume "!!x. P(x)"
- show "ALL x. P(x)" ..
+ then show "ALL x. P(x)" ..
next
assume "ALL x. P(x)"
- thus "!!x. P(x)" ..
+ then show "!!x. P(x)" ..
qed
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
proof
assume "A ==> B"
- thus "A --> B" ..
+ then show "A --> B" ..
next
assume "A --> B" and A
- thus B by (rule mp)
+ then show B by (rule mp)
qed
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
proof
assume "x == y"
- show "x = y" by (unfold prems) (rule refl)
+ show "x = y" unfolding `x == y` by (rule refl)
next
assume "x = y"
- thus "x == y" by (rule eq_reflection)
+ then show "x == y" by (rule eq_reflection)
qed
lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)"
proof
assume "A == B"
- show "A <-> B" by (unfold prems) (rule iff_refl)
+ show "A <-> B" unfolding `A == B` by (rule iff_refl)
next
assume "A <-> B"
- thus "A == B" by (rule iff_reflection)
+ then show "A == B" by (rule iff_reflection)
qed
lemma atomize_conj [atomize]:
--- a/src/FOL/ex/LocaleTest.thy Thu May 10 22:11:38 2007 +0200
+++ b/src/FOL/ex/LocaleTest.thy Fri May 11 00:43:45 2007 +0200
@@ -173,7 +173,7 @@
ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
-lemma (in ID) th_y: "d == (a = b)" .
+lemma (in ID) th_y: "d == (a = b)" by fact
thm i2.th_y thm i3.th_y
--- a/src/HOL/Algebra/UnivPoly.thy Thu May 10 22:11:38 2007 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Fri May 11 00:43:45 2007 +0200
@@ -1229,7 +1229,8 @@
shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
proof -
interpret UP_univ_prop [R S h P s _]
- by (auto! intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
+ using `UP_pre_univ_prop R S h` P_def R S
+ by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
from R
show ?thesis by (rule Eval_monom)
qed
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Thu May 10 22:11:38 2007 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Fri May 11 00:43:45 2007 +0200
@@ -187,11 +187,11 @@
have "f i * g (k-i) = 0"
proof cases
assume "n < i"
- show ?thesis by (auto! simp add: ring_simps)
+ with `bound n f` show ?thesis by (auto simp add: ring_simps)
next
assume "~ (n < i)"
with bound have "m < k-i" by arith
- then show ?thesis by (auto! simp add: ring_simps)
+ with `bound m g` show ?thesis by (auto simp add: ring_simps)
qed
}
then show "setsum (%i. f i * g (k-i)) {..k} = 0"
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu May 10 22:11:38 2007 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Fri May 11 00:43:45 2007 +0200
@@ -266,6 +266,6 @@
qed
finally show ?thesis .
qed
-qed (simp_all! add: continuous_def)
+qed (insert `continuous V norm f`, simp_all add: continuous_def)
end
--- a/src/HOL/ZF/Zet.thy Thu May 10 22:11:38 2007 +0200
+++ b/src/HOL/ZF/Zet.thy Fri May 11 00:43:45 2007 +0200
@@ -53,7 +53,7 @@
shows "Inv A g (g x) \<in> A"
apply (simp add: Inv_def)
apply (rule someI2)
- apply (auto!)
+ using `x \<in> A` apply auto
done
lemma zet_image_mem:
--- a/src/ZF/ex/Group.thy Thu May 10 22:11:38 2007 +0200
+++ b/src/ZF/ex/Group.thy Fri May 11 00:43:45 2007 +0200
@@ -64,13 +64,13 @@
by (simp add: update_carrier_def)
lemma carrier_update_carrier [simp]: "carrier(update_carrier(M,B)) = B"
-by (simp add: update_carrier_def)
+ by (simp add: update_carrier_def)
lemma mult_update_carrier [simp]: "mmult(update_carrier(M,B),x,y) = mmult(M,x,y)"
-by (simp add: update_carrier_def mmult_def)
+ by (simp add: update_carrier_def mmult_def)
lemma one_update_carrier [simp]: "one(update_carrier(M,B)) = one(M)"
-by (simp add: update_carrier_def one_def)
+ by (simp add: update_carrier_def one_def)
lemma (in monoid) inv_unique:
@@ -92,7 +92,7 @@
assumes inv_ex:
"\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
-lemma (in group) is_group [simp]: "group(G)" .
+lemma (in group) is_group [simp]: "group(G)" by fact
theorem groupI:
includes struct G
@@ -308,7 +308,7 @@
lemma DirProdGroup_group:
includes group G + group H
shows "group (G \<Otimes> H)"
-by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
+ by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
simp add: DirProdGroup_def)
lemma carrier_DirProdGroup [simp]:
@@ -322,7 +322,7 @@
lemma mult_DirProdGroup [simp]:
"[|g \<in> carrier(G); h \<in> carrier(H); g' \<in> carrier(G); h' \<in> carrier(H)|]
==> <g, h> \<cdot>\<^bsub>G \<Otimes> H\<^esub> <g', h'> = <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>"
-by (simp add: DirProdGroup_def)
+ by (simp add: DirProdGroup_def)
lemma inv_DirProdGroup [simp]:
includes group G + group H
@@ -366,7 +366,7 @@
"G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G"
-by (simp add: iso_def hom_def id_type id_bij)
+ by (simp add: iso_def hom_def id_type id_bij)
lemma (in group) iso_sym:
@@ -380,18 +380,18 @@
lemma (in group) iso_trans:
"\<lbrakk>h \<in> G \<cong> H; i \<in> H \<cong> I\<rbrakk> \<Longrightarrow> i O h \<in> G \<cong> I"
-by (auto simp add: iso_def hom_compose comp_bij)
+ by (auto simp add: iso_def hom_compose comp_bij)
lemma DirProdGroup_commute_iso:
includes group G + group H
shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"
-by (auto simp add: iso_def hom_def inj_def surj_def bij_def)
+ by (auto simp add: iso_def hom_def inj_def surj_def bij_def)
lemma DirProdGroup_assoc_iso:
includes group G + group H + group I
shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
\<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"
-by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def)
+ by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def)
text{*Basis for homomorphism proofs: we assume two groups @{term G} and
@term{H}, with a homomorphism @{term h} between them*}
@@ -1003,7 +1003,7 @@
shows "H \<in> rcosets H"
proof -
have "H #> \<one> = H"
- by (rule coset_join2, auto)
+ using _ `subgroup(H, G)` by (rule coset_join2) simp_all
then show ?thesis
by (auto simp add: RCOSETS_def intro: sym)
qed