Removed uses of context element includes.
--- a/src/HOL/Algebra/AbelCoset.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy Tue Jul 15 16:50:09 2008 +0200
@@ -60,7 +60,7 @@
a_r_coset_def r_coset_def
lemma a_r_coset_def':
- includes struct G
+ fixes G (structure)
shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}"
unfolding a_r_coset_defs
by simp
@@ -69,7 +69,7 @@
a_l_coset_def l_coset_def
lemma a_l_coset_def':
- includes struct G
+ fixes G (structure)
shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}"
unfolding a_l_coset_defs
by simp
@@ -78,7 +78,7 @@
A_RCOSETS_def RCOSETS_def
lemma A_RCOSETS_def':
- includes struct G
+ fixes G (structure)
shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}"
unfolding A_RCOSETS_defs
by (fold a_r_coset_def, simp)
@@ -87,7 +87,7 @@
set_add_def set_mult_def
lemma set_add_def':
- includes struct G
+ fixes G (structure)
shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"
unfolding set_add_defs
by simp
@@ -96,7 +96,7 @@
A_SET_INV_def SET_INV_def
lemma A_SET_INV_def':
- includes struct G
+ fixes G (structure)
shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
unfolding A_SET_INV_defs
by (fold a_inv_def)
@@ -188,7 +188,7 @@
by (rule additive_subgroup_axioms)
lemma additive_subgroupI:
- includes struct G
+ fixes G (structure)
assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
shows "additive_subgroup H G"
by (rule additive_subgroup.intro) (rule a_subgroup)
@@ -240,7 +240,7 @@
qed
lemma abelian_subgroupI2:
- includes struct G
+ fixes G (structure)
assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
shows "abelian_subgroup H G"
@@ -265,7 +265,7 @@
qed
lemma abelian_subgroupI3:
- includes struct G
+ fixes G (structure)
assumes asg: "additive_subgroup H G"
and ag: "abelian_group G"
shows "abelian_subgroup H G"
@@ -451,7 +451,7 @@
lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
lemma A_FactGroup_def':
- includes struct G
+ fixes G (structure)
shows "G A_Mod H \<equiv> \<lparr>carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\<rparr>"
unfolding A_FactGroup_defs
by (fold A_RCOSETS_def set_add_def)
@@ -534,16 +534,20 @@
subsection {* Homomorphisms *}
lemma abelian_group_homI:
- includes abelian_group G
- includes abelian_group H
+ assumes "abelian_group G"
+ assumes "abelian_group H"
assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
(| carrier = carrier H, mult = add H, one = zero H |) h"
shows "abelian_group_hom G H h"
-apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
- apply (rule G.abelian_group_axioms)
- apply (rule H.abelian_group_axioms)
-apply (rule a_group_hom)
-done
+proof -
+ interpret G: abelian_group [G] by fact
+ interpret H: abelian_group [H] by fact
+ show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
+ apply fact
+ apply fact
+ apply (rule a_group_hom)
+ done
+qed
lemma (in abelian_group_hom) is_abelian_group_hom:
"abelian_group_hom G H h"
@@ -688,10 +692,11 @@
--"variant"
lemma (in abelian_subgroup) a_rcos_module_minus:
- includes ring G
+ assumes "ring G"
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
proof -
+ interpret G: ring [G] by fact
from carr
have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
with carr
--- a/src/HOL/Algebra/Coset.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/Coset.thy Tue Jul 15 16:50:09 2008 +0200
@@ -109,23 +109,27 @@
text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
lemma (in group) repr_independenceD:
- includes subgroup H G
+ assumes "subgroup H G"
assumes ycarr: "y \<in> carrier G"
and repr: "H #> x = H #> y"
shows "y \<in> H #> x"
- apply (subst repr)
+proof -
+ interpret subgroup [H G] by fact
+ show ?thesis apply (subst repr)
apply (intro rcos_self)
apply (rule ycarr)
apply (rule is_subgroup)
done
+qed
text {* Elements of a right coset are in the carrier *}
lemma (in subgroup) elemrcos_carrier:
- includes group
+ assumes "group G"
assumes acarr: "a \<in> carrier G"
and a': "a' \<in> H #> a"
shows "a' \<in> carrier G"
proof -
+ interpret group [G] by fact
from subset and acarr
have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
from this and a'
@@ -134,38 +138,42 @@
qed
lemma (in subgroup) rcos_const:
- includes group
+ assumes "group G"
assumes hH: "h \<in> H"
shows "H #> h = H"
- apply (unfold r_coset_def)
- apply rule
- apply rule
- apply clarsimp
- apply (intro subgroup.m_closed)
- apply (rule is_subgroup)
+proof -
+ interpret group [G] by fact
+ show ?thesis apply (unfold r_coset_def)
+ apply rule
+ apply rule
+ apply clarsimp
+ apply (intro subgroup.m_closed)
+ apply (rule is_subgroup)
apply assumption
- apply (rule hH)
- apply rule
- apply simp
-proof -
- fix h'
- assume h'H: "h' \<in> H"
- note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
- from carr
- have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
- from h'H hH
- have "h' \<otimes> inv h \<in> H" by simp
- from this and a
- show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
+ apply (rule hH)
+ apply rule
+ apply simp
+ proof -
+ fix h'
+ assume h'H: "h' \<in> H"
+ note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
+ from carr
+ have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
+ from h'H hH
+ have "h' \<otimes> inv h \<in> H" by simp
+ from this and a
+ show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
+ qed
qed
text {* Step one for lemma @{text "rcos_module"} *}
lemma (in subgroup) rcos_module_imp:
- includes group
+ assumes "group G"
assumes xcarr: "x \<in> carrier G"
and x'cos: "x' \<in> H #> x"
shows "(x' \<otimes> inv x) \<in> H"
proof -
+ interpret group [G] by fact
from xcarr x'cos
have x'carr: "x' \<in> carrier G"
by (rule elemrcos_carrier[OF is_group])
@@ -200,11 +208,12 @@
text {* Step two for lemma @{text "rcos_module"} *}
lemma (in subgroup) rcos_module_rev:
- includes group
+ assumes "group G"
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
and xixH: "(x' \<otimes> inv x) \<in> H"
shows "x' \<in> H #> x"
proof -
+ interpret group [G] by fact
from xixH
have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
from this
@@ -231,27 +240,30 @@
text {* Module property of right cosets *}
lemma (in subgroup) rcos_module:
- includes group
+ assumes "group G"
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
-proof
- assume "x' \<in> H #> x"
- from this and carr
- show "x' \<otimes> inv x \<in> H"
+proof -
+ interpret group [G] by fact
+ show ?thesis proof assume "x' \<in> H #> x"
+ from this and carr
+ show "x' \<otimes> inv x \<in> H"
by (intro rcos_module_imp[OF is_group])
-next
- assume "x' \<otimes> inv x \<in> H"
- from this and carr
- show "x' \<in> H #> x"
+ next
+ assume "x' \<otimes> inv x \<in> H"
+ from this and carr
+ show "x' \<in> H #> x"
by (intro rcos_module_rev[OF is_group])
+ qed
qed
text {* Right cosets are subsets of the carrier. *}
lemma (in subgroup) rcosets_carrier:
- includes group
+ assumes "group G"
assumes XH: "X \<in> rcosets H"
shows "X \<subseteq> carrier G"
proof -
+ interpret group [G] by fact
from XH have "\<exists>x\<in> carrier G. X = H #> x"
unfolding RCOSETS_def
by fast
@@ -331,11 +343,12 @@
qed
lemma (in subgroup) lcos_module_rev:
- includes group
+ assumes "group G"
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
and xixH: "(inv x \<otimes> x') \<in> H"
shows "x' \<in> x <# H"
proof -
+ interpret group [G] by fact
from xixH
have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
from this
@@ -584,29 +597,33 @@
lemma (in subgroup) equiv_rcong:
- includes group G
+ assumes "group G"
shows "equiv (carrier G) (rcong H)"
-proof (intro equiv.intro)
- show "refl (carrier G) (rcong H)"
- by (auto simp add: r_congruent_def refl_def)
-next
- show "sym (rcong H)"
- proof (simp add: r_congruent_def sym_def, clarify)
- fix x y
- assume [simp]: "x \<in> carrier G" "y \<in> carrier G"
- and "inv x \<otimes> y \<in> H"
- hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed)
- thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
- qed
-next
- show "trans (rcong H)"
- proof (simp add: r_congruent_def trans_def, clarify)
- fix x y z
- assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
- and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
- hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
- hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv)
- thus "inv x \<otimes> z \<in> H" by simp
+proof -
+ interpret group [G] by fact
+ show ?thesis
+ proof (intro equiv.intro)
+ show "refl (carrier G) (rcong H)"
+ by (auto simp add: r_congruent_def refl_def)
+ next
+ show "sym (rcong H)"
+ proof (simp add: r_congruent_def sym_def, clarify)
+ fix x y
+ assume [simp]: "x \<in> carrier G" "y \<in> carrier G"
+ and "inv x \<otimes> y \<in> H"
+ hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed)
+ thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
+ qed
+ next
+ show "trans (rcong H)"
+ proof (simp add: r_congruent_def trans_def, clarify)
+ fix x y z
+ assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
+ and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
+ hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
+ hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv)
+ thus "inv x \<otimes> z \<in> H" by simp
+ qed
qed
qed
@@ -625,31 +642,38 @@
*)
lemma (in subgroup) l_coset_eq_rcong:
- includes group G
+ assumes "group G"
assumes a: "a \<in> carrier G"
shows "a <# H = rcong H `` {a}"
-by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
-
+proof -
+ interpret group [G] by fact
+ show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
+qed
subsubsection{*Two Distinct Right Cosets are Disjoint*}
lemma (in group) rcos_equation:
- includes subgroup H G
- shows
- "\<lbrakk>ha \<otimes> a = h \<otimes> b; a \<in> carrier G; b \<in> carrier G;
- h \<in> H; ha \<in> H; hb \<in> H\<rbrakk>
- \<Longrightarrow> hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
-apply (rule UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
-apply (simp add: )
-apply (simp add: m_assoc transpose_inv)
-done
+ assumes "subgroup H G"
+ 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"
+ shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
+proof -
+ interpret subgroup [H G] by fact
+ from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
+ apply (simp add: )
+ apply (simp add: m_assoc transpose_inv)
+ done
+qed
lemma (in group) rcos_disjoint:
- includes subgroup H G
- shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
-apply (simp add: RCOSETS_def r_coset_def)
-apply (blast intro: rcos_equation prems sym)
-done
+ assumes "subgroup H G"
+ assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
+ shows "a \<inter> b = {}"
+proof -
+ interpret subgroup [H G] by fact
+ from p show ?thesis apply (simp add: RCOSETS_def r_coset_def)
+ apply (blast intro: rcos_equation prems sym)
+ done
+qed
subsection {* Further lemmas for @{text "r_congruent"} *}
@@ -732,12 +756,16 @@
"order S \<equiv> card (carrier S)"
lemma (in group) rcosets_part_G:
- includes subgroup
+ assumes "subgroup H G"
shows "\<Union>(rcosets H) = carrier G"
-apply (rule equalityI)
- apply (force simp add: RCOSETS_def r_coset_def)
-apply (auto simp add: RCOSETS_def intro: rcos_self prems)
-done
+proof -
+ interpret subgroup [H G] by fact
+ show ?thesis
+ apply (rule equalityI)
+ apply (force simp add: RCOSETS_def r_coset_def)
+ apply (auto simp add: RCOSETS_def intro: rcos_self prems)
+ done
+qed
lemma (in group) cosets_finite:
"\<lbrakk>c \<in> rcosets H; H \<subseteq> carrier G; finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
@@ -815,9 +843,10 @@
by (auto simp add: RCOSETS_def rcos_sum m_assoc)
lemma (in subgroup) subgroup_in_rcosets:
- includes group G
+ assumes "group G"
shows "H \<in> rcosets H"
proof -
+ interpret group [G] by fact
from _ subgroup_axioms have "H #> \<one> = H"
by (rule coset_join2) auto
then show ?thesis
--- a/src/HOL/Algebra/Group.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/Group.thy Tue Jul 15 16:50:09 2008 +0200
@@ -396,9 +396,13 @@
by (rule subgroup.subset)
lemma (in subgroup) subgroup_is_group [intro]:
- includes group G
- shows "group (G\<lparr>carrier := H\<rparr>)"
- by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
+ assumes "group G"
+ shows "group (G\<lparr>carrier := H\<rparr>)"
+proof -
+ interpret group [G] by fact
+ show ?thesis
+ by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
+qed
text {*
Since @{term H} is nonempty, it contains some element @{term x}. Since
@@ -453,9 +457,11 @@
one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
lemma DirProd_monoid:
- includes monoid G + monoid H
+ assumes "monoid G" and "monoid H"
shows "monoid (G \<times>\<times> H)"
proof -
+ interpret G: monoid [G] by fact
+ interpret H: monoid [H] by fact
from prems
show ?thesis by (unfold monoid_def DirProd_def, auto)
qed
@@ -463,11 +469,15 @@
text{*Does not use the previous result because it's easier just to use auto.*}
lemma DirProd_group:
- includes group G + group H
+ assumes "group G" and "group H"
shows "group (G \<times>\<times> H)"
- by (rule groupI)
+proof -
+ interpret G: group [G] by fact
+ interpret H: group [H] by fact
+ show ?thesis by (rule groupI)
(auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
simp add: DirProd_def)
+qed
lemma carrier_DirProd [simp]:
"carrier (G \<times>\<times> H) = carrier G \<times> carrier H"
@@ -482,23 +492,29 @@
by (simp add: DirProd_def)
lemma inv_DirProd [simp]:
- includes group G + group H
+ assumes "group G" and "group H"
assumes g: "g \<in> carrier G"
and h: "h \<in> carrier H"
shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
- apply (rule group.inv_equality [OF DirProd_group])
+proof -
+ interpret G: group [G] by fact
+ interpret H: group [H] by fact
+ show ?thesis apply (rule group.inv_equality [OF DirProd_group])
apply (simp_all add: prems group.l_inv)
done
+qed
text{*This alternative proof of the previous result demonstrates interpret.
It uses @{text Prod.inv_equality} (available after @{text interpret})
instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
lemma
- includes group G + group H
+ assumes "group G" and "group H"
assumes g: "g \<in> carrier G"
and h: "h \<in> carrier H"
shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
proof -
+ interpret G: group [G] by fact
+ interpret H: group [H] by fact
interpret Prod: group ["G \<times>\<times> H"]
by (auto intro: DirProd_group group.intro group.axioms prems)
show ?thesis by (simp add: Prod.inv_equality g h)
--- a/src/HOL/Algebra/Ideal.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/Ideal.thy Tue Jul 15 16:50:09 2008 +0200
@@ -28,18 +28,21 @@
by (rule ideal_axioms)
lemma idealI:
- includes ring
+ fixes R (structure)
+ assumes "ring R"
assumes a_subgroup: "subgroup I \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
shows "ideal I R"
- apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
+proof -
+ interpret ring [R] by fact
+ show ?thesis apply (intro ideal.intro ideal_axioms.intro additive_subgroupI)
apply (rule a_subgroup)
apply (rule is_ring)
apply (erule (1) I_l_closed)
apply (erule (1) I_r_closed)
done
-
+qed
subsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
@@ -58,11 +61,14 @@
by (rule principalideal_axioms)
lemma principalidealI:
- includes ideal
+ fixes R (structure)
+ assumes "ideal I R"
assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
shows "principalideal I R"
- by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
-
+proof -
+ interpret ideal [I R] by fact
+ show ?thesis by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
+qed
subsection {* Maximal Ideals *}
@@ -75,13 +81,16 @@
by (rule maximalideal_axioms)
lemma maximalidealI:
- includes ideal
+ fixes R
+ assumes "ideal I R"
assumes I_notcarr: "carrier R \<noteq> I"
and I_maximal: "\<And>J. \<lbrakk>ideal J R; I \<subseteq> J; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> J = I \<or> J = carrier R"
shows "maximalideal I R"
- by (intro maximalideal.intro maximalideal_axioms.intro)
+proof -
+ interpret ideal [I R] by fact
+ show ?thesis by (intro maximalideal.intro maximalideal_axioms.intro)
(rule is_ideal, rule I_notcarr, rule I_maximal)
-
+qed
subsection {* Prime Ideals *}
@@ -94,31 +103,40 @@
by (rule primeideal_axioms)
lemma primeidealI:
- includes ideal
- includes cring
+ fixes R (structure)
+ assumes "ideal I R"
+ assumes "cring R"
assumes I_notcarr: "carrier R \<noteq> I"
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"
shows "primeideal I R"
- by (intro primeideal.intro primeideal_axioms.intro)
+proof -
+ interpret ideal [I R] by fact
+ interpret cring [R] by fact
+ show ?thesis by (intro primeideal.intro primeideal_axioms.intro)
(rule is_ideal, rule is_cring, rule I_notcarr, rule I_prime)
+qed
lemma primeidealI2:
- includes additive_subgroup I R
- includes cring
+ fixes R (structure)
+ assumes "additive_subgroup I R"
+ assumes "cring R"
assumes I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
and I_notcarr: "carrier R \<noteq> I"
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"
shows "primeideal I R"
-apply (intro_locales)
- apply (intro ideal_axioms.intro)
- apply (erule (1) I_l_closed)
- apply (erule (1) I_r_closed)
-apply (intro primeideal_axioms.intro)
- apply (rule I_notcarr)
-apply (erule (2) I_prime)
-done
-
+proof -
+ interpret additive_subgroup [I R] by fact
+ interpret cring [R] by fact
+ show ?thesis apply (intro_locales)
+ apply (intro ideal_axioms.intro)
+ apply (erule (1) I_l_closed)
+ apply (erule (1) I_r_closed)
+ apply (intro primeideal_axioms.intro)
+ apply (rule I_notcarr)
+ apply (erule (2) I_prime)
+ done
+qed
section {* Properties of Ideals *}
@@ -185,9 +203,13 @@
text {* \paragraph{Intersection of two ideals} The intersection of any
two ideals is again an ideal in @{term R} *}
lemma (in ring) i_intersect:
- includes ideal I R
- includes ideal J R
+ assumes "ideal I R"
+ assumes "ideal J R"
shows "ideal (I \<inter> J) R"
+proof -
+ interpret ideal [I R] by fact
+ interpret ideal [J R] by fact
+ show ?thesis
apply (intro idealI subgroup.intro)
apply (rule is_ring)
apply (force simp add: a_subset)
@@ -199,7 +221,7 @@
apply (clarsimp, rule)
apply (fast intro: ideal.I_r_closed ideal.intro prems)+
done
-
+qed
subsubsection {* Intersection of a Set of Ideals *}
@@ -511,15 +533,18 @@
text {* @{const "cgenideal"} is minimal *}
lemma (in ring) cgenideal_minimal:
- includes ideal J R
+ assumes "ideal J R"
assumes aJ: "a \<in> J"
shows "PIdl a \<subseteq> J"
-unfolding cgenideal_def
-apply rule
-apply clarify
-using aJ
-apply (erule I_l_closed)
-done
+proof -
+ interpret ideal [J R] by fact
+ show ?thesis unfolding cgenideal_def
+ apply rule
+ apply clarify
+ using aJ
+ apply (erule I_l_closed)
+ done
+qed
lemma (in cring) cgenideal_eq_genideal:
assumes icarr: "i \<in> carrier R"
@@ -636,9 +661,10 @@
text {* Every principal ideal is a right coset of the carrier *}
lemma (in principalideal) rcos_generate:
- includes cring
+ assumes "cring R"
shows "\<exists>x\<in>I. I = carrier R #> x"
proof -
+ interpret cring [R] by fact
from generate
obtain i
where icarr: "i \<in> carrier R"
@@ -667,10 +693,11 @@
subsection {* Prime Ideals *}
lemma (in ideal) primeidealCD:
- includes cring
+ assumes "cring R"
assumes notprime: "\<not> primeideal I R"
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)"
proof (rule ccontr, clarsimp)
+ interpret cring [R] by fact
assume InR: "carrier R \<noteq> I"
and "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)"
hence I_prime: "\<And> a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" by simp
@@ -685,11 +712,16 @@
qed
lemma (in ideal) primeidealCE:
- includes cring
+ assumes "cring R"
assumes notprime: "\<not> primeideal I R"
obtains "carrier R = I"
| "\<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"
- using primeidealCD [OF R.is_cring notprime] by blast
+proof -
+ interpret R: cring [R] by fact
+ assume "carrier R = I ==> thesis"
+ 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"
+ then show thesis using primeidealCD [OF R.is_cring notprime] by blast
+qed
text {* If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain *}
lemma (in cring) zeroprimeideal_domainI:
@@ -739,103 +771,108 @@
qed
lemma (in ideal) helper_max_prime:
- includes cring
+ assumes "cring R"
assumes acarr: "a \<in> carrier R"
shows "ideal {x\<in>carrier R. a \<otimes> x \<in> I} R"
-apply (rule idealI)
- apply (rule cring.axioms[OF is_cring])
- apply (rule subgroup.intro)
- apply (simp, fast)
+proof -
+ interpret cring [R] by fact
+ show ?thesis apply (rule idealI)
+ apply (rule cring.axioms[OF is_cring])
+ apply (rule subgroup.intro)
+ apply (simp, fast)
apply clarsimp apply (simp add: r_distr acarr)
- apply (simp add: acarr)
- apply (simp add: a_inv_def[symmetric], clarify) defer 1
- apply clarsimp defer 1
- apply (fast intro!: helper_I_closed acarr)
-proof -
- fix x
- assume xcarr: "x \<in> carrier R"
- and ax: "a \<otimes> x \<in> I"
- from ax and acarr xcarr
- have "\<ominus>(a \<otimes> x) \<in> I" by simp
- also from acarr xcarr
- have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra
- finally
- show "a \<otimes> (\<ominus>x) \<in> I" .
- from acarr
- have "a \<otimes> \<zero> = \<zero>" by simp
-next
- fix x y
- assume xcarr: "x \<in> carrier R"
- and ycarr: "y \<in> carrier R"
- and ayI: "a \<otimes> y \<in> I"
- from ayI and acarr xcarr ycarr
- have "a \<otimes> (y \<otimes> x) \<in> I" by (simp add: helper_I_closed)
- moreover from xcarr ycarr
- have "y \<otimes> x = x \<otimes> y" by (simp add: m_comm)
- ultimately
- show "a \<otimes> (x \<otimes> y) \<in> I" by simp
+ apply (simp add: acarr)
+ apply (simp add: a_inv_def[symmetric], clarify) defer 1
+ apply clarsimp defer 1
+ apply (fast intro!: helper_I_closed acarr)
+ proof -
+ fix x
+ assume xcarr: "x \<in> carrier R"
+ and ax: "a \<otimes> x \<in> I"
+ from ax and acarr xcarr
+ have "\<ominus>(a \<otimes> x) \<in> I" by simp
+ also from acarr xcarr
+ have "\<ominus>(a \<otimes> x) = a \<otimes> (\<ominus>x)" by algebra
+ finally
+ show "a \<otimes> (\<ominus>x) \<in> I" .
+ from acarr
+ have "a \<otimes> \<zero> = \<zero>" by simp
+ next
+ fix x y
+ assume xcarr: "x \<in> carrier R"
+ and ycarr: "y \<in> carrier R"
+ and ayI: "a \<otimes> y \<in> I"
+ from ayI and acarr xcarr ycarr
+ have "a \<otimes> (y \<otimes> x) \<in> I" by (simp add: helper_I_closed)
+ moreover from xcarr ycarr
+ have "y \<otimes> x = x \<otimes> y" by (simp add: m_comm)
+ ultimately
+ show "a \<otimes> (x \<otimes> y) \<in> I" by simp
+ qed
qed
text {* In a cring every maximal ideal is prime *}
lemma (in cring) maximalideal_is_prime:
- includes maximalideal
+ assumes "maximalideal I R"
shows "primeideal I R"
-apply (rule ccontr)
-apply (rule primeidealCE)
- apply (rule is_cring)
- apply assumption
- apply (simp add: I_notcarr)
proof -
- assume "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
- from this
- obtain a b
- where acarr: "a \<in> carrier R"
- and bcarr: "b \<in> carrier R"
- and abI: "a \<otimes> b \<in> I"
- and anI: "a \<notin> I"
- and bnI: "b \<notin> I"
+ interpret maximalideal [I R] by fact
+ show ?thesis apply (rule ccontr)
+ apply (rule primeidealCE)
+ apply (rule is_cring)
+ apply assumption
+ apply (simp add: I_notcarr)
+ proof -
+ assume "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"
+ from this
+ obtain a b
+ where acarr: "a \<in> carrier R"
+ and bcarr: "b \<in> carrier R"
+ and abI: "a \<otimes> b \<in> I"
+ and anI: "a \<notin> I"
+ and bnI: "b \<notin> I"
by fast
- def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
-
- from R.is_cring and acarr
- have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
-
- have IsubJ: "I \<subseteq> J"
- proof
- fix x
- assume xI: "x \<in> I"
- from this and acarr
- have "a \<otimes> x \<in> I" by (intro I_l_closed)
- from xI[THEN a_Hcarr] this
- show "x \<in> J" unfolding J_def by fast
+ def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
+
+ from R.is_cring and acarr
+ have idealJ: "ideal J R" unfolding J_def by (rule helper_max_prime)
+
+ have IsubJ: "I \<subseteq> J"
+ proof
+ fix x
+ assume xI: "x \<in> I"
+ from this and acarr
+ have "a \<otimes> x \<in> I" by (intro I_l_closed)
+ from xI[THEN a_Hcarr] this
+ show "x \<in> J" unfolding J_def by fast
+ qed
+
+ from abI and acarr bcarr
+ have "b \<in> J" unfolding J_def by fast
+ from bnI and this
+ have JnI: "J \<noteq> I" by fast
+ from acarr
+ have "a = a \<otimes> \<one>" by algebra
+ from this and anI
+ have "a \<otimes> \<one> \<notin> I" by simp
+ from one_closed and this
+ have "\<one> \<notin> J" unfolding J_def by fast
+ hence Jncarr: "J \<noteq> carrier R" by fast
+
+ interpret ideal ["J" "R"] by (rule idealJ)
+
+ have "J = I \<or> J = carrier R"
+ apply (intro I_maximal)
+ apply (rule idealJ)
+ apply (rule IsubJ)
+ apply (rule a_subset)
+ done
+
+ from this and JnI and Jncarr
+ show "False" by simp
qed
-
- from abI and acarr bcarr
- have "b \<in> J" unfolding J_def by fast
- from bnI and this
- have JnI: "J \<noteq> I" by fast
- from acarr
- have "a = a \<otimes> \<one>" by algebra
- from this and anI
- have "a \<otimes> \<one> \<notin> I" by simp
- from one_closed and this
- have "\<one> \<notin> J" unfolding J_def by fast
- hence Jncarr: "J \<noteq> carrier R" by fast
-
- interpret ideal ["J" "R"] by (rule idealJ)
-
- have "J = I \<or> J = carrier R"
- apply (intro I_maximal)
- apply (rule idealJ)
- apply (rule IsubJ)
- apply (rule a_subset)
- done
-
- from this and JnI and Jncarr
- show "False" by simp
qed
-
subsection {* Derived Theorems Involving Ideals *}
--"A non-zero cring that has only the two trivial ideals is a field"
--- a/src/HOL/Algebra/QuotRing.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/QuotRing.thy Tue Jul 15 16:50:09 2008 +0200
@@ -155,27 +155,32 @@
text {* The quotient of a cring is also commutative *}
lemma (in ideal) quotient_is_cring:
- includes cring
+ assumes "cring R"
shows "cring (R Quot I)"
-apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
+proof -
+ interpret cring [R] by fact
+ show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
apply (rule quotient_is_ring)
apply (rule ring.axioms[OF quotient_is_ring])
apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric])
apply clarify
apply (simp add: rcoset_mult_add m_comm)
done
+qed
text {* Cosets as a ring homomorphism on crings *}
lemma (in ideal) rcos_ring_hom_cring:
- includes cring
+ assumes "cring R"
shows "ring_hom_cring R (R Quot I) (op +> I)"
-apply (rule ring_hom_cringI)
+proof -
+ interpret cring [R] by fact
+ show ?thesis apply (rule ring_hom_cringI)
apply (rule rcos_ring_hom_ring)
apply (rule R.is_cring)
apply (rule quotient_is_cring)
apply (rule R.is_cring)
done
-
+qed
subsection {* Factorization over Prime Ideals *}
@@ -236,9 +241,11 @@
The proof follows ``W. Adkins, S. Weintraub: Algebra --
An Approach via Module Theory'' *}
lemma (in maximalideal) quotient_is_field:
- includes cring
+ assumes "cring R"
shows "field (R Quot I)"
-apply (intro cring.cring_fieldI2)
+proof -
+ interpret cring [R] by fact
+ show ?thesis apply (intro cring.cring_fieldI2)
apply (rule quotient_is_cring, rule is_cring)
defer 1
apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
@@ -338,5 +345,6 @@
from rcarr and this[symmetric]
show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
qed
+qed
end
--- a/src/HOL/Algebra/Ring.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/Ring.thy Tue Jul 15 16:50:09 2008 +0200
@@ -539,16 +539,26 @@
text {* Two examples for use of method algebra *}
lemma
- includes ring R + cring S
- shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==>
- a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
- by algebra
+ fixes R (structure) and S (structure)
+ assumes "ring R" "cring S"
+ assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
+ shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
+proof -
+ interpret ring [R] by fact
+ interpret cring [S] by fact
+ML_val {* Algebra.print_structures @{context} *}
+ from RS show ?thesis by algebra
+qed
lemma
- includes cring
- shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
- by algebra
-
+ fixes R (structure)
+ assumes "ring R"
+ assumes R: "a \<in> carrier R" "b \<in> carrier R"
+ shows "a \<ominus> (a \<ominus> b) = b"
+proof -
+ interpret ring [R] by fact
+ from R show ?thesis by algebra
+qed
subsubsection {* Sums over Finite Sets *}
--- a/src/HOL/Algebra/RingHom.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/RingHom.thy Tue Jul 15 16:50:09 2008 +0200
@@ -31,55 +31,73 @@
done
lemma (in ring_hom_ring) is_ring_hom_ring:
- includes struct R + struct S
- shows "ring_hom_ring R S h"
-by (rule ring_hom_ring_axioms)
+ "ring_hom_ring R S h"
+ by (rule ring_hom_ring_axioms)
lemma ring_hom_ringI:
- includes ring R + ring S
+ fixes R (structure) and S (structure)
+ assumes "ring R" "ring S"
assumes (* morphism: "h \<in> carrier R \<rightarrow> carrier S" *)
hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
and compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
and compatible_add: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
shows "ring_hom_ring R S h"
-apply unfold_locales
+proof -
+ interpret ring [R] by fact
+ interpret ring [S] by fact
+ show ?thesis apply unfold_locales
apply (unfold ring_hom_def, safe)
apply (simp add: hom_closed Pi_def)
apply (erule (1) compatible_mult)
apply (erule (1) compatible_add)
apply (rule compatible_one)
done
+qed
lemma ring_hom_ringI2:
- includes ring R + ring S
+ assumes "ring R" "ring S"
assumes h: "h \<in> ring_hom R S"
shows "ring_hom_ring R S h"
-apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
-apply (rule R.is_ring)
-apply (rule S.is_ring)
-apply (rule h)
-done
+proof -
+ interpret R: ring [R] by fact
+ interpret S: ring [S] by fact
+ show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
+ apply (rule R.is_ring)
+ apply (rule S.is_ring)
+ apply (rule h)
+ done
+qed
lemma ring_hom_ringI3:
- includes abelian_group_hom R S + ring R + ring S
+ fixes R (structure) and S (structure)
+ assumes "abelian_group_hom R S h" "ring R" "ring S"
assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
shows "ring_hom_ring R S h"
-apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
-apply (insert group_hom.homh[OF a_group_hom])
-apply (unfold hom_def ring_hom_def, simp)
-apply safe
-apply (erule (1) compatible_mult)
-apply (rule compatible_one)
-done
+proof -
+ interpret abelian_group_hom [R S h] by fact
+ interpret R: ring [R] by fact
+ interpret S: ring [S] by fact
+ show ?thesis apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
+ apply (insert group_hom.homh[OF a_group_hom])
+ apply (unfold hom_def ring_hom_def, simp)
+ apply safe
+ apply (erule (1) compatible_mult)
+ apply (rule compatible_one)
+ done
+qed
lemma ring_hom_cringI:
- includes ring_hom_ring R S h + cring R + cring S
+ assumes "ring_hom_ring R S h" "cring R" "cring S"
shows "ring_hom_cring R S h"
- by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
+proof -
+ interpret ring_hom_ring [R S h] by fact
+ interpret R: cring [R] by fact
+ interpret S: cring [S] by fact
+ show ?thesis by (intro ring_hom_cring.intro ring_hom_cring_axioms.intro)
(rule R.is_cring, rule S.is_cring, rule homh)
-
+qed
subsection {* The kernel of a ring homomorphism *}
--- a/src/HOL/Algebra/UnivPoly.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Tue Jul 15 16:50:09 2008 +0200
@@ -1254,15 +1254,17 @@
cring.axioms prems)
lemma (in UP_pre_univ_prop) UP_hom_unique:
- includes ring_hom_cring P S Phi
+ assumes "ring_hom_cring P S Phi"
assumes Phi: "Phi (monom P \<one> (Suc 0)) = s"
"!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
- includes ring_hom_cring P S Psi
+ assumes "ring_hom_cring P S Psi"
assumes Psi: "Psi (monom P \<one> (Suc 0)) = s"
"!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
and P: "p \<in> carrier P" and S: "s \<in> carrier S"
shows "Phi p = Psi p"
proof -
+ interpret ring_hom_cring [P S Phi] by fact
+ interpret ring_hom_cring [P S Psi] by fact
have "Phi p =
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)"
by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
--- a/src/HOL/Finite_Set.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Finite_Set.thy Tue Jul 15 16:50:09 2008 +0200
@@ -753,11 +753,14 @@
*}
lemma fold_fusion:
- includes ab_semigroup_mult g
+ assumes "ab_semigroup_mult g"
assumes fin: "finite A"
and hyp: "\<And>x y. h (g x y) = times x (h y)"
shows "h (fold g j w A) = fold times j (h w) A"
- using fin hyp by (induct set: finite) simp_all
+proof -
+ interpret ab_semigroup_mult [g] by fact
+ show ?thesis using fin hyp by (induct set: finite) simp_all
+qed
lemma fold_cong:
"finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold times g z A = fold times h z A"
--- a/src/HOL/Hyperreal/FrechetDeriv.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Hyperreal/FrechetDeriv.thy Tue Jul 15 16:50:09 2008 +0200
@@ -61,19 +61,23 @@
by simp
lemma bounded_linear_add:
- includes bounded_linear f
- includes bounded_linear g
+ assumes "bounded_linear f"
+ assumes "bounded_linear g"
shows "bounded_linear (\<lambda>x. f x + g x)"
-apply (unfold_locales)
-apply (simp only: f.add g.add add_ac)
-apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
-apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
-apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
-apply (rule_tac x="Kf + Kg" in exI, safe)
-apply (subst right_distrib)
-apply (rule order_trans [OF norm_triangle_ineq])
-apply (rule add_mono, erule spec, erule spec)
-done
+proof -
+ interpret f: bounded_linear [f] by fact
+ interpret g: bounded_linear [g] by fact
+ show ?thesis apply (unfold_locales)
+ apply (simp only: f.add g.add add_ac)
+ apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
+ apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
+ apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
+ apply (rule_tac x="Kf + Kg" in exI, safe)
+ apply (subst right_distrib)
+ apply (rule order_trans [OF norm_triangle_ineq])
+ apply (rule add_mono, erule spec, erule spec)
+ done
+qed
lemma norm_ratio_ineq:
fixes x y :: "'a::real_normed_vector"
@@ -117,13 +121,16 @@
subsection {* Subtraction *}
lemma bounded_linear_minus:
- includes bounded_linear f
+ assumes "bounded_linear f"
shows "bounded_linear (\<lambda>x. - f x)"
-apply (unfold_locales)
-apply (simp add: f.add)
-apply (simp add: f.scaleR)
-apply (simp add: f.bounded)
-done
+proof -
+ interpret f: bounded_linear [f] by fact
+ show ?thesis apply (unfold_locales)
+ apply (simp add: f.add)
+ apply (simp add: f.scaleR)
+ apply (simp add: f.bounded)
+ done
+qed
lemma FDERIV_minus:
"FDERIV f x :> F \<Longrightarrow> FDERIV (\<lambda>x. - f x) x :> (\<lambda>h. - F h)"
@@ -169,30 +176,34 @@
by simp
lemma bounded_linear_compose:
- includes bounded_linear f
- includes bounded_linear g
+ assumes "bounded_linear f"
+ assumes "bounded_linear g"
shows "bounded_linear (\<lambda>x. f (g x))"
-proof (unfold_locales)
- fix x y show "f (g (x + y)) = f (g x) + f (g y)"
- by (simp only: f.add g.add)
-next
- fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
- by (simp only: f.scaleR g.scaleR)
-next
- from f.pos_bounded
- obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
- from g.pos_bounded
- obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
- show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
- proof (intro exI allI)
- fix x
- have "norm (f (g x)) \<le> norm (g x) * Kf"
- using f .
- also have "\<dots> \<le> (norm x * Kg) * Kf"
- using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
- also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
- by (rule mult_assoc)
- finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
+proof -
+ interpret f: bounded_linear [f] by fact
+ interpret g: bounded_linear [g] by fact
+ show ?thesis proof (unfold_locales)
+ fix x y show "f (g (x + y)) = f (g x) + f (g y)"
+ by (simp only: f.add g.add)
+ next
+ fix r x show "f (g (scaleR r x)) = scaleR r (f (g x))"
+ by (simp only: f.scaleR g.scaleR)
+ next
+ from f.pos_bounded
+ obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
+ from g.pos_bounded
+ obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
+ show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
+ proof (intro exI allI)
+ fix x
+ have "norm (f (g x)) \<le> norm (g x) * Kf"
+ using f .
+ also have "\<dots> \<le> (norm x * Kg) * Kf"
+ using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
+ also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
+ by (rule mult_assoc)
+ finally show "norm (f (g x)) \<le> norm x * (Kg * Kf)" .
+ qed
qed
qed
--- a/src/HOL/Library/Multiset.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Jul 15 16:50:09 2008 +0200
@@ -1421,9 +1421,12 @@
qed
lemma fold_mset_fusion:
- includes left_commutative g
- 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"
-by (induct A) auto
+ assumes "left_commutative g"
+ 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")
+proof -
+ interpret left_commutative [g] by fact
+ show "PROP ?P" by (induct A) auto
+qed
lemma fold_mset_rec:
assumes "a \<in># A"
--- a/src/HOL/MicroJava/BV/Err.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/MicroJava/BV/Err.thy Tue Jul 15 16:50:09 2008 +0200
@@ -135,19 +135,21 @@
"~(Err <_(le r) x)"
by (simp add: lesssub_def lesub_def le_def split: err.split)
-lemma semilat_errI [intro]: includes semilat
-shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
-apply(insert semilat)
-apply (unfold semilat_Def closed_def plussub_def lesub_def
- lift2_def Err.le_def err_def)
-apply (simp split: err.split)
-done
+lemma semilat_errI [intro]:
+ assumes semilat: "semilat (A, r, f)"
+ shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
+ apply(insert semilat)
+ apply (unfold semilat_Def closed_def plussub_def lesub_def
+ lift2_def Err.le_def err_def)
+ apply (simp split: err.split)
+ done
lemma err_semilat_eslI_aux:
-includes semilat shows "err_semilat(esl(A,r,f))"
-apply (unfold sl_def esl_def)
-apply (simp add: semilat_errI[OF semilat])
-done
+ assumes semilat: "semilat (A, r, f)"
+ shows "err_semilat(esl(A,r,f))"
+ apply (unfold sl_def esl_def)
+ apply (simp add: semilat_errI[OF semilat])
+ done
lemma err_semilat_eslI [intro, simp]:
"\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
--- a/src/HOL/MicroJava/BV/Kildall.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy Tue Jul 15 16:50:09 2008 +0200
@@ -313,36 +313,44 @@
apply (blast intro: order_trans)
done
-lemma termination_lemma: includes semilat
-shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow>
- ss <[r] merges f qs ss \<or>
- 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"
-apply(insert semilat)
- apply (unfold lesssub_def)
- apply (simp (no_asm_simp) add: merges_incr)
- apply (rule impI)
- apply (rule merges_same_conv [THEN iffD1, elim_format])
- apply assumption+
+lemma termination_lemma:
+ assumes semilat: "semilat (A, r, f)"
+ shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow>
+ ss <[r] merges f qs ss \<or>
+ 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")
+proof -
+ interpret semilat [A r f] by fact
+ show "PROP ?P" apply(insert semilat)
+ apply (unfold lesssub_def)
+ apply (simp (no_asm_simp) add: merges_incr)
+ apply (rule impI)
+ apply (rule merges_same_conv [THEN iffD1, elim_format])
+ apply assumption+
defer
apply (rule sym, assumption)
- defer apply simp
- apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
- apply (blast intro!: psubsetI elim: equalityE)
- apply clarsimp
- apply (drule bspec, assumption)
- apply (drule bspec, assumption)
- apply clarsimp
- done
+ defer apply simp
+ apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
+ apply (blast intro!: psubsetI elim: equalityE)
+ apply clarsimp
+ apply (drule bspec, assumption)
+ apply (drule bspec, assumption)
+ apply clarsimp
+ done
+qed
-lemma iter_properties[rule_format]: includes semilat
-shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
+lemma iter_properties[rule_format]:
+ assumes semilat: "semilat (A, r, f)"
+ shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
\<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
iter f step ss0 w0 = (ss',w')
\<longrightarrow>
ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and>
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
-apply(insert semilat)
+ (is "PROP ?P")
+proof -
+ interpret semilat [A r f] by fact
+ show "PROP ?P" apply(insert semilat)
apply (unfold iter_def stables_def)
apply (rule_tac P = "%(ss,w).
ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
@@ -434,8 +442,10 @@
apply clarsimp
done
+qed
-lemma kildall_properties: includes semilat
+lemma kildall_properties:
+assumes semilat: "semilat (A, r, f)"
shows "\<lbrakk> acc r; pres_type step n A; mono r step n A;
bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
kildall r f step ss0 \<in> list n A \<and>
@@ -443,6 +453,10 @@
ss0 <=[r] kildall r f step ss0 \<and>
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow>
kildall r f step ss0 <=[r] ts)"
+ (is "PROP ?P")
+proof -
+ interpret semilat [A r f] by fact
+ show "PROP ?P"
apply (unfold kildall_def)
apply(case_tac "iter f step ss0 (unstables r step ss0)")
apply(simp)
@@ -450,11 +464,16 @@
apply (simp_all add: unstables_def stable_def)
apply (rule semilat)
done
-
+qed
-lemma is_bcv_kildall: includes semilat
+lemma is_bcv_kildall:
+assumes semilat: "semilat (A, r, f)"
shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk>
\<Longrightarrow> is_bcv r T step n A (kildall r f step)"
+ (is "PROP ?P")
+proof -
+ interpret semilat [A r f] by fact
+ show "PROP ?P"
apply(unfold is_bcv_def wt_step_def)
apply(insert semilat kildall_properties[of A])
apply(simp add:stables_def)
@@ -472,5 +491,6 @@
apply simp
apply (blast intro!: le_listD less_lengthI)
done
+qed
end
--- a/src/HOL/MicroJava/BV/Listn.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy Tue Jul 15 16:50:09 2008 +0200
@@ -378,7 +378,10 @@
lemma Listn_sl_aux:
-includes semilat shows "semilat (Listn.sl n (A,r,f))"
+assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))"
+proof -
+ interpret semilat [A r f] by fact
+show ?thesis
apply (unfold Listn.sl_def)
apply (simp (no_asm) only: semilat_Def split_conv)
apply (rule conjI)
@@ -388,6 +391,7 @@
apply (simp (no_asm) only: list_def)
apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
done
+qed
lemma Listn_sl: "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
by(simp add: Listn_sl_aux split_tupled_all)
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Tue Jul 15 16:50:09 2008 +0200
@@ -62,17 +62,20 @@
done
-lemma plusplus_closed: includes semilat shows
- "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
-proof (induct x)
- show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
- fix y x xs
- assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
- assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
- from xs obtain x: "x \<in> A" and xs': "set xs \<subseteq> A" by simp
- from x y have "(x +_f y) \<in> A" ..
- with xs' have "xs ++_f (x +_f y) \<in> A" by (rule IH)
- thus "(x#xs) ++_f y \<in> A" by simp
+lemma plusplus_closed: assumes "semilat (A, r, f)" shows
+ "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A" (is "PROP ?P")
+proof -
+ interpret semilat [A r f] by fact
+ show "PROP ?P" proof (induct x)
+ show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
+ fix y x xs
+ assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
+ assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
+ from xs obtain x: "x \<in> A" and xs': "set xs \<subseteq> A" by simp
+ from x y have "(x +_f y) \<in> A" ..
+ with xs' have "xs ++_f (x +_f y) \<in> A" by (rule IH)
+ thus "(x#xs) ++_f y \<in> A" by simp
+ qed
qed
lemma (in semilat) pp_ub2:
@@ -154,10 +157,13 @@
qed
-lemma ub1': includes semilat
-shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
+lemma ub1':
+ assumes "semilat (A, r, f)"
+ shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
\<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y"
proof -
+ interpret semilat [A r f] by fact
+
let "b <=_r ?map ++_f y" = ?thesis
assume "y \<in> A"
--- a/src/HOL/Real/HahnBanach/Bounds.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Tue Jul 15 16:50:09 2008 +0200
@@ -24,23 +24,26 @@
the_lub ("\<Squnion>_" [90] 90)
lemma the_lub_equality [elim?]:
- includes lub
+ assumes "lub A x"
shows "\<Squnion>A = (x::'a::order)"
-proof (unfold the_lub_def)
- from lub_axioms show "The (lub A) = x"
- proof
- fix x' assume lub': "lub A x'"
- show "x' = x"
- proof (rule order_antisym)
- from lub' show "x' \<le> x"
- proof
- fix a assume "a \<in> A"
- then show "a \<le> x" ..
- qed
- show "x \<le> x'"
- proof
- fix a assume "a \<in> A"
- with lub' show "a \<le> x'" ..
+proof -
+ interpret lub [A x] by fact
+ show ?thesis proof (unfold the_lub_def)
+ from `lub A x` show "The (lub A) = x"
+ proof
+ fix x' assume lub': "lub A x'"
+ show "x' = x"
+ proof (rule order_antisym)
+ from lub' show "x' \<le> x"
+ proof
+ fix a assume "a \<in> A"
+ then show "a \<le> x" ..
+ qed
+ show "x \<le> x'"
+ proof
+ fix a assume "a \<in> A"
+ with lub' show "a \<le> x'" ..
+ qed
qed
qed
qed
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Jul 15 16:50:09 2008 +0200
@@ -26,7 +26,8 @@
declare continuous.intro [intro?] continuous_axioms.intro [intro?]
lemma continuousI [intro]:
- includes norm_syntax + linearform
+ fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>")
+ assumes "linearform V f"
assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
shows "continuous V norm f"
proof
@@ -74,6 +75,8 @@
fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
+locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm
+
lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
by (simp add: B_def)
@@ -82,20 +85,11 @@
normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
*}
-(* Alternative statement of the lemma as
- lemma (in fn_norm)
- includes normed_vectorspace + continuous
- shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- is not possible:
- fn_norm contrains parameter norm to type "'a::zero => real",
- normed_vectorspace and continuous contrain this parameter to
- "'a::{minus, plus, zero} => real, which is less general.
-*)
-
-lemma (in normed_vectorspace) fn_norm_works:
- includes fn_norm + continuous
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
+ assumes "continuous V norm f"
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
proof -
+ interpret continuous [V norm f] by fact
txt {* The existence of the supremum is shown using the
completeness of the reals. Completeness means, that every
non-empty bounded set of reals has a supremum. *}
@@ -158,39 +152,40 @@
then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex)
qed
-lemma (in normed_vectorspace) fn_norm_ub [iff?]:
- includes fn_norm + continuous
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
+ assumes "continuous V norm f"
assumes b: "b \<in> B V f"
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
proof -
+ interpret continuous [V norm f] by fact
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- unfolding B_def fn_norm_def
using `continuous V norm f` by (rule fn_norm_works)
from this and b show ?thesis ..
qed
-lemma (in normed_vectorspace) fn_norm_leastB:
- includes fn_norm + continuous
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
+ assumes "continuous V norm f"
assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
proof -
+ interpret continuous [V norm f] by fact
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- unfolding B_def fn_norm_def
using `continuous V norm f` by (rule fn_norm_works)
from this and b show ?thesis ..
qed
text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
-lemma (in normed_vectorspace) fn_norm_ge_zero [iff]:
- includes fn_norm + continuous
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
+ assumes "continuous V norm f"
shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
proof -
+ interpret continuous [V norm f] by fact
txt {* The function norm is defined as the supremum of @{text B}.
So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
0"}, provided the supremum exists and @{text B} is not empty. *}
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
- unfolding B_def fn_norm_def
+(* unfolding B_def fn_norm_def *)
using `continuous V norm f` by (rule fn_norm_works)
moreover have "0 \<in> B V f" ..
ultimately show ?thesis ..
@@ -203,34 +198,37 @@
\end{center}
*}
-lemma (in normed_vectorspace) fn_norm_le_cong:
- includes fn_norm + continuous + linearform
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
+ assumes "continuous V norm f" "linearform V f"
assumes x: "x \<in> V"
shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
-proof cases
- assume "x = 0"
- then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
- also have "f 0 = 0" by rule unfold_locales
- also have "\<bar>\<dots>\<bar> = 0" by simp
- also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
- unfolding B_def fn_norm_def
- using `continuous V norm f` by (rule fn_norm_ge_zero)
- from x have "0 \<le> norm x" ..
- with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
- finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
-next
- assume "x \<noteq> 0"
- with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
- then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
- also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
- proof (rule mult_right_mono)
- from x show "0 \<le> \<parallel>x\<parallel>" ..
- from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
- by (auto simp add: B_def real_divide_def)
- with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
- unfolding B_def fn_norm_def by (rule fn_norm_ub)
+proof -
+ interpret continuous [V norm f] by fact
+ interpret linearform [V f] .
+ show ?thesis proof cases
+ assume "x = 0"
+ then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
+ also have "f 0 = 0" by rule unfold_locales
+ also have "\<bar>\<dots>\<bar> = 0" by simp
+ also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
+ using `continuous V norm f` by (rule fn_norm_ge_zero)
+ from x have "0 \<le> norm x" ..
+ with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
+ finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
+ next
+ assume "x \<noteq> 0"
+ with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
+ then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
+ also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
+ proof (rule mult_right_mono)
+ from x show "0 \<le> \<parallel>x\<parallel>" ..
+ from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
+ by (auto simp add: B_def real_divide_def)
+ with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
+ by (rule fn_norm_ub)
+ qed
+ finally show ?thesis .
qed
- finally show ?thesis .
qed
text {*
@@ -241,35 +239,38 @@
\end{center}
*}
-lemma (in normed_vectorspace) fn_norm_least [intro?]:
- includes fn_norm + continuous
+lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
+ assumes "continuous V norm f"
assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
-proof (rule fn_norm_leastB [folded B_def fn_norm_def])
- fix b assume b: "b \<in> B V f"
- show "b \<le> c"
- proof cases
- assume "b = 0"
- with ge show ?thesis by simp
- next
- assume "b \<noteq> 0"
- with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
+proof -
+ interpret continuous [V norm f] by fact
+ show ?thesis proof (rule fn_norm_leastB [folded B_def fn_norm_def])
+ fix b assume b: "b \<in> B V f"
+ show "b \<le> c"
+ proof cases
+ assume "b = 0"
+ with ge show ?thesis by simp
+ next
+ assume "b \<noteq> 0"
+ with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
and x_neq: "x \<noteq> 0" and x: "x \<in> V"
- by (auto simp add: B_def real_divide_def)
- note b_rep
- also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
- proof (rule mult_right_mono)
- have "0 < \<parallel>x\<parallel>" using x x_neq ..
- then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
- from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+ by (auto simp add: B_def real_divide_def)
+ note b_rep
+ also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
+ proof (rule mult_right_mono)
+ have "0 < \<parallel>x\<parallel>" using x x_neq ..
+ then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
+ from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+ qed
+ also have "\<dots> = c"
+ proof -
+ from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
+ then show ?thesis by simp
+ qed
+ finally show ?thesis .
qed
- also have "\<dots> = c"
- proof -
- from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
- then show ?thesis by simp
- qed
- finally show ?thesis .
- qed
-qed (insert `continuous V norm f`, simp_all add: continuous_def)
+ qed (insert `continuous V norm f`, simp_all add: continuous_def)
+qed
end
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Jul 15 16:50:09 2008 +0200
@@ -53,17 +53,21 @@
*}
theorem HahnBanach:
- includes vectorspace E + subspace F E + seminorm E p + linearform F f
+ assumes E: "vectorspace E" and "subspace F E"
+ and "seminorm E p" and "linearform F f"
assumes fp: "\<forall>x \<in> F. f x \<le> p x"
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)"
-- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *}
-- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *}
-- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *}
proof -
+ interpret vectorspace [E] by fact
+ interpret subspace [F E] by fact
+ interpret seminorm [E p] by fact
+ interpret linearform [F f] by fact
def M \<equiv> "norm_pres_extensions E p F f"
hence M: "M = \<dots>" by (simp only:)
- note E = `vectorspace E`
- then have F: "vectorspace F" ..
+ from E have F: "vectorspace F" ..
note FE = `F \<unlhd> E`
{
fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c"
@@ -306,17 +310,22 @@
*}
theorem abs_HahnBanach:
- includes vectorspace E + subspace F E + linearform F f + seminorm E p
+ assumes E: "vectorspace E" and FE: "subspace F E"
+ and lf: "linearform F f" and sn: "seminorm E p"
assumes fp: "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
shows "\<exists>g. linearform E g
\<and> (\<forall>x \<in> F. g x = f x)
\<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)"
proof -
- note E = `vectorspace E`
+ interpret vectorspace [E] by fact
+ interpret subspace [F E] by fact
+ interpret linearform [F f] by fact
+ interpret seminorm [E p] by fact
+(* note E = `vectorspace E`
note FE = `subspace F E`
note sn = `seminorm E p`
note lf = `linearform F f`
- 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)"
+*) 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)"
using E FE sn lf
proof (rule HahnBanach)
show "\<forall>x \<in> F. f x \<le> p x"
@@ -342,22 +351,31 @@
*}
theorem norm_HahnBanach:
- includes normed_vectorspace E + subspace F E + linearform F f + fn_norm + continuous F norm ("\<parallel>_\<parallel>") f
+ fixes V and norm ("\<parallel>_\<parallel>")
+ 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}"
+ fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
+ defines "\<And>V f. \<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
+ assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
+ and linearform: "linearform F f" and "continuous F norm f"
shows "\<exists>g. linearform E g
\<and> continuous E norm g
\<and> (\<forall>x \<in> F. g x = f x)
\<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
proof -
+ interpret normed_vectorspace [E norm] by fact
+ interpret normed_vectorspace_with_fn_norm [E norm B fn_norm]
+ by (auto simp: B_def fn_norm_def) intro_locales
+ interpret subspace [F E] by fact
+ interpret linearform [F f] by fact
+ interpret continuous [F norm f] by fact
have E: "vectorspace E" by unfold_locales
- have E_norm: "normed_vectorspace E norm" by rule unfold_locales
- note FE = `F \<unlhd> E`
have F: "vectorspace F" by rule unfold_locales
- note linearform = `linearform F f`
have F_norm: "normed_vectorspace F norm"
using FE E_norm by (rule subspace_normed_vs)
have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
- by (rule normed_vectorspace.fn_norm_ge_zero
- [OF F_norm `continuous F norm f`, folded B_def fn_norm_def])
+ by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
+ [OF normed_vectorspace_with_fn_norm.intro,
+ OF F_norm `continuous F norm f` , folded B_def fn_norm_def])
txt {* We define a function @{text p} on @{text E} as follows:
@{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
@@ -406,8 +424,9 @@
fix x assume "x \<in> F"
from this and `continuous F norm f`
show "\<bar>f x\<bar> \<le> p x"
- by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
- [OF F_norm, folded B_def fn_norm_def])
+ by (unfold p_def) (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
+ [OF normed_vectorspace_with_fn_norm.intro,
+ OF F_norm, folded B_def fn_norm_def])
qed
txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
@@ -463,7 +482,9 @@
txt {* The other direction is achieved by a similar argument. *}
show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
- proof (rule normed_vectorspace.fn_norm_least [OF F_norm, folded B_def fn_norm_def])
+ proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
+ [OF normed_vectorspace_with_fn_norm.intro,
+ OF F_norm, folded B_def fn_norm_def])
show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
proof
fix x assume x: "x \<in> F"
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Jul 15 16:50:09 2008 +0200
@@ -40,10 +40,11 @@
*}
lemma ex_xi:
- includes vectorspace F
+ assumes "vectorspace F"
assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
proof -
+ interpret vectorspace [F] by fact
txt {* From the completeness of the reals follows:
The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
non-empty and has an upper bound. *}
@@ -86,183 +87,190 @@
*}
lemma h'_lf:
- includes var H + var h + var E
assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
and H'_def: "H' \<equiv> H + lin x0"
and HE: "H \<unlhd> E"
- includes linearform H h
+ assumes "linearform H h"
assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
- includes vectorspace E
+ assumes E: "vectorspace E"
shows "linearform H' h'"
-proof
- note E = `vectorspace E`
- have H': "vectorspace H'"
- proof (unfold H'_def)
- from `x0 \<in> E`
- have "lin x0 \<unlhd> E" ..
- with HE show "vectorspace (H + lin x0)" using E ..
- qed
- {
- fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
- show "h' (x1 + x2) = h' x1 + h' x2"
- proof -
- from H' x1 x2 have "x1 + x2 \<in> H'"
- by (rule vectorspace.add_closed)
- with x1 x2 obtain y y1 y2 a a1 a2 where
- x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
+proof -
+ interpret linearform [H h] by fact
+ interpret vectorspace [E] by fact
+ show ?thesis proof
+ note E = `vectorspace E`
+ have H': "vectorspace H'"
+ proof (unfold H'_def)
+ from `x0 \<in> E`
+ have "lin x0 \<unlhd> E" ..
+ with HE show "vectorspace (H + lin x0)" using E ..
+ qed
+ {
+ fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
+ show "h' (x1 + x2) = h' x1 + h' x2"
+ proof -
+ from H' x1 x2 have "x1 + x2 \<in> H'"
+ by (rule vectorspace.add_closed)
+ with x1 x2 obtain y y1 y2 a a1 a2 where
+ x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
- by (unfold H'_def sum_def lin_def) blast
-
- have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
- proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
- from HE y1 y2 show "y1 + y2 \<in> H"
- by (rule subspace.add_closed)
- from x0 and HE y y1 y2
- have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto
- with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
- by (simp add: add_ac add_mult_distrib2)
- also note x1x2
- finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
+ by (unfold H'_def sum_def lin_def) blast
+
+ have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
+ proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
+ from HE y1 y2 show "y1 + y2 \<in> H"
+ by (rule subspace.add_closed)
+ from x0 and HE y y1 y2
+ have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto
+ with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
+ by (simp add: add_ac add_mult_distrib2)
+ also note x1x2
+ finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
+ qed
+
+ from h'_def x1x2 E HE y x0
+ have "h' (x1 + x2) = h y + a * xi"
+ by (rule h'_definite)
+ also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
+ by (simp only: ya)
+ also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
+ by simp
+ also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
+ by (simp add: left_distrib)
+ also from h'_def x1_rep E HE y1 x0
+ have "h y1 + a1 * xi = h' x1"
+ by (rule h'_definite [symmetric])
+ also from h'_def x2_rep E HE y2 x0
+ have "h y2 + a2 * xi = h' x2"
+ by (rule h'_definite [symmetric])
+ finally show ?thesis .
qed
-
- from h'_def x1x2 E HE y x0
- have "h' (x1 + x2) = h y + a * xi"
- by (rule h'_definite)
- also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
- by (simp only: ya)
- also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
- by simp
- also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
- by (simp add: left_distrib)
- also from h'_def x1_rep E HE y1 x0
- have "h y1 + a1 * xi = h' x1"
- by (rule h'_definite [symmetric])
- also from h'_def x2_rep E HE y2 x0
- have "h y2 + a2 * xi = h' x2"
- by (rule h'_definite [symmetric])
- finally show ?thesis .
- qed
- next
- fix x1 c assume x1: "x1 \<in> H'"
- show "h' (c \<cdot> x1) = c * (h' x1)"
- proof -
- from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
- by (rule vectorspace.mult_closed)
- with x1 obtain y a y1 a1 where
- cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
+ next
+ fix x1 c assume x1: "x1 \<in> H'"
+ show "h' (c \<cdot> x1) = c * (h' x1)"
+ proof -
+ from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
+ by (rule vectorspace.mult_closed)
+ with x1 obtain y a y1 a1 where
+ cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
- by (unfold H'_def sum_def lin_def) blast
-
- have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
- proof (rule decomp_H')
- from HE y1 show "c \<cdot> y1 \<in> H"
- by (rule subspace.mult_closed)
- from x0 and HE y y1
- have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto
- with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
- by (simp add: mult_assoc add_mult_distrib1)
- also note cx1_rep
- finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
+ by (unfold H'_def sum_def lin_def) blast
+
+ have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
+ proof (rule decomp_H')
+ from HE y1 show "c \<cdot> y1 \<in> H"
+ by (rule subspace.mult_closed)
+ from x0 and HE y y1
+ have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto
+ with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
+ by (simp add: mult_assoc add_mult_distrib1)
+ also note cx1_rep
+ finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
+ qed
+
+ from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
+ by (rule h'_definite)
+ also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
+ by (simp only: ya)
+ also from y1 have "h (c \<cdot> y1) = c * h y1"
+ by simp
+ also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
+ by (simp only: right_distrib)
+ also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
+ by (rule h'_definite [symmetric])
+ finally show ?thesis .
qed
-
- from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
- by (rule h'_definite)
- also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
- by (simp only: ya)
- also from y1 have "h (c \<cdot> y1) = c * h y1"
- by simp
- also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
- by (simp only: right_distrib)
- also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
- by (rule h'_definite [symmetric])
- finally show ?thesis .
- qed
- }
+ }
+ qed
qed
text {* \medskip The linear extension @{text h'} of @{text h}
is bounded by the seminorm @{text p}. *}
lemma h'_norm_pres:
- includes var H + var h + var E
assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
and H'_def: "H' \<equiv> H + lin x0"
and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
- includes vectorspace E + subspace H E + seminorm E p + linearform H h
+ assumes E: "vectorspace E" and HE: "subspace H E"
+ and "seminorm E p" and "linearform H h"
assumes a: "\<forall>y \<in> H. h y \<le> p y"
and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
shows "\<forall>x \<in> H'. h' x \<le> p x"
-proof
- note E = `vectorspace E`
- note HE = `subspace H E`
- fix x assume x': "x \<in> H'"
- show "h' x \<le> p x"
- proof -
- from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
- and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
- from x' obtain y a where
+proof -
+ interpret vectorspace [E] by fact
+ interpret subspace [H E] by fact
+ interpret seminorm [E p] by fact
+ interpret linearform [H h] by fact
+ show ?thesis proof
+ fix x assume x': "x \<in> H'"
+ show "h' x \<le> p x"
+ proof -
+ from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
+ and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
+ from x' obtain y a where
x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
- by (unfold H'_def sum_def lin_def) blast
- from y have y': "y \<in> E" ..
- from y have ay: "inverse a \<cdot> y \<in> H" by simp
-
- from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
- by (rule h'_definite)
- also have "\<dots> \<le> p (y + a \<cdot> x0)"
- proof (rule linorder_cases)
- assume z: "a = 0"
- then have "h y + a * xi = h y" by simp
- also from a y have "\<dots> \<le> p y" ..
- also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
- finally show ?thesis .
- next
- txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
- with @{text ya} taken as @{text "y / a"}: *}
- assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
- from a1 ay
- have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
- with lz have "a * xi \<le>
+ by (unfold H'_def sum_def lin_def) blast
+ from y have y': "y \<in> E" ..
+ from y have ay: "inverse a \<cdot> y \<in> H" by simp
+
+ from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
+ by (rule h'_definite)
+ also have "\<dots> \<le> p (y + a \<cdot> x0)"
+ proof (rule linorder_cases)
+ assume z: "a = 0"
+ then have "h y + a * xi = h y" by simp
+ also from a y have "\<dots> \<le> p y" ..
+ also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
+ finally show ?thesis .
+ next
+ txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
+ with @{text ya} taken as @{text "y / a"}: *}
+ assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
+ from a1 ay
+ have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
+ with lz have "a * xi \<le>
a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
- by (simp add: mult_left_mono_neg order_less_imp_le)
-
- also have "\<dots> =
+ by (simp add: mult_left_mono_neg order_less_imp_le)
+
+ also have "\<dots> =
- a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
- by (simp add: right_diff_distrib)
- also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
+ by (simp add: right_diff_distrib)
+ also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
p (a \<cdot> (inverse a \<cdot> y + x0))"
- by (simp add: abs_homogenous)
- also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
- by (simp add: add_mult_distrib1 mult_assoc [symmetric])
- also from nz y have "a * (h (inverse a \<cdot> y)) = h y"
- by simp
- finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
- then show ?thesis by simp
- next
- txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
- with @{text ya} taken as @{text "y / a"}: *}
- assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
- from a2 ay
- have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
- with gz have "a * xi \<le>
+ by (simp add: abs_homogenous)
+ also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
+ by (simp add: add_mult_distrib1 mult_assoc [symmetric])
+ also from nz y have "a * (h (inverse a \<cdot> y)) = h y"
+ by simp
+ finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
+ then show ?thesis by simp
+ next
+ txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
+ with @{text ya} taken as @{text "y / a"}: *}
+ assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
+ from a2 ay
+ have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
+ with gz have "a * xi \<le>
a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
- by simp
- also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
- by (simp add: right_diff_distrib)
- also from gz x0 y'
- have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
- by (simp add: abs_homogenous)
- also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
- by (simp add: add_mult_distrib1 mult_assoc [symmetric])
- also from nz y have "a * h (inverse a \<cdot> y) = h y"
- by simp
- finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
- then show ?thesis by simp
+ by simp
+ also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
+ by (simp add: right_diff_distrib)
+ also from gz x0 y'
+ have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
+ by (simp add: abs_homogenous)
+ also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
+ by (simp add: add_mult_distrib1 mult_assoc [symmetric])
+ also from nz y have "a * h (inverse a \<cdot> y) = h y"
+ by simp
+ finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
+ then show ?thesis by simp
+ qed
+ also from x_rep have "\<dots> = p x" by (simp only:)
+ finally show ?thesis .
qed
- also from x_rep have "\<dots> = p x" by (simp only:)
- finally show ?thesis .
qed
qed
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Tue Jul 15 16:50:09 2008 +0200
@@ -399,9 +399,14 @@
*}
lemma abs_ineq_iff:
- includes subspace H E + vectorspace E + seminorm E p + linearform H h
+ assumes "subspace H E" and "vectorspace E" and "seminorm E p"
+ and "linearform H h"
shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
proof
+ interpret subspace [H E] by fact
+ interpret vectorspace [E] by fact
+ interpret seminorm [E p] by fact
+ interpret linearform [H h] by fact
have H: "vectorspace H" using `vectorspace E` ..
{
assume l: ?L
--- a/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 16:50:09 2008 +0200
@@ -20,9 +20,10 @@
declare linearform.intro [intro?]
lemma (in linearform) neg [iff]:
- includes vectorspace
+ assumes "vectorspace V"
shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
proof -
+ interpret vectorspace [V] by fact
assume x: "x \<in> V"
hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
also from x have "... = (- 1) * (f x)" by (rule mult)
@@ -31,9 +32,10 @@
qed
lemma (in linearform) diff [iff]:
- includes vectorspace
+ assumes "vectorspace V"
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
proof -
+ interpret vectorspace [V] by fact
assume x: "x \<in> V" and y: "y \<in> V"
hence "x - y = x + - y" by (rule diff_eq1)
also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)
@@ -44,9 +46,10 @@
text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
lemma (in linearform) zero [iff]:
- includes vectorspace
+ assumes "vectorspace V"
shows "f 0 = 0"
proof -
+ interpret vectorspace [V] by fact
have "f 0 = f (0 - 0)" by simp
also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
also have "\<dots> = 0" by simp
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Tue Jul 15 16:50:09 2008 +0200
@@ -27,9 +27,10 @@
declare seminorm.intro [intro?]
lemma (in seminorm) diff_subadditive:
- includes vectorspace
+ assumes "vectorspace V"
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
proof -
+ interpret vectorspace [V] by fact
assume x: "x \<in> V" and y: "y \<in> V"
hence "x - y = x + - 1 \<cdot> y"
by (simp add: diff_eq2 negate_eq2a)
@@ -42,9 +43,10 @@
qed
lemma (in seminorm) minus:
- includes vectorspace
+ assumes "vectorspace V"
shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
proof -
+ interpret vectorspace [V] by fact
assume x: "x \<in> V"
hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
@@ -95,14 +97,19 @@
*}
lemma subspace_normed_vs [intro?]:
- includes subspace F E + normed_vectorspace E
+ fixes F E norm
+ assumes "subspace F E" "normed_vectorspace E norm"
shows "normed_vectorspace F norm"
-proof
- show "vectorspace F" by (rule vectorspace) unfold_locales
-next
- have "NormedSpace.norm E norm" by unfold_locales
- with subset show "NormedSpace.norm F norm"
- by (simp add: norm_def seminorm_def norm_axioms_def)
+proof -
+ interpret subspace [F E] by fact
+ interpret normed_vectorspace [E norm] by fact
+ show ?thesis proof
+ show "vectorspace F" by (rule vectorspace) unfold_locales
+ next
+ have "NormedSpace.norm E norm" by unfold_locales
+ with subset show "NormedSpace.norm F norm"
+ by (simp add: norm_def seminorm_def norm_axioms_def)
+ qed
qed
end
--- a/src/HOL/Real/HahnBanach/Subspace.thy Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Tue Jul 15 16:50:09 2008 +0200
@@ -41,10 +41,12 @@
by (rule subspace.subsetD)
lemma (in subspace) diff_closed [iff]:
- includes vectorspace
- shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U"
- by (simp add: diff_eq1 negate_eq1)
-
+ assumes "vectorspace V"
+ shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U" (is "PROP ?P")
+proof -
+ interpret vectorspace [V] by fact
+ show "PROP ?P" by (simp add: diff_eq1 negate_eq1)
+qed
text {*
\medskip Similar as for linear spaces, the existence of the zero
@@ -53,9 +55,10 @@
*}
lemma (in subspace) zero [intro]:
- includes vectorspace
+ assumes "vectorspace V"
shows "0 \<in> U"
proof -
+ interpret vectorspace [V] by fact
have "U \<noteq> {}" by (rule U_V.non_empty)
then obtain x where x: "x \<in> U" by blast
hence "x \<in> V" .. hence "0 = x - x" by simp
@@ -64,32 +67,37 @@
qed
lemma (in subspace) neg_closed [iff]:
- includes vectorspace
- shows "x \<in> U \<Longrightarrow> - x \<in> U"
- by (simp add: negate_eq1)
-
+ assumes "vectorspace V"
+ shows "x \<in> U \<Longrightarrow> - x \<in> U" (is "PROP ?P")
+proof -
+ interpret vectorspace [V] by fact
+ show "PROP ?P" by (simp add: negate_eq1)
+qed
text {* \medskip Further derived laws: every subspace is a vector space. *}
lemma (in subspace) vectorspace [iff]:
- includes vectorspace
+ assumes "vectorspace V"
shows "vectorspace U"
-proof
- show "U \<noteq> {}" ..
- fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
- fix a b :: real
- from x y show "x + y \<in> U" by simp
- from x show "a \<cdot> x \<in> U" by simp
- from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)
- from x y show "x + y = y + x" by (simp add: add_ac)
- from x show "x - x = 0" by simp
- from x show "0 + x = x" by simp
- from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib)
- from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib)
- from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc)
- from x show "1 \<cdot> x = x" by simp
- from x show "- x = - 1 \<cdot> x" by (simp add: negate_eq1)
- from x y show "x - y = x + - y" by (simp add: diff_eq1)
+proof -
+ interpret vectorspace [V] by fact
+ show ?thesis proof
+ show "U \<noteq> {}" ..
+ fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
+ fix a b :: real
+ from x y show "x + y \<in> U" by simp
+ from x show "a \<cdot> x \<in> U" by simp
+ from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)
+ from x y show "x + y = y + x" by (simp add: add_ac)
+ from x show "x - x = 0" by simp
+ from x show "0 + x = x" by simp
+ from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib)
+ from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib)
+ from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc)
+ from x show "1 \<cdot> x = x" by simp
+ from x show "- x = - 1 \<cdot> x" by (simp add: negate_eq1)
+ from x y show "x - y = x + - y" by (simp add: diff_eq1)
+ qed
qed
@@ -236,61 +244,70 @@
text {* @{text U} is a subspace of @{text "U + V"}. *}
lemma subspace_sum1 [iff]:
- includes vectorspace U + vectorspace V
+ assumes "vectorspace U" "vectorspace V"
shows "U \<unlhd> U + V"
-proof
- show "U \<noteq> {}" ..
- show "U \<subseteq> U + V"
- proof
- fix x assume x: "x \<in> U"
- moreover have "0 \<in> V" ..
- ultimately have "x + 0 \<in> U + V" ..
- with x show "x \<in> U + V" by simp
+proof -
+ interpret vectorspace [U] by fact
+ interpret vectorspace [V] by fact
+ show ?thesis proof
+ show "U \<noteq> {}" ..
+ show "U \<subseteq> U + V"
+ proof
+ fix x assume x: "x \<in> U"
+ moreover have "0 \<in> V" ..
+ ultimately have "x + 0 \<in> U + V" ..
+ with x show "x \<in> U + V" by simp
+ qed
+ fix x y assume x: "x \<in> U" and "y \<in> U"
+ thus "x + y \<in> U" by simp
+ from x show "\<And>a. a \<cdot> x \<in> U" by simp
qed
- fix x y assume x: "x \<in> U" and "y \<in> U"
- thus "x + y \<in> U" by simp
- from x show "\<And>a. a \<cdot> x \<in> U" by simp
qed
text {* The sum of two subspaces is again a subspace. *}
lemma sum_subspace [intro?]:
- includes subspace U E + vectorspace E + subspace V E
+ assumes "subspace U E" "vectorspace E" "subspace V E"
shows "U + V \<unlhd> E"
-proof
- have "0 \<in> U + V"
- proof
- show "0 \<in> U" using `vectorspace E` ..
- show "0 \<in> V" using `vectorspace E` ..
- show "(0::'a) = 0 + 0" by simp
- qed
- thus "U + V \<noteq> {}" by blast
- show "U + V \<subseteq> E"
- proof
- fix x assume "x \<in> U + V"
- then obtain u v where "x = u + v" and
- "u \<in> U" and "v \<in> V" ..
- then show "x \<in> E" by simp
- qed
- fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
- show "x + y \<in> U + V"
- proof -
- from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
- moreover
- from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" ..
- ultimately
- have "ux + uy \<in> U"
- and "vx + vy \<in> V"
- and "x + y = (ux + uy) + (vx + vy)"
- using x y by (simp_all add: add_ac)
- thus ?thesis ..
- qed
- fix a show "a \<cdot> x \<in> U + V"
- proof -
- from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
- hence "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
- and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)
- thus ?thesis ..
+proof -
+ interpret subspace [U E] by fact
+ interpret vectorspace [E] by fact
+ interpret subspace [V E] by fact
+ show ?thesis proof
+ have "0 \<in> U + V"
+ proof
+ show "0 \<in> U" using `vectorspace E` ..
+ show "0 \<in> V" using `vectorspace E` ..
+ show "(0::'a) = 0 + 0" by simp
+ qed
+ thus "U + V \<noteq> {}" by blast
+ show "U + V \<subseteq> E"
+ proof
+ fix x assume "x \<in> U + V"
+ then obtain u v where "x = u + v" and
+ "u \<in> U" and "v \<in> V" ..
+ then show "x \<in> E" by simp
+ qed
+ fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
+ show "x + y \<in> U + V"
+ proof -
+ from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
+ moreover
+ from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" ..
+ ultimately
+ have "ux + uy \<in> U"
+ and "vx + vy \<in> V"
+ and "x + y = (ux + uy) + (vx + vy)"
+ using x y by (simp_all add: add_ac)
+ thus ?thesis ..
+ qed
+ fix a show "a \<cdot> x \<in> U + V"
+ proof -
+ from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
+ hence "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
+ and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)
+ thus ?thesis ..
+ qed
qed
qed
@@ -312,37 +329,42 @@
*}
lemma decomp:
- includes vectorspace E + subspace U E + subspace V E
+ assumes "vectorspace E" "subspace U E" "subspace V E"
assumes direct: "U \<inter> V = {0}"
and u1: "u1 \<in> U" and u2: "u2 \<in> U"
and v1: "v1 \<in> V" and v2: "v2 \<in> V"
and sum: "u1 + v1 = u2 + v2"
shows "u1 = u2 \<and> v1 = v2"
-proof
- have U: "vectorspace U"
- using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
- have V: "vectorspace V"
- using `subspace V E` `vectorspace E` by (rule subspace.vectorspace)
- from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
- by (simp add: add_diff_swap)
- from u1 u2 have u: "u1 - u2 \<in> U"
- by (rule vectorspace.diff_closed [OF U])
- with eq have v': "v2 - v1 \<in> U" by (simp only:)
- from v2 v1 have v: "v2 - v1 \<in> V"
- by (rule vectorspace.diff_closed [OF V])
- with eq have u': " u1 - u2 \<in> V" by (simp only:)
-
- show "u1 = u2"
- proof (rule add_minus_eq)
- from u1 show "u1 \<in> E" ..
- from u2 show "u2 \<in> E" ..
- from u u' and direct show "u1 - u2 = 0" by blast
- qed
- show "v1 = v2"
- proof (rule add_minus_eq [symmetric])
- from v1 show "v1 \<in> E" ..
- from v2 show "v2 \<in> E" ..
- from v v' and direct show "v2 - v1 = 0" by blast
+proof -
+ interpret vectorspace [E] by fact
+ interpret subspace [U E] by fact
+ interpret subspace [V E] by fact
+ show ?thesis proof
+ have U: "vectorspace U" (* FIXME: use interpret *)
+ using `subspace U E` `vectorspace E` by (rule subspace.vectorspace)
+ have V: "vectorspace V"
+ using `subspace V E` `vectorspace E` by (rule subspace.vectorspace)
+ from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
+ by (simp add: add_diff_swap)
+ from u1 u2 have u: "u1 - u2 \<in> U"
+ by (rule vectorspace.diff_closed [OF U])
+ with eq have v': "v2 - v1 \<in> U" by (simp only:)
+ from v2 v1 have v: "v2 - v1 \<in> V"
+ by (rule vectorspace.diff_closed [OF V])
+ with eq have u': " u1 - u2 \<in> V" by (simp only:)
+
+ show "u1 = u2"
+ proof (rule add_minus_eq)
+ from u1 show "u1 \<in> E" ..
+ from u2 show "u2 \<in> E" ..
+ from u u' and direct show "u1 - u2 = 0" by blast
+ qed
+ show "v1 = v2"
+ proof (rule add_minus_eq [symmetric])
+ from v1 show "v1 \<in> E" ..
+ from v2 show "v2 \<in> E" ..
+ from v v' and direct show "v2 - v1 = 0" by blast
+ qed
qed
qed
@@ -356,48 +378,52 @@
*}
lemma decomp_H':
- includes vectorspace E + subspace H E
+ assumes "vectorspace E" "subspace H E"
assumes y1: "y1 \<in> H" and y2: "y2 \<in> H"
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
shows "y1 = y2 \<and> a1 = a2"
-proof
- have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
- proof (rule decomp)
- show "a1 \<cdot> x' \<in> lin x'" ..
- show "a2 \<cdot> x' \<in> lin x'" ..
- show "H \<inter> lin x' = {0}"
- proof
- show "H \<inter> lin x' \<subseteq> {0}"
+proof -
+ interpret vectorspace [E] by fact
+ interpret subspace [H E] by fact
+ show ?thesis proof
+ have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
+ proof (rule decomp)
+ show "a1 \<cdot> x' \<in> lin x'" ..
+ show "a2 \<cdot> x' \<in> lin x'" ..
+ show "H \<inter> lin x' = {0}"
proof
- fix x assume x: "x \<in> H \<inter> lin x'"
- then obtain a where xx': "x = a \<cdot> x'"
- by blast
- have "x = 0"
- proof cases
- assume "a = 0"
- with xx' and x' show ?thesis by simp
- next
- assume a: "a \<noteq> 0"
- from x have "x \<in> H" ..
- with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
- with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
- with `x' \<notin> H` show ?thesis by contradiction
- qed
- thus "x \<in> {0}" ..
+ show "H \<inter> lin x' \<subseteq> {0}"
+ proof
+ fix x assume x: "x \<in> H \<inter> lin x'"
+ then obtain a where xx': "x = a \<cdot> x'"
+ by blast
+ have "x = 0"
+ proof cases
+ assume "a = 0"
+ with xx' and x' show ?thesis by simp
+ next
+ assume a: "a \<noteq> 0"
+ from x have "x \<in> H" ..
+ with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
+ with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
+ with `x' \<notin> H` show ?thesis by contradiction
+ qed
+ thus "x \<in> {0}" ..
+ qed
+ show "{0} \<subseteq> H \<inter> lin x'"
+ proof -
+ have "0 \<in> H" using `vectorspace E` ..
+ moreover have "0 \<in> lin x'" using `x' \<in> E` ..
+ ultimately show ?thesis by blast
+ qed
qed
- show "{0} \<subseteq> H \<inter> lin x'"
- proof -
- have "0 \<in> H" using `vectorspace E` ..
- moreover have "0 \<in> lin x'" using `x' \<in> E` ..
- ultimately show ?thesis by blast
- qed
- qed
- show "lin x' \<unlhd> E" using `x' \<in> E` ..
- qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
- thus "y1 = y2" ..
- from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
- with x' show "a1 = a2" by (simp add: mult_right_cancel)
+ show "lin x' \<unlhd> E" using `x' \<in> E` ..
+ qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq)
+ thus "y1 = y2" ..
+ from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
+ with x' show "a1 = a2" by (simp add: mult_right_cancel)
+ qed
qed
text {*
@@ -408,19 +434,23 @@
*}
lemma decomp_H'_H:
- includes vectorspace E + subspace H E
+ assumes "vectorspace E" "subspace H E"
assumes t: "t \<in> H"
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
-proof (rule, simp_all only: split_paired_all split_conv)
- from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
- fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"
- have "y = t \<and> a = 0"
- proof (rule decomp_H')
- from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
- from ya show "y \<in> H" ..
- qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
- with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
+proof -
+ interpret vectorspace [E] by fact
+ interpret subspace [H E] by fact
+ show ?thesis proof (rule, simp_all only: split_paired_all split_conv)
+ from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
+ fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"
+ have "y = t \<and> a = 0"
+ proof (rule decomp_H')
+ from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
+ from ya show "y \<in> H" ..
+ qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+)
+ with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
+ qed
qed
text {*
@@ -430,16 +460,18 @@
*}
lemma h'_definite:
- includes var H
+ fixes H
assumes h'_def:
"h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
in (h y) + a * xi)"
and x: "x = y + a \<cdot> x'"
- includes vectorspace E + subspace H E
+ assumes "vectorspace E" "subspace H E"
assumes y: "y \<in> H"
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
shows "h' x = h y + a * xi"
proof -
+ interpret vectorspace [E] by fact
+ interpret subspace [H E] by fact
from x y x' have "x \<in> H + lin x'" by auto
have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
proof (rule ex_ex1I)