Removed uses of context element includes.
authorballarin
Tue Jul 15 16:50:09 2008 +0200 (2008-07-15)
changeset 276112c01c0bdb385
parent 27610 8882d47e075f
child 27612 d3eb431db035
Removed uses of context element includes.
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/QuotRing.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/FrechetDeriv.thy
src/HOL/Library/Multiset.thy
src/HOL/MicroJava/BV/Err.thy
src/HOL/MicroJava/BV/Kildall.thy
src/HOL/MicroJava/BV/Listn.thy
src/HOL/MicroJava/BV/SemilatAlg.thy
src/HOL/Real/HahnBanach/Bounds.thy
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
src/HOL/Real/HahnBanach/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/Subspace.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Tue Jul 15 16:02:10 2008 +0200
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Tue Jul 15 16:50:09 2008 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4    a_r_coset_def r_coset_def
     1.5  
     1.6  lemma a_r_coset_def':
     1.7 -  includes struct G
     1.8 +  fixes G (structure)
     1.9    shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}"
    1.10  unfolding a_r_coset_defs
    1.11  by simp
    1.12 @@ -69,7 +69,7 @@
    1.13    a_l_coset_def l_coset_def
    1.14  
    1.15  lemma a_l_coset_def':
    1.16 -  includes struct G
    1.17 +  fixes G (structure)
    1.18    shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}"
    1.19  unfolding a_l_coset_defs
    1.20  by simp
    1.21 @@ -78,7 +78,7 @@
    1.22    A_RCOSETS_def RCOSETS_def
    1.23  
    1.24  lemma A_RCOSETS_def':
    1.25 -  includes struct G
    1.26 +  fixes G (structure)
    1.27    shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}"
    1.28  unfolding A_RCOSETS_defs
    1.29  by (fold a_r_coset_def, simp)
    1.30 @@ -87,7 +87,7 @@
    1.31    set_add_def set_mult_def
    1.32  
    1.33  lemma set_add_def':
    1.34 -  includes struct G
    1.35 +  fixes G (structure)
    1.36    shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"
    1.37  unfolding set_add_defs
    1.38  by simp
    1.39 @@ -96,7 +96,7 @@
    1.40    A_SET_INV_def SET_INV_def
    1.41  
    1.42  lemma A_SET_INV_def':
    1.43 -  includes struct G
    1.44 +  fixes G (structure)
    1.45    shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
    1.46  unfolding A_SET_INV_defs
    1.47  by (fold a_inv_def)
    1.48 @@ -188,7 +188,7 @@
    1.49  by (rule additive_subgroup_axioms)
    1.50  
    1.51  lemma additive_subgroupI:
    1.52 -  includes struct G
    1.53 +  fixes G (structure)
    1.54    assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.55    shows "additive_subgroup H G"
    1.56  by (rule additive_subgroup.intro) (rule a_subgroup)
    1.57 @@ -240,7 +240,7 @@
    1.58  qed
    1.59  
    1.60  lemma abelian_subgroupI2:
    1.61 -  includes struct G
    1.62 +  fixes G (structure)
    1.63    assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.64        and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.65    shows "abelian_subgroup H G"
    1.66 @@ -265,7 +265,7 @@
    1.67  qed
    1.68  
    1.69  lemma abelian_subgroupI3:
    1.70 -  includes struct G
    1.71 +  fixes G (structure)
    1.72    assumes asg: "additive_subgroup H G"
    1.73        and ag: "abelian_group G"
    1.74    shows "abelian_subgroup H G"
    1.75 @@ -451,7 +451,7 @@
    1.76  lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
    1.77  
    1.78  lemma A_FactGroup_def':
    1.79 -  includes struct G
    1.80 +  fixes G (structure)
    1.81    shows "G A_Mod H \<equiv> \<lparr>carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\<rparr>"
    1.82  unfolding A_FactGroup_defs
    1.83  by (fold A_RCOSETS_def set_add_def)
    1.84 @@ -534,16 +534,20 @@
    1.85  subsection {* Homomorphisms *}
    1.86  
    1.87  lemma abelian_group_homI:
    1.88 -  includes abelian_group G
    1.89 -  includes abelian_group H
    1.90 +  assumes "abelian_group G"
    1.91 +  assumes "abelian_group H"
    1.92    assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
    1.93                                    (| carrier = carrier H, mult = add H, one = zero H |) h"
    1.94    shows "abelian_group_hom G H h"
    1.95 -apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
    1.96 -  apply (rule G.abelian_group_axioms)
    1.97 - apply (rule H.abelian_group_axioms)
    1.98 -apply (rule a_group_hom)
    1.99 -done
   1.100 +proof -
   1.101 +  interpret G: abelian_group [G] by fact
   1.102 +  interpret H: abelian_group [H] by fact
   1.103 +  show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
   1.104 +    apply fact
   1.105 +    apply fact
   1.106 +    apply (rule a_group_hom)
   1.107 +    done
   1.108 +qed
   1.109  
   1.110  lemma (in abelian_group_hom) is_abelian_group_hom:
   1.111    "abelian_group_hom G H h"
   1.112 @@ -688,10 +692,11 @@
   1.113  
   1.114  --"variant"
   1.115  lemma (in abelian_subgroup) a_rcos_module_minus:
   1.116 -  includes ring G
   1.117 +  assumes "ring G"
   1.118    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   1.119    shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
   1.120  proof -
   1.121 +  interpret G: ring [G] by fact
   1.122    from carr
   1.123    have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
   1.124    with carr
     2.1 --- a/src/HOL/Algebra/Coset.thy	Tue Jul 15 16:02:10 2008 +0200
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Tue Jul 15 16:50:09 2008 +0200
     2.3 @@ -109,23 +109,27 @@
     2.4  
     2.5  text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
     2.6  lemma (in group) repr_independenceD:
     2.7 -  includes subgroup H G
     2.8 +  assumes "subgroup H G"
     2.9    assumes ycarr: "y \<in> carrier G"
    2.10        and repr:  "H #> x = H #> y"
    2.11    shows "y \<in> H #> x"
    2.12 -  apply (subst repr)
    2.13 +proof -
    2.14 +  interpret subgroup [H G] by fact
    2.15 +  show ?thesis  apply (subst repr)
    2.16    apply (intro rcos_self)
    2.17     apply (rule ycarr)
    2.18     apply (rule is_subgroup)
    2.19    done
    2.20 +qed
    2.21  
    2.22  text {* Elements of a right coset are in the carrier *}
    2.23  lemma (in subgroup) elemrcos_carrier:
    2.24 -  includes group
    2.25 +  assumes "group G"
    2.26    assumes acarr: "a \<in> carrier G"
    2.27      and a': "a' \<in> H #> a"
    2.28    shows "a' \<in> carrier G"
    2.29  proof -
    2.30 +  interpret group [G] by fact
    2.31    from subset and acarr
    2.32    have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
    2.33    from this and a'
    2.34 @@ -134,38 +138,42 @@
    2.35  qed
    2.36  
    2.37  lemma (in subgroup) rcos_const:
    2.38 -  includes group
    2.39 +  assumes "group G"
    2.40    assumes hH: "h \<in> H"
    2.41    shows "H #> h = H"
    2.42 -  apply (unfold r_coset_def)
    2.43 -  apply rule
    2.44 -   apply rule
    2.45 -   apply clarsimp
    2.46 -   apply (intro subgroup.m_closed)
    2.47 -     apply (rule is_subgroup)
    2.48 +proof -
    2.49 +  interpret group [G] by fact
    2.50 +  show ?thesis apply (unfold r_coset_def)
    2.51 +    apply rule
    2.52 +    apply rule
    2.53 +    apply clarsimp
    2.54 +    apply (intro subgroup.m_closed)
    2.55 +    apply (rule is_subgroup)
    2.56      apply assumption
    2.57 -   apply (rule hH)
    2.58 -  apply rule
    2.59 -  apply simp
    2.60 -proof -
    2.61 -  fix h'
    2.62 -  assume h'H: "h' \<in> H"
    2.63 -  note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
    2.64 -  from carr
    2.65 -  have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
    2.66 -  from h'H hH
    2.67 -  have "h' \<otimes> inv h \<in> H" by simp
    2.68 -  from this and a
    2.69 -  show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
    2.70 +    apply (rule hH)
    2.71 +    apply rule
    2.72 +    apply simp
    2.73 +  proof -
    2.74 +    fix h'
    2.75 +    assume h'H: "h' \<in> H"
    2.76 +    note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
    2.77 +    from carr
    2.78 +    have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
    2.79 +    from h'H hH
    2.80 +    have "h' \<otimes> inv h \<in> H" by simp
    2.81 +    from this and a
    2.82 +    show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
    2.83 +  qed
    2.84  qed
    2.85  
    2.86  text {* Step one for lemma @{text "rcos_module"} *}
    2.87  lemma (in subgroup) rcos_module_imp:
    2.88 -  includes group
    2.89 +  assumes "group G"
    2.90    assumes xcarr: "x \<in> carrier G"
    2.91        and x'cos: "x' \<in> H #> x"
    2.92    shows "(x' \<otimes> inv x) \<in> H"
    2.93  proof -
    2.94 +  interpret group [G] by fact
    2.95    from xcarr x'cos
    2.96        have x'carr: "x' \<in> carrier G"
    2.97        by (rule elemrcos_carrier[OF is_group])
    2.98 @@ -200,11 +208,12 @@
    2.99  
   2.100  text {* Step two for lemma @{text "rcos_module"} *}
   2.101  lemma (in subgroup) rcos_module_rev:
   2.102 -  includes group
   2.103 +  assumes "group G"
   2.104    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   2.105        and xixH: "(x' \<otimes> inv x) \<in> H"
   2.106    shows "x' \<in> H #> x"
   2.107  proof -
   2.108 +  interpret group [G] by fact
   2.109    from xixH
   2.110        have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
   2.111    from this
   2.112 @@ -231,27 +240,30 @@
   2.113  
   2.114  text {* Module property of right cosets *}
   2.115  lemma (in subgroup) rcos_module:
   2.116 -  includes group
   2.117 +  assumes "group G"
   2.118    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   2.119    shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
   2.120 -proof
   2.121 -  assume "x' \<in> H #> x"
   2.122 -  from this and carr
   2.123 -      show "x' \<otimes> inv x \<in> H"
   2.124 +proof -
   2.125 +  interpret group [G] by fact
   2.126 +  show ?thesis proof  assume "x' \<in> H #> x"
   2.127 +    from this and carr
   2.128 +    show "x' \<otimes> inv x \<in> H"
   2.129        by (intro rcos_module_imp[OF is_group])
   2.130 -next
   2.131 -  assume "x' \<otimes> inv x \<in> H"
   2.132 -  from this and carr
   2.133 -      show "x' \<in> H #> x"
   2.134 +  next
   2.135 +    assume "x' \<otimes> inv x \<in> H"
   2.136 +    from this and carr
   2.137 +    show "x' \<in> H #> x"
   2.138        by (intro rcos_module_rev[OF is_group])
   2.139 +  qed
   2.140  qed
   2.141  
   2.142  text {* Right cosets are subsets of the carrier. *} 
   2.143  lemma (in subgroup) rcosets_carrier:
   2.144 -  includes group
   2.145 +  assumes "group G"
   2.146    assumes XH: "X \<in> rcosets H"
   2.147    shows "X \<subseteq> carrier G"
   2.148  proof -
   2.149 +  interpret group [G] by fact
   2.150    from XH have "\<exists>x\<in> carrier G. X = H #> x"
   2.151        unfolding RCOSETS_def
   2.152        by fast
   2.153 @@ -331,11 +343,12 @@
   2.154  qed
   2.155  
   2.156  lemma (in subgroup) lcos_module_rev:
   2.157 -  includes group
   2.158 +  assumes "group G"
   2.159    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   2.160        and xixH: "(inv x \<otimes> x') \<in> H"
   2.161    shows "x' \<in> x <# H"
   2.162  proof -
   2.163 +  interpret group [G] by fact
   2.164    from xixH
   2.165        have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
   2.166    from this
   2.167 @@ -584,29 +597,33 @@
   2.168  
   2.169  
   2.170  lemma (in subgroup) equiv_rcong:
   2.171 -   includes group G
   2.172 +   assumes "group G"
   2.173     shows "equiv (carrier G) (rcong H)"
   2.174 -proof (intro equiv.intro)
   2.175 -  show "refl (carrier G) (rcong H)"
   2.176 -    by (auto simp add: r_congruent_def refl_def) 
   2.177 -next
   2.178 -  show "sym (rcong H)"
   2.179 -  proof (simp add: r_congruent_def sym_def, clarify)
   2.180 -    fix x y
   2.181 -    assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
   2.182 -       and "inv x \<otimes> y \<in> H"
   2.183 -    hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
   2.184 -    thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
   2.185 -  qed
   2.186 -next
   2.187 -  show "trans (rcong H)"
   2.188 -  proof (simp add: r_congruent_def trans_def, clarify)
   2.189 -    fix x y z
   2.190 -    assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   2.191 -       and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
   2.192 -    hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
   2.193 -    hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv) 
   2.194 -    thus "inv x \<otimes> z \<in> H" by simp
   2.195 +proof -
   2.196 +  interpret group [G] by fact
   2.197 +  show ?thesis
   2.198 +  proof (intro equiv.intro)
   2.199 +    show "refl (carrier G) (rcong H)"
   2.200 +      by (auto simp add: r_congruent_def refl_def) 
   2.201 +  next
   2.202 +    show "sym (rcong H)"
   2.203 +    proof (simp add: r_congruent_def sym_def, clarify)
   2.204 +      fix x y
   2.205 +      assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
   2.206 +	 and "inv x \<otimes> y \<in> H"
   2.207 +      hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
   2.208 +      thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
   2.209 +    qed
   2.210 +  next
   2.211 +    show "trans (rcong H)"
   2.212 +    proof (simp add: r_congruent_def trans_def, clarify)
   2.213 +      fix x y z
   2.214 +      assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   2.215 +	 and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
   2.216 +      hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
   2.217 +      hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv) 
   2.218 +      thus "inv x \<otimes> z \<in> H" by simp
   2.219 +    qed
   2.220    qed
   2.221  qed
   2.222  
   2.223 @@ -625,31 +642,38 @@
   2.224  *)
   2.225  
   2.226  lemma (in subgroup) l_coset_eq_rcong:
   2.227 -  includes group G
   2.228 +  assumes "group G"
   2.229    assumes a: "a \<in> carrier G"
   2.230    shows "a <# H = rcong H `` {a}"
   2.231 -by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
   2.232 -
   2.233 +proof -
   2.234 +  interpret group [G] by fact
   2.235 +  show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
   2.236 +qed
   2.237  
   2.238  subsubsection{*Two Distinct Right Cosets are Disjoint*}
   2.239  
   2.240  lemma (in group) rcos_equation:
   2.241 -  includes subgroup H G
   2.242 -  shows
   2.243 -     "\<lbrakk>ha \<otimes> a = h \<otimes> b; a \<in> carrier G;  b \<in> carrier G;  
   2.244 -        h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
   2.245 -      \<Longrightarrow> hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
   2.246 -apply (rule UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
   2.247 -apply (simp add: ) 
   2.248 -apply (simp add: m_assoc transpose_inv)
   2.249 -done
   2.250 +  assumes "subgroup H G"
   2.251 +  assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
   2.252 +  shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
   2.253 +proof -
   2.254 +  interpret subgroup [H G] by fact
   2.255 +  from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
   2.256 +    apply (simp add: )
   2.257 +    apply (simp add: m_assoc transpose_inv)
   2.258 +    done
   2.259 +qed
   2.260  
   2.261  lemma (in group) rcos_disjoint:
   2.262 -  includes subgroup H G
   2.263 -  shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
   2.264 -apply (simp add: RCOSETS_def r_coset_def)
   2.265 -apply (blast intro: rcos_equation prems sym)
   2.266 -done
   2.267 +  assumes "subgroup H G"
   2.268 +  assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
   2.269 +  shows "a \<inter> b = {}"
   2.270 +proof -
   2.271 +  interpret subgroup [H G] by fact
   2.272 +  from p show ?thesis apply (simp add: RCOSETS_def r_coset_def)
   2.273 +    apply (blast intro: rcos_equation prems sym)
   2.274 +    done
   2.275 +qed
   2.276  
   2.277  subsection {* Further lemmas for @{text "r_congruent"} *}
   2.278  
   2.279 @@ -732,12 +756,16 @@
   2.280    "order S \<equiv> card (carrier S)"
   2.281  
   2.282  lemma (in group) rcosets_part_G:
   2.283 -  includes subgroup
   2.284 +  assumes "subgroup H G"
   2.285    shows "\<Union>(rcosets H) = carrier G"
   2.286 -apply (rule equalityI)
   2.287 - apply (force simp add: RCOSETS_def r_coset_def)
   2.288 -apply (auto simp add: RCOSETS_def intro: rcos_self prems)
   2.289 -done
   2.290 +proof -
   2.291 +  interpret subgroup [H G] by fact
   2.292 +  show ?thesis
   2.293 +    apply (rule equalityI)
   2.294 +    apply (force simp add: RCOSETS_def r_coset_def)
   2.295 +    apply (auto simp add: RCOSETS_def intro: rcos_self prems)
   2.296 +    done
   2.297 +qed
   2.298  
   2.299  lemma (in group) cosets_finite:
   2.300       "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
   2.301 @@ -815,9 +843,10 @@
   2.302  by (auto simp add: RCOSETS_def rcos_sum m_assoc)
   2.303  
   2.304  lemma (in subgroup) subgroup_in_rcosets:
   2.305 -  includes group G
   2.306 +  assumes "group G"
   2.307    shows "H \<in> rcosets H"
   2.308  proof -
   2.309 +  interpret group [G] by fact
   2.310    from _ subgroup_axioms have "H #> \<one> = H"
   2.311      by (rule coset_join2) auto
   2.312    then show ?thesis
     3.1 --- a/src/HOL/Algebra/Group.thy	Tue Jul 15 16:02:10 2008 +0200
     3.2 +++ b/src/HOL/Algebra/Group.thy	Tue Jul 15 16:50:09 2008 +0200
     3.3 @@ -396,9 +396,13 @@
     3.4    by (rule subgroup.subset)
     3.5  
     3.6  lemma (in subgroup) subgroup_is_group [intro]:
     3.7 -  includes group G
     3.8 -  shows "group (G\<lparr>carrier := H\<rparr>)" 
     3.9 -  by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
    3.10 +  assumes "group G"
    3.11 +  shows "group (G\<lparr>carrier := H\<rparr>)"
    3.12 +proof -
    3.13 +  interpret group [G] by fact
    3.14 +  show ?thesis
    3.15 +    by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
    3.16 +qed
    3.17  
    3.18  text {*
    3.19    Since @{term H} is nonempty, it contains some element @{term x}.  Since
    3.20 @@ -453,9 +457,11 @@
    3.21                  one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
    3.22  
    3.23  lemma DirProd_monoid:
    3.24 -  includes monoid G + monoid H
    3.25 +  assumes "monoid G" and "monoid H"
    3.26    shows "monoid (G \<times>\<times> H)"
    3.27  proof -
    3.28 +  interpret G: monoid [G] by fact
    3.29 +  interpret H: monoid [H] by fact
    3.30    from prems
    3.31    show ?thesis by (unfold monoid_def DirProd_def, auto) 
    3.32  qed
    3.33 @@ -463,11 +469,15 @@
    3.34  
    3.35  text{*Does not use the previous result because it's easier just to use auto.*}
    3.36  lemma DirProd_group:
    3.37 -  includes group G + group H
    3.38 +  assumes "group G" and "group H"
    3.39    shows "group (G \<times>\<times> H)"
    3.40 -  by (rule groupI)
    3.41 +proof -
    3.42 +  interpret G: group [G] by fact
    3.43 +  interpret H: group [H] by fact
    3.44 +  show ?thesis by (rule groupI)
    3.45       (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
    3.46             simp add: DirProd_def)
    3.47 +qed
    3.48  
    3.49  lemma carrier_DirProd [simp]:
    3.50       "carrier (G \<times>\<times> H) = carrier G \<times> carrier H"
    3.51 @@ -482,23 +492,29 @@
    3.52    by (simp add: DirProd_def)
    3.53  
    3.54  lemma inv_DirProd [simp]:
    3.55 -  includes group G + group H
    3.56 +  assumes "group G" and "group H"
    3.57    assumes g: "g \<in> carrier G"
    3.58        and h: "h \<in> carrier H"
    3.59    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
    3.60 -  apply (rule group.inv_equality [OF DirProd_group])
    3.61 +proof -
    3.62 +  interpret G: group [G] by fact
    3.63 +  interpret H: group [H] by fact
    3.64 +  show ?thesis apply (rule group.inv_equality [OF DirProd_group])
    3.65    apply (simp_all add: prems group.l_inv)
    3.66    done
    3.67 +qed
    3.68  
    3.69  text{*This alternative proof of the previous result demonstrates interpret.
    3.70     It uses @{text Prod.inv_equality} (available after @{text interpret})
    3.71     instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
    3.72  lemma
    3.73 -  includes group G + group H
    3.74 +  assumes "group G" and "group H"
    3.75    assumes g: "g \<in> carrier G"
    3.76        and h: "h \<in> carrier H"
    3.77    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
    3.78  proof -
    3.79 +  interpret G: group [G] by fact
    3.80 +  interpret H: group [H] by fact
    3.81    interpret Prod: group ["G \<times>\<times> H"]
    3.82      by (auto intro: DirProd_group group.intro group.axioms prems)
    3.83    show ?thesis by (simp add: Prod.inv_equality g h)
     4.1 --- a/src/HOL/Algebra/Ideal.thy	Tue Jul 15 16:02:10 2008 +0200
     4.2 +++ b/src/HOL/Algebra/Ideal.thy	Tue Jul 15 16:50:09 2008 +0200
     4.3 @@ -28,18 +28,21 @@
     4.4  by (rule ideal_axioms)
     4.5  
     4.6  lemma idealI:
     4.7 -  includes ring
     4.8 +  fixes R (structure)
     4.9 +  assumes "ring R"
    4.10    assumes a_subgroup: "subgroup I \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
    4.11        and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    4.12        and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
    4.13    shows "ideal I R"
    4.14 -  apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
    4.15 +proof -
    4.16 +  interpret ring [R] by fact
    4.17 +  show ?thesis  apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
    4.18       apply (rule a_subgroup)
    4.19      apply (rule is_ring)
    4.20     apply (erule (1) I_l_closed)
    4.21    apply (erule (1) I_r_closed)
    4.22    done
    4.23 -
    4.24 +qed
    4.25  
    4.26  subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
    4.27  
    4.28 @@ -58,11 +61,14 @@
    4.29  by (rule principalideal_axioms)
    4.30  
    4.31  lemma principalidealI:
    4.32 -  includes ideal
    4.33 +  fixes R (structure)
    4.34 +  assumes "ideal I R"
    4.35    assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
    4.36    shows "principalideal I R"
    4.37 -  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
    4.38 -
    4.39 +proof -
    4.40 +  interpret ideal [I R] by fact
    4.41 +  show ?thesis  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
    4.42 +qed
    4.43  
    4.44  subsection {* Maximal Ideals *}
    4.45  
    4.46 @@ -75,13 +81,16 @@
    4.47  by (rule maximalideal_axioms)
    4.48  
    4.49  lemma maximalidealI:
    4.50 -  includes ideal
    4.51 +  fixes R
    4.52 +  assumes "ideal I R"
    4.53    assumes I_notcarr: "carrier R \<noteq> I"
    4.54       and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
    4.55    shows "maximalideal I R"
    4.56 -  by (intro maximalideal.intro maximalideal_axioms.intro)
    4.57 +proof -
    4.58 +  interpret ideal [I R] by fact
    4.59 +  show ?thesis by (intro maximalideal.intro maximalideal_axioms.intro)
    4.60      (rule is_ideal, rule I_notcarr, rule I_maximal)
    4.61 -
    4.62 +qed
    4.63  
    4.64  subsection {* Prime Ideals *}
    4.65  
    4.66 @@ -94,31 +103,40 @@
    4.67  by (rule primeideal_axioms)
    4.68  
    4.69  lemma primeidealI:
    4.70 -  includes ideal
    4.71 -  includes cring
    4.72 +  fixes R (structure)
    4.73 +  assumes "ideal I R"
    4.74 +  assumes "cring R"
    4.75    assumes I_notcarr: "carrier R \<noteq> I"
    4.76        and 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"
    4.77    shows "primeideal I R"
    4.78 -  by (intro primeideal.intro primeideal_axioms.intro)
    4.79 +proof -
    4.80 +  interpret ideal [I R] by fact
    4.81 +  interpret cring [R] by fact
    4.82 +  show ?thesis by (intro primeideal.intro primeideal_axioms.intro)
    4.83      (rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
    4.84 +qed
    4.85  
    4.86  lemma primeidealI2:
    4.87 -  includes additive_subgroup I R
    4.88 -  includes cring
    4.89 +  fixes R (structure)
    4.90 +  assumes "additive_subgroup I R"
    4.91 +  assumes "cring R"
    4.92    assumes I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    4.93        and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
    4.94        and I_notcarr: "carrier R \<noteq> I"
    4.95        and 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"
    4.96    shows "primeideal I R"
    4.97 -apply (intro_locales)
    4.98 - apply (intro ideal_axioms.intro)
    4.99 -  apply (erule (1) I_l_closed)
   4.100 - apply (erule (1) I_r_closed)
   4.101 -apply (intro primeideal_axioms.intro)
   4.102 - apply (rule I_notcarr)
   4.103 -apply (erule (2) I_prime)
   4.104 -done
   4.105 -
   4.106 +proof -
   4.107 +  interpret additive_subgroup [I R] by fact
   4.108 +  interpret cring [R] by fact
   4.109 +  show ?thesis apply (intro_locales)
   4.110 +    apply (intro ideal_axioms.intro)
   4.111 +    apply (erule (1) I_l_closed)
   4.112 +    apply (erule (1) I_r_closed)
   4.113 +    apply (intro primeideal_axioms.intro)
   4.114 +    apply (rule I_notcarr)
   4.115 +    apply (erule (2) I_prime)
   4.116 +    done
   4.117 +qed
   4.118  
   4.119  section {* Properties of Ideals *}
   4.120  
   4.121 @@ -185,9 +203,13 @@
   4.122  text {* \paragraph{Intersection of two ideals} The intersection of any
   4.123    two ideals is again an ideal in @{term R} *}
   4.124  lemma (in ring) i_intersect:
   4.125 -  includes ideal I R
   4.126 -  includes ideal J R
   4.127 +  assumes "ideal I R"
   4.128 +  assumes "ideal J R"
   4.129    shows "ideal (I \<inter> J) R"
   4.130 +proof -
   4.131 +  interpret ideal [I R] by fact
   4.132 +  interpret ideal [J R] by fact
   4.133 +  show ?thesis
   4.134  apply (intro idealI subgroup.intro)
   4.135        apply (rule is_ring)
   4.136       apply (force simp add: a_subset)
   4.137 @@ -199,7 +221,7 @@
   4.138  apply (clarsimp, rule)
   4.139   apply (fast intro: ideal.I_r_closed ideal.intro prems)+
   4.140  done
   4.141 -
   4.142 +qed
   4.143  
   4.144  subsubsection {* Intersection of a Set of Ideals *}
   4.145  
   4.146 @@ -511,15 +533,18 @@
   4.147  text {* @{const "cgenideal"} is minimal *}
   4.148  
   4.149  lemma (in ring) cgenideal_minimal:
   4.150 -  includes ideal J R
   4.151 +  assumes "ideal J R"
   4.152    assumes aJ: "a \<in> J"
   4.153    shows "PIdl a \<subseteq> J"
   4.154 -unfolding cgenideal_def
   4.155 -apply rule
   4.156 -apply clarify
   4.157 -using aJ
   4.158 -apply (erule I_l_closed)
   4.159 -done
   4.160 +proof -
   4.161 +  interpret ideal [J R] by fact
   4.162 +  show ?thesis unfolding cgenideal_def
   4.163 +    apply rule
   4.164 +    apply clarify
   4.165 +    using aJ
   4.166 +    apply (erule I_l_closed)
   4.167 +    done
   4.168 +qed
   4.169  
   4.170  lemma (in cring) cgenideal_eq_genideal:
   4.171    assumes icarr: "i \<in> carrier R"
   4.172 @@ -636,9 +661,10 @@
   4.173  
   4.174  text {* Every principal ideal is a right coset of the carrier *}
   4.175  lemma (in principalideal) rcos_generate:
   4.176 -  includes cring
   4.177 +  assumes "cring R"
   4.178    shows "\<exists>x\<in>I. I = carrier R #> x"
   4.179  proof -
   4.180 +  interpret cring [R] by fact
   4.181    from generate
   4.182        obtain i
   4.183          where icarr: "i \<in> carrier R"
   4.184 @@ -667,10 +693,11 @@
   4.185  subsection {* Prime Ideals *}
   4.186  
   4.187  lemma (in ideal) primeidealCD:
   4.188 -  includes cring
   4.189 +  assumes "cring R"
   4.190    assumes notprime: "\<not> primeideal I R"
   4.191    shows "carrier R = I \<or> (\<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)"
   4.192  proof (rule ccontr, clarsimp)
   4.193 +  interpret cring [R] by fact
   4.194    assume InR: "carrier R \<noteq> I"
   4.195       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)"
   4.196    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
   4.197 @@ -685,11 +712,16 @@
   4.198  qed
   4.199  
   4.200  lemma (in ideal) primeidealCE:
   4.201 -  includes cring
   4.202 +  assumes "cring R"
   4.203    assumes notprime: "\<not> primeideal I R"
   4.204    obtains "carrier R = I"
   4.205      | "\<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"
   4.206 -  using primeidealCD [OF R.is_cring notprime] by blast
   4.207 +proof -
   4.208 +  interpret R: cring [R] by fact
   4.209 +  assume "carrier R = I ==> thesis"
   4.210 +    and "\<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 \<Longrightarrow> thesis"
   4.211 +  then show thesis using primeidealCD [OF R.is_cring notprime] by blast
   4.212 +qed
   4.213  
   4.214  text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *}
   4.215  lemma (in cring) zeroprimeideal_domainI:
   4.216 @@ -739,103 +771,108 @@
   4.217  qed
   4.218  
   4.219  lemma (in ideal) helper_max_prime:
   4.220 -  includes cring
   4.221 +  assumes "cring R"
   4.222    assumes acarr: "a \<in> carrier R"
   4.223    shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"
   4.224 -apply (rule idealI)
   4.225 -   apply (rule cring.axioms[OF is_cring])
   4.226 -  apply (rule subgroup.intro)
   4.227 -     apply (simp, fast)
   4.228 +proof -
   4.229 +  interpret cring [R] by fact
   4.230 +  show ?thesis apply (rule idealI)
   4.231 +    apply (rule cring.axioms[OF is_cring])
   4.232 +    apply (rule subgroup.intro)
   4.233 +    apply (simp, fast)
   4.234      apply clarsimp apply (simp add: r_distr acarr)
   4.235 -   apply (simp add: acarr)
   4.236 -  apply (simp add: a_inv_def[symmetric], clarify) defer 1
   4.237 -  apply clarsimp defer 1
   4.238 -  apply (fast intro!: helper_I_closed acarr)
   4.239 -proof -
   4.240 -  fix x
   4.241 -  assume xcarr: "x \<in> carrier R"
   4.242 -     and ax: "a \<otimes> x \<in> I"
   4.243 -  from ax and acarr xcarr
   4.244 -      have "\<ominus>(a \<otimes> x) \<in> I" by simp
   4.245 -  also from acarr xcarr
   4.246 -      have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra
   4.247 -  finally
   4.248 -      show "a \<otimes> (\<ominus>x) \<in> I" .
   4.249 -  from acarr
   4.250 -      have "a \<otimes> \<zero> = \<zero>" by simp
   4.251 -next
   4.252 -  fix x y
   4.253 -  assume xcarr: "x \<in> carrier R"
   4.254 -     and ycarr: "y \<in> carrier R"
   4.255 -     and ayI: "a \<otimes> y \<in> I"
   4.256 -  from ayI and acarr xcarr ycarr
   4.257 -      have "a \<otimes> (y \<otimes> x) \<in> I" by (simp add: helper_I_closed)
   4.258 -  moreover from xcarr ycarr
   4.259 -      have "y \<otimes> x = x \<otimes> y" by (simp add: m_comm)
   4.260 -  ultimately
   4.261 -      show "a \<otimes> (x \<otimes> y) \<in> I" by simp
   4.262 +    apply (simp add: acarr)
   4.263 +    apply (simp add: a_inv_def[symmetric], clarify) defer 1
   4.264 +    apply clarsimp defer 1
   4.265 +    apply (fast intro!: helper_I_closed acarr)
   4.266 +  proof -
   4.267 +    fix x
   4.268 +    assume xcarr: "x \<in> carrier R"
   4.269 +      and ax: "a \<otimes> x \<in> I"
   4.270 +    from ax and acarr xcarr
   4.271 +    have "\<ominus>(a \<otimes> x) \<in> I" by simp
   4.272 +    also from acarr xcarr
   4.273 +    have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra
   4.274 +    finally
   4.275 +    show "a \<otimes> (\<ominus>x) \<in> I" .
   4.276 +    from acarr
   4.277 +    have "a \<otimes> \<zero> = \<zero>" by simp
   4.278 +  next
   4.279 +    fix x y
   4.280 +    assume xcarr: "x \<in> carrier R"
   4.281 +      and ycarr: "y \<in> carrier R"
   4.282 +      and ayI: "a \<otimes> y \<in> I"
   4.283 +    from ayI and acarr xcarr ycarr
   4.284 +    have "a \<otimes> (y \<otimes> x) \<in> I" by (simp add: helper_I_closed)
   4.285 +    moreover from xcarr ycarr
   4.286 +    have "y \<otimes> x = x \<otimes> y" by (simp add: m_comm)
   4.287 +    ultimately
   4.288 +    show "a \<otimes> (x \<otimes> y) \<in> I" by simp
   4.289 +  qed
   4.290  qed
   4.291  
   4.292  text {* In a cring every maximal ideal is prime *}
   4.293  lemma (in cring) maximalideal_is_prime:
   4.294 -  includes maximalideal
   4.295 +  assumes "maximalideal I R"
   4.296    shows "primeideal I R"
   4.297 -apply (rule ccontr)
   4.298 -apply (rule primeidealCE)
   4.299 -   apply (rule is_cring)
   4.300 -  apply assumption
   4.301 - apply (simp add: I_notcarr)
   4.302  proof -
   4.303 -  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"
   4.304 -  from this
   4.305 -      obtain a b
   4.306 -        where acarr: "a \<in> carrier R"
   4.307 -        and bcarr: "b \<in> carrier R"
   4.308 -        and abI: "a \<otimes> b \<in> I"
   4.309 -        and anI: "a \<notin> I"
   4.310 -        and bnI: "b \<notin> I"
   4.311 +  interpret maximalideal [I R] by fact
   4.312 +  show ?thesis apply (rule ccontr)
   4.313 +    apply (rule primeidealCE)
   4.314 +    apply (rule is_cring)
   4.315 +    apply assumption
   4.316 +    apply (simp add: I_notcarr)
   4.317 +  proof -
   4.318 +    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"
   4.319 +    from this
   4.320 +    obtain a b
   4.321 +      where acarr: "a \<in> carrier R"
   4.322 +      and bcarr: "b \<in> carrier R"
   4.323 +      and abI: "a \<otimes> b \<in> I"
   4.324 +      and anI: "a \<notin> I"
   4.325 +      and bnI: "b \<notin> I"
   4.326        by fast
   4.327 -  def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
   4.328 -
   4.329 -  from R.is_cring and acarr
   4.330 -  have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
   4.331 -
   4.332 -  have IsubJ: "I \<subseteq> J"
   4.333 -  proof
   4.334 -    fix x
   4.335 -    assume xI: "x \<in> I"
   4.336 -    from this and acarr
   4.337 -    have "a \<otimes> x \<in> I" by (intro I_l_closed)
   4.338 -    from xI[THEN a_Hcarr] this
   4.339 -    show "x \<in> J" unfolding J_def by fast
   4.340 +    def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
   4.341 +    
   4.342 +    from R.is_cring and acarr
   4.343 +    have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
   4.344 +    
   4.345 +    have IsubJ: "I \<subseteq> J"
   4.346 +    proof
   4.347 +      fix x
   4.348 +      assume xI: "x \<in> I"
   4.349 +      from this and acarr
   4.350 +      have "a \<otimes> x \<in> I" by (intro I_l_closed)
   4.351 +      from xI[THEN a_Hcarr] this
   4.352 +      show "x \<in> J" unfolding J_def by fast
   4.353 +    qed
   4.354 +    
   4.355 +    from abI and acarr bcarr
   4.356 +    have "b \<in> J" unfolding J_def by fast
   4.357 +    from bnI and this
   4.358 +    have JnI: "J \<noteq> I" by fast
   4.359 +    from acarr
   4.360 +    have "a = a \<otimes> \<one>" by algebra
   4.361 +    from this and anI
   4.362 +    have "a \<otimes> \<one> \<notin> I" by simp
   4.363 +    from one_closed and this
   4.364 +    have "\<one> \<notin> J" unfolding J_def by fast
   4.365 +    hence Jncarr: "J \<noteq> carrier R" by fast
   4.366 +    
   4.367 +    interpret ideal ["J" "R"] by (rule idealJ)
   4.368 +    
   4.369 +    have "J = I \<or> J = carrier R"
   4.370 +      apply (intro I_maximal)
   4.371 +      apply (rule idealJ)
   4.372 +      apply (rule IsubJ)
   4.373 +      apply (rule a_subset)
   4.374 +      done
   4.375 +    
   4.376 +    from this and JnI and Jncarr
   4.377 +    show "False" by simp
   4.378    qed
   4.379 -
   4.380 -  from abI and acarr bcarr
   4.381 -      have "b \<in> J" unfolding J_def by fast
   4.382 -  from bnI and this
   4.383 -      have JnI: "J \<noteq> I" by fast
   4.384 -  from acarr
   4.385 -      have "a = a \<otimes> \<one>" by algebra
   4.386 -  from this and anI
   4.387 -      have "a \<otimes> \<one> \<notin> I" by simp
   4.388 -  from one_closed and this
   4.389 -      have "\<one> \<notin> J" unfolding J_def by fast
   4.390 -  hence Jncarr: "J \<noteq> carrier R" by fast
   4.391 -
   4.392 -  interpret ideal ["J" "R"] by (rule idealJ)
   4.393 -
   4.394 -  have "J = I \<or> J = carrier R"
   4.395 -     apply (intro I_maximal)
   4.396 -     apply (rule idealJ)
   4.397 -     apply (rule IsubJ)
   4.398 -     apply (rule a_subset)
   4.399 -     done
   4.400 -
   4.401 -  from this and JnI and Jncarr
   4.402 -      show "False" by simp
   4.403  qed
   4.404  
   4.405 -
   4.406  subsection {* Derived Theorems Involving Ideals *}
   4.407  
   4.408  --"A non-zero cring that has only the two trivial ideals is a field"
     5.1 --- a/src/HOL/Algebra/QuotRing.thy	Tue Jul 15 16:02:10 2008 +0200
     5.2 +++ b/src/HOL/Algebra/QuotRing.thy	Tue Jul 15 16:50:09 2008 +0200
     5.3 @@ -155,27 +155,32 @@
     5.4  
     5.5  text {* The quotient of a cring is also commutative *}
     5.6  lemma (in ideal) quotient_is_cring:
     5.7 -  includes cring
     5.8 +  assumes "cring R"
     5.9    shows "cring (R Quot I)"
    5.10 -apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
    5.11 +proof -
    5.12 +  interpret cring [R] by fact
    5.13 +  show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
    5.14    apply (rule quotient_is_ring)
    5.15   apply (rule ring.axioms[OF quotient_is_ring])
    5.16  apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric])
    5.17  apply clarify
    5.18  apply (simp add: rcoset_mult_add m_comm)
    5.19  done
    5.20 +qed
    5.21  
    5.22  text {* Cosets as a ring homomorphism on crings *}
    5.23  lemma (in ideal) rcos_ring_hom_cring:
    5.24 -  includes cring
    5.25 +  assumes "cring R"
    5.26    shows "ring_hom_cring R (R Quot I) (op +> I)"
    5.27 -apply (rule ring_hom_cringI)
    5.28 +proof -
    5.29 +  interpret cring [R] by fact
    5.30 +  show ?thesis apply (rule ring_hom_cringI)
    5.31    apply (rule rcos_ring_hom_ring)
    5.32   apply (rule R.is_cring)
    5.33  apply (rule quotient_is_cring)
    5.34  apply (rule R.is_cring)
    5.35  done
    5.36 -
    5.37 +qed
    5.38  
    5.39  subsection {* Factorization over Prime Ideals *}
    5.40  
    5.41 @@ -236,9 +241,11 @@
    5.42          The proof follows ``W. Adkins, S. Weintraub: Algebra --
    5.43          An Approach via Module Theory'' *}
    5.44  lemma (in maximalideal) quotient_is_field:
    5.45 -  includes cring
    5.46 +  assumes "cring R"
    5.47    shows "field (R Quot I)"
    5.48 -apply (intro cring.cring_fieldI2)
    5.49 +proof -
    5.50 +  interpret cring [R] by fact
    5.51 +  show ?thesis apply (intro cring.cring_fieldI2)
    5.52    apply (rule quotient_is_cring, rule is_cring)
    5.53   defer 1
    5.54   apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
    5.55 @@ -338,5 +345,6 @@
    5.56    from rcarr and this[symmetric]
    5.57    show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
    5.58  qed
    5.59 +qed
    5.60  
    5.61  end
     6.1 --- a/src/HOL/Algebra/Ring.thy	Tue Jul 15 16:02:10 2008 +0200
     6.2 +++ b/src/HOL/Algebra/Ring.thy	Tue Jul 15 16:50:09 2008 +0200
     6.3 @@ -539,16 +539,26 @@
     6.4  text {* Two examples for use of method algebra *}
     6.5  
     6.6  lemma
     6.7 -  includes ring R + cring S
     6.8 -  shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==> 
     6.9 -  a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
    6.10 -  by algebra
    6.11 +  fixes R (structure) and S (structure)
    6.12 +  assumes "ring R" "cring S"
    6.13 +  assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
    6.14 +  shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
    6.15 +proof -
    6.16 +  interpret ring [R] by fact
    6.17 +  interpret cring [S] by fact
    6.18 +ML_val {* Algebra.print_structures @{context} *}
    6.19 +  from RS show ?thesis by algebra
    6.20 +qed
    6.21  
    6.22  lemma
    6.23 -  includes cring
    6.24 -  shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
    6.25 -  by algebra
    6.26 -
    6.27 +  fixes R (structure)
    6.28 +  assumes "ring R"
    6.29 +  assumes R: "a \<in> carrier R" "b \<in> carrier R"
    6.30 +  shows "a \<ominus> (a \<ominus> b) = b"
    6.31 +proof -
    6.32 +  interpret ring [R] by fact
    6.33 +  from R show ?thesis by algebra
    6.34 +qed
    6.35  
    6.36  subsubsection {* Sums over Finite Sets *}
    6.37  
     7.1 --- a/src/HOL/Algebra/RingHom.thy	Tue Jul 15 16:02:10 2008 +0200
     7.2 +++ b/src/HOL/Algebra/RingHom.thy	Tue Jul 15 16:50:09 2008 +0200
     7.3 @@ -31,55 +31,73 @@
     7.4  done
     7.5  
     7.6  lemma (in ring_hom_ring) is_ring_hom_ring:
     7.7 -  includes struct R + struct S
     7.8 -  shows "ring_hom_ring R S h"
     7.9 -by (rule ring_hom_ring_axioms)
    7.10 +  "ring_hom_ring R S h"
    7.11 +  by (rule ring_hom_ring_axioms)
    7.12  
    7.13  lemma ring_hom_ringI:
    7.14 -  includes ring R + ring S
    7.15 +  fixes R (structure) and S (structure)
    7.16 +  assumes "ring R" "ring S"
    7.17    assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
    7.18            hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
    7.19        and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    7.20        and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
    7.21        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    7.22    shows "ring_hom_ring R S h"
    7.23 -apply unfold_locales
    7.24 +proof -
    7.25 +  interpret ring [R] by fact
    7.26 +  interpret ring [S] by fact
    7.27 +  show ?thesis apply unfold_locales
    7.28  apply (unfold ring_hom_def, safe)
    7.29     apply (simp add: hom_closed Pi_def)
    7.30    apply (erule (1) compatible_mult)
    7.31   apply (erule (1) compatible_add)
    7.32  apply (rule compatible_one)
    7.33  done
    7.34 +qed
    7.35  
    7.36  lemma ring_hom_ringI2:
    7.37 -  includes ring R + ring S
    7.38 +  assumes "ring R" "ring S"
    7.39    assumes h: "h \<in> ring_hom R S"
    7.40    shows "ring_hom_ring R S h"
    7.41 -apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
    7.42 -apply (rule R.is_ring)
    7.43 -apply (rule S.is_ring)
    7.44 -apply (rule h)
    7.45 -done
    7.46 +proof -
    7.47 +  interpret R: ring [R] by fact
    7.48 +  interpret S: ring [S] by fact
    7.49 +  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
    7.50 +    apply (rule R.is_ring)
    7.51 +    apply (rule S.is_ring)
    7.52 +    apply (rule h)
    7.53 +    done
    7.54 +qed
    7.55  
    7.56  lemma ring_hom_ringI3:
    7.57 -  includes abelian_group_hom R S + ring R + ring S 
    7.58 +  fixes R (structure) and S (structure)
    7.59 +  assumes "abelian_group_hom R S h" "ring R" "ring S" 
    7.60    assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
    7.61        and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    7.62    shows "ring_hom_ring R S h"
    7.63 -apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
    7.64 -apply (insert group_hom.homh[OF a_group_hom])
    7.65 -apply (unfold hom_def ring_hom_def, simp)
    7.66 -apply safe
    7.67 -apply (erule (1) compatible_mult)
    7.68 -apply (rule compatible_one)
    7.69 -done
    7.70 +proof -
    7.71 +  interpret abelian_group_hom [R S h] by fact
    7.72 +  interpret R: ring [R] by fact
    7.73 +  interpret S: ring [S] by fact
    7.74 +  show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
    7.75 +    apply (insert group_hom.homh[OF a_group_hom])
    7.76 +    apply (unfold hom_def ring_hom_def, simp)
    7.77 +    apply safe
    7.78 +    apply (erule (1) compatible_mult)
    7.79 +    apply (rule compatible_one)
    7.80 +    done
    7.81 +qed
    7.82  
    7.83  lemma ring_hom_cringI:
    7.84 -  includes ring_hom_ring R S h + cring R + cring S
    7.85 +  assumes "ring_hom_ring R S h" "cring R" "cring S"
    7.86    shows "ring_hom_cring R S h"
    7.87 -  by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    7.88 +proof -
    7.89 +  interpret ring_hom_ring [R S h] by fact
    7.90 +  interpret R: cring [R] by fact
    7.91 +  interpret S: cring [S] by fact
    7.92 +  show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
    7.93      (rule R.is_cring, rule S.is_cring, rule homh)
    7.94 -
    7.95 +qed
    7.96  
    7.97  subsection {* The kernel of a ring homomorphism *}
    7.98  
     8.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Jul 15 16:02:10 2008 +0200
     8.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Tue Jul 15 16:50:09 2008 +0200
     8.3 @@ -1254,15 +1254,17 @@
     8.4      cring.axioms prems)
     8.5  
     8.6  lemma (in UP_pre_univ_prop) UP_hom_unique:
     8.7 -  includes ring_hom_cring P S Phi
     8.8 +  assumes "ring_hom_cring P S Phi"
     8.9    assumes Phi: "Phi (monom P \<one> (Suc 0)) = s"
    8.10        "!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
    8.11 -  includes ring_hom_cring P S Psi
    8.12 +  assumes "ring_hom_cring P S Psi"
    8.13    assumes Psi: "Psi (monom P \<one> (Suc 0)) = s"
    8.14        "!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
    8.15      and P: "p \<in> carrier P" and S: "s \<in> carrier S"
    8.16    shows "Phi p = Psi p"
    8.17  proof -
    8.18 +  interpret ring_hom_cring [P S Phi] by fact
    8.19 +  interpret ring_hom_cring [P S Psi] by fact
    8.20    have "Phi p =
    8.21        Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 (^)\<^bsub>P\<^esub> i)"
    8.22      by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
     9.1 --- a/src/HOL/Finite_Set.thy	Tue Jul 15 16:02:10 2008 +0200
     9.2 +++ b/src/HOL/Finite_Set.thy	Tue Jul 15 16:50:09 2008 +0200
     9.3 @@ -753,11 +753,14 @@
     9.4  *}
     9.5  
     9.6  lemma fold_fusion:
     9.7 -  includes ab_semigroup_mult g
     9.8 +  assumes "ab_semigroup_mult g"
     9.9    assumes fin: "finite A"
    9.10      and hyp: "\<And>x y. h (g x y) = times x (h y)"
    9.11    shows "h (fold g j w A) = fold times j (h w) A"
    9.12 -  using fin hyp by (induct set: finite) simp_all
    9.13 +proof -
    9.14 +  interpret ab_semigroup_mult [g] by fact
    9.15 +  show ?thesis using fin hyp by (induct set: finite) simp_all
    9.16 +qed
    9.17  
    9.18  lemma fold_cong:
    9.19    "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold times g z A = fold times h z A"
    10.1 --- a/src/HOL/Hyperreal/FrechetDeriv.thy	Tue Jul 15 16:02:10 2008 +0200
    10.2 +++ b/src/HOL/Hyperreal/FrechetDeriv.thy	Tue Jul 15 16:50:09 2008 +0200
    10.3 @@ -61,19 +61,23 @@
    10.4  by simp
    10.5  
    10.6  lemma bounded_linear_add:
    10.7 -  includes bounded_linear f
    10.8 -  includes bounded_linear g
    10.9 +  assumes "bounded_linear f"
   10.10 +  assumes "bounded_linear g"
   10.11    shows "bounded_linear (\<lambda>x. f x + g x)"
   10.12 -apply (unfold_locales)
   10.13 -apply (simp only: f.add g.add add_ac)
   10.14 -apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
   10.15 -apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
   10.16 -apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
   10.17 -apply (rule_tac x="Kf + Kg" in exI, safe)
   10.18 -apply (subst right_distrib)
   10.19 -apply (rule order_trans [OF norm_triangle_ineq])
   10.20 -apply (rule add_mono, erule spec, erule spec)
   10.21 -done
   10.22 +proof -
   10.23 +  interpret f: bounded_linear [f] by fact
   10.24 +  interpret g: bounded_linear [g] by fact
   10.25 +  show ?thesis apply (unfold_locales)
   10.26 +    apply (simp only: f.add g.add add_ac)
   10.27 +    apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
   10.28 +    apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
   10.29 +    apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
   10.30 +    apply (rule_tac x="Kf + Kg" in exI, safe)
   10.31 +    apply (subst right_distrib)
   10.32 +    apply (rule order_trans [OF norm_triangle_ineq])
   10.33 +    apply (rule add_mono, erule spec, erule spec)
   10.34 +    done
   10.35 +qed
   10.36  
   10.37  lemma norm_ratio_ineq:
   10.38    fixes x y :: "'a::real_normed_vector"
   10.39 @@ -117,13 +121,16 @@
   10.40  subsection {* Subtraction *}
   10.41  
   10.42  lemma bounded_linear_minus:
   10.43 -  includes bounded_linear f
   10.44 +  assumes "bounded_linear f"
   10.45    shows "bounded_linear (\<lambda>x. - f x)"
   10.46 -apply (unfold_locales)
   10.47 -apply (simp add: f.add)
   10.48 -apply (simp add: f.scaleR)
   10.49 -apply (simp add: f.bounded)
   10.50 -done
   10.51 +proof -
   10.52 +  interpret f: bounded_linear [f] by fact
   10.53 +  show ?thesis apply (unfold_locales)
   10.54 +    apply (simp add: f.add)
   10.55 +    apply (simp add: f.scaleR)
   10.56 +    apply (simp add: f.bounded)
   10.57 +    done
   10.58 +qed
   10.59  
   10.60  lemma FDERIV_minus:
   10.61    "FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)"
   10.62 @@ -169,30 +176,34 @@
   10.63  by simp
   10.64  
   10.65  lemma bounded_linear_compose:
   10.66 -  includes bounded_linear f
   10.67 -  includes bounded_linear g
   10.68 +  assumes "bounded_linear f"
   10.69 +  assumes "bounded_linear g"
   10.70    shows "bounded_linear (\<lambda>x. f (g x))"
   10.71 -proof (unfold_locales)
   10.72 -  fix x y show "f (g (x + y)) = f (g x) + f (g y)"
   10.73 -    by (simp only: f.add g.add)
   10.74 -next
   10.75 -  fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
   10.76 -    by (simp only: f.scaleR g.scaleR)
   10.77 -next
   10.78 -  from f.pos_bounded
   10.79 -  obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
   10.80 -  from g.pos_bounded
   10.81 -  obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
   10.82 -  show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
   10.83 -  proof (intro exI allI)
   10.84 -    fix x
   10.85 -    have "norm (f (g x)) \<le> norm (g x) * Kf"
   10.86 -      using f .
   10.87 -    also have "\<dots> \<le> (norm x * Kg) * Kf"
   10.88 -      using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
   10.89 -    also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
   10.90 -      by (rule mult_assoc)
   10.91 -    finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
   10.92 +proof -
   10.93 +  interpret f: bounded_linear [f] by fact
   10.94 +  interpret g: bounded_linear [g] by fact
   10.95 +  show ?thesis proof (unfold_locales)
   10.96 +    fix x y show "f (g (x + y)) = f (g x) + f (g y)"
   10.97 +      by (simp only: f.add g.add)
   10.98 +  next
   10.99 +    fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
  10.100 +      by (simp only: f.scaleR g.scaleR)
  10.101 +  next
  10.102 +    from f.pos_bounded
  10.103 +    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
  10.104 +    from g.pos_bounded
  10.105 +    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
  10.106 +    show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
  10.107 +    proof (intro exI allI)
  10.108 +      fix x
  10.109 +      have "norm (f (g x)) \<le> norm (g x) * Kf"
  10.110 +	using f .
  10.111 +      also have "\<dots> \<le> (norm x * Kg) * Kf"
  10.112 +	using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
  10.113 +      also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
  10.114 +	by (rule mult_assoc)
  10.115 +      finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
  10.116 +    qed
  10.117    qed
  10.118  qed
  10.119  
    11.1 --- a/src/HOL/Library/Multiset.thy	Tue Jul 15 16:02:10 2008 +0200
    11.2 +++ b/src/HOL/Library/Multiset.thy	Tue Jul 15 16:50:09 2008 +0200
    11.3 @@ -1421,9 +1421,12 @@
    11.4  qed
    11.5  
    11.6  lemma fold_mset_fusion:
    11.7 -  includes left_commutative g
    11.8 -  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A"
    11.9 -by (induct A) auto
   11.10 +  assumes "left_commutative g"
   11.11 +  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
   11.12 +proof -
   11.13 +  interpret left_commutative [g] by fact
   11.14 +  show "PROP ?P" by (induct A) auto
   11.15 +qed
   11.16  
   11.17  lemma fold_mset_rec:
   11.18    assumes "a \<in># A" 
    12.1 --- a/src/HOL/MicroJava/BV/Err.thy	Tue Jul 15 16:02:10 2008 +0200
    12.2 +++ b/src/HOL/MicroJava/BV/Err.thy	Tue Jul 15 16:50:09 2008 +0200
    12.3 @@ -135,19 +135,21 @@
    12.4    "~(Err <_(le r) x)"
    12.5    by (simp add: lesssub_def lesub_def le_def split: err.split)
    12.6  
    12.7 -lemma semilat_errI [intro]: includes semilat
    12.8 -shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
    12.9 -apply(insert semilat)
   12.10 -apply (unfold semilat_Def closed_def plussub_def lesub_def 
   12.11 -              lift2_def Err.le_def err_def)
   12.12 -apply (simp split: err.split)
   12.13 -done
   12.14 +lemma semilat_errI [intro]:
   12.15 +  assumes semilat: "semilat (A, r, f)"
   12.16 +  shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
   12.17 +  apply(insert semilat)
   12.18 +  apply (unfold semilat_Def closed_def plussub_def lesub_def 
   12.19 +    lift2_def Err.le_def err_def)
   12.20 +  apply (simp split: err.split)
   12.21 +  done
   12.22  
   12.23  lemma err_semilat_eslI_aux:
   12.24 -includes semilat shows "err_semilat(esl(A,r,f))"
   12.25 -apply (unfold sl_def esl_def)
   12.26 -apply (simp add: semilat_errI[OF semilat])
   12.27 -done
   12.28 +  assumes semilat: "semilat (A, r, f)"
   12.29 +  shows "err_semilat(esl(A,r,f))"
   12.30 +  apply (unfold sl_def esl_def)
   12.31 +  apply (simp add: semilat_errI[OF semilat])
   12.32 +  done
   12.33  
   12.34  lemma err_semilat_eslI [intro, simp]:
   12.35   "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
    13.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Tue Jul 15 16:02:10 2008 +0200
    13.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Tue Jul 15 16:50:09 2008 +0200
    13.3 @@ -313,36 +313,44 @@
    13.4    apply (blast intro: order_trans)
    13.5    done
    13.6  
    13.7 -lemma termination_lemma: includes semilat
    13.8 -shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
    13.9 -      ss <[r] merges f qs ss \<or> 
   13.10 -  merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w"
   13.11 -apply(insert semilat)
   13.12 -  apply (unfold lesssub_def)
   13.13 -  apply (simp (no_asm_simp) add: merges_incr)
   13.14 -  apply (rule impI)
   13.15 -  apply (rule merges_same_conv [THEN iffD1, elim_format]) 
   13.16 -  apply assumption+
   13.17 +lemma termination_lemma:
   13.18 +  assumes semilat: "semilat (A, r, f)"
   13.19 +  shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
   13.20 +  ss <[r] merges f qs ss \<or> 
   13.21 +  merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w" (is "PROP ?P")
   13.22 +proof -
   13.23 +  interpret semilat [A r f] by fact
   13.24 +  show "PROP ?P" apply(insert semilat)
   13.25 +    apply (unfold lesssub_def)
   13.26 +    apply (simp (no_asm_simp) add: merges_incr)
   13.27 +    apply (rule impI)
   13.28 +    apply (rule merges_same_conv [THEN iffD1, elim_format]) 
   13.29 +    apply assumption+
   13.30      defer
   13.31      apply (rule sym, assumption)
   13.32 -   defer apply simp
   13.33 -   apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
   13.34 -   apply (blast intro!: psubsetI elim: equalityE)
   13.35 -   apply clarsimp
   13.36 -   apply (drule bspec, assumption) 
   13.37 -   apply (drule bspec, assumption)
   13.38 -   apply clarsimp
   13.39 -  done 
   13.40 +    defer apply simp
   13.41 +    apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
   13.42 +    apply (blast intro!: psubsetI elim: equalityE)
   13.43 +    apply clarsimp
   13.44 +    apply (drule bspec, assumption) 
   13.45 +    apply (drule bspec, assumption)
   13.46 +    apply clarsimp
   13.47 +    done
   13.48 +qed
   13.49  
   13.50 -lemma iter_properties[rule_format]: includes semilat
   13.51 -shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
   13.52 +lemma iter_properties[rule_format]:
   13.53 +  assumes semilat: "semilat (A, r, f)"
   13.54 +  shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
   13.55       bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
   13.56       \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
   13.57     iter f step ss0 w0 = (ss',w')
   13.58     \<longrightarrow>
   13.59     ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and>
   13.60     (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
   13.61 -apply(insert semilat)
   13.62 +  (is "PROP ?P")
   13.63 +proof -
   13.64 +  interpret semilat [A r f] by fact
   13.65 +  show "PROP ?P" apply(insert semilat)
   13.66  apply (unfold iter_def stables_def)
   13.67  apply (rule_tac P = "%(ss,w).
   13.68   ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
   13.69 @@ -434,8 +442,10 @@
   13.70  apply clarsimp
   13.71  done
   13.72  
   13.73 +qed
   13.74  
   13.75 -lemma kildall_properties: includes semilat
   13.76 +lemma kildall_properties:
   13.77 +assumes semilat: "semilat (A, r, f)"
   13.78  shows "\<lbrakk> acc r; pres_type step n A; mono r step n A;
   13.79       bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
   13.80    kildall r f step ss0 \<in> list n A \<and>
   13.81 @@ -443,6 +453,10 @@
   13.82    ss0 <=[r] kildall r f step ss0 \<and>
   13.83    (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow>
   13.84                   kildall r f step ss0 <=[r] ts)"
   13.85 +  (is "PROP ?P")
   13.86 +proof -
   13.87 +  interpret semilat [A r f] by fact
   13.88 +  show "PROP ?P"
   13.89  apply (unfold kildall_def)
   13.90  apply(case_tac "iter f step ss0 (unstables r step ss0)")
   13.91  apply(simp)
   13.92 @@ -450,11 +464,16 @@
   13.93  apply (simp_all add: unstables_def stable_def)
   13.94  apply (rule semilat)
   13.95  done
   13.96 -
   13.97 +qed
   13.98  
   13.99 -lemma is_bcv_kildall: includes semilat
  13.100 +lemma is_bcv_kildall:
  13.101 +assumes semilat: "semilat (A, r, f)"
  13.102  shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk>
  13.103    \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
  13.104 +  (is "PROP ?P")
  13.105 +proof -
  13.106 +  interpret semilat [A r f] by fact
  13.107 +  show "PROP ?P"
  13.108  apply(unfold is_bcv_def wt_step_def)
  13.109  apply(insert semilat kildall_properties[of A])
  13.110  apply(simp add:stables_def)
  13.111 @@ -472,5 +491,6 @@
  13.112   apply simp
  13.113  apply (blast intro!: le_listD less_lengthI)
  13.114  done
  13.115 +qed
  13.116  
  13.117  end
    14.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Tue Jul 15 16:02:10 2008 +0200
    14.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Jul 15 16:50:09 2008 +0200
    14.3 @@ -378,7 +378,10 @@
    14.4  
    14.5  
    14.6  lemma Listn_sl_aux:
    14.7 -includes semilat shows "semilat (Listn.sl n (A,r,f))"
    14.8 +assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))"
    14.9 +proof -
   14.10 +  interpret semilat [A r f] by fact
   14.11 +show ?thesis
   14.12  apply (unfold Listn.sl_def)
   14.13  apply (simp (no_asm) only: semilat_Def split_conv)
   14.14  apply (rule conjI)
   14.15 @@ -388,6 +391,7 @@
   14.16  apply (simp (no_asm) only: list_def)
   14.17  apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
   14.18  done
   14.19 +qed
   14.20  
   14.21  lemma Listn_sl: "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
   14.22   by(simp add: Listn_sl_aux split_tupled_all)
    15.1 --- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Tue Jul 15 16:02:10 2008 +0200
    15.2 +++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Tue Jul 15 16:50:09 2008 +0200
    15.3 @@ -62,17 +62,20 @@
    15.4    done
    15.5  
    15.6  
    15.7 -lemma plusplus_closed: includes semilat shows
    15.8 -  "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
    15.9 -proof (induct x)
   15.10 -  show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
   15.11 -  fix y x xs
   15.12 -  assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
   15.13 -  assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
   15.14 -  from xs obtain x: "x \<in> A" and xs': "set xs \<subseteq> A" by simp
   15.15 -  from x y have "(x +_f y) \<in> A" ..
   15.16 -  with xs' have "xs ++_f (x +_f y) \<in> A" by (rule IH)
   15.17 -  thus "(x#xs) ++_f y \<in> A" by simp
   15.18 +lemma plusplus_closed: assumes "semilat (A, r, f)" shows
   15.19 +  "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A" (is "PROP ?P")
   15.20 +proof -
   15.21 +  interpret semilat [A r f] by fact
   15.22 +  show "PROP ?P" proof (induct x)
   15.23 +    show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
   15.24 +    fix y x xs
   15.25 +    assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
   15.26 +    assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
   15.27 +    from xs obtain x: "x \<in> A" and xs': "set xs \<subseteq> A" by simp
   15.28 +    from x y have "(x +_f y) \<in> A" ..
   15.29 +    with xs' have "xs ++_f (x +_f y) \<in> A" by (rule IH)
   15.30 +    thus "(x#xs) ++_f y \<in> A" by simp
   15.31 +  qed
   15.32  qed
   15.33  
   15.34  lemma (in semilat) pp_ub2:
   15.35 @@ -154,10 +157,13 @@
   15.36  qed
   15.37  
   15.38  
   15.39 -lemma ub1': includes semilat
   15.40 -shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> 
   15.41 +lemma ub1':
   15.42 +  assumes "semilat (A, r, f)"
   15.43 +  shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> 
   15.44    \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y" 
   15.45  proof -
   15.46 +  interpret semilat [A r f] by fact
   15.47 +
   15.48    let "b <=_r ?map ++_f y" = ?thesis
   15.49  
   15.50    assume "y \<in> A"
    16.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Tue Jul 15 16:02:10 2008 +0200
    16.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Tue Jul 15 16:50:09 2008 +0200
    16.3 @@ -24,23 +24,26 @@
    16.4    the_lub  ("\<Squnion>_" [90] 90)
    16.5  
    16.6  lemma the_lub_equality [elim?]:
    16.7 -  includes lub
    16.8 +  assumes "lub A x"
    16.9    shows "\<Squnion>A = (x::'a::order)"
   16.10 -proof (unfold the_lub_def)
   16.11 -  from lub_axioms show "The (lub A) = x"
   16.12 -  proof
   16.13 -    fix x' assume lub': "lub A x'"
   16.14 -    show "x' = x"
   16.15 -    proof (rule order_antisym)
   16.16 -      from lub' show "x' \<le> x"
   16.17 -      proof
   16.18 -        fix a assume "a \<in> A"
   16.19 -        then show "a \<le> x" ..
   16.20 -      qed
   16.21 -      show "x \<le> x'"
   16.22 -      proof
   16.23 -        fix a assume "a \<in> A"
   16.24 -        with lub' show "a \<le> x'" ..
   16.25 +proof -
   16.26 +  interpret lub [A x] by fact
   16.27 +  show ?thesis proof (unfold the_lub_def)
   16.28 +    from `lub A x` show "The (lub A) = x"
   16.29 +    proof
   16.30 +      fix x' assume lub': "lub A x'"
   16.31 +      show "x' = x"
   16.32 +      proof (rule order_antisym)
   16.33 +	from lub' show "x' \<le> x"
   16.34 +	proof
   16.35 +          fix a assume "a \<in> A"
   16.36 +          then show "a \<le> x" ..
   16.37 +	qed
   16.38 +	show "x \<le> x'"
   16.39 +	proof
   16.40 +          fix a assume "a \<in> A"
   16.41 +          with lub' show "a \<le> x'" ..
   16.42 +	qed
   16.43        qed
   16.44      qed
   16.45    qed
    17.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Jul 15 16:02:10 2008 +0200
    17.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Jul 15 16:50:09 2008 +0200
    17.3 @@ -26,7 +26,8 @@
    17.4  declare continuous.intro [intro?] continuous_axioms.intro [intro?]
    17.5  
    17.6  lemma continuousI [intro]:
    17.7 -  includes norm_syntax + linearform
    17.8 +  fixes norm :: "_ \<Rightarrow> real"  ("\<parallel>_\<parallel>")
    17.9 +  assumes "linearform V f"
   17.10    assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
   17.11    shows "continuous V norm f"
   17.12  proof
   17.13 @@ -74,6 +75,8 @@
   17.14    fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
   17.15    defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
   17.16  
   17.17 +locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm
   17.18 +
   17.19  lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
   17.20    by (simp add: B_def)
   17.21  
   17.22 @@ -82,20 +85,11 @@
   17.23    normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
   17.24  *}
   17.25  
   17.26 -(* Alternative statement of the lemma as
   17.27 -     lemma (in fn_norm)
   17.28 -       includes normed_vectorspace + continuous
   17.29 -       shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
   17.30 -   is not possible:
   17.31 -   fn_norm contrains parameter norm to type "'a::zero => real",
   17.32 -   normed_vectorspace and continuous contrain this parameter to
   17.33 -   "'a::{minus, plus, zero} => real, which is less general.
   17.34 -*)
   17.35 -
   17.36 -lemma (in normed_vectorspace) fn_norm_works:
   17.37 -  includes fn_norm + continuous
   17.38 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
   17.39 +  assumes "continuous V norm f"
   17.40    shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
   17.41  proof -
   17.42 +  interpret continuous [V norm f] by fact
   17.43    txt {* The existence of the supremum is shown using the
   17.44      completeness of the reals. Completeness means, that every
   17.45      non-empty bounded set of reals has a supremum. *}
   17.46 @@ -158,39 +152,40 @@
   17.47    then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex)
   17.48  qed
   17.49  
   17.50 -lemma (in normed_vectorspace) fn_norm_ub [iff?]:
   17.51 -  includes fn_norm + continuous
   17.52 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
   17.53 +  assumes "continuous V norm f"
   17.54    assumes b: "b \<in> B V f"
   17.55    shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
   17.56  proof -
   17.57 +  interpret continuous [V norm f] by fact
   17.58    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
   17.59 -    unfolding B_def fn_norm_def
   17.60      using `continuous V norm f` by (rule fn_norm_works)
   17.61    from this and b show ?thesis ..
   17.62  qed
   17.63  
   17.64 -lemma (in normed_vectorspace) fn_norm_leastB:
   17.65 -  includes fn_norm + continuous
   17.66 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
   17.67 +  assumes "continuous V norm f"
   17.68    assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
   17.69    shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
   17.70  proof -
   17.71 +  interpret continuous [V norm f] by fact
   17.72    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
   17.73 -    unfolding B_def fn_norm_def
   17.74      using `continuous V norm f` by (rule fn_norm_works)
   17.75    from this and b show ?thesis ..
   17.76  qed
   17.77  
   17.78  text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
   17.79  
   17.80 -lemma (in normed_vectorspace) fn_norm_ge_zero [iff]:
   17.81 -  includes fn_norm + continuous
   17.82 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
   17.83 +  assumes "continuous V norm f"
   17.84    shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
   17.85  proof -
   17.86 +  interpret continuous [V norm f] by fact
   17.87    txt {* The function norm is defined as the supremum of @{text B}.
   17.88      So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
   17.89      0"}, provided the supremum exists and @{text B} is not empty. *}
   17.90    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
   17.91 -    unfolding B_def fn_norm_def
   17.92 +(*    unfolding B_def fn_norm_def *)
   17.93      using `continuous V norm f` by (rule fn_norm_works)
   17.94    moreover have "0 \<in> B V f" ..
   17.95    ultimately show ?thesis ..
   17.96 @@ -203,34 +198,37 @@
   17.97    \end{center}
   17.98  *}
   17.99  
  17.100 -lemma (in normed_vectorspace) fn_norm_le_cong:
  17.101 -  includes fn_norm + continuous + linearform
  17.102 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
  17.103 +  assumes "continuous V norm f" "linearform V f"
  17.104    assumes x: "x \<in> V"
  17.105    shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
  17.106 -proof cases
  17.107 -  assume "x = 0"
  17.108 -  then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
  17.109 -  also have "f 0 = 0" by rule unfold_locales
  17.110 -  also have "\<bar>\<dots>\<bar> = 0" by simp
  17.111 -  also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
  17.112 -    unfolding B_def fn_norm_def
  17.113 -    using `continuous V norm f` by (rule fn_norm_ge_zero)
  17.114 -  from x have "0 \<le> norm x" ..
  17.115 -  with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
  17.116 -  finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
  17.117 -next
  17.118 -  assume "x \<noteq> 0"
  17.119 -  with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
  17.120 -  then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
  17.121 -  also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
  17.122 -  proof (rule mult_right_mono)
  17.123 -    from x show "0 \<le> \<parallel>x\<parallel>" ..
  17.124 -    from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
  17.125 -      by (auto simp add: B_def real_divide_def)
  17.126 -    with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
  17.127 -      unfolding B_def fn_norm_def by (rule fn_norm_ub)
  17.128 +proof -
  17.129 +  interpret continuous [V norm f] by fact
  17.130 +  interpret linearform [V f] .
  17.131 +  show ?thesis proof cases
  17.132 +    assume "x = 0"
  17.133 +    then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
  17.134 +    also have "f 0 = 0" by rule unfold_locales
  17.135 +    also have "\<bar>\<dots>\<bar> = 0" by simp
  17.136 +    also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
  17.137 +      using `continuous V norm f` by (rule fn_norm_ge_zero)
  17.138 +    from x have "0 \<le> norm x" ..
  17.139 +    with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
  17.140 +    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
  17.141 +  next
  17.142 +    assume "x \<noteq> 0"
  17.143 +    with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
  17.144 +    then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
  17.145 +    also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
  17.146 +    proof (rule mult_right_mono)
  17.147 +      from x show "0 \<le> \<parallel>x\<parallel>" ..
  17.148 +      from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
  17.149 +	by (auto simp add: B_def real_divide_def)
  17.150 +      with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
  17.151 +	by (rule fn_norm_ub)
  17.152 +    qed
  17.153 +    finally show ?thesis .
  17.154    qed
  17.155 -  finally show ?thesis .
  17.156  qed
  17.157  
  17.158  text {*
  17.159 @@ -241,35 +239,38 @@
  17.160    \end{center}
  17.161  *}
  17.162  
  17.163 -lemma (in normed_vectorspace) fn_norm_least [intro?]:
  17.164 -  includes fn_norm + continuous
  17.165 +lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
  17.166 +  assumes "continuous V norm f"
  17.167    assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
  17.168    shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
  17.169 -proof (rule fn_norm_leastB [folded B_def fn_norm_def])
  17.170 -  fix b assume b: "b \<in> B V f"
  17.171 -  show "b \<le> c"
  17.172 -  proof cases
  17.173 -    assume "b = 0"
  17.174 -    with ge show ?thesis by simp
  17.175 -  next
  17.176 -    assume "b \<noteq> 0"
  17.177 -    with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
  17.178 +proof -
  17.179 +  interpret continuous [V norm f] by fact
  17.180 +  show ?thesis proof (rule fn_norm_leastB [folded B_def fn_norm_def])
  17.181 +    fix b assume b: "b \<in> B V f"
  17.182 +    show "b \<le> c"
  17.183 +    proof cases
  17.184 +      assume "b = 0"
  17.185 +      with ge show ?thesis by simp
  17.186 +    next
  17.187 +      assume "b \<noteq> 0"
  17.188 +      with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
  17.189          and x_neq: "x \<noteq> 0" and x: "x \<in> V"
  17.190 -      by (auto simp add: B_def real_divide_def)
  17.191 -    note b_rep
  17.192 -    also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
  17.193 -    proof (rule mult_right_mono)
  17.194 -      have "0 < \<parallel>x\<parallel>" using x x_neq ..
  17.195 -      then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
  17.196 -      from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
  17.197 +	by (auto simp add: B_def real_divide_def)
  17.198 +      note b_rep
  17.199 +      also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
  17.200 +      proof (rule mult_right_mono)
  17.201 +	have "0 < \<parallel>x\<parallel>" using x x_neq ..
  17.202 +	then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
  17.203 +	from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
  17.204 +      qed
  17.205 +      also have "\<dots> = c"
  17.206 +      proof -
  17.207 +	from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
  17.208 +	then show ?thesis by simp
  17.209 +      qed
  17.210 +      finally show ?thesis .
  17.211      qed
  17.212 -    also have "\<dots> = c"
  17.213 -    proof -
  17.214 -      from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
  17.215 -      then show ?thesis by simp
  17.216 -    qed
  17.217 -    finally show ?thesis .
  17.218 -  qed
  17.219 -qed (insert `continuous V norm f`, simp_all add: continuous_def)
  17.220 +  qed (insert `continuous V norm f`, simp_all add: continuous_def)
  17.221 +qed
  17.222  
  17.223  end
    18.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Jul 15 16:02:10 2008 +0200
    18.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Jul 15 16:50:09 2008 +0200
    18.3 @@ -53,17 +53,21 @@
    18.4  *}
    18.5  
    18.6  theorem HahnBanach:
    18.7 -  includes vectorspace E + subspace F E + seminorm E p + linearform F f
    18.8 +  assumes E: "vectorspace E" and "subspace F E"
    18.9 +    and "seminorm E p" and "linearform F f"
   18.10    assumes fp: "\<forall>x \<in> F. f x \<le> p x"
   18.11    shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
   18.12      -- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *}
   18.13      -- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *}
   18.14      -- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *}
   18.15  proof -
   18.16 +  interpret vectorspace [E] by fact
   18.17 +  interpret subspace [F E] by fact
   18.18 +  interpret seminorm [E p] by fact
   18.19 +  interpret linearform [F f] by fact
   18.20    def M \<equiv> "norm_pres_extensions E p F f"
   18.21    hence M: "M = \<dots>" by (simp only:)
   18.22 -  note E = `vectorspace E`
   18.23 -  then have F: "vectorspace F" ..
   18.24 +  from E have F: "vectorspace F" ..
   18.25    note FE = `F \<unlhd> E`
   18.26    {
   18.27      fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c"
   18.28 @@ -306,17 +310,22 @@
   18.29  *}
   18.30  
   18.31  theorem abs_HahnBanach:
   18.32 -  includes vectorspace E + subspace F E + linearform F f + seminorm E p
   18.33 +  assumes E: "vectorspace E" and FE: "subspace F E"
   18.34 +    and lf: "linearform F f" and sn: "seminorm E p"
   18.35    assumes fp: "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
   18.36    shows "\<exists>g. linearform E g
   18.37      \<and> (\<forall>x \<in> F. g x = f x)
   18.38      \<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
   18.39  proof -
   18.40 -  note E = `vectorspace E`
   18.41 +  interpret vectorspace [E] by fact
   18.42 +  interpret subspace [F E] by fact
   18.43 +  interpret linearform [F f] by fact
   18.44 +  interpret seminorm [E p] by fact
   18.45 +(*  note E = `vectorspace E`
   18.46    note FE = `subspace F E`
   18.47    note sn = `seminorm E p`
   18.48    note lf = `linearform F f`
   18.49 -  have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
   18.50 +*)  have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) \<and> (\<forall>x \<in> E. g x \<le> p x)"
   18.51    using E FE sn lf
   18.52    proof (rule HahnBanach)
   18.53      show "\<forall>x \<in> F. f x \<le> p x"
   18.54 @@ -342,22 +351,31 @@
   18.55  *}
   18.56  
   18.57  theorem norm_HahnBanach:
   18.58 -  includes normed_vectorspace E + subspace F E + linearform F f + fn_norm + continuous F norm ("\<parallel>_\<parallel>") f
   18.59 +  fixes V and norm ("\<parallel>_\<parallel>")
   18.60 +  fixes B defines "\<And>V f. B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
   18.61 +  fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
   18.62 +  defines "\<And>V f. \<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
   18.63 +  assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
   18.64 +    and linearform: "linearform F f" and "continuous F norm f"
   18.65    shows "\<exists>g. linearform E g
   18.66       \<and> continuous E norm g
   18.67       \<and> (\<forall>x \<in> F. g x = f x)
   18.68       \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
   18.69  proof -
   18.70 +  interpret normed_vectorspace [E norm] by fact
   18.71 +  interpret normed_vectorspace_with_fn_norm [E norm B fn_norm]
   18.72 +    by (auto simp: B_def fn_norm_def) intro_locales
   18.73 +  interpret subspace [F E] by fact
   18.74 +  interpret linearform [F f] by fact
   18.75 +  interpret continuous [F norm f] by fact
   18.76    have E: "vectorspace E" by unfold_locales
   18.77 -  have E_norm: "normed_vectorspace E norm" by rule unfold_locales
   18.78 -  note FE = `F \<unlhd> E`
   18.79    have F: "vectorspace F" by rule unfold_locales
   18.80 -  note linearform = `linearform F f`
   18.81    have F_norm: "normed_vectorspace F norm"
   18.82      using FE E_norm by (rule subspace_normed_vs)
   18.83    have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
   18.84 -    by (rule normed_vectorspace.fn_norm_ge_zero
   18.85 -      [OF F_norm `continuous F norm f`, folded B_def fn_norm_def])
   18.86 +    by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
   18.87 +      [OF normed_vectorspace_with_fn_norm.intro,
   18.88 +       OF F_norm `continuous F norm f` , folded B_def fn_norm_def])
   18.89    txt {* We define a function @{text p} on @{text E} as follows:
   18.90      @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
   18.91    def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
   18.92 @@ -406,8 +424,9 @@
   18.93      fix x assume "x \<in> F"
   18.94      from this and `continuous F norm f`
   18.95      show "\<bar>f x\<bar> \<le> p x"
   18.96 -      by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
   18.97 -        [OF F_norm, folded B_def fn_norm_def])
   18.98 +      by (unfold p_def) (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
   18.99 +        [OF normed_vectorspace_with_fn_norm.intro,
  18.100 +         OF F_norm, folded B_def fn_norm_def])
  18.101    qed
  18.102  
  18.103    txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
  18.104 @@ -463,7 +482,9 @@
  18.105      txt {* The other direction is achieved by a similar argument. *}
  18.106  
  18.107      show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
  18.108 -    proof (rule normed_vectorspace.fn_norm_least [OF F_norm, folded B_def fn_norm_def])
  18.109 +    proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
  18.110 +	[OF normed_vectorspace_with_fn_norm.intro,
  18.111 +	 OF F_norm, folded B_def fn_norm_def])
  18.112        show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
  18.113        proof
  18.114  	fix x assume x: "x \<in> F"
    19.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Tue Jul 15 16:02:10 2008 +0200
    19.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Tue Jul 15 16:50:09 2008 +0200
    19.3 @@ -40,10 +40,11 @@
    19.4  *}
    19.5  
    19.6  lemma ex_xi:
    19.7 -  includes vectorspace F
    19.8 +  assumes "vectorspace F"
    19.9    assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
   19.10    shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
   19.11  proof -
   19.12 +  interpret vectorspace [F] by fact
   19.13    txt {* From the completeness of the reals follows:
   19.14      The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
   19.15      non-empty and has an upper bound. *}
   19.16 @@ -86,183 +87,190 @@
   19.17  *}
   19.18  
   19.19  lemma h'_lf:
   19.20 -  includes var H + var h + var E
   19.21    assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
   19.22        SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
   19.23      and H'_def: "H' \<equiv> H + lin x0"
   19.24      and HE: "H \<unlhd> E"
   19.25 -  includes linearform H h
   19.26 +  assumes "linearform H h"
   19.27    assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
   19.28 -  includes vectorspace E
   19.29 +  assumes E: "vectorspace E"
   19.30    shows "linearform H' h'"
   19.31 -proof
   19.32 -  note E = `vectorspace E`
   19.33 -  have H': "vectorspace H'"
   19.34 -  proof (unfold H'_def)
   19.35 -    from `x0 \<in> E`
   19.36 -    have "lin x0 \<unlhd> E" ..
   19.37 -    with HE show "vectorspace (H + lin x0)" using E ..
   19.38 -  qed
   19.39 -  {
   19.40 -    fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
   19.41 -    show "h' (x1 + x2) = h' x1 + h' x2"
   19.42 -    proof -
   19.43 -      from H' x1 x2 have "x1 + x2 \<in> H'"
   19.44 -        by (rule vectorspace.add_closed)
   19.45 -      with x1 x2 obtain y y1 y2 a a1 a2 where
   19.46 -            x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
   19.47 +proof -
   19.48 +  interpret linearform [H h] by fact
   19.49 +  interpret vectorspace [E] by fact
   19.50 +  show ?thesis proof
   19.51 +    note E = `vectorspace E`
   19.52 +    have H': "vectorspace H'"
   19.53 +    proof (unfold H'_def)
   19.54 +      from `x0 \<in> E`
   19.55 +      have "lin x0 \<unlhd> E" ..
   19.56 +      with HE show "vectorspace (H + lin x0)" using E ..
   19.57 +    qed
   19.58 +    {
   19.59 +      fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
   19.60 +      show "h' (x1 + x2) = h' x1 + h' x2"
   19.61 +      proof -
   19.62 +	from H' x1 x2 have "x1 + x2 \<in> H'"
   19.63 +          by (rule vectorspace.add_closed)
   19.64 +	with x1 x2 obtain y y1 y2 a a1 a2 where
   19.65 +          x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
   19.66            and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
   19.67            and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
   19.68 -        by (unfold H'_def sum_def lin_def) blast
   19.69 -
   19.70 -      have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
   19.71 -      proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
   19.72 -        from HE y1 y2 show "y1 + y2 \<in> H"
   19.73 -          by (rule subspace.add_closed)
   19.74 -        from x0 and HE y y1 y2
   19.75 -        have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
   19.76 -        with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
   19.77 -          by (simp add: add_ac add_mult_distrib2)
   19.78 -        also note x1x2
   19.79 -        finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
   19.80 +          by (unfold H'_def sum_def lin_def) blast
   19.81 +	
   19.82 +	have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
   19.83 +	proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
   19.84 +          from HE y1 y2 show "y1 + y2 \<in> H"
   19.85 +            by (rule subspace.add_closed)
   19.86 +          from x0 and HE y y1 y2
   19.87 +          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
   19.88 +          with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
   19.89 +            by (simp add: add_ac add_mult_distrib2)
   19.90 +          also note x1x2
   19.91 +          finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
   19.92 +	qed
   19.93 +	
   19.94 +	from h'_def x1x2 E HE y x0
   19.95 +	have "h' (x1 + x2) = h y + a * xi"
   19.96 +          by (rule h'_definite)
   19.97 +	also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
   19.98 +          by (simp only: ya)
   19.99 +	also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
  19.100 +          by simp
  19.101 +	also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
  19.102 +          by (simp add: left_distrib)
  19.103 +	also from h'_def x1_rep E HE y1 x0
  19.104 +	have "h y1 + a1 * xi = h' x1"
  19.105 +          by (rule h'_definite [symmetric])
  19.106 +	also from h'_def x2_rep E HE y2 x0
  19.107 +	have "h y2 + a2 * xi = h' x2"
  19.108 +          by (rule h'_definite [symmetric])
  19.109 +	finally show ?thesis .
  19.110        qed
  19.111 -
  19.112 -      from h'_def x1x2 E HE y x0
  19.113 -      have "h' (x1 + x2) = h y + a * xi"
  19.114 -        by (rule h'_definite)
  19.115 -      also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
  19.116 -        by (simp only: ya)
  19.117 -      also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
  19.118 -        by simp
  19.119 -      also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
  19.120 -        by (simp add: left_distrib)
  19.121 -      also from h'_def x1_rep E HE y1 x0
  19.122 -      have "h y1 + a1 * xi = h' x1"
  19.123 -        by (rule h'_definite [symmetric])
  19.124 -      also from h'_def x2_rep E HE y2 x0
  19.125 -      have "h y2 + a2 * xi = h' x2"
  19.126 -        by (rule h'_definite [symmetric])
  19.127 -      finally show ?thesis .
  19.128 -    qed
  19.129 -  next
  19.130 -    fix x1 c assume x1: "x1 \<in> H'"
  19.131 -    show "h' (c \<cdot> x1) = c * (h' x1)"
  19.132 -    proof -
  19.133 -      from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
  19.134 -        by (rule vectorspace.mult_closed)
  19.135 -      with x1 obtain y a y1 a1 where
  19.136 -            cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
  19.137 +    next
  19.138 +      fix x1 c assume x1: "x1 \<in> H'"
  19.139 +      show "h' (c \<cdot> x1) = c * (h' x1)"
  19.140 +      proof -
  19.141 +	from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
  19.142 +          by (rule vectorspace.mult_closed)
  19.143 +	with x1 obtain y a y1 a1 where
  19.144 +          cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
  19.145            and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
  19.146 -        by (unfold H'_def sum_def lin_def) blast
  19.147 -
  19.148 -      have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
  19.149 -      proof (rule decomp_H')
  19.150 -        from HE y1 show "c \<cdot> y1 \<in> H"
  19.151 -          by (rule subspace.mult_closed)
  19.152 -        from x0 and HE y y1
  19.153 -        have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
  19.154 -        with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
  19.155 -          by (simp add: mult_assoc add_mult_distrib1)
  19.156 -        also note cx1_rep
  19.157 -        finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
  19.158 +          by (unfold H'_def sum_def lin_def) blast
  19.159 +	
  19.160 +	have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
  19.161 +	proof (rule decomp_H')
  19.162 +          from HE y1 show "c \<cdot> y1 \<in> H"
  19.163 +            by (rule subspace.mult_closed)
  19.164 +          from x0 and HE y y1
  19.165 +          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
  19.166 +          with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
  19.167 +            by (simp add: mult_assoc add_mult_distrib1)
  19.168 +          also note cx1_rep
  19.169 +          finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
  19.170 +	qed
  19.171 +	
  19.172 +	from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
  19.173 +          by (rule h'_definite)
  19.174 +	also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
  19.175 +          by (simp only: ya)
  19.176 +	also from y1 have "h (c \<cdot> y1) = c * h y1"
  19.177 +          by simp
  19.178 +	also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
  19.179 +          by (simp only: right_distrib)
  19.180 +	also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
  19.181 +          by (rule h'_definite [symmetric])
  19.182 +	finally show ?thesis .
  19.183        qed
  19.184 -
  19.185 -      from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
  19.186 -        by (rule h'_definite)
  19.187 -      also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
  19.188 -        by (simp only: ya)
  19.189 -      also from y1 have "h (c \<cdot> y1) = c * h y1"
  19.190 -        by simp
  19.191 -      also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
  19.192 -        by (simp only: right_distrib)
  19.193 -      also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
  19.194 -        by (rule h'_definite [symmetric])
  19.195 -      finally show ?thesis .
  19.196 -    qed
  19.197 -  }
  19.198 +    }
  19.199 +  qed
  19.200  qed
  19.201  
  19.202  text {* \medskip The linear extension @{text h'} of @{text h}
  19.203    is bounded by the seminorm @{text p}. *}
  19.204  
  19.205  lemma h'_norm_pres:
  19.206 -  includes var H + var h + var E
  19.207    assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
  19.208        SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
  19.209      and H'_def: "H' \<equiv> H + lin x0"
  19.210      and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
  19.211 -  includes vectorspace E + subspace H E + seminorm E p + linearform H h
  19.212 +  assumes E: "vectorspace E" and HE: "subspace H E"
  19.213 +    and "seminorm E p" and "linearform H h"
  19.214    assumes a: "\<forall>y \<in> H. h y \<le> p y"
  19.215      and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
  19.216    shows "\<forall>x \<in> H'. h' x \<le> p x"
  19.217 -proof
  19.218 -  note E = `vectorspace E`
  19.219 -  note HE = `subspace H E`
  19.220 -  fix x assume x': "x \<in> H'"
  19.221 -  show "h' x \<le> p x"
  19.222 -  proof -
  19.223 -    from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
  19.224 -      and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
  19.225 -    from x' obtain y a where
  19.226 +proof -
  19.227 +  interpret vectorspace [E] by fact
  19.228 +  interpret subspace [H E] by fact
  19.229 +  interpret seminorm [E p] by fact
  19.230 +  interpret linearform [H h] by fact
  19.231 +  show ?thesis proof
  19.232 +    fix x assume x': "x \<in> H'"
  19.233 +    show "h' x \<le> p x"
  19.234 +    proof -
  19.235 +      from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
  19.236 +	and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
  19.237 +      from x' obtain y a where
  19.238          x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
  19.239 -      by (unfold H'_def sum_def lin_def) blast
  19.240 -    from y have y': "y \<in> E" ..
  19.241 -    from y have ay: "inverse a \<cdot> y \<in> H" by simp
  19.242 -
  19.243 -    from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
  19.244 -      by (rule h'_definite)
  19.245 -    also have "\<dots> \<le> p (y + a \<cdot> x0)"
  19.246 -    proof (rule linorder_cases)
  19.247 -      assume z: "a = 0"
  19.248 -      then have "h y + a * xi = h y" by simp
  19.249 -      also from a y have "\<dots> \<le> p y" ..
  19.250 -      also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
  19.251 -      finally show ?thesis .
  19.252 -    next
  19.253 -      txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
  19.254 -        with @{text ya} taken as @{text "y / a"}: *}
  19.255 -      assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
  19.256 -      from a1 ay
  19.257 -      have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
  19.258 -      with lz have "a * xi \<le>
  19.259 +	by (unfold H'_def sum_def lin_def) blast
  19.260 +      from y have y': "y \<in> E" ..
  19.261 +      from y have ay: "inverse a \<cdot> y \<in> H" by simp
  19.262 +      
  19.263 +      from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
  19.264 +	by (rule h'_definite)
  19.265 +      also have "\<dots> \<le> p (y + a \<cdot> x0)"
  19.266 +      proof (rule linorder_cases)
  19.267 +	assume z: "a = 0"
  19.268 +	then have "h y + a * xi = h y" by simp
  19.269 +	also from a y have "\<dots> \<le> p y" ..
  19.270 +	also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
  19.271 +	finally show ?thesis .
  19.272 +      next
  19.273 +	txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
  19.274 +          with @{text ya} taken as @{text "y / a"}: *}
  19.275 +	assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
  19.276 +	from a1 ay
  19.277 +	have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
  19.278 +	with lz have "a * xi \<le>
  19.279            a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
  19.280 -        by (simp add: mult_left_mono_neg order_less_imp_le)
  19.281 -
  19.282 -      also have "\<dots> =
  19.283 +          by (simp add: mult_left_mono_neg order_less_imp_le)
  19.284 +	
  19.285 +	also have "\<dots> =
  19.286            - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
  19.287 -	by (simp add: right_diff_distrib)
  19.288 -      also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
  19.289 +	  by (simp add: right_diff_distrib)
  19.290 +	also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
  19.291            p (a \<cdot> (inverse a \<cdot> y + x0))"
  19.292 -        by (simp add: abs_homogenous)
  19.293 -      also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
  19.294 -        by (simp add: add_mult_distrib1 mult_assoc [symmetric])
  19.295 -      also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
  19.296 -        by simp
  19.297 -      finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
  19.298 -      then show ?thesis by simp
  19.299 -    next
  19.300 -      txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
  19.301 -        with @{text ya} taken as @{text "y / a"}: *}
  19.302 -      assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
  19.303 -      from a2 ay
  19.304 -      have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
  19.305 -      with gz have "a * xi \<le>
  19.306 +          by (simp add: abs_homogenous)
  19.307 +	also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
  19.308 +          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
  19.309 +	also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
  19.310 +          by simp
  19.311 +	finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
  19.312 +	then show ?thesis by simp
  19.313 +      next
  19.314 +	txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
  19.315 +          with @{text ya} taken as @{text "y / a"}: *}
  19.316 +	assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
  19.317 +	from a2 ay
  19.318 +	have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
  19.319 +	with gz have "a * xi \<le>
  19.320            a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
  19.321 -        by simp
  19.322 -      also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
  19.323 -	by (simp add: right_diff_distrib)
  19.324 -      also from gz x0 y'
  19.325 -      have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
  19.326 -        by (simp add: abs_homogenous)
  19.327 -      also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
  19.328 -        by (simp add: add_mult_distrib1 mult_assoc [symmetric])
  19.329 -      also from nz y have "a * h (inverse a \<cdot> y) = h y"
  19.330 -        by simp
  19.331 -      finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
  19.332 -      then show ?thesis by simp
  19.333 +          by simp
  19.334 +	also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
  19.335 +	  by (simp add: right_diff_distrib)
  19.336 +	also from gz x0 y'
  19.337 +	have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
  19.338 +          by (simp add: abs_homogenous)
  19.339 +	also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
  19.340 +          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
  19.341 +	also from nz y have "a * h (inverse a \<cdot> y) = h y"
  19.342 +          by simp
  19.343 +	finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
  19.344 +	then show ?thesis by simp
  19.345 +      qed
  19.346 +      also from x_rep have "\<dots> = p x" by (simp only:)
  19.347 +      finally show ?thesis .
  19.348      qed
  19.349 -    also from x_rep have "\<dots> = p x" by (simp only:)
  19.350 -    finally show ?thesis .
  19.351    qed
  19.352  qed
  19.353  
    20.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Tue Jul 15 16:02:10 2008 +0200
    20.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Tue Jul 15 16:50:09 2008 +0200
    20.3 @@ -399,9 +399,14 @@
    20.4  *}
    20.5  
    20.6  lemma abs_ineq_iff:
    20.7 -  includes subspace H E + vectorspace E + seminorm E p + linearform H h
    20.8 +  assumes "subspace H E" and "vectorspace E" and "seminorm E p"
    20.9 +    and "linearform H h"
   20.10    shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
   20.11  proof
   20.12 +  interpret subspace [H E] by fact
   20.13 +  interpret vectorspace [E] by fact
   20.14 +  interpret seminorm [E p] by fact
   20.15 +  interpret linearform [H h] by fact
   20.16    have H: "vectorspace H" using `vectorspace E` ..
   20.17    {
   20.18      assume l: ?L
    21.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Tue Jul 15 16:02:10 2008 +0200
    21.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Tue Jul 15 16:50:09 2008 +0200
    21.3 @@ -20,9 +20,10 @@
    21.4  declare linearform.intro [intro?]
    21.5  
    21.6  lemma (in linearform) neg [iff]:
    21.7 -  includes vectorspace
    21.8 +  assumes "vectorspace V"
    21.9    shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
   21.10  proof -
   21.11 +  interpret vectorspace [V] by fact
   21.12    assume x: "x \<in> V"
   21.13    hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
   21.14    also from x have "... = (- 1) * (f x)" by (rule mult)
   21.15 @@ -31,9 +32,10 @@
   21.16  qed
   21.17  
   21.18  lemma (in linearform) diff [iff]:
   21.19 -  includes vectorspace
   21.20 +  assumes "vectorspace V"
   21.21    shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
   21.22  proof -
   21.23 +  interpret vectorspace [V] by fact
   21.24    assume x: "x \<in> V" and y: "y \<in> V"
   21.25    hence "x - y = x + - y" by (rule diff_eq1)
   21.26    also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)
   21.27 @@ -44,9 +46,10 @@
   21.28  text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
   21.29  
   21.30  lemma (in linearform) zero [iff]:
   21.31 -  includes vectorspace
   21.32 +  assumes "vectorspace V"
   21.33    shows "f 0 = 0"
   21.34  proof -
   21.35 +  interpret vectorspace [V] by fact
   21.36    have "f 0 = f (0 - 0)" by simp
   21.37    also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
   21.38    also have "\<dots> = 0" by simp
    22.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Jul 15 16:02:10 2008 +0200
    22.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Jul 15 16:50:09 2008 +0200
    22.3 @@ -27,9 +27,10 @@
    22.4  declare seminorm.intro [intro?]
    22.5  
    22.6  lemma (in seminorm) diff_subadditive:
    22.7 -  includes vectorspace
    22.8 +  assumes "vectorspace V"
    22.9    shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
   22.10  proof -
   22.11 +  interpret vectorspace [V] by fact
   22.12    assume x: "x \<in> V" and y: "y \<in> V"
   22.13    hence "x - y = x + - 1 \<cdot> y"
   22.14      by (simp add: diff_eq2 negate_eq2a)
   22.15 @@ -42,9 +43,10 @@
   22.16  qed
   22.17  
   22.18  lemma (in seminorm) minus:
   22.19 -  includes vectorspace
   22.20 +  assumes "vectorspace V"
   22.21    shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
   22.22  proof -
   22.23 +  interpret vectorspace [V] by fact
   22.24    assume x: "x \<in> V"
   22.25    hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
   22.26    also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
   22.27 @@ -95,14 +97,19 @@
   22.28  *}
   22.29  
   22.30  lemma subspace_normed_vs [intro?]:
   22.31 -  includes subspace F E + normed_vectorspace E
   22.32 +  fixes F E norm
   22.33 +  assumes "subspace F E" "normed_vectorspace E norm"
   22.34    shows "normed_vectorspace F norm"
   22.35 -proof
   22.36 -  show "vectorspace F" by (rule vectorspace) unfold_locales
   22.37 -next
   22.38 -  have "NormedSpace.norm E norm" by unfold_locales
   22.39 -  with subset show "NormedSpace.norm F norm"
   22.40 -    by (simp add: norm_def seminorm_def norm_axioms_def)
   22.41 +proof -
   22.42 +  interpret subspace [F E] by fact
   22.43 +  interpret normed_vectorspace [E norm] by fact
   22.44 +  show ?thesis proof
   22.45 +    show "vectorspace F" by (rule vectorspace) unfold_locales
   22.46 +  next
   22.47 +    have "NormedSpace.norm E norm" by unfold_locales
   22.48 +    with subset show "NormedSpace.norm F norm"
   22.49 +      by (simp add: norm_def seminorm_def norm_axioms_def)
   22.50 +  qed
   22.51  qed
   22.52  
   22.53  end
    23.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Jul 15 16:02:10 2008 +0200
    23.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Jul 15 16:50:09 2008 +0200
    23.3 @@ -41,10 +41,12 @@
    23.4    by (rule subspace.subsetD)
    23.5  
    23.6  lemma (in subspace) diff_closed [iff]:
    23.7 -  includes vectorspace
    23.8 -  shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U"
    23.9 -  by (simp add: diff_eq1 negate_eq1)
   23.10 -
   23.11 +  assumes "vectorspace V"
   23.12 +  shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U" (is "PROP ?P")
   23.13 +proof -
   23.14 +  interpret vectorspace [V] by fact
   23.15 +  show "PROP ?P" by (simp add: diff_eq1 negate_eq1)
   23.16 +qed
   23.17  
   23.18  text {*
   23.19    \medskip Similar as for linear spaces, the existence of the zero
   23.20 @@ -53,9 +55,10 @@
   23.21  *}
   23.22  
   23.23  lemma (in subspace) zero [intro]:
   23.24 -  includes vectorspace
   23.25 +  assumes "vectorspace V"
   23.26    shows "0 \<in> U"
   23.27  proof -
   23.28 +  interpret vectorspace [V] by fact
   23.29    have "U \<noteq> {}" by (rule U_V.non_empty)
   23.30    then obtain x where x: "x \<in> U" by blast
   23.31    hence "x \<in> V" .. hence "0 = x - x" by simp
   23.32 @@ -64,32 +67,37 @@
   23.33  qed
   23.34  
   23.35  lemma (in subspace) neg_closed [iff]:
   23.36 -  includes vectorspace
   23.37 -  shows "x \<in> U \<Longrightarrow> - x \<in> U"
   23.38 -  by (simp add: negate_eq1)
   23.39 -
   23.40 +  assumes "vectorspace V"
   23.41 +  shows "x \<in> U \<Longrightarrow> - x \<in> U" (is "PROP ?P")
   23.42 +proof -
   23.43 +  interpret vectorspace [V] by fact
   23.44 +  show "PROP ?P" by (simp add: negate_eq1)
   23.45 +qed
   23.46  
   23.47  text {* \medskip Further derived laws: every subspace is a vector space. *}
   23.48  
   23.49  lemma (in subspace) vectorspace [iff]:
   23.50 -  includes vectorspace
   23.51 +  assumes "vectorspace V"
   23.52    shows "vectorspace U"
   23.53 -proof
   23.54 -  show "U \<noteq> {}" ..
   23.55 -  fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
   23.56 -  fix a b :: real
   23.57 -  from x y show "x + y \<in> U" by simp
   23.58 -  from x show "a \<cdot> x \<in> U" by simp
   23.59 -  from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)
   23.60 -  from x y show "x + y = y + x" by (simp add: add_ac)
   23.61 -  from x show "x - x = 0" by simp
   23.62 -  from x show "0 + x = x" by simp
   23.63 -  from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib)
   23.64 -  from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib)
   23.65 -  from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc)
   23.66 -  from x show "1 \<cdot> x = x" by simp
   23.67 -  from x show "- x = - 1 \<cdot> x" by (simp add: negate_eq1)
   23.68 -  from x y show "x - y = x + - y" by (simp add: diff_eq1)
   23.69 +proof -
   23.70 +  interpret vectorspace [V] by fact
   23.71 +  show ?thesis proof
   23.72 +    show "U \<noteq> {}" ..
   23.73 +    fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
   23.74 +    fix a b :: real
   23.75 +    from x y show "x + y \<in> U" by simp
   23.76 +    from x show "a \<cdot> x \<in> U" by simp
   23.77 +    from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)
   23.78 +    from x y show "x + y = y + x" by (simp add: add_ac)
   23.79 +    from x show "x - x = 0" by simp
   23.80 +    from x show "0 + x = x" by simp
   23.81 +    from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib)
   23.82 +    from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib)
   23.83 +    from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc)
   23.84 +    from x show "1 \<cdot> x = x" by simp
   23.85 +    from x show "- x = - 1 \<cdot> x" by (simp add: negate_eq1)
   23.86 +    from x y show "x - y = x + - y" by (simp add: diff_eq1)
   23.87 +  qed
   23.88  qed
   23.89  
   23.90  
   23.91 @@ -236,61 +244,70 @@
   23.92  text {* @{text U} is a subspace of @{text "U + V"}. *}
   23.93  
   23.94  lemma subspace_sum1 [iff]:
   23.95 -  includes vectorspace U + vectorspace V
   23.96 +  assumes "vectorspace U" "vectorspace V"
   23.97    shows "U \<unlhd> U + V"
   23.98 -proof
   23.99 -  show "U \<noteq> {}" ..
  23.100 -  show "U \<subseteq> U + V"
  23.101 -  proof
  23.102 -    fix x assume x: "x \<in> U"
  23.103 -    moreover have "0 \<in> V" ..
  23.104 -    ultimately have "x + 0 \<in> U + V" ..
  23.105 -    with x show "x \<in> U + V" by simp
  23.106 +proof -
  23.107 +  interpret vectorspace [U] by fact
  23.108 +  interpret vectorspace [V] by fact
  23.109 +  show ?thesis proof
  23.110 +    show "U \<noteq> {}" ..
  23.111 +    show "U \<subseteq> U + V"
  23.112 +    proof
  23.113 +      fix x assume x: "x \<in> U"
  23.114 +      moreover have "0 \<in> V" ..
  23.115 +      ultimately have "x + 0 \<in> U + V" ..
  23.116 +      with x show "x \<in> U + V" by simp
  23.117 +    qed
  23.118 +    fix x y assume x: "x \<in> U" and "y \<in> U"
  23.119 +    thus "x + y \<in> U" by simp
  23.120 +    from x show "\<And>a. a \<cdot> x \<in> U" by simp
  23.121    qed
  23.122 -  fix x y assume x: "x \<in> U" and "y \<in> U"
  23.123 -  thus "x + y \<in> U" by simp
  23.124 -  from x show "\<And>a. a \<cdot> x \<in> U" by simp
  23.125  qed
  23.126  
  23.127  text {* The sum of two subspaces is again a subspace. *}
  23.128  
  23.129  lemma sum_subspace [intro?]:
  23.130 -  includes subspace U E + vectorspace E + subspace V E
  23.131 +  assumes "subspace U E" "vectorspace E" "subspace V E"
  23.132    shows "U + V \<unlhd> E"
  23.133 -proof
  23.134 -  have "0 \<in> U + V"
  23.135 -  proof
  23.136 -    show "0 \<in> U" using `vectorspace E` ..
  23.137 -    show "0 \<in> V" using `vectorspace E` ..
  23.138 -    show "(0::'a) = 0 + 0" by simp
  23.139 -  qed
  23.140 -  thus "U + V \<noteq> {}" by blast
  23.141 -  show "U + V \<subseteq> E"
  23.142 -  proof
  23.143 -    fix x assume "x \<in> U + V"
  23.144 -    then obtain u v where "x = u + v" and
  23.145 -      "u \<in> U" and "v \<in> V" ..
  23.146 -    then show "x \<in> E" by simp
  23.147 -  qed
  23.148 -  fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
  23.149 -  show "x + y \<in> U + V"
  23.150 -  proof -
  23.151 -    from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
  23.152 -    moreover
  23.153 -    from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" ..
  23.154 -    ultimately
  23.155 -    have "ux + uy \<in> U"
  23.156 -      and "vx + vy \<in> V"
  23.157 -      and "x + y = (ux + uy) + (vx + vy)"
  23.158 -      using x y by (simp_all add: add_ac)
  23.159 -    thus ?thesis ..
  23.160 -  qed
  23.161 -  fix a show "a \<cdot> x \<in> U + V"
  23.162 -  proof -
  23.163 -    from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
  23.164 -    hence "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
  23.165 -      and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)
  23.166 -    thus ?thesis ..
  23.167 +proof -
  23.168 +  interpret subspace [U E] by fact
  23.169 +  interpret vectorspace [E] by fact
  23.170 +  interpret subspace [V E] by fact
  23.171 +  show ?thesis proof
  23.172 +    have "0 \<in> U + V"
  23.173 +    proof
  23.174 +      show "0 \<in> U" using `vectorspace E` ..
  23.175 +      show "0 \<in> V" using `vectorspace E` ..
  23.176 +      show "(0::'a) = 0 + 0" by simp
  23.177 +    qed
  23.178 +    thus "U + V \<noteq> {}" by blast
  23.179 +    show "U + V \<subseteq> E"
  23.180 +    proof
  23.181 +      fix x assume "x \<in> U + V"
  23.182 +      then obtain u v where "x = u + v" and
  23.183 +	"u \<in> U" and "v \<in> V" ..
  23.184 +      then show "x \<in> E" by simp
  23.185 +    qed
  23.186 +    fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
  23.187 +    show "x + y \<in> U + V"
  23.188 +    proof -
  23.189 +      from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
  23.190 +      moreover
  23.191 +      from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" ..
  23.192 +      ultimately
  23.193 +      have "ux + uy \<in> U"
  23.194 +	and "vx + vy \<in> V"
  23.195 +	and "x + y = (ux + uy) + (vx + vy)"
  23.196 +	using x y by (simp_all add: add_ac)
  23.197 +      thus ?thesis ..
  23.198 +    qed
  23.199 +    fix a show "a \<cdot> x \<in> U + V"
  23.200 +    proof -
  23.201 +      from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
  23.202 +      hence "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
  23.203 +	and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)
  23.204 +      thus ?thesis ..
  23.205 +    qed
  23.206    qed
  23.207  qed
  23.208  
  23.209 @@ -312,37 +329,42 @@
  23.210  *}
  23.211  
  23.212  lemma decomp:
  23.213 -  includes vectorspace E + subspace U E + subspace V E
  23.214 +  assumes "vectorspace E" "subspace U E" "subspace V E"
  23.215    assumes direct: "U \<inter> V = {0}"
  23.216      and u1: "u1 \<in> U" and u2: "u2 \<in> U"
  23.217      and v1: "v1 \<in> V" and v2: "v2 \<in> V"
  23.218      and sum: "u1 + v1 = u2 + v2"
  23.219    shows "u1 = u2 \<and> v1 = v2"
  23.220 -proof
  23.221 -  have U: "vectorspace U"
  23.222 -    using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
  23.223 -  have V: "vectorspace V"
  23.224 -    using `subspace V E` `vectorspace E` by (rule subspace.vectorspace)
  23.225 -  from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
  23.226 -    by (simp add: add_diff_swap)
  23.227 -  from u1 u2 have u: "u1 - u2 \<in> U"
  23.228 -    by (rule vectorspace.diff_closed [OF U])
  23.229 -  with eq have v': "v2 - v1 \<in> U" by (simp only:)
  23.230 -  from v2 v1 have v: "v2 - v1 \<in> V"
  23.231 -    by (rule vectorspace.diff_closed [OF V])
  23.232 -  with eq have u': " u1 - u2 \<in> V" by (simp only:)
  23.233 -
  23.234 -  show "u1 = u2"
  23.235 -  proof (rule add_minus_eq)
  23.236 -    from u1 show "u1 \<in> E" ..
  23.237 -    from u2 show "u2 \<in> E" ..
  23.238 -    from u u' and direct show "u1 - u2 = 0" by blast
  23.239 -  qed
  23.240 -  show "v1 = v2"
  23.241 -  proof (rule add_minus_eq [symmetric])
  23.242 -    from v1 show "v1 \<in> E" ..
  23.243 -    from v2 show "v2 \<in> E" ..
  23.244 -    from v v' and direct show "v2 - v1 = 0" by blast
  23.245 +proof -
  23.246 +  interpret vectorspace [E] by fact
  23.247 +  interpret subspace [U E] by fact
  23.248 +  interpret subspace [V E] by fact
  23.249 +  show ?thesis proof
  23.250 +    have U: "vectorspace U"  (* FIXME: use interpret *)
  23.251 +      using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
  23.252 +    have V: "vectorspace V"
  23.253 +      using `subspace V E` `vectorspace E` by (rule subspace.vectorspace)
  23.254 +    from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
  23.255 +      by (simp add: add_diff_swap)
  23.256 +    from u1 u2 have u: "u1 - u2 \<in> U"
  23.257 +      by (rule vectorspace.diff_closed [OF U])
  23.258 +    with eq have v': "v2 - v1 \<in> U" by (simp only:)
  23.259 +    from v2 v1 have v: "v2 - v1 \<in> V"
  23.260 +      by (rule vectorspace.diff_closed [OF V])
  23.261 +    with eq have u': " u1 - u2 \<in> V" by (simp only:)
  23.262 +    
  23.263 +    show "u1 = u2"
  23.264 +    proof (rule add_minus_eq)
  23.265 +      from u1 show "u1 \<in> E" ..
  23.266 +      from u2 show "u2 \<in> E" ..
  23.267 +      from u u' and direct show "u1 - u2 = 0" by blast
  23.268 +    qed
  23.269 +    show "v1 = v2"
  23.270 +    proof (rule add_minus_eq [symmetric])
  23.271 +      from v1 show "v1 \<in> E" ..
  23.272 +      from v2 show "v2 \<in> E" ..
  23.273 +      from v v' and direct show "v2 - v1 = 0" by blast
  23.274 +    qed
  23.275    qed
  23.276  qed
  23.277  
  23.278 @@ -356,48 +378,52 @@
  23.279  *}
  23.280  
  23.281  lemma decomp_H':
  23.282 -  includes vectorspace E + subspace H E
  23.283 +  assumes "vectorspace E" "subspace H E"
  23.284    assumes y1: "y1 \<in> H" and y2: "y2 \<in> H"
  23.285      and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
  23.286      and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
  23.287    shows "y1 = y2 \<and> a1 = a2"
  23.288 -proof
  23.289 -  have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
  23.290 -  proof (rule decomp)
  23.291 -    show "a1 \<cdot> x' \<in> lin x'" ..
  23.292 -    show "a2 \<cdot> x' \<in> lin x'" ..
  23.293 -    show "H \<inter> lin x' = {0}"
  23.294 -    proof
  23.295 -      show "H \<inter> lin x' \<subseteq> {0}"
  23.296 +proof -
  23.297 +  interpret vectorspace [E] by fact
  23.298 +  interpret subspace [H E] by fact
  23.299 +  show ?thesis proof
  23.300 +    have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
  23.301 +    proof (rule decomp)
  23.302 +      show "a1 \<cdot> x' \<in> lin x'" ..
  23.303 +      show "a2 \<cdot> x' \<in> lin x'" ..
  23.304 +      show "H \<inter> lin x' = {0}"
  23.305        proof
  23.306 -        fix x assume x: "x \<in> H \<inter> lin x'"
  23.307 -        then obtain a where xx': "x = a \<cdot> x'"
  23.308 -          by blast
  23.309 -        have "x = 0"
  23.310 -        proof cases
  23.311 -          assume "a = 0"
  23.312 -          with xx' and x' show ?thesis by simp
  23.313 -        next
  23.314 -          assume a: "a \<noteq> 0"
  23.315 -          from x have "x \<in> H" ..
  23.316 -          with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
  23.317 -          with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
  23.318 -          with `x' \<notin> H` show ?thesis by contradiction
  23.319 -        qed
  23.320 -        thus "x \<in> {0}" ..
  23.321 +	show "H \<inter> lin x' \<subseteq> {0}"
  23.322 +	proof
  23.323 +          fix x assume x: "x \<in> H \<inter> lin x'"
  23.324 +          then obtain a where xx': "x = a \<cdot> x'"
  23.325 +            by blast
  23.326 +          have "x = 0"
  23.327 +          proof cases
  23.328 +            assume "a = 0"
  23.329 +            with xx' and x' show ?thesis by simp
  23.330 +          next
  23.331 +            assume a: "a \<noteq> 0"
  23.332 +            from x have "x \<in> H" ..
  23.333 +            with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
  23.334 +            with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
  23.335 +            with `x' \<notin> H` show ?thesis by contradiction
  23.336 +          qed
  23.337 +          thus "x \<in> {0}" ..
  23.338 +	qed
  23.339 +	show "{0} \<subseteq> H \<inter> lin x'"
  23.340 +	proof -
  23.341 +          have "0 \<in> H" using `vectorspace E` ..
  23.342 +          moreover have "0 \<in> lin x'" using `x' \<in> E` ..
  23.343 +          ultimately show ?thesis by blast
  23.344 +	qed
  23.345        qed
  23.346 -      show "{0} \<subseteq> H \<inter> lin x'"
  23.347 -      proof -
  23.348 -        have "0 \<in> H" using `vectorspace E` ..
  23.349 -        moreover have "0 \<in> lin x'" using `x' \<in> E` ..
  23.350 -        ultimately show ?thesis by blast
  23.351 -      qed
  23.352 -    qed
  23.353 -    show "lin x' \<unlhd> E" using `x' \<in> E` ..
  23.354 -  qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
  23.355 -  thus "y1 = y2" ..
  23.356 -  from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
  23.357 -  with x' show "a1 = a2" by (simp add: mult_right_cancel)
  23.358 +      show "lin x' \<unlhd> E" using `x' \<in> E` ..
  23.359 +    qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
  23.360 +    thus "y1 = y2" ..
  23.361 +    from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
  23.362 +    with x' show "a1 = a2" by (simp add: mult_right_cancel)
  23.363 +  qed
  23.364  qed
  23.365  
  23.366  text {*
  23.367 @@ -408,19 +434,23 @@
  23.368  *}
  23.369  
  23.370  lemma decomp_H'_H:
  23.371 -  includes vectorspace E + subspace H E
  23.372 +  assumes "vectorspace E" "subspace H E"
  23.373    assumes t: "t \<in> H"
  23.374      and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
  23.375    shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
  23.376 -proof (rule, simp_all only: split_paired_all split_conv)
  23.377 -  from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
  23.378 -  fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"
  23.379 -  have "y = t \<and> a = 0"
  23.380 -  proof (rule decomp_H')
  23.381 -    from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
  23.382 -    from ya show "y \<in> H" ..
  23.383 -  qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
  23.384 -  with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
  23.385 +proof -
  23.386 +  interpret vectorspace [E] by fact
  23.387 +  interpret subspace [H E] by fact
  23.388 +  show ?thesis proof (rule, simp_all only: split_paired_all split_conv)
  23.389 +    from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
  23.390 +    fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"
  23.391 +    have "y = t \<and> a = 0"
  23.392 +    proof (rule decomp_H')
  23.393 +      from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
  23.394 +      from ya show "y \<in> H" ..
  23.395 +    qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
  23.396 +    with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
  23.397 +  qed
  23.398  qed
  23.399  
  23.400  text {*
  23.401 @@ -430,16 +460,18 @@
  23.402  *}
  23.403  
  23.404  lemma h'_definite:
  23.405 -  includes var H
  23.406 +  fixes H
  23.407    assumes h'_def:
  23.408      "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
  23.409                  in (h y) + a * xi)"
  23.410      and x: "x = y + a \<cdot> x'"
  23.411 -  includes vectorspace E + subspace H E
  23.412 +  assumes "vectorspace E" "subspace H E"
  23.413    assumes y: "y \<in> H"
  23.414      and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
  23.415    shows "h' x = h y + a * xi"
  23.416  proof -
  23.417 +  interpret vectorspace [E] by fact
  23.418 +  interpret subspace [H E] by fact
  23.419    from x y x' have "x \<in> H + lin x'" by auto
  23.420    have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
  23.421    proof (rule ex_ex1I)