tuned proofs;
authorwenzelm
Fri May 11 00:43:45 2007 +0200 (2007-05-11)
changeset 2293111cc1ccad58e
parent 22930 f99617e7103f
child 22932 53005f898665
tuned proofs;
src/FOL/IFOL.thy
src/FOL/ex/LocaleTest.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/ZF/Zet.thy
src/ZF/ex/Group.thy
     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.7 -qed (simp_all! add: continuous_def)
     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.5    apply (simp add: Inv_def)
     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.4    by (simp add: update_carrier_def)
     7.5  
     7.6  lemma carrier_update_carrier [simp]: "carrier(update_carrier(M,B)) = B"
     7.7 -by (simp add: update_carrier_def) 
     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.35            simp add: DirProdGroup_def)
    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.42 -by (simp add: DirProdGroup_def)
    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