--- a/src/HOL/Algebra/Bij.thy Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/Bij.thy Fri Apr 23 21:46:04 2004 +0200
@@ -3,41 +3,41 @@
Author: Florian Kammueller, with new proofs by L C Paulson
*)
-
-header{*Bijections of a Set, Permutation Groups, Automorphism Groups*}
+header {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
theory Bij = Group:
constdefs
- Bij :: "'a set => (('a => 'a)set)"
+ Bij :: "'a set => ('a => 'a) set"
--{*Only extensional functions, since otherwise we get too many.*}
- "Bij S == extensional S \<inter> {f. f`S = S & inj_on f S}"
+ "Bij S == extensional S \<inter> {f. f`S = S & inj_on f S}"
- BijGroup :: "'a set => (('a => 'a) monoid)"
- "BijGroup S == (| carrier = Bij S,
- mult = %g: Bij S. %f: Bij S. compose S g f,
- one = %x: S. x |)"
+ BijGroup :: "'a set => ('a => 'a) monoid"
+ "BijGroup S ==
+ (| carrier = Bij S,
+ mult = %g: Bij S. %f: Bij S. compose S g f,
+ one = %x: S. x |)"
declare Id_compose [simp] compose_Id [simp]
lemma Bij_imp_extensional: "f \<in> Bij S ==> f \<in> extensional S"
-by (simp add: Bij_def)
+ by (simp add: Bij_def)
lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S"
-by (auto simp add: Bij_def Pi_def)
+ by (auto simp add: Bij_def Pi_def)
lemma Bij_imp_apply: "f \<in> Bij S ==> f ` S = S"
-by (simp add: Bij_def)
+ by (simp add: Bij_def)
lemma Bij_imp_inj_on: "f \<in> Bij S ==> inj_on f S"
-by (simp add: Bij_def)
+ by (simp add: Bij_def)
lemma BijI: "[| f \<in> extensional(S); f`S = S; inj_on f S |] ==> f \<in> Bij S"
-by (simp add: Bij_def)
+ by (simp add: Bij_def)
-subsection{*Bijections Form a Group*}
+subsection {*Bijections Form a Group *}
lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S"
apply (simp add: Bij_def)
@@ -60,7 +60,7 @@
lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S"
apply (rule BijI)
- apply (simp add: compose_extensional)
+ apply (simp add: compose_extensional)
apply (blast del: equalityI
intro: surj_compose dest: Bij_imp_apply Bij_imp_inj_on)
apply (blast intro: inj_on_compose dest: Bij_imp_apply Bij_imp_inj_on)
@@ -70,44 +70,44 @@
"f \<in> Bij S ==> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
apply (rule compose_Inv_id)
apply (simp add: Bij_imp_inj_on)
-apply (simp add: Bij_imp_apply)
+apply (simp add: Bij_imp_apply)
done
theorem group_BijGroup: "group (BijGroup S)"
-apply (simp add: BijGroup_def)
+apply (simp add: BijGroup_def)
apply (rule groupI)
apply (simp add: compose_Bij)
apply (simp add: id_Bij)
apply (simp add: compose_Bij)
apply (blast intro: compose_assoc [symmetric] Bij_imp_funcset)
apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
-apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij)
+apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij)
done
subsection{*Automorphisms Form a Group*}
lemma Bij_Inv_mem: "[| f \<in> Bij S; x : S |] ==> Inv S f x : S"
-by (simp add: Bij_def Inv_mem)
+by (simp add: Bij_def Inv_mem)
lemma Bij_Inv_lemma:
assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)"
- shows "[| h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S |]
+ shows "[| h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S |]
==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
-apply (simp add: Bij_def)
+apply (simp add: Bij_def)
apply (subgoal_tac "EX x':S. EX y':S. x = h x' & y = h y'", clarify)
apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast)
done
constdefs
- auto :: "('a,'b) monoid_scheme => ('a => 'a)set"
+ auto :: "('a, 'b) monoid_scheme => ('a => 'a) set"
"auto G == hom G G \<inter> Bij (carrier G)"
- AutoGroup :: "[('a,'c) monoid_scheme] => ('a=>'a) monoid"
+ AutoGroup :: "('a, 'c) monoid_scheme => ('a => 'a) monoid"
"AutoGroup G == BijGroup (carrier G) (|carrier := auto G |)"
lemma id_in_auto: "group G ==> (%x: carrier G. x) \<in> auto G"
- by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
+ by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
lemma mult_funcset: "group G ==> mult G \<in> carrier G -> carrier G -> carrier G"
by (simp add: Pi_I group.axioms)
@@ -122,27 +122,26 @@
"f \<in> Bij S ==> m_inv (BijGroup S) f = (%x: S. (Inv S f) x)"
apply (rule group.inv_equality)
apply (rule group_BijGroup)
-apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
+apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
done
lemma subgroup_auto:
"group G ==> subgroup (auto G) (BijGroup (carrier G))"
-apply (rule group.subgroupI)
- apply (rule group_BijGroup)
- apply (force simp add: auto_def BijGroup_def)
- apply (blast intro: dest: id_in_auto)
+apply (rule group.subgroupI)
+ apply (rule group_BijGroup)
+ apply (force simp add: auto_def BijGroup_def)
+ apply (blast intro: dest: id_in_auto)
apply (simp del: restrict_apply
- add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
+ add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
apply (simp add: BijGroup_def auto_def Bij_imp_funcset compose_hom compose_Bij)
done
theorem AutoGroup: "group G ==> group (AutoGroup G)"
-apply (simp add: AutoGroup_def)
+apply (simp add: AutoGroup_def)
apply (rule Group.subgroup.groupI)
-apply (erule subgroup_auto)
-apply (insert Bij.group_BijGroup [of "carrier G"])
-apply (simp_all add: group_def)
+apply (erule subgroup_auto)
+apply (insert Bij.group_BijGroup [of "carrier G"])
+apply (simp_all add: group_def)
done
end
-
--- a/src/HOL/Algebra/CRing.thy Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/CRing.thy Fri Apr 23 21:46:04 2004 +0200
@@ -189,13 +189,13 @@
syntax
"_finsum" :: "index => idt => 'a set => 'b => 'b"
- ("\<Oplus>__:_. _" [1000, 0, 51, 10] 10)
+ ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
syntax (xsymbols)
"_finsum" :: "index => idt => 'a set => 'b => 'b"
- ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+ ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
syntax (HTML output)
"_finsum" :: "index => idt => 'a set => 'b => 'b"
- ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+ ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
translations
"\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A" -- {* Beware of argument permutation! *}
--- a/src/HOL/Algebra/Coset.thy Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy Fri Apr 23 21:46:04 2004 +0200
@@ -7,26 +7,26 @@
theory Coset = Group + Exponent:
-declare (in group) l_inv [simp] r_inv [simp]
+declare (in group) l_inv [simp] and r_inv [simp]
constdefs (structure G)
- r_coset :: "[_,'a set, 'a] => 'a set"
- "r_coset G H a == (% x. x \<otimes> a) ` H"
+ r_coset :: "[_,'a set, 'a] => 'a set"
+ "r_coset G H a == (% x. x \<otimes> a) ` H"
l_coset :: "[_, 'a, 'a set] => 'a set"
- "l_coset G a H == (% x. a \<otimes> x) ` H"
+ "l_coset G a H == (% x. a \<otimes> x) ` H"
rcosets :: "[_, 'a set] => ('a set)set"
- "rcosets G H == r_coset G H ` (carrier G)"
+ "rcosets G H == r_coset G H ` (carrier G)"
set_mult :: "[_, 'a set ,'a set] => 'a set"
- "set_mult G H K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
+ "set_mult G H K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
set_inv :: "[_,'a set] => 'a set"
- "set_inv G H == m_inv G ` H"
+ "set_inv G H == m_inv G ` H"
normal :: "['a set, _] => bool" (infixl "<|" 60)
- "normal H G == subgroup H G &
+ "normal H G == subgroup H G &
(\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
syntax (xsymbols)
@@ -56,13 +56,13 @@
apply (auto simp add: Pi_def)
done
-lemma card_bij:
- "[|f \<in> A\<rightarrow>B; inj_on f A;
+lemma card_bij:
+ "[|f \<in> A\<rightarrow>B; inj_on f A;
g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
-by (blast intro: card_inj order_antisym)
+by (blast intro: card_inj order_antisym)
-subsection{*Lemmas Using Locale Constants*}
+subsection {*Lemmas Using *}
lemma (in coset) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
by (auto simp add: rcos_def r_coset_def)
@@ -77,7 +77,7 @@
by (simp add: setmult_def set_mult_def image_def)
lemma (in coset) coset_mult_assoc:
- "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
+ "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
==> (M #> g) #> h = M #> (g \<otimes> h)"
by (force simp add: r_coset_eq m_assoc)
@@ -85,14 +85,14 @@
by (force simp add: r_coset_eq)
lemma (in coset) coset_mult_inv1:
- "[| M #> (x \<otimes> (inv y)) = M; x \<in> carrier G ; y \<in> carrier G;
+ "[| M #> (x \<otimes> (inv y)) = M; x \<in> carrier G ; y \<in> carrier G;
M <= carrier G |] ==> M #> x = M #> y"
apply (erule subst [of concl: "%z. M #> x = z #> y"])
apply (simp add: coset_mult_assoc m_assoc)
done
lemma (in coset) coset_mult_inv2:
- "[| M #> x = M #> y; x \<in> carrier G; y \<in> carrier G; M <= carrier G |]
+ "[| M #> x = M #> y; x \<in> carrier G; y \<in> carrier G; M <= carrier G |]
==> M #> (x \<otimes> (inv y)) = M "
apply (simp add: coset_mult_assoc [symmetric])
apply (simp add: coset_mult_assoc)
@@ -110,7 +110,7 @@
lemma (in coset) solve_equation:
"\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<otimes> x = y"
apply (rule bexI [of _ "y \<otimes> (inv x)"])
-apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
+apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
subgroup.subset [THEN subsetD])
done
@@ -133,30 +133,30 @@
text{*Really needed?*}
lemma (in coset) transpose_inv:
- "[| x \<otimes> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
+ "[| x \<otimes> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
==> (inv x) \<otimes> z = y"
by (force simp add: m_assoc [symmetric])
lemma (in coset) repr_independence:
"[| y \<in> H #> x; x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y"
-by (auto simp add: r_coset_eq m_assoc [symmetric]
+by (auto simp add: r_coset_eq m_assoc [symmetric]
subgroup.subset [THEN subsetD]
subgroup.m_closed solve_equation)
lemma (in coset) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
apply (simp add: r_coset_eq)
-apply (blast intro: l_one subgroup.subset [THEN subsetD]
+apply (blast intro: l_one subgroup.subset [THEN subsetD]
subgroup.one_closed)
done
-subsection{*normal subgroups*}
+subsection {* Normal subgroups *}
(*????????????????
text "Allows use of theorems proved in the locale coset"
lemma subgroup_imp_coset: "subgroup H G ==> coset G"
apply (drule subgroup_imp_group)
-apply (simp add: group_def coset_def)
+apply (simp add: group_def coset_def)
done
*)
@@ -180,7 +180,7 @@
lemma (in coset) normal_inv_op_closed1:
"\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
apply (auto simp add: l_coset_eq r_coset_eq normal_iff)
-apply (drule bspec, assumption)
+apply (drule bspec, assumption)
apply (drule equalityD1 [THEN subsetD], blast, clarify)
apply (simp add: m_assoc subgroup.subset [THEN subsetD])
apply (erule subst)
@@ -189,12 +189,12 @@
lemma (in coset) normal_inv_op_closed2:
"\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
-apply (drule normal_inv_op_closed1 [of H "(inv x)"])
+apply (drule normal_inv_op_closed1 [of H "(inv x)"])
apply auto
done
lemma (in coset) lcos_m_assoc:
- "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
+ "[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |]
==> g <# (h <# M) = (g \<otimes> h) <# M"
by (force simp add: l_coset_eq m_assoc)
@@ -208,8 +208,8 @@
lemma (in coset) l_coset_swap:
"[| y \<in> x <# H; x \<in> carrier G; subgroup H G |] ==> x \<in> y <# H"
proof (simp add: l_coset_eq)
- assume "\<exists>h\<in>H. x \<otimes> h = y"
- and x: "x \<in> carrier G"
+ assume "\<exists>h\<in>H. x \<otimes> h = y"
+ and x: "x \<in> carrier G"
and sb: "subgroup H G"
then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
show "\<exists>h\<in>H. y \<otimes> h = x"
@@ -223,28 +223,28 @@
lemma (in coset) l_coset_carrier:
"[| y \<in> x <# H; x \<in> carrier G; subgroup H G |] ==> y \<in> carrier G"
-by (auto simp add: l_coset_eq m_assoc
+by (auto simp add: l_coset_eq m_assoc
subgroup.subset [THEN subsetD] subgroup.m_closed)
lemma (in coset) l_repr_imp_subset:
- assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
+ assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
shows "y <# H \<subseteq> x <# H"
proof -
from y
obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_eq)
thus ?thesis using x sb
- by (auto simp add: l_coset_eq m_assoc
+ by (auto simp add: l_coset_eq m_assoc
subgroup.subset [THEN subsetD] subgroup.m_closed)
qed
lemma (in coset) l_repr_independence:
- assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
+ assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
shows "x <# H = y <# H"
-proof
+proof
show "x <# H \<subseteq> y <# H"
- by (rule l_repr_imp_subset,
+ by (rule l_repr_imp_subset,
(blast intro: l_coset_swap l_coset_carrier y x sb)+)
- show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
+ show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
qed
lemma (in coset) setmult_subset_G:
@@ -255,29 +255,30 @@
apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def)
apply (rule_tac x = x in bexI)
apply (rule bexI [of _ "\<one>"])
-apply (auto simp add: subgroup.m_closed subgroup.one_closed
+apply (auto simp add: subgroup.m_closed subgroup.one_closed
r_one subgroup.subset [THEN subsetD])
done
-(* set of inverses of an r_coset *)
+text {* Set of inverses of an @{text r_coset}. *}
+
lemma (in coset) rcos_inv:
assumes normalHG: "H <| G"
and xinG: "x \<in> carrier G"
shows "set_inv G (H #> x) = H #> (inv x)"
proof -
- have H_subset: "H <= carrier G"
+ have H_subset: "H <= carrier G"
by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG])
show ?thesis
proof (auto simp add: r_coset_eq image_def set_inv_def)
fix h
assume "h \<in> H"
hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)"
- by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD])
- thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)"
+ by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD])
+ thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)"
using prems
- by (blast intro: normal_inv_op_closed1 normal_imp_subgroup
- subgroup.m_inv_closed)
+ by (blast intro: normal_inv_op_closed1 normal_imp_subgroup
+ subgroup.m_inv_closed)
next
fix h
assume "h \<in> H"
@@ -285,9 +286,9 @@
by (simp add: xinG m_assoc H_subset [THEN subsetD])
hence "(\<exists>j\<in>H. j \<otimes> x = inv (h \<otimes> (inv x))) \<and> h \<otimes> inv x = inv (inv (h \<otimes> (inv x)))"
using prems
- by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
- blast intro: eq normal_inv_op_closed2 normal_imp_subgroup
- subgroup.m_inv_closed)
+ by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD],
+ blast intro: eq normal_inv_op_closed2 normal_imp_subgroup
+ subgroup.m_inv_closed)
thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" ..
qed
qed
@@ -314,7 +315,7 @@
apply (simp add: setrcos_eq, clarify)
apply (subgoal_tac "x : carrier G")
prefer 2
- apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup)
+ apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup)
apply (drule repr_independence)
apply assumption
apply (erule normal_imp_subgroup)
@@ -322,56 +323,57 @@
done
-(* some rules for <#> with #> or <# *)
+text {* Some rules for @{text "<#>"} with @{text "#>"} or @{text "<#"}. *}
+
lemma (in coset) setmult_rcos_assoc:
- "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
+ "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
==> H <#> (K #> x) = (H <#> K) #> x"
apply (auto simp add: rcos_def r_coset_def setmult_def set_mult_def)
apply (force simp add: m_assoc)+
done
lemma (in coset) rcos_assoc_lcos:
- "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
+ "[| H <= carrier G; K <= carrier G; x \<in> carrier G |]
==> (H #> x) <#> K = H <#> (x <# K)"
-apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def
+apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def
setmult_def set_mult_def Sigma_def image_def)
apply (force intro!: exI bexI simp add: m_assoc)+
done
lemma (in coset) rcos_mult_step1:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset]
r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
lemma (in coset) rcos_mult_step2:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
by (simp add: normal_imp_rcos_eq_lcos)
lemma (in coset) rcos_mult_step3:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc
setmult_subset_G subgroup_mult_id
subgroup.subset normal_imp_subgroup)
lemma (in coset) rcos_sum:
- "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
+ "[| H <| G; x \<in> carrier G; y \<in> carrier G |]
==> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
-(*generalizes subgroup_mult_id*)
lemma (in coset) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M"
-by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
- setmult_rcos_assoc subgroup_mult_id)
+ -- {* generalizes @{text subgroup_mult_id} *}
+ by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset
+ setmult_rcos_assoc subgroup_mult_id)
-subsection{*Lemmas Leading to Lagrange's Theorem*}
+subsection {*Lemmas Leading to Lagrange's Theorem *}
-lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union> rcosets G H = carrier G"
+lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union>rcosets G H = carrier G"
apply (rule equalityI)
-apply (force simp add: subgroup.subset [THEN subsetD]
+apply (force simp add: subgroup.subset [THEN subsetD]
setrcos_eq r_coset_eq)
apply (auto simp add: setrcos_eq subgroup.subset rcos_self)
done
@@ -398,13 +400,13 @@
by (force simp add: inj_on_def subsetD)
lemma (in coset) card_cosets_equal:
- "[| c \<in> rcosets G H; H <= carrier G; finite(carrier G) |]
+ "[| c \<in> rcosets G H; H <= carrier G; finite(carrier G) |]
==> card c = card H"
apply (auto simp add: setrcos_eq)
apply (rule card_bij_eq)
- apply (rule inj_on_f, assumption+)
+ apply (rule inj_on_f, assumption+)
apply (force simp add: m_assoc subsetD r_coset_eq)
- apply (rule inj_on_g, assumption+)
+ apply (rule inj_on_g, assumption+)
apply (force simp add: m_assoc subsetD r_coset_eq)
txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
apply (simp add: r_coset_subset_G [THEN finite_subset])
@@ -414,8 +416,8 @@
subsection{*Two distinct right cosets are disjoint*}
lemma (in coset) rcos_equation:
- "[|subgroup H G; a \<in> carrier G; b \<in> carrier G; ha \<otimes> a = h \<otimes> b;
- h \<in> H; ha \<in> H; hb \<in> H|]
+ "[|subgroup H G; a \<in> carrier G; b \<in> carrier G; ha \<otimes> a = h \<otimes> b;
+ h \<in> H; ha \<in> H; hb \<in> H|]
==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
apply (simp add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
@@ -439,16 +441,16 @@
constdefs
FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
(infixl "Mod" 60)
- "FactGroup G H ==
- (| carrier = rcosets G H,
- mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
- one = H (*,
- m_inv = (%X: rcosets G H. set_inv G X) *) |)"
+ "FactGroup G H ==
+ (| carrier = rcosets G H,
+ mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
+ one = H (*,
+ m_inv = (%X: rcosets G H. set_inv G X) *) |)"
lemma (in coset) setmult_closed:
- "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
+ "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
==> K1 <#> K2 \<in> rcosets G H"
-by (auto simp add: normal_imp_subgroup [THEN subgroup.subset]
+by (auto simp add: normal_imp_subgroup [THEN subgroup.subset]
rcos_sum setrcos_eq)
lemma (in group) setinv_closed:
@@ -467,9 +469,9 @@
*)
lemma (in coset) setrcos_assoc:
- "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
+ "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
-by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
+by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup
subgroup.subset m_assoc)
lemma (in group) subgroup_in_rcosets:
@@ -486,10 +488,10 @@
(*
lemma subgroup_in_rcosets:
"subgroup H G ==> H \<in> rcosets G H"
-apply (frule subgroup_imp_coset)
-apply (frule subgroup_imp_group)
+apply (frule subgroup_imp_coset)
+apply (frule subgroup_imp_group)
apply (simp add: coset.setrcos_eq)
-apply (blast del: equalityI
+apply (blast del: equalityI
intro!: group.subgroup.one_closed group.one_closed
coset.coset_join2 [symmetric])
done
@@ -497,7 +499,7 @@
lemma (in coset) setrcos_inv_mult_group_eq:
"[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
-by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
+by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
subgroup.subset)
(*
lemma (in group) factorgroup_is_magma:
@@ -511,8 +513,8 @@
*)
theorem (in group) factorgroup_is_group:
"H <| G ==> group (G Mod H)"
-apply (insert is_coset)
-apply (simp add: FactGroup_def)
+apply (insert is_coset)
+apply (simp add: FactGroup_def)
apply (rule groupI)
apply (simp add: coset.setmult_closed)
apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
--- a/src/HOL/Algebra/FiniteProduct.thy Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Fri Apr 23 21:46:04 2004 +0200
@@ -290,13 +290,13 @@
syntax
"_finprod" :: "index => idt => 'a set => 'b => 'b"
- ("\<Otimes>__:_. _" [1000, 0, 51, 10] 10)
+ ("(3\<Otimes>__:_. _)" [1000, 0, 51, 10] 10)
syntax (xsymbols)
"_finprod" :: "index => idt => 'a set => 'b => 'b"
- ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
+ ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
syntax (HTML output)
"_finprod" :: "index => idt => 'a set => 'b => 'b"
- ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
+ ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
translations
"\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A" -- {* Beware of argument permutation! *}
--- a/src/HOL/Algebra/Lattice.thy Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/Lattice.thy Fri Apr 23 21:46:04 2004 +0200
@@ -186,6 +186,7 @@
shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
by (unfold greatest_def) blast
+
subsubsection {* Supremum *}
lemma (in lattice) joinI:
@@ -212,7 +213,8 @@
shows "x \<in> carrier L ==> \<Squnion> {x} = x"
by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
-text {* Condition on A: supremum exists. *}
+
+text {* Condition on @{text A}: supremum exists. *}
lemma (in lattice) sup_insertI:
"[| !!s. least L s (Upper L (insert x A)) ==> P s;
--- a/src/HOL/Algebra/Sylow.thy Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/Sylow.thy Fri Apr 23 21:46:04 2004 +0200
@@ -4,7 +4,7 @@
See Florian Kamm\"uller and L. C. Paulson,
A Formal Proof of Sylow's theorem:
- An Experiment in Abstract Algebra with Isabelle HOL
+ An Experiment in Abstract Algebra with Isabelle HOL
J. Automated Reasoning 23 (1999), 235-264
*)
@@ -15,11 +15,11 @@
subsection {*Order of a Group and Lagrange's Theorem*}
constdefs
- order :: "('a,'b) semigroup_scheme => nat"
+ order :: "('a, 'b) semigroup_scheme => nat"
"order S == card (carrier S)"
theorem (in coset) lagrange:
- "[| finite(carrier G); subgroup H G |]
+ "[| finite(carrier G); subgroup H G |]
==> card(rcosets G H) * card(H) = order(G)"
apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
apply (subst mult_commute)
@@ -40,11 +40,11 @@
and finite_G [iff]: "finite (carrier G)"
defines "calM == {s. s <= carrier(G) & card(s) = p^a}"
and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
- (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
+ (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
lemma (in sylow) RelM_refl: "refl calM RelM"
-apply (auto simp add: refl_def RelM_def calM_def)
-apply (blast intro!: coset_mult_one [symmetric])
+apply (auto simp add: refl_def RelM_def calM_def)
+apply (blast intro!: coset_mult_one [symmetric])
done
lemma (in sylow) RelM_sym: "sym RelM"
@@ -58,7 +58,7 @@
qed
lemma (in sylow) RelM_trans: "trans RelM"
-by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
+by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
lemma (in sylow) RelM_equiv: "equiv calM RelM"
apply (unfold equiv_def)
@@ -91,9 +91,9 @@
lemma card_nonempty: "0 < card(S) ==> S \<noteq> {}"
by force
-lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
-apply (subgoal_tac "0 < card M1")
- apply (blast dest: card_nonempty)
+lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
+apply (subgoal_tac "0 < card M1")
+ apply (blast dest: card_nonempty)
apply (cut_tac prime_p [THEN prime_imp_one_less])
apply (simp (no_asm_simp) add: card_M1)
done
@@ -112,18 +112,18 @@
show ?thesis
proof
show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
- by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
+ by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
proof (rule restrictI)
- fix z assume zH: "z \<in> H"
- show "m1 \<otimes> z \<in> M1"
- proof -
- from zH
- have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
- by (auto simp add: H_def)
- show ?thesis
- by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
- qed
+ fix z assume zH: "z \<in> H"
+ show "m1 \<otimes> z \<in> M1"
+ proof -
+ from zH
+ have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
+ by (auto simp add: H_def)
+ show ?thesis
+ by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
+ qed
qed
qed
qed
@@ -135,8 +135,8 @@
by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
lemma (in sylow) existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M"
-apply (subgoal_tac "M \<noteq> {}")
- apply blast
+apply (subgoal_tac "M \<noteq> {}")
+ apply blast
apply (cut_tac EmptyNotInEquivSet, blast)
done
@@ -245,7 +245,7 @@
text{*Injections between @{term M} and @{term "rcosets G H"} show that
their cardinalities are equal.*}
-lemma ElemClassEquiv:
+lemma ElemClassEquiv:
"[| equiv A r; C\<in>A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
apply (unfold equiv_def quotient_def sym_def trans_def, blast)
done
@@ -257,11 +257,11 @@
apply (blast dest!: bspec)
done
-lemmas (in sylow_central) M_elem_map_carrier =
- M_elem_map [THEN someI_ex, THEN conjunct1]
+lemmas (in sylow_central) M_elem_map_carrier =
+ M_elem_map [THEN someI_ex, THEN conjunct1]
lemmas (in sylow_central) M_elem_map_eq =
- M_elem_map [THEN someI_ex, THEN conjunct2]
+ M_elem_map [THEN someI_ex, THEN conjunct2]
lemma (in sylow_central) M_funcset_setrcos_H:
"(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets G H"
@@ -293,14 +293,14 @@
"H1\<in>rcosets G H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
by (auto simp add: setrcos_eq)
-lemmas (in sylow_central) H_elem_map_carrier =
- H_elem_map [THEN someI_ex, THEN conjunct1]
+lemmas (in sylow_central) H_elem_map_carrier =
+ H_elem_map [THEN someI_ex, THEN conjunct1]
lemmas (in sylow_central) H_elem_map_eq =
- H_elem_map [THEN someI_ex, THEN conjunct2]
+ H_elem_map [THEN someI_ex, THEN conjunct2]
-lemma EquivElemClass:
+lemma EquivElemClass:
"[|equiv A r; M\<in>A // r; M1\<in>M; (M1, M2)\<in>r |] ==> M2\<in>M"
apply (unfold equiv_def quotient_def sym_def trans_def, blast)
done
@@ -329,7 +329,7 @@
apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
apply (rule coset_join2)
apply (blast intro: m_closed inv_closed H_elem_map_carrier)
-apply (rule H_is_subgroup)
+apply (rule H_is_subgroup)
apply (simp add: H_I coset_mult_inv2 M1_subset_G H_elem_map_carrier)
done
@@ -344,9 +344,9 @@
done
lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets G H)"
-apply (insert inj_M_GmodH inj_GmodH_M)
-apply (blast intro: card_bij finite_M H_is_subgroup
- setrcos_subset_PowG [THEN finite_subset]
+apply (insert inj_M_GmodH inj_GmodH_M)
+apply (blast intro: card_bij finite_M H_is_subgroup
+ setrcos_subset_PowG [THEN finite_subset]
finite_Pow_iff [THEN iffD2])
done
@@ -364,7 +364,7 @@
lemma (in sylow_central) lemma_leq2: "card(H) <= p^a"
apply (subst card_M1 [symmetric])
apply (cut_tac M1_inj_H)
-apply (blast intro!: M1_subset_G intro:
+apply (blast intro!: M1_subset_G intro:
card_inj H_into_carrier_G finite_subset [OF _ finite_G])
done
@@ -372,15 +372,15 @@
by (blast intro: le_anti_sym lemma_leq1 lemma_leq2)
lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G & card(H) = p^a"
-apply (cut_tac lemma_A1, clarify)
-apply (frule existsM1inM, clarify)
+apply (cut_tac lemma_A1, clarify)
+apply (frule existsM1inM, clarify)
apply (subgoal_tac "sylow_central G p a m M1 M")
apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq)
-apply (simp add: sylow_central_def sylow_central_axioms_def prems)
+apply (simp add: sylow_central_def sylow_central_axioms_def prems)
done
text{*Needed because the locale's automatic definition refers to
- @{term "semigroup G"} and @{term "group_axioms G"} rather than
+ @{term "semigroup G"} and @{term "group_axioms G"} rather than
simply to @{term "group G"}.*}
lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
by (simp add: sylow_def group_def)
@@ -389,7 +389,7 @@
"[|p \<in> prime; group(G); order(G) = (p^a) * m; finite (carrier G)|]
==> \<exists>H. subgroup H G & card(H) = p^a"
apply (rule sylow.sylow_thm [of G p a m])
-apply (simp add: sylow_eq sylow_axioms_def)
+apply (simp add: sylow_eq sylow_axioms_def)
done
end
--- a/src/HOL/Algebra/UnivPoly.thy Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Apr 23 21:46:04 2004 +0200
@@ -10,43 +10,32 @@
theory UnivPoly = Module:
text {*
- Polynomials are formalised as modules with additional operations for
- extracting coefficients from polynomials and for obtaining monomials
- from coefficients and exponents (record @{text "up_ring"}).
- The carrier set is
- a set of bounded functions from Nat to the coefficient domain.
- Bounded means that these functions return zero above a certain bound
- (the degree). There is a chapter on the formalisation of polynomials
- in my PhD thesis (http://www4.in.tum.de/\~{}ballarin/publications/),
- which was implemented with axiomatic type classes. This was later
- ported to Locales.
+ Polynomials are formalised as modules with additional operations for
+ extracting coefficients from polynomials and for obtaining monomials
+ from coefficients and exponents (record @{text "up_ring"}). The
+ carrier set is a set of bounded functions from Nat to the
+ coefficient domain. Bounded means that these functions return zero
+ above a certain bound (the degree). There is a chapter on the
+ formalisation of polynomials in my PhD thesis
+ (\url{http://www4.in.tum.de/~ballarin/publications/}), which was
+ implemented with axiomatic type classes. This was later ported to
+ Locales.
*}
+
subsection {* The Constructor for Univariate Polynomials *}
-(* Could alternatively use locale ...
-locale bound = cring + var bound +
- defines ...
-*)
-
-constdefs
- bound :: "['a, nat, nat => 'a] => bool"
- "bound z n f == (ALL i. n < i --> f i = z)"
+locale bound =
+ fixes z :: 'a
+ and n :: nat
+ and f :: "nat => 'a"
+ assumes bound: "!!m. n < m \<Longrightarrow> f m = z"
-lemma boundI [intro!]:
- "[| !! m. n < m ==> f m = z |] ==> bound z n f"
- by (unfold bound_def) fast
-
-lemma boundE [elim?]:
- "[| bound z n f; (!! m. n < m ==> f m = z) ==> P |] ==> P"
- by (unfold bound_def) fast
-
-lemma boundD [dest]:
- "[| bound z n f; n < m |] ==> f m = z"
- by (unfold bound_def) fast
+declare bound.intro [intro!]
+ and bound.bound [dest]
lemma bound_below:
- assumes bound: "bound z m f" and nonzero: "f n ~= z" shows "n <= m"
+ assumes bound: "bound z m f" and nonzero: "f n \<noteq> z" shows "n \<le> m"
proof (rule classical)
assume "~ ?thesis"
then have "m < n" by arith
@@ -130,45 +119,45 @@
lemma (in cring) up_mult_closed:
"[| p \<in> up R; q \<in> up R |] ==>
- (%n. finsum R (%i. p i \<otimes> q (n-i)) {..n}) \<in> up R"
+ (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
proof
fix n
assume "p \<in> up R" "q \<in> up R"
- then show "finsum R (%i. p i \<otimes> q (n-i)) {..n} \<in> carrier R"
+ then show "(\<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> carrier R"
by (simp add: mem_upD funcsetI)
next
assume UP: "p \<in> up R" "q \<in> up R"
- show "EX n. bound \<zero> n (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
+ show "EX n. bound \<zero> n (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i))"
proof -
from UP obtain n where boundn: "bound \<zero> n p" by fast
from UP obtain m where boundm: "bound \<zero> m q" by fast
- have "bound \<zero> (n + m) (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
+ have "bound \<zero> (n + m) (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n - i))"
proof
- fix k
- assume bound: "n + m < k"
+ fix k assume bound: "n + m < k"
{
- fix i
- have "p i \<otimes> q (k-i) = \<zero>"
- proof (cases "n < i")
- case True
- with boundn have "p i = \<zero>" by auto
+ fix i
+ have "p i \<otimes> q (k-i) = \<zero>"
+ proof (cases "n < i")
+ case True
+ with boundn have "p i = \<zero>" by auto
moreover from UP have "q (k-i) \<in> carrier R" by auto
- ultimately show ?thesis by simp
- next
- case False
- with bound have "m < k-i" by arith
- with boundm have "q (k-i) = \<zero>" by auto
- moreover from UP have "p i \<in> carrier R" by auto
- ultimately show ?thesis by simp
- qed
+ ultimately show ?thesis by simp
+ next
+ case False
+ with bound have "m < k-i" by arith
+ with boundm have "q (k-i) = \<zero>" by auto
+ moreover from UP have "p i \<in> carrier R" by auto
+ ultimately show ?thesis by simp
+ qed
}
- then show "finsum R (%i. p i \<otimes> q (k-i)) {..k} = \<zero>"
- by (simp add: Pi_def)
+ then show "(\<Oplus>i \<in> {..k}. p i \<otimes> q (k-i)) = \<zero>"
+ by (simp add: Pi_def)
qed
then show ?thesis by fast
qed
qed
+
subsection {* Effect of operations on coefficients *}
locale UP = struct R + struct P +
@@ -214,7 +203,7 @@
lemma (in UP_cring) coeff_mult [simp]:
"[| p \<in> carrier P; q \<in> carrier P |] ==>
- coeff P (p \<otimes>\<^sub>2 q) n = finsum R (%i. coeff P p i \<otimes> coeff P q (n-i)) {..n}"
+ coeff P (p \<otimes>\<^sub>2 q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (n-i))"
by (simp add: UP_def up_mult_closed)
lemma (in UP) up_eqI:
@@ -225,10 +214,10 @@
fix x
from prem and R show "p x = q x" by (simp add: UP_def)
qed
-
+
subsection {* Polynomials form a commutative ring. *}
-text {* Operations are closed over @{term "P"}. *}
+text {* Operations are closed over @{term P}. *}
lemma (in UP_cring) UP_mult_closed [simp]:
"[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^sub>2 q \<in> carrier P"
@@ -307,9 +296,9 @@
assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
"c \<in> UNIV -> carrier R"
then have "k <= n ==>
- finsum R (%j. finsum R (%i. a i \<otimes> b (j-i)) {..j} \<otimes> c (n-j)) {..k} =
- finsum R (%j. a j \<otimes> finsum R (%i. b i \<otimes> c (n-j-i)) {..k-j}) {..k}"
- (is "_ ==> ?eq k")
+ (\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
+ (\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
+ (concl is "?eq k")
proof (induct k)
case 0 then show ?case by (simp add: Pi_def m_assoc)
next
@@ -317,7 +306,7 @@
then have "k <= n" by arith
then have "?eq k" by (rule Suc)
with R show ?case
- by (simp cong: finsum_cong
+ by (simp cong: finsum_cong
add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
(simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
qed
@@ -353,19 +342,19 @@
assumes R: "p \<in> carrier P" "q \<in> carrier P"
shows "p \<otimes>\<^sub>2 q = q \<otimes>\<^sub>2 p"
proof (rule up_eqI)
- fix n
+ fix n
{
fix k and a b :: "nat=>'a"
assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
- then have "k <= n ==>
- finsum R (%i. a i \<otimes> b (n-i)) {..k} =
- finsum R (%i. a (k-i) \<otimes> b (i+n-k)) {..k}"
- (is "_ ==> ?eq k")
+ then have "k <= n ==>
+ (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) =
+ (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
+ (concl is "?eq k")
proof (induct k)
case 0 then show ?case by (simp add: Pi_def)
next
case (Suc k) then show ?case
- by (subst finsum_Suc2) (simp add: Pi_def a_comm)+
+ by (subst finsum_Suc2) (simp add: Pi_def a_comm)+
qed
}
note l = this
@@ -557,6 +546,7 @@
lemmas (in UP_cring) UP_finsum_rdistr =
cring.finsum_rdistr [OF UP_cring]
+
subsection {* Polynomials form an Algebra *}
lemma (in UP_cring) UP_smult_l_distr:
@@ -658,64 +648,64 @@
proof (cases "k = Suc n")
case True show ?thesis
proof -
- from True have less_add_diff:
- "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
+ from True have less_add_diff:
+ "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
also from True
- have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
- coeff P (monom P \<one> 1) (k - i)) ({..n(} Un {n})"
- by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
- also have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
- coeff P (monom P \<one> 1) (k - i)) {..n}"
- by (simp only: ivl_disj_un_singleton)
- also from True have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
- coeff P (monom P \<one> 1) (k - i)) ({..n} Un {)n..k})"
- by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
- order_less_imp_not_eq Pi_def)
+ have "... = (\<Oplus>i \<in> {..n(} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
+ coeff P (monom P \<one> 1) (k - i))"
+ by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
+ also have "... = (\<Oplus>i \<in> {..n}. coeff P (monom P \<one> n) i \<otimes>
+ coeff P (monom P \<one> 1) (k - i))"
+ by (simp only: ivl_disj_un_singleton)
+ also from True have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. coeff P (monom P \<one> n) i \<otimes>
+ coeff P (monom P \<one> 1) (k - i))"
+ by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
+ order_less_imp_not_eq Pi_def)
also from True have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
- by (simp add: ivl_disj_un_one)
+ by (simp add: ivl_disj_un_one)
finally show ?thesis .
qed
next
case False
note neq = False
let ?s =
- "(\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>))"
+ "\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>)"
from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
- also have "... = finsum R ?s {..k}"
+ also have "... = (\<Oplus>i \<in> {..k}. ?s i)"
proof -
- have f1: "finsum R ?s {..n(} = \<zero>" by (simp cong: finsum_cong add: Pi_def)
- from neq have f2: "finsum R ?s {n} = \<zero>"
- by (simp cong: finsum_cong add: Pi_def) arith
- have f3: "n < k ==> finsum R ?s {)n..k} = \<zero>"
- by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
+ have f1: "(\<Oplus>i \<in> {..n(}. ?s i) = \<zero>" by (simp cong: finsum_cong add: Pi_def)
+ from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
+ by (simp cong: finsum_cong add: Pi_def) arith
+ have f3: "n < k ==> (\<Oplus>i \<in> {)n..k}. ?s i) = \<zero>"
+ by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
show ?thesis
proof (cases "k < n")
- case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
+ case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
next
- case False then have n_le_k: "n <= k" by arith
- show ?thesis
- proof (cases "n = k")
- case True
- then have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
- by (simp cong: finsum_cong add: finsum_Un_disjoint
- ivl_disj_int_singleton Pi_def)
- also from True have "... = finsum R ?s {..k}"
- by (simp only: ivl_disj_un_singleton)
- finally show ?thesis .
- next
- case False with n_le_k have n_less_k: "n < k" by arith
- with neq have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
- by (simp add: finsum_Un_disjoint f1 f2
- ivl_disj_int_singleton Pi_def del: Un_insert_right)
- also have "... = finsum R ?s {..n}"
- by (simp only: ivl_disj_un_singleton)
- also from n_less_k neq have "... = finsum R ?s ({..n} \<union> {)n..k})"
- by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
- also from n_less_k have "... = finsum R ?s {..k}"
- by (simp only: ivl_disj_un_one)
- finally show ?thesis .
- qed
+ case False then have n_le_k: "n <= k" by arith
+ show ?thesis
+ proof (cases "n = k")
+ case True
+ then have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
+ by (simp cong: finsum_cong add: finsum_Un_disjoint
+ ivl_disj_int_singleton Pi_def)
+ also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
+ by (simp only: ivl_disj_un_singleton)
+ finally show ?thesis .
+ next
+ case False with n_le_k have n_less_k: "n < k" by arith
+ with neq have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
+ by (simp add: finsum_Un_disjoint f1 f2
+ ivl_disj_int_singleton Pi_def del: Un_insert_right)
+ also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
+ by (simp only: ivl_disj_un_singleton)
+ also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. ?s i)"
+ by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
+ also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)"
+ by (simp only: ivl_disj_un_one)
+ finally show ?thesis .
+ qed
qed
qed
also have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k" by simp
@@ -789,7 +779,7 @@
"deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
lemma (in UP_cring) deg_aboveI:
- "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
+ "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
by (unfold deg_def P_def) (fast intro: Least_le)
(*
lemma coeff_bound_ex: "EX n. bound n (coeff p)"
@@ -798,7 +788,7 @@
then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
then show ?thesis ..
qed
-
+
lemma bound_coeff_obtain:
assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
proof -
@@ -811,18 +801,18 @@
"[| deg R p < m; p \<in> carrier P |] ==> coeff P p m = \<zero>"
proof -
assume R: "p \<in> carrier P" and "deg R p < m"
- from R obtain n where "bound \<zero> n (coeff P p)"
+ from R obtain n where "bound \<zero> n (coeff P p)"
by (auto simp add: UP_def P_def)
then have "bound \<zero> (deg R p) (coeff P p)"
by (auto simp: deg_def P_def dest: LeastI)
- then show ?thesis by (rule boundD)
+ then show ?thesis ..
qed
lemma (in UP_cring) deg_belowI:
assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
and R: "p \<in> carrier P"
shows "n <= deg R p"
--- {* Logically, this is a slightly stronger version of
+-- {* Logically, this is a slightly stronger version of
@{thm [source] deg_aboveD} *}
proof (cases "n=0")
case True then show ?thesis by simp
@@ -847,7 +837,7 @@
then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
by (unfold bound_def) fast
then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
- then show ?thesis by auto
+ then show ?thesis by auto
qed
with deg_belowI R have "deg R p = m" by fastsimp
with m_coeff show ?thesis by simp
@@ -890,7 +880,7 @@
shows "deg R (p \<oplus>\<^sub>2 q) <= max (deg R p) (deg R q)"
proof (cases "deg R p <= deg R q")
case True show ?thesis
- by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
+ by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
next
case False show ?thesis
by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
@@ -933,7 +923,7 @@
proof (rule le_anti_sym)
show "deg R (\<ominus>\<^sub>2 p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
next
- show "deg R p <= deg R (\<ominus>\<^sub>2 p)"
+ show "deg R p <= deg R (\<ominus>\<^sub>2 p)"
by (simp add: deg_belowI lcoeff_nonzero_deg
inj_on_iff [OF a_inv_inj, of _ "\<zero>", simplified] R)
qed
@@ -999,10 +989,10 @@
deg_aboveD less_add_diff R Pi_def)
also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})"
by (simp only: ivl_disj_un_singleton)
- also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
+ also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
by (simp cong: finsum_cong add: finsum_Un_disjoint
- ivl_disj_int_singleton deg_aboveD R Pi_def)
- finally have "finsum R ?s {.. deg R p + deg R q}
+ ivl_disj_int_singleton deg_aboveD R Pi_def)
+ finally have "finsum R ?s {.. deg R p + deg R q}
= coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
with nz show "finsum R ?s {.. deg R p + deg R q} ~= \<zero>"
by (simp add: integral_iff lcoeff_nonzero R)
@@ -1021,7 +1011,7 @@
lemma (in UP_cring) up_repr:
assumes R: "p \<in> carrier P"
- shows "finsum P (%i. monom P (coeff P p i) i) {..deg R p} = p"
+ shows "(\<Oplus>\<^sub>2 i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
proof (rule up_eqI)
let ?s = "(%i. monom P (coeff P p i) i)"
fix k
@@ -1030,23 +1020,23 @@
show "coeff P (finsum P ?s {..deg R p}) k = coeff P p k"
proof (cases "k <= deg R p")
case True
- hence "coeff P (finsum P ?s {..deg R p}) k =
+ hence "coeff P (finsum P ?s {..deg R p}) k =
coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k"
by (simp only: ivl_disj_un_one)
also from True
have "... = coeff P (finsum P ?s {..k}) k"
by (simp cong: finsum_cong add: finsum_Un_disjoint
- ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
+ ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
also
have "... = coeff P (finsum P ?s ({..k(} Un {k})) k"
by (simp only: ivl_disj_un_singleton)
also have "... = coeff P p k"
by (simp cong: finsum_cong add: setsum_Un_disjoint
- ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
+ ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
finally show ?thesis .
next
case False
- hence "coeff P (finsum P ?s {..deg R p}) k =
+ hence "coeff P (finsum P ?s {..deg R p}) k =
coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k"
by (simp only: ivl_disj_un_singleton)
also from False have "... = coeff P p k"
@@ -1107,11 +1097,11 @@
also from pq have "... = 0" by simp
finally have "deg R p + deg R q = 0" .
then have f1: "deg R p = 0 & deg R q = 0" by simp
- from f1 R have "p = finsum P (%i. (monom P (coeff P p i) i)) {..0}"
+ from f1 R have "p = (\<Oplus>\<^sub>2 i \<in> {..0}. monom P (coeff P p i) i)"
by (simp only: up_repr_le)
also from R have "... = monom P (coeff P p 0) 0" by simp
finally have p: "p = monom P (coeff P p 0) 0" .
- from f1 R have "q = finsum P (%i. (monom P (coeff P q i) i)) {..0}"
+ from f1 R have "q = (\<Oplus>\<^sub>2 i \<in> {..0}. monom P (coeff P q i) i)"
by (simp only: up_repr_le)
also from R have "... = monom P (coeff P q 0) 0" by simp
finally have q: "q = monom P (coeff P q 0) 0" .
@@ -1149,49 +1139,49 @@
by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff
inj_on_iff [OF monom_inj, of _ "\<zero>", simplified])
+
subsection {* Evaluation Homomorphism and Universal Property*}
+(* alternative congruence rule (possibly more efficient)
+lemma (in abelian_monoid) finsum_cong2:
+ "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
+ !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
+ sorry*)
+
ML_setup {*
simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
*}
-(* alternative congruence rule (possibly more efficient)
-lemma (in abelian_monoid) finsum_cong2:
- "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
- !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
- sorry
-*)
-
theorem (in cring) diagonal_sum:
"[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
- finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..n + m} =
- finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
+ (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
+ (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
proof -
assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
{
fix j
have "j <= n + m ==>
- finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..j} =
- finsum R (%k. finsum R (%i. f k \<otimes> g i) {..j - k}) {..j}"
+ (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
+ (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..j - k}. f k \<otimes> g i)"
proof (induct j)
case 0 from Rf Rg show ?case by (simp add: Pi_def)
next
- case (Suc j)
+ case (Suc j)
(* The following could be simplified if there was a reasoner for
- total orders integrated with simip. *)
+ total orders integrated with simip. *)
have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
- using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+ using Suc by (auto intro!: funcset_mem [OF Rg]) arith
have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
- using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+ using Suc by (auto intro!: funcset_mem [OF Rg]) arith
have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
- using Suc by (auto intro!: funcset_mem [OF Rf])
+ using Suc by (auto intro!: funcset_mem [OF Rf])
have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
- using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+ using Suc by (auto intro!: funcset_mem [OF Rg]) arith
have R11: "g 0 \<in> carrier R"
- using Suc by (auto intro!: funcset_mem [OF Rg])
+ using Suc by (auto intro!: funcset_mem [OF Rg])
from Suc show ?case
- by (simp cong: finsum_cong add: Suc_diff_le a_ac
- Pi_def R6 R8 R9 R10 R11)
+ by (simp cong: finsum_cong add: Suc_diff_le a_ac
+ Pi_def R6 R8 R9 R10 R11)
qed
}
then show ?thesis by fast
@@ -1204,9 +1194,8 @@
theorem (in cring) cauchy_product:
assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
- shows "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
- finsum R f {..n} \<otimes> finsum R g {..m}"
-(* State revese direction? *)
+ shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
+ (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)" (* State revese direction? *)
proof -
have f: "!!x. f x \<in> carrier R"
proof -
@@ -1220,24 +1209,20 @@
show "g x \<in> carrier R"
using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def)
qed
- from f g have "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
- finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
+ from f g have "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
+ (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
by (simp add: diagonal_sum Pi_def)
- also have "... = finsum R
- (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) ({..n} Un {)n..n + m})"
+ also have "... = (\<Oplus>k \<in> {..n} \<union> {)n..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
by (simp only: ivl_disj_un_one)
- also from f g have "... = finsum R
- (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n}"
+ also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
by (simp cong: finsum_cong
- add: boundD [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
- also from f g have "... = finsum R
- (%k. finsum R (%i. f k \<otimes> g i) ({..m} Un {)m..n + m - k})) {..n}"
+ add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
+ also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {)m..n + m - k}. f k \<otimes> g i)"
by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
- also from f g have "... = finsum R
- (%k. finsum R (%i. f k \<otimes> g i) {..m}) {..n}"
+ also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)"
by (simp cong: finsum_cong
- add: boundD [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
- also from f g have "... = finsum R f {..n} \<otimes> finsum R g {..m}"
+ add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
+ also from f g have "... = (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"
by (simp add: finsum_ldistr diagonal_sum Pi_def,
simp cong: finsum_cong add: finsum_rdistr Pi_def)
finally show ?thesis .
@@ -1256,13 +1241,13 @@
then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
else arbitrary"
*)
-
+
locale ring_hom_UP_cring = ring_hom_cring R S + UP_cring R
lemma (in ring_hom_UP_cring) eval_on_carrier:
"p \<in> carrier P ==>
eval R S phi s p =
- finsum S (%i. mult S (phi (coeff P p i)) (pow S s i)) {..deg R p}"
+ (\<Oplus>\<^sub>2 i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^sub>2 pow S s i)"
by (unfold eval_def, fold P_def) simp
lemma (in ring_hom_UP_cring) eval_extensional:
@@ -1282,31 +1267,29 @@
then show "eval R S h s (p \<otimes>\<^sub>3 q) = eval R S h s p \<otimes>\<^sub>2 eval R S h s q"
proof (simp only: eval_on_carrier UP_mult_closed)
from RS have
- "finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<otimes>\<^sub>3 q)} =
- finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
- ({..deg R (p \<otimes>\<^sub>3 q)} Un {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q})"
+ "(\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)}. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
+ (\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)} \<union> {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q}.
+ h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp cong: finsum_cong
- add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
- del: coeff_mult)
+ add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
+ del: coeff_mult)
also from RS have "... =
- finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p + deg R q}"
+ (\<Oplus>\<^sub>2 i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp only: ivl_disj_un_one deg_mult_cring)
also from RS have "... =
- finsum S (%i.
- finsum S (%k.
- (h (coeff P p k) \<otimes>\<^sub>2 h (coeff P q (i-k))) \<otimes>\<^sub>2 (s (^)\<^sub>2 k \<otimes>\<^sub>2 s (^)\<^sub>2 (i-k)))
- {..i}) {..deg R p + deg R q}"
+ (\<Oplus>\<^sub>2 i \<in> {..deg R p + deg R q}.
+ \<Oplus>\<^sub>2 k \<in> {..i}. h (coeff P p k) \<otimes>\<^sub>2 h (coeff P q (i - k)) \<otimes>\<^sub>2 (s (^)\<^sub>2 k \<otimes>\<^sub>2 s (^)\<^sub>2 (i - k)))"
by (simp cong: finsum_cong add: nat_pow_mult Pi_def
- S.m_ac S.finsum_rdistr)
+ S.m_ac S.finsum_rdistr)
also from RS have "... =
- finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
- finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
- by (simp add: S.cauchy_product [THEN sym] boundI deg_aboveD S.m_ac
- Pi_def)
+ (\<Oplus>\<^sub>2i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<otimes>\<^sub>2
+ (\<Oplus>\<^sub>2i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
+ by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
+ Pi_def)
finally show
- "finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<otimes>\<^sub>3 q)} =
- finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
- finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" .
+ "(\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)}. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
+ (\<Oplus>\<^sub>2 i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<otimes>\<^sub>2
+ (\<Oplus>\<^sub>2 i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)" .
qed
next
fix p q
@@ -1314,36 +1297,35 @@
then show "eval R S h s (p \<oplus>\<^sub>3 q) = eval R S h s p \<oplus>\<^sub>2 eval R S h s q"
proof (simp only: eval_on_carrier UP_a_closed)
from RS have
- "finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<oplus>\<^sub>3 q)} =
- finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
- ({..deg R (p \<oplus>\<^sub>3 q)} Un {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)})"
+ "(\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)}. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
+ (\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)} \<union> {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)}.
+ h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp cong: finsum_cong
- add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
- del: coeff_add)
+ add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
+ del: coeff_add)
also from RS have "... =
- finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
- {..max (deg R p) (deg R q)}"
+ (\<Oplus>\<^sub>2 i \<in> {..max (deg R p) (deg R q)}. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp add: ivl_disj_un_one)
also from RS have "... =
- finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)} \<oplus>\<^sub>2
- finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)}"
+ (\<Oplus>\<^sub>2i\<in>{..max (deg R p) (deg R q)}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
+ (\<Oplus>\<^sub>2i\<in>{..max (deg R p) (deg R q)}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp cong: finsum_cong
- add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
+ add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
also have "... =
- finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
- ({..deg R p} Un {)deg R p..max (deg R p) (deg R q)}) \<oplus>\<^sub>2
- finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
- ({..deg R q} Un {)deg R q..max (deg R p) (deg R q)})"
+ (\<Oplus>\<^sub>2 i \<in> {..deg R p} \<union> {)deg R p..max (deg R p) (deg R q)}.
+ h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
+ (\<Oplus>\<^sub>2 i \<in> {..deg R q} \<union> {)deg R q..max (deg R p) (deg R q)}.
+ h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
also from RS have "... =
- finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
- finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
+ (\<Oplus>\<^sub>2 i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
+ (\<Oplus>\<^sub>2 i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp cong: finsum_cong
- add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
+ add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
finally show
- "finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<oplus>\<^sub>3 q)} =
- finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
- finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
+ "(\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)}. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
+ (\<Oplus>\<^sub>2i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
+ (\<Oplus>\<^sub>2i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
.
qed
next
@@ -1414,14 +1396,14 @@
"s \<in> carrier S ==> eval R S h s (monom P \<one> 1) = s"
proof (simp only: eval_on_carrier monom_closed R.one_closed)
assume S: "s \<in> carrier S"
- then have "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
- {..deg R (monom P \<one> 1)} =
- finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
- ({..deg R (monom P \<one> 1)} Un {)deg R (monom P \<one> 1)..1})"
+ then have
+ "(\<Oplus>\<^sub>2 i \<in> {..deg R (monom P \<one> 1)}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
+ (\<Oplus>\<^sub>2i\<in>{..deg R (monom P \<one> 1)} \<union> {)deg R (monom P \<one> 1)..1}.
+ h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp cong: finsum_cong del: coeff_monom
add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
- also have "... =
- finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..1}"
+ also have "... =
+ (\<Oplus>\<^sub>2 i \<in> {..1}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
also have "... = s"
proof (cases "s = \<zero>\<^sub>2")
@@ -1429,8 +1411,8 @@
next
case False with S show ?thesis by (simp add: Pi_def)
qed
- finally show "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
- {..deg R (monom P \<one> 1)} = s" .
+ finally show "(\<Oplus>\<^sub>2 i \<in> {..deg R (monom P \<one> 1)}.
+ h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) = s" .
qed
lemma (in UP_cring) monom_pow:
@@ -1491,15 +1473,13 @@
by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
have Psi_hom: "ring_hom_cring P S Psi"
by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
- have "Phi p = Phi (finsum P
- (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
+ have "Phi p = Phi (\<Oplus>\<^sub>3i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^sub>3 monom P \<one> 1 (^)\<^sub>3 i)"
by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
- also have "... = Psi (finsum P
- (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
- by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom]
+ also have "... = Psi (\<Oplus>\<^sub>3i\<in>{..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^sub>3 monom P \<one> 1 (^)\<^sub>3 i)"
+ by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom]
ring_hom_cring.hom_mult [OF Phi_hom]
ring_hom_cring.hom_pow [OF Phi_hom] Phi
- ring_hom_cring.hom_finsum [OF Psi_hom]
+ ring_hom_cring.hom_finsum [OF Psi_hom]
ring_hom_cring.hom_mult [OF Psi_hom]
ring_hom_cring.hom_pow [OF Psi_hom] Psi RS Pi_def comp_def)
also have "... = Psi p"
@@ -1511,13 +1491,13 @@
theorem (in ring_hom_UP_cring) UP_universal_property:
"s \<in> carrier S ==>
EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
- Phi (monom P \<one> 1) = s &
+ Phi (monom P \<one> 1) = s &
(ALL r : carrier R. Phi (monom P r 0) = h r)"
- using eval_monom1
+ using eval_monom1
apply (auto intro: eval_ring_hom eval_const eval_extensional)
- apply (rule extensionalityI)
- apply (auto intro: UP_hom_unique)
- done
+ apply (rule extensionalityI)
+ apply (auto intro: UP_hom_unique)
+ done
subsection {* Sample application of evaluation homomorphism *}
@@ -1545,7 +1525,8 @@
text {*
An instantiation mechanism would now import all theorems and lemmas
valid in the context of homomorphisms between @{term INTEG} and @{term
- "UP INTEG"}. *}
+ "UP INTEG"}.
+*}
lemma INTEG_closed [intro, simp]:
"z \<in> carrier INTEG"
@@ -1562,6 +1543,4 @@
lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"
by (simp add: ring_hom_UP_cring.eval_monom [OF INTEG_id])
--- {* Calculates @{term "x = 500"} *}
-
end
--- a/src/HOL/Algebra/document/root.tex Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/document/root.tex Fri Apr 23 21:46:04 2004 +0200
@@ -2,6 +2,17 @@
\documentclass[11pt,a4paper]{article}
\usepackage{graphicx}
\usepackage{isabelle,isabellesym}
+\usepackage{amssymb}
+\usepackage[latin1]{inputenc}
+\usepackage[only,bigsqcap]{stmaryrd}
+%\usepackage{masmath}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% proper setup for best-style documents
+\urlstyle{rm}
+\isabellestyle{it}
%\usepackage{substr}
@@ -10,33 +21,6 @@
% \chapter{\BehindSubString{Chapter: }{#1}}}{%
% \section{#1}}}
-% further packages required for unusual symbols (see also isabellesym.sty)
-
-%\usepackage{latexsym} % for \<leadsto>, \<box>, \<diamond>,
- % \<sqsupset>, \<mho>, \<Join>
- % and \<lhd> and others!
-\usepackage{amssymb} % for \<lesssim>, \<greatersim>,
- % \<lessapprox>, \<greaterapprox>,
- % \<triangleq>, \<yen>, \<lozenge>
-%\usepackage[english]{babel} % for \<guillemotleft> \<guillemotright>
-\usepackage[latin1]{inputenc} % for \<onesuperior>, \<onequarter>,
- % \<twosuperior>, \<onehalf>,
- % \<threesuperior>, \<threequarters>
- % \<degree>
-\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter>
-%\usepackage{wasysym}
-%\usepackage{eufrak} % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
-%\usepackage{textcomp} % for \<zero> ... \<nine>, \<cent>
- % \<currency>
-%\usepackage{marvosym} % for \<euro>
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-% proper setup for best-style documents
-\urlstyle{rm}
-\isabellestyle{it}
-
\begin{document}
@@ -53,10 +37,6 @@
\parindent 0pt\parskip 0.5ex
-% include generated text of all theories
\input{session}
-%\bibliographystyle{abbrv}
-%\bibliography{root}
-
\end{document}