author wenzelm Fri May 11 00:43:45 2007 +0200 (2007-05-11) changeset 22931 11cc1ccad58e parent 22930 f99617e7103f child 22932 53005f898665
tuned proofs;
 src/FOL/IFOL.thy file | annotate | diff | revisions src/FOL/ex/LocaleTest.thy file | annotate | diff | revisions src/HOL/Algebra/UnivPoly.thy file | annotate | diff | revisions src/HOL/Algebra/poly/UnivPoly2.thy file | annotate | diff | revisions src/HOL/Real/HahnBanach/FunctionNorm.thy file | annotate | diff | revisions src/HOL/ZF/Zet.thy file | annotate | diff | revisions src/ZF/ex/Group.thy file | annotate | diff | revisions
```     1.1 --- a/src/FOL/IFOL.thy	Thu May 10 22:11:38 2007 +0200
1.2 +++ b/src/FOL/IFOL.thy	Fri May 11 00:43:45 2007 +0200
1.3 @@ -676,37 +676,37 @@
1.4  lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
1.5  proof
1.6    assume "!!x. P(x)"
1.7 -  show "ALL x. P(x)" ..
1.8 +  then show "ALL x. P(x)" ..
1.9  next
1.10    assume "ALL x. P(x)"
1.11 -  thus "!!x. P(x)" ..
1.12 +  then show "!!x. P(x)" ..
1.13  qed
1.14
1.15  lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
1.16  proof
1.17    assume "A ==> B"
1.18 -  thus "A --> B" ..
1.19 +  then show "A --> B" ..
1.20  next
1.21    assume "A --> B" and A
1.22 -  thus B by (rule mp)
1.23 +  then show B by (rule mp)
1.24  qed
1.25
1.26  lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
1.27  proof
1.28    assume "x == y"
1.29 -  show "x = y" by (unfold prems) (rule refl)
1.30 +  show "x = y" unfolding `x == y` by (rule refl)
1.31  next
1.32    assume "x = y"
1.33 -  thus "x == y" by (rule eq_reflection)
1.34 +  then show "x == y" by (rule eq_reflection)
1.35  qed
1.36
1.37  lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)"
1.38  proof
1.39    assume "A == B"
1.40 -  show "A <-> B" by (unfold prems) (rule iff_refl)
1.41 +  show "A <-> B" unfolding `A == B` by (rule iff_refl)
1.42  next
1.43    assume "A <-> B"
1.44 -  thus "A == B" by (rule iff_reflection)
1.45 +  then show "A == B" by (rule iff_reflection)
1.46  qed
1.47
1.48  lemma atomize_conj [atomize]:
```
```     2.1 --- a/src/FOL/ex/LocaleTest.thy	Thu May 10 22:11:38 2007 +0200
2.2 +++ b/src/FOL/ex/LocaleTest.thy	Fri May 11 00:43:45 2007 +0200
2.3 @@ -173,7 +173,7 @@
2.4
2.5  ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
2.6
2.7 -lemma (in ID) th_y: "d == (a = b)" .
2.8 +lemma (in ID) th_y: "d == (a = b)" by fact
2.9
2.10  thm i2.th_y thm i3.th_y
2.11
```
```     3.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu May 10 22:11:38 2007 +0200
3.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri May 11 00:43:45 2007 +0200
3.3 @@ -1229,7 +1229,8 @@
3.4    shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
3.5  proof -
3.6    interpret UP_univ_prop [R S h P s _]
3.7 -    by (auto! intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
3.8 +    using `UP_pre_univ_prop R S h` P_def R S
3.9 +    by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
3.10    from R
3.11    show ?thesis by (rule Eval_monom)
3.12  qed
```
```     4.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Thu May 10 22:11:38 2007 +0200
4.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri May 11 00:43:45 2007 +0200
4.3 @@ -187,11 +187,11 @@
4.4  	  have "f i * g (k-i) = 0"
4.5  	  proof cases
4.6  	    assume "n < i"
4.7 -	    show ?thesis by (auto! simp add: ring_simps)
4.8 +	    with `bound n f` show ?thesis by (auto simp add: ring_simps)
4.9  	  next
4.10  	    assume "~ (n < i)"
4.11  	    with bound have "m < k-i" by arith
4.12 -	    then show ?thesis by (auto! simp add: ring_simps)
4.13 +	    with `bound m g` show ?thesis by (auto simp add: ring_simps)
4.14  	  qed
4.15  	}
4.16  	then show "setsum (%i. f i * g (k-i)) {..k} = 0"
```
```     5.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu May 10 22:11:38 2007 +0200
5.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri May 11 00:43:45 2007 +0200
5.3 @@ -266,6 +266,6 @@
5.4      qed
5.5      finally show ?thesis .
5.6    qed
5.8 +qed (insert `continuous V norm f`, simp_all add: continuous_def)
5.9
5.10  end
```
```     6.1 --- a/src/HOL/ZF/Zet.thy	Thu May 10 22:11:38 2007 +0200
6.2 +++ b/src/HOL/ZF/Zet.thy	Fri May 11 00:43:45 2007 +0200
6.3 @@ -53,7 +53,7 @@
6.4    shows "Inv A g (g x) \<in> A"
6.6    apply (rule someI2)
6.7 -  apply (auto!)
6.8 +  using `x \<in> A` apply auto
6.9    done
6.10
6.11  lemma zet_image_mem:
```
```     7.1 --- a/src/ZF/ex/Group.thy	Thu May 10 22:11:38 2007 +0200
7.2 +++ b/src/ZF/ex/Group.thy	Fri May 11 00:43:45 2007 +0200
7.3 @@ -64,13 +64,13 @@
7.5
7.6  lemma carrier_update_carrier [simp]: "carrier(update_carrier(M,B)) = B"
7.8 +  by (simp add: update_carrier_def)
7.9
7.10  lemma mult_update_carrier [simp]: "mmult(update_carrier(M,B),x,y) = mmult(M,x,y)"
7.11 -by (simp add: update_carrier_def mmult_def)
7.12 +  by (simp add: update_carrier_def mmult_def)
7.13
7.14  lemma one_update_carrier [simp]: "one(update_carrier(M,B)) = one(M)"
7.15 -by (simp add: update_carrier_def one_def)
7.16 +  by (simp add: update_carrier_def one_def)
7.17
7.18
7.19  lemma (in monoid) inv_unique:
7.20 @@ -92,7 +92,7 @@
7.21    assumes inv_ex:
7.22       "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
7.23
7.24 -lemma (in group) is_group [simp]: "group(G)" .
7.25 +lemma (in group) is_group [simp]: "group(G)" by fact
7.26
7.27  theorem groupI:
7.28    includes struct G
7.29 @@ -308,7 +308,7 @@
7.30  lemma DirProdGroup_group:
7.31    includes group G + group H
7.32    shows "group (G \<Otimes> H)"
7.33 -by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
7.34 +  by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
7.36
7.37  lemma carrier_DirProdGroup [simp]:
7.38 @@ -322,7 +322,7 @@
7.39  lemma mult_DirProdGroup [simp]:
7.40       "[|g \<in> carrier(G); h \<in> carrier(H); g' \<in> carrier(G); h' \<in> carrier(H)|]
7.41        ==> <g, h> \<cdot>\<^bsub>G \<Otimes> H\<^esub> <g', h'> = <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>"
7.43 +  by (simp add: DirProdGroup_def)
7.44
7.45  lemma inv_DirProdGroup [simp]:
7.46    includes group G + group H
7.47 @@ -366,7 +366,7 @@
7.48    "G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
7.49
7.50  lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G"
7.51 -by (simp add: iso_def hom_def id_type id_bij)
7.52 +  by (simp add: iso_def hom_def id_type id_bij)
7.53
7.54
7.55  lemma (in group) iso_sym:
7.56 @@ -380,18 +380,18 @@
7.57
7.58  lemma (in group) iso_trans:
7.59       "\<lbrakk>h \<in> G \<cong> H; i \<in> H \<cong> I\<rbrakk> \<Longrightarrow> i O h \<in> G \<cong> I"
7.60 -by (auto simp add: iso_def hom_compose comp_bij)
7.61 +  by (auto simp add: iso_def hom_compose comp_bij)
7.62
7.63  lemma DirProdGroup_commute_iso:
7.64    includes group G + group H
7.65    shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"
7.66 -by (auto simp add: iso_def hom_def inj_def surj_def bij_def)
7.67 +  by (auto simp add: iso_def hom_def inj_def surj_def bij_def)
7.68
7.69  lemma DirProdGroup_assoc_iso:
7.70    includes group G + group H + group I
7.71    shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
7.72            \<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"
7.73 -by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def)
7.74 +  by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def)
7.75
7.76  text{*Basis for homomorphism proofs: we assume two groups @{term G} and
7.77    @term{H}, with a homomorphism @{term h} between them*}
7.78 @@ -1003,7 +1003,7 @@
7.79    shows "H \<in> rcosets H"
7.80  proof -
7.81    have "H #> \<one> = H"
7.82 -    by (rule coset_join2, auto)
7.83 +    using _ `subgroup(H, G)` by (rule coset_join2) simp_all
7.84    then show ?thesis
7.85      by (auto simp add: RCOSETS_def intro: sym)
7.86  qed
```