--- a/src/HOL/Algebra/AbelCoset.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy Sat Oct 10 16:26:23 2015 +0200
@@ -6,12 +6,12 @@
imports Coset Ring
begin
-subsection {* More Lifting from Groups to Abelian Groups *}
+subsection \<open>More Lifting from Groups to Abelian Groups\<close>
-subsubsection {* Definitions *}
+subsubsection \<open>Definitions\<close>
-text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come
- up with better syntax here *}
+text \<open>Hiding @{text "<+>"} from @{theory Sum_Type} until I come
+ up with better syntax here\<close>
no_notation Sum_Type.Plus (infixr "<+>" 65)
@@ -41,12 +41,12 @@
definition
A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
- --{*Actually defined for groups rather than monoids*}
+ --\<open>Actually defined for groups rather than monoids\<close>
where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
definition
a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
- --{*the kernel of a homomorphism (additive)*}
+ --\<open>the kernel of a homomorphism (additive)\<close>
where "a_kernel G H h =
kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
\<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
@@ -103,7 +103,7 @@
by (fold a_inv_def)
-subsubsection {* Cosets *}
+subsubsection \<open>Cosets\<close>
lemma (in abelian_group) a_coset_add_assoc:
"[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
@@ -163,7 +163,7 @@
by (rule group.rcosetsI [OF a_group,
folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps])
-text{*Really needed?*}
+text\<open>Really needed?\<close>
lemma (in abelian_group) a_transpose_inv:
"[| x \<oplus> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
==> (\<ominus> x) \<oplus> z = y"
@@ -179,7 +179,7 @@
*)
-subsubsection {* Subgroups *}
+subsubsection \<open>Subgroups\<close>
locale additive_subgroup =
fixes H and G (structure)
@@ -216,9 +216,9 @@
folded a_inv_def, simplified monoid_record_simps])
-subsubsection {* Additive subgroups are normal *}
+subsubsection \<open>Additive subgroups are normal\<close>
-text {* Every subgroup of an @{text "abelian_group"} is normal *}
+text \<open>Every subgroup of an @{text "abelian_group"} is normal\<close>
locale abelian_subgroup = additive_subgroup + abelian_group G +
assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
@@ -287,7 +287,7 @@
by (rule normal.inv_op_closed2 [OF a_normal,
folded a_inv_def, simplified monoid_record_simps])
-text{*Alternative characterization of normal subgroups*}
+text\<open>Alternative characterization of normal subgroups\<close>
lemma (in abelian_group) a_normal_inv_iff:
"(N \<lhd> \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>) =
(subgroup N \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
@@ -378,12 +378,12 @@
lemma (in abelian_subgroup) rcosets_add_eq:
"M \<in> a_rcosets H \<Longrightarrow> H <+> M = M"
- -- {* generalizes @{text subgroup_mult_id} *}
+ -- \<open>generalizes @{text subgroup_mult_id}\<close>
by (rule normal.rcosets_mult_eq [OF a_normal,
folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
-subsubsection {* Congruence Relation *}
+subsubsection \<open>Congruence Relation\<close>
lemma (in abelian_subgroup) a_equiv_rcong:
shows "equiv (carrier G) (racong H)"
@@ -444,7 +444,7 @@
(fast intro!: additive_subgroup.a_subgroup)+
-subsubsection {* Factorization *}
+subsubsection \<open>Factorization\<close>
lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
@@ -486,8 +486,8 @@
by (rule normal.factorgroup_is_group [OF a_normal,
folded A_FactGroup_def, simplified monoid_record_simps])
-text {* Since the Factorization is based on an \emph{abelian} subgroup, is results in
- a commutative group *}
+text \<open>Since the Factorization is based on an \emph{abelian} subgroup, is results in
+ a commutative group\<close>
theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
"comm_group (G A_Mod H)"
apply (intro comm_group.intro comm_monoid.intro) prefer 3
@@ -506,21 +506,21 @@
by (rule normal.inv_FactGroup [OF a_normal,
folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps])
-text{*The coset map is a homomorphism from @{term G} to the quotient group
- @{term "G Mod H"}*}
+text\<open>The coset map is a homomorphism from @{term G} to the quotient group
+ @{term "G Mod H"}\<close>
lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:
"(\<lambda>a. H +> a) \<in> hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> (G A_Mod H)"
by (rule normal.r_coset_hom_Mod [OF a_normal,
folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])
-text {* The isomorphism theorems have been omitted from lifting, at
- least for now *}
+text \<open>The isomorphism theorems have been omitted from lifting, at
+ least for now\<close>
-subsubsection{*The First Isomorphism Theorem*}
+subsubsection\<open>The First Isomorphism Theorem\<close>
-text{*The quotient by the kernel of a homomorphism is isomorphic to the
- range of that homomorphism.*}
+text\<open>The quotient by the kernel of a homomorphism is isomorphic to the
+ range of that homomorphism.\<close>
lemmas a_kernel_defs =
a_kernel_def kernel_def
@@ -530,7 +530,7 @@
by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
-subsubsection {* Homomorphisms *}
+subsubsection \<open>Homomorphisms\<close>
lemma abelian_group_homI:
assumes "abelian_group G"
@@ -591,7 +591,7 @@
folded a_kernel_def, simplified ring_record_simps])
done
-text{*The kernel of a homomorphism is an abelian subgroup*}
+text\<open>The kernel of a homomorphism is an abelian subgroup\<close>
lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
"abelian_subgroup (a_kernel G H h) G"
apply (rule abelian_subgroupI)
@@ -623,16 +623,16 @@
by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
-text{*If the homomorphism @{term h} is onto @{term H}, then so is the
-homomorphism from the quotient group*}
+text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
+homomorphism from the quotient group\<close>
lemma (in abelian_group_hom) A_FactGroup_onto:
assumes h: "h ` carrier G = carrier H"
shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
by (rule group_hom.FactGroup_onto[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
-text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
- quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
+text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
+ quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
theorem (in abelian_group_hom) A_FactGroup_iso:
"h ` carrier G = carrier H
\<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
@@ -641,9 +641,9 @@
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
-subsubsection {* Cosets *}
+subsubsection \<open>Cosets\<close>
-text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
+text \<open>Not eveything from \texttt{CosetExt.thy} is lifted here.\<close>
lemma (in additive_subgroup) a_Hcarr [simp]:
assumes hH: "h \<in> H"
@@ -725,7 +725,7 @@
folded A_RCOSETS_def, simplified monoid_record_simps])
-subsubsection {* Addition of Subgroups *}
+subsubsection \<open>Addition of Subgroups\<close>
lemma (in abelian_monoid) set_add_closed:
assumes Acarr: "A \<subseteq> carrier G"
--- a/src/HOL/Algebra/Bij.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Bij.thy Sat Oct 10 16:26:23 2015 +0200
@@ -6,11 +6,11 @@
imports Group
begin
-section {* Bijections of a Set, Permutation and Automorphism Groups *}
+section \<open>Bijections of a Set, Permutation and Automorphism Groups\<close>
definition
Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
- --{*Only extensional functions, since otherwise we get too many.*}
+ --\<open>Only extensional functions, since otherwise we get too many.\<close>
where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
definition
@@ -30,7 +30,7 @@
by (auto simp add: Bij_def bij_betw_imp_funcset)
-subsection {*Bijections Form a Group *}
+subsection \<open>Bijections Form a Group\<close>
lemma restrict_inv_into_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_into S f) x) \<in> Bij S"
by (simp add: Bij_def bij_betw_inv_into)
@@ -57,7 +57,7 @@
done
-subsection{*Automorphisms Form a Group*}
+subsection\<open>Automorphisms Form a Group\<close>
lemma Bij_inv_into_mem: "\<lbrakk> f \<in> Bij S; x \<in> S\<rbrakk> \<Longrightarrow> inv_into S f x \<in> S"
by (simp add: Bij_def bij_betw_def inv_into_into)
--- a/src/HOL/Algebra/Congruence.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Congruence.thy Sat Oct 10 16:26:23 2015 +0200
@@ -7,15 +7,15 @@
imports Main
begin
-section {* Objects *}
+section \<open>Objects\<close>
-subsection {* Structure with Carrier Set. *}
+subsection \<open>Structure with Carrier Set.\<close>
record 'a partial_object =
carrier :: "'a set"
-subsection {* Structure with Carrier and Equivalence Relation @{text eq} *}
+subsection \<open>Structure with Carrier and Equivalence Relation @{text eq}\<close>
record 'a eq_object = "'a partial_object" +
eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
--- a/src/HOL/Algebra/Coset.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Coset.thy Sat Oct 10 16:26:23 2015 +0200
@@ -8,7 +8,7 @@
imports Group
begin
-section {*Cosets and Quotient Groups*}
+section \<open>Cosets and Quotient Groups\<close>
definition
r_coset :: "[_, 'a set, 'a] \<Rightarrow> 'a set" (infixl "#>\<index>" 60)
@@ -39,7 +39,7 @@
"H \<lhd> G \<equiv> normal H G"
-subsection {*Basic Properties of Cosets*}
+subsection \<open>Basic Properties of Cosets\<close>
lemma (in group) coset_mult_assoc:
"[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
@@ -85,7 +85,7 @@
lemma (in group) coset_join2:
"\<lbrakk>x \<in> carrier G; subgroup H G; x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
- --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
+ --\<open>Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.\<close>
by (force simp add: subgroup.m_closed r_coset_def solve_equation)
lemma (in monoid) r_coset_subset_G:
@@ -100,7 +100,7 @@
"\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
by (auto simp add: RCOSETS_def)
-text{*Really needed?*}
+text\<open>Really needed?\<close>
lemma (in group) transpose_inv:
"[| x \<otimes> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
==> (inv x) \<otimes> z = y"
@@ -112,7 +112,7 @@
subgroup.one_closed)
done
-text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
+text (in group) \<open>Opposite of @{thm [source] "repr_independence"}\<close>
lemma (in group) repr_independenceD:
assumes "subgroup H G"
assumes ycarr: "y \<in> carrier G"
@@ -127,7 +127,7 @@
done
qed
-text {* Elements of a right coset are in the carrier *}
+text \<open>Elements of a right coset are in the carrier\<close>
lemma (in subgroup) elemrcos_carrier:
assumes "group G"
assumes acarr: "a \<in> carrier G"
@@ -171,7 +171,7 @@
qed
qed
-text {* Step one for lemma @{text "rcos_module"} *}
+text \<open>Step one for lemma @{text "rcos_module"}\<close>
lemma (in subgroup) rcos_module_imp:
assumes "group G"
assumes xcarr: "x \<in> carrier G"
@@ -211,7 +211,7 @@
show "x' \<otimes> (inv x) \<in> H" by simp
qed
-text {* Step two for lemma @{text "rcos_module"} *}
+text \<open>Step two for lemma @{text "rcos_module"}\<close>
lemma (in subgroup) rcos_module_rev:
assumes "group G"
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
@@ -243,7 +243,7 @@
by fast
qed
-text {* Module property of right cosets *}
+text \<open>Module property of right cosets\<close>
lemma (in subgroup) rcos_module:
assumes "group G"
assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
@@ -262,7 +262,7 @@
qed
qed
-text {* Right cosets are subsets of the carrier. *}
+text \<open>Right cosets are subsets of the carrier.\<close>
lemma (in subgroup) rcosets_carrier:
assumes "group G"
assumes XH: "X \<in> rcosets H"
@@ -283,7 +283,7 @@
by (rule r_coset_subset_G)
qed
-text {* Multiplication of general subsets *}
+text \<open>Multiplication of general subsets\<close>
lemma (in monoid) set_mult_closed:
assumes Acarr: "A \<subseteq> carrier G"
and Bcarr: "B \<subseteq> carrier G"
@@ -381,7 +381,7 @@
qed
-subsection {* Normal subgroups *}
+subsection \<open>Normal subgroups\<close>
lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
by (simp add: normal_def subgroup_def)
@@ -407,7 +407,7 @@
apply (blast intro: inv_op_closed1)
done
-text{*Alternative characterization of normal subgroups*}
+text\<open>Alternative characterization of normal subgroups\<close>
lemma (in group) normal_inv_iff:
"(N \<lhd> G) =
(subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
@@ -456,7 +456,7 @@
qed
-subsection{*More Properties of Cosets*}
+subsection\<open>More Properties of Cosets\<close>
lemma (in group) lcos_m_assoc:
"[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
@@ -524,7 +524,7 @@
done
-subsubsection {* Set of Inverses of an @{text r_coset}. *}
+subsubsection \<open>Set of Inverses of an @{text r_coset}.\<close>
lemma (in normal) rcos_inv:
assumes x: "x \<in> carrier G"
@@ -549,7 +549,7 @@
qed
-subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
+subsubsection \<open>Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.\<close>
lemma (in group) setmult_rcos_assoc:
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
@@ -584,12 +584,12 @@
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
- -- {* generalizes @{text subgroup_mult_id} *}
+ -- \<open>generalizes @{text subgroup_mult_id}\<close>
by (auto simp add: RCOSETS_def subset
setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
-subsubsection{*An Equivalence Relation*}
+subsubsection\<open>An Equivalence Relation\<close>
definition
r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set" ("rcong\<index> _")
@@ -628,9 +628,9 @@
qed
qed
-text{*Equivalence classes of @{text rcong} correspond to left cosets.
+text\<open>Equivalence classes of @{text rcong} correspond to left cosets.
Was there a mistake in the definitions? I'd have expected them to
- correspond to right cosets.*}
+ correspond to right cosets.\<close>
(* CB: This is correct, but subtle.
We call H #> a the right coset of a relative to H. According to
@@ -652,7 +652,7 @@
qed
-subsubsection{*Two Distinct Right Cosets are Disjoint*}
+subsubsection\<open>Two Distinct Right Cosets are Disjoint\<close>
lemma (in group) rcos_equation:
assumes "subgroup H G"
@@ -679,9 +679,9 @@
qed
-subsection {* Further lemmas for @{text "r_congruent"} *}
+subsection \<open>Further lemmas for @{text "r_congruent"}\<close>
-text {* The relation is a congruence *}
+text \<open>The relation is a congruence\<close>
lemma (in normal) congruent_rcong:
shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
@@ -753,7 +753,7 @@
qed
-subsection {*Order of a Group and Lagrange's Theorem*}
+subsection \<open>Order of a Group and Lagrange's Theorem\<close>
definition
order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
@@ -777,7 +777,7 @@
apply (simp add: r_coset_subset_G [THEN finite_subset])
done
-text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
+text\<open>The next two lemmas support the proof of @{text card_cosets_equal}.\<close>
lemma (in group) inj_on_f:
"\<lbrakk>H \<subseteq> carrier G; a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
apply (rule inj_onI)
@@ -799,7 +799,7 @@
apply (force simp add: m_assoc subsetD r_coset_def)
apply (rule inj_on_g, assumption+)
apply (force simp add: m_assoc subsetD r_coset_def)
- txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
+ txt\<open>The sets @{term "H #> a"} and @{term "H"} are finite.\<close>
apply (simp add: r_coset_subset_G [THEN finite_subset])
apply (blast intro: finite_subset)
done
@@ -824,11 +824,11 @@
done
-subsection {*Quotient Groups: Factorization of a Group*}
+subsection \<open>Quotient Groups: Factorization of a Group\<close>
definition
FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
- --{*Actually defined for groups rather than monoids*}
+ --\<open>Actually defined for groups rather than monoids\<close>
where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
lemma (in normal) setmult_closed:
@@ -880,21 +880,21 @@
apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
done
-text{*The coset map is a homomorphism from @{term G} to the quotient group
- @{term "G Mod H"}*}
+text\<open>The coset map is a homomorphism from @{term G} to the quotient group
+ @{term "G Mod H"}\<close>
lemma (in normal) r_coset_hom_Mod:
"(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
-subsection{*The First Isomorphism Theorem*}
+subsection\<open>The First Isomorphism Theorem\<close>
-text{*The quotient by the kernel of a homomorphism is isomorphic to the
- range of that homomorphism.*}
+text\<open>The quotient by the kernel of a homomorphism is isomorphic to the
+ range of that homomorphism.\<close>
definition
kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
- --{*the kernel of a homomorphism*}
+ --\<open>the kernel of a homomorphism\<close>
where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
@@ -902,7 +902,7 @@
apply (auto simp add: kernel_def group.intro is_group)
done
-text{*The kernel of a homomorphism is a normal subgroup*}
+text\<open>The kernel of a homomorphism is a normal subgroup\<close>
lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
apply (simp add: G.normal_inv_iff subgroup_kernel)
apply (simp add: kernel_def)
@@ -957,7 +957,7 @@
qed
-text{*Lemma for the following injectivity result*}
+text\<open>Lemma for the following injectivity result\<close>
lemma (in group_hom) FactGroup_subset:
"\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
\<Longrightarrow> kernel G H h #> g \<subseteq> kernel G H h #> g'"
@@ -986,8 +986,8 @@
show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
qed
-text{*If the homomorphism @{term h} is onto @{term H}, then so is the
-homomorphism from the quotient group*}
+text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
+homomorphism from the quotient group\<close>
lemma (in group_hom) FactGroup_onto:
assumes h: "h ` carrier G = carrier H"
shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
@@ -1008,8 +1008,8 @@
qed
-text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
- quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
+text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
+ quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
theorem (in group_hom) FactGroup_iso:
"h ` carrier G = carrier H
\<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
--- a/src/HOL/Algebra/Divisibility.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,15 +3,15 @@
Author: Stephan Hohe
*)
-section {* Divisibility in monoids and rings *}
+section \<open>Divisibility in monoids and rings\<close>
theory Divisibility
imports "~~/src/HOL/Library/Permutation" Coset Group
begin
-section {* Factorial Monoids *}
-
-subsection {* Monoids with Cancellation Law *}
+section \<open>Factorial Monoids\<close>
+
+subsection \<open>Monoids with Cancellation Law\<close>
locale monoid_cancel = monoid +
assumes l_cancel:
@@ -57,7 +57,7 @@
..
-subsection {* Products of Units in Monoids *}
+subsection \<open>Products of Units in Monoids\<close>
lemma (in monoid) Units_m_closed[simp, intro]:
assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G"
@@ -144,9 +144,9 @@
qed
-subsection {* Divisibility and Association *}
-
-subsubsection {* Function definitions *}
+subsection \<open>Divisibility and Association\<close>
+
+subsubsection \<open>Function definitions\<close>
definition
factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
@@ -174,7 +174,7 @@
(\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides\<^bsub>G\<^esub> (a \<otimes>\<^bsub>G\<^esub> b) \<longrightarrow> p divides\<^bsub>G\<^esub> a \<or> p divides\<^bsub>G\<^esub> b)"
-subsubsection {* Divisibility *}
+subsubsection \<open>Divisibility\<close>
lemma dividesI:
fixes G (structure)
@@ -309,7 +309,7 @@
by (fast dest: divides_unit intro: unit_divides)
-subsubsection {* Association *}
+subsubsection \<open>Association\<close>
lemma associatedI:
fixes G (structure)
@@ -449,7 +449,7 @@
done
-subsubsection {* Division and associativity *}
+subsubsection \<open>Division and associativity\<close>
lemma divides_antisym:
fixes G (structure)
@@ -497,7 +497,7 @@
done
-subsubsection {* Multiplication and associativity *}
+subsubsection \<open>Multiplication and associativity\<close>
lemma (in monoid_cancel) mult_cong_r:
assumes "b \<sim> b'"
@@ -545,7 +545,7 @@
done
-subsubsection {* Units *}
+subsubsection \<open>Units\<close>
lemma (in monoid_cancel) assoc_unit_l [trans]:
assumes asc: "a \<sim> b" and bunit: "b \<in> Units G"
@@ -604,7 +604,7 @@
done
-subsubsection {* Proper factors *}
+subsubsection \<open>Proper factors\<close>
lemma properfactorI:
fixes G (structure)
@@ -785,9 +785,9 @@
by (intro properfactor_trans2[OF ab] divides_prod_l, simp+)
-subsection {* Irreducible Elements and Primes *}
-
-subsubsection {* Irreducible elements *}
+subsection \<open>Irreducible Elements and Primes\<close>
+
+subsubsection \<open>Irreducible elements\<close>
lemma irreducibleI:
fixes G (structure)
@@ -903,7 +903,7 @@
qed
-subsubsection {* Prime elements *}
+subsubsection \<open>Prime elements\<close>
lemma primeI:
fixes G (structure)
@@ -943,9 +943,9 @@
apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed)
done
-subsection {* Factorization and Factorial Monoids *}
-
-subsubsection {* Function definitions *}
+subsection \<open>Factorization and Factorial Monoids\<close>
+
+subsubsection \<open>Function definitions\<close>
definition
factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
@@ -972,9 +972,9 @@
set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
-subsubsection {* Comparing lists of elements *}
-
-text {* Association on lists *}
+subsubsection \<open>Comparing lists of elements\<close>
+
+text \<open>Association on lists\<close>
lemma (in monoid) listassoc_refl [simp, intro]:
assumes "set as \<subseteq> carrier G"
@@ -1019,7 +1019,7 @@
done
-text {* Permutations *}
+text \<open>Permutations\<close>
lemma perm_map [intro]:
assumes p: "a <~~> b"
@@ -1077,7 +1077,7 @@
perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"]
-text {* Essentially equal factorizations *}
+text \<open>Essentially equal factorizations\<close>
lemma (in monoid) essentially_equalI:
assumes ex: "fs1 <~~> fs1'" "fs1' [\<sim>] fs2"
@@ -1149,9 +1149,9 @@
qed
-subsubsection {* Properties of lists of elements *}
-
-text {* Multiplication of factors in a list *}
+subsubsection \<open>Properties of lists of elements\<close>
+
+text \<open>Multiplication of factors in a list\<close>
lemma (in monoid) multlist_closed [simp, intro]:
assumes ascarr: "set fs \<subseteq> carrier G"
@@ -1224,7 +1224,7 @@
done
-subsubsection {* Factorization in irreducible elements *}
+subsubsection \<open>Factorization in irreducible elements\<close>
lemma wfactorsI:
fixes G (structure)
@@ -1328,7 +1328,7 @@
qed
-text {* Comparing wfactors *}
+text \<open>Comparing wfactors\<close>
lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:
assumes fact: "wfactors G fs a"
@@ -1389,7 +1389,7 @@
qed
-subsubsection {* Essentially equal factorizations *}
+subsubsection \<open>Essentially equal factorizations\<close>
lemma (in comm_monoid_cancel) unitfactor_ee:
assumes uunit: "u \<in> Units G"
@@ -1719,7 +1719,7 @@
qed
-subsubsection {* Factorial monoids and wfactors *}
+subsubsection \<open>Factorial monoids and wfactors\<close>
lemma (in comm_monoid_cancel) factorial_monoidI:
assumes wfactors_exists:
@@ -1782,9 +1782,9 @@
qed (blast intro: factors_wfactors wfactors_unique)
-subsection {* Factorizations as Multisets *}
-
-text {* Gives useful operations like intersection *}
+subsection \<open>Factorizations as Multisets\<close>
+
+text \<open>Gives useful operations like intersection\<close>
(* FIXME: use class_of x instead of closure_of {x} *)
@@ -1795,7 +1795,7 @@
"fmset G as = mset (map (\<lambda>a. assocs G a) as)"
-text {* Helper lemmas *}
+text \<open>Helper lemmas\<close>
lemma (in monoid) assocs_repr_independence:
assumes "y \<in> assocs G x"
@@ -1834,7 +1834,7 @@
assocs_repr_independenceD[THEN assocs_assoc]
-subsubsection {* Comparing multisets *}
+subsubsection \<open>Comparing multisets\<close>
lemma (in monoid) fmset_perm_cong:
assumes prm: "as <~~> bs"
@@ -2022,7 +2022,7 @@
by (fast intro: ee_fmset fmset_ee)
-subsubsection {* Interpreting multisets as factorizations *}
+subsubsection \<open>Interpreting multisets as factorizations\<close>
lemma (in monoid) mset_fmsetEx:
assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"
@@ -2089,7 +2089,7 @@
qed
-subsubsection {* Multiplication on multisets *}
+subsubsection \<open>Multiplication on multisets\<close>
lemma (in factorial_monoid) mult_wfactors_fmset:
assumes afs: "wfactors G as a" and bfs: "wfactors G bs b" and cfs: "wfactors G cs (a \<otimes> b)"
@@ -2131,7 +2131,7 @@
qed
-subsubsection {* Divisibility on multisets *}
+subsubsection \<open>Divisibility on multisets\<close>
lemma (in factorial_monoid) divides_fmsubset:
assumes ab: "a divides b"
@@ -2215,7 +2215,7 @@
by (blast intro: divides_fmsubset fmsubset_divides)
-text {* Proper factors on multisets *}
+text \<open>Proper factors on multisets\<close>
lemma (in factorial_monoid) fmset_properfactor:
assumes asubb: "fmset G as \<le># fmset G bs"
@@ -2250,7 +2250,7 @@
apply (metis assms divides_fmsubset fmsubset_divides)
done
-subsection {* Irreducible Elements are Prime *}
+subsection \<open>Irreducible Elements are Prime\<close>
lemma (in factorial_monoid) irreducible_is_prime:
assumes pirr: "irreducible G p"
@@ -2490,9 +2490,9 @@
qed
-subsection {* Greatest Common Divisors and Lowest Common Multiples *}
-
-subsubsection {* Definitions *}
+subsection \<open>Greatest Common Divisors and Lowest Common Multiples\<close>
+
+subsubsection \<open>Definitions\<close>
definition
isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ gcdof\<index> _ _)" [81,81,81] 80)
@@ -2529,7 +2529,7 @@
"wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"
-subsubsection {* Connections to \texttt{Lattice.thy} *}
+subsubsection \<open>Connections to \texttt{Lattice.thy}\<close>
lemma gcdof_greatestLower:
fixes G (structure)
@@ -2571,7 +2571,7 @@
by fast
-subsubsection {* Existence of gcd and lcm *}
+subsubsection \<open>Existence of gcd and lcm\<close>
lemma (in factorial_monoid) gcdof_exists:
assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
@@ -2753,9 +2753,9 @@
qed
-subsection {* Conditions for Factoriality *}
-
-subsubsection {* Gcd condition *}
+subsection \<open>Conditions for Factoriality\<close>
+
+subsubsection \<open>Gcd condition\<close>
lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
shows "weak_lower_semilattice (division_rel G)"
@@ -3153,7 +3153,7 @@
by (rule primeness_condition)
-subsubsection {* Divisor chain condition *}
+subsubsection \<open>Divisor chain condition\<close>
lemma (in divisor_chain_condition_monoid) wfactors_exist:
assumes acarr: "a \<in> carrier G"
@@ -3243,7 +3243,7 @@
qed
-subsubsection {* Primeness condition *}
+subsubsection \<open>Primeness condition\<close>
lemma (in comm_monoid_cancel) multlist_prime_pos:
assumes carr: "a \<in> carrier G" "set as \<subseteq> carrier G"
@@ -3481,9 +3481,9 @@
done
-subsubsection {* Application to factorial monoids *}
-
-text {* Number of factors for wellfoundedness *}
+subsubsection \<open>Application to factorial monoids\<close>
+
+text \<open>Number of factors for wellfoundedness\<close>
definition
factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
@@ -3678,7 +3678,7 @@
qed
-subsection {* Factoriality Theorems *}
+subsection \<open>Factoriality Theorems\<close>
theorem factorial_condition_one: (* Jacobson theorem 2.21 *)
shows "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) =
--- a/src/HOL/Algebra/Exponent.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Exponent.thy Sat Oct 10 16:26:23 2015 +0200
@@ -9,16 +9,16 @@
imports Main "~~/src/HOL/Number_Theory/Primes"
begin
-section {*Sylow's Theorem*}
+section \<open>Sylow's Theorem\<close>
-subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}
+subsection \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
definition
exponent :: "nat => nat => nat"
where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
-text{*Prime Theorems*}
+text\<open>Prime Theorems\<close>
lemma prime_iff:
"(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
@@ -100,7 +100,7 @@
done
-text{*Exponent Theorems*}
+text\<open>Exponent Theorems\<close>
lemma exponent_ge [rule_format]:
"[|p^k dvd n; prime p; 0<n|] ==> k <= exponent p n"
@@ -182,7 +182,7 @@
done
-text{*Main Combinatorial Argument*}
+text\<open>Main Combinatorial Argument\<close>
lemma gcd_mult': fixes a::nat shows "gcd b (a * b) = b"
by (simp add: mult.commute[of a b])
@@ -236,7 +236,7 @@
apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
done
-text{*Suc rules that we have to delete from the simpset*}
+text\<open>Suc rules that we have to delete from the simpset\<close>
lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
(*The bound K is needed; otherwise it's too weak to be used.*)
@@ -252,9 +252,9 @@
prefer 2 apply (simp, clarify)
apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) =
exponent p (Suc k)")
- txt{*First, use the assumed equation. We simplify the LHS to
+ txt\<open>First, use the assumed equation. We simplify the LHS to
@{term "exponent p (Suc (j + k) choose Suc k) + exponent p (Suc k)"}
- the common terms cancel, proving the conclusion.*}
+ the common terms cancel, proving the conclusion.\<close>
apply (simp del: bad_Sucs add: exponent_mult_add)
apply (simp del: bad_Sucs add: mult_ac Suc_times_binomial exponent_mult_add)
@@ -297,14 +297,14 @@
prefer 2 apply simp
apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
prefer 2 apply (force simp add: prime_iff)
-txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
+txt\<open>A similar trick to the one used in @{text p_not_div_choose_lemma}:
insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
first
- transform the binomial coefficient, then use @{text exponent_mult_add}.*}
+ transform the binomial coefficient, then use @{text exponent_mult_add}.\<close>
apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
a + exponent p m")
apply (simp add: exponent_mult_add)
-txt{*one subgoal left!*}
+txt\<open>one subgoal left!\<close>
apply (auto simp: mult_ac)
apply (subst times_binomial_minus1_eq, simp)
apply (simp add: diff_le_mono exponent_mult_add)
--- a/src/HOL/Algebra/FiniteProduct.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Sat Oct 10 16:26:23 2015 +0200
@@ -8,14 +8,14 @@
imports Group
begin
-subsection {* Product Operator for Commutative Monoids *}
+subsection \<open>Product Operator for Commutative Monoids\<close>
-subsubsection {* Inductive Definition of a Relation for Products over Sets *}
+subsubsection \<open>Inductive Definition of a Relation for Products over Sets\<close>
-text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
+text \<open>Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
possible, because here we have explicit typing rules like
@{text "x \<in> carrier G"}. We introduce an explicit argument for the domain
- @{text D}. *}
+ @{text D}.\<close>
inductive_set
foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
@@ -61,7 +61,7 @@
qed
-text {* Left-Commutative Operations *}
+text \<open>Left-Commutative Operations\<close>
locale LCD =
fixes B :: "'b set"
@@ -111,7 +111,7 @@
apply (erule foldSetD.cases)
apply blast
apply clarify
- txt {* force simplification of @{text "card A < card (insert ...)"}. *}
+ txt \<open>force simplification of @{text "card A < card (insert ...)"}.\<close>
apply (erule rev_mp)
apply (simp add: less_Suc_eq_le)
apply (rule impI)
@@ -119,7 +119,7 @@
apply (subgoal_tac "Aa = Ab")
prefer 2 apply (blast elim!: equalityE)
apply blast
- txt {* case @{prop "xa \<notin> xb"}. *}
+ txt \<open>case @{prop "xa \<notin> xb"}.\<close>
apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb \<in> Aa & xa \<in> Ab")
prefer 2 apply (blast elim!: equalityE)
apply clarify
@@ -221,7 +221,7 @@
==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
by (simp add: foldD_nest_Un_Int)
--- {* Delete rules to do with @{text foldSetD} relation. *}
+-- \<open>Delete rules to do with @{text foldSetD} relation.\<close>
declare foldSetD_imp_finite [simp del]
empty_foldSetDE [rule del]
@@ -230,12 +230,12 @@
foldSetD_closed [rule del]
-text {* Commutative Monoids *}
+text \<open>Commutative Monoids\<close>
-text {*
+text \<open>
We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
instead of @{text "'b => 'a => 'a"}.
-*}
+\<close>
locale ACeD =
fixes D :: "'a set"
@@ -263,7 +263,7 @@
proof -
assume "x \<in> D"
then have "x \<cdot> e = x" by (rule ident)
- with `x \<in> D` show ?thesis by (simp add: commute)
+ with \<open>x \<in> D\<close> show ?thesis by (simp add: commute)
qed
lemma (in ACeD) foldD_Un_Int:
@@ -285,7 +285,7 @@
left_commute LCD.foldD_closed [OF LCD.intro [of D]])
-subsubsection {* Products over Finite Sets *}
+subsubsection \<open>Products over Finite Sets\<close>
definition
finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
@@ -299,7 +299,7 @@
("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
translations
"\<Otimes>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finprod \<struct>\<index> (%i. b) A"
- -- {* Beware of argument permutation! *}
+ -- \<open>Beware of argument permutation!\<close>
lemma (in comm_monoid) finprod_empty [simp]:
"finprod G f {} = \<one>"
@@ -367,7 +367,7 @@
"[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
finprod G g A \<otimes> finprod G g B"
--- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
+-- \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
proof (induct set: finite)
case empty then show ?case by simp
next
@@ -450,12 +450,12 @@
(* This order of prems is slightly faster (3%) than the last two swapped. *)
by (rule finprod_cong') (auto simp add: simp_implies_def)
-text {*Usually, if this rule causes a failed congruence proof error,
+text \<open>Usually, if this rule causes a failed congruence proof error,
the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
Adding @{thm [source] Pi_def} to the simpset is often useful.
For this reason, @{thm [source] finprod_cong}
is not added to the simpset by default.
-*}
+\<close>
end
@@ -497,7 +497,7 @@
case (infinite A)
hence "\<not> finite (h ` A)"
using finite_imageD by blast
- with `\<not> finite A` show ?case by simp
+ with \<open>\<not> finite A\<close> show ?case by simp
qed (auto simp add: Pi_def)
lemma finprod_const:
--- a/src/HOL/Algebra/Group.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Group.thy Sat Oct 10 16:26:23 2015 +0200
@@ -8,13 +8,13 @@
imports Lattice "~~/src/HOL/Library/FuncSet"
begin
-section {* Monoids and Groups *}
+section \<open>Monoids and Groups\<close>
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
-text {*
+text \<open>
Definitions follow @{cite "Jacobson:1985"}.
-*}
+\<close>
record 'a monoid = "'a partial_object" +
mult :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
@@ -26,7 +26,7 @@
definition
Units :: "_ => 'a set"
- --{*The set of invertible elements*}
+ --\<open>The set of invertible elements\<close>
where "Units G = {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
consts
@@ -187,7 +187,7 @@
with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
qed
-text {* Power *}
+text \<open>Power\<close>
lemma (in monoid) nat_pow_closed [intro, simp]:
"x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
@@ -218,11 +218,11 @@
(* Jacobson defines the order of a monoid here. *)
-subsection {* Groups *}
+subsection \<open>Groups\<close>
-text {*
+text \<open>
A group is a monoid all of whose elements are invertible.
-*}
+\<close>
locale group = monoid +
assumes Units: "carrier G <= Units G"
@@ -321,7 +321,7 @@
using Units_l_inv by simp
-subsection {* Cancellation Laws and Basic Properties *}
+subsection \<open>Cancellation Laws and Basic Properties\<close>
lemma (in group) l_cancel [simp]:
"[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
@@ -397,7 +397,7 @@
"\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> a = b \<otimes> inv c \<longleftrightarrow> b = a \<otimes> c"
by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
-text {* Power *}
+text \<open>Power\<close>
lemma (in group) int_pow_def2:
"a (^) (z::int) = (if z < 0 then inv (a (^) (nat (-z))) else a (^) (nat z))"
@@ -435,7 +435,7 @@
qed
-subsection {* Subgroups *}
+subsection \<open>Subgroups\<close>
locale subgroup =
fixes H and G (structure)
@@ -469,18 +469,18 @@
done
qed
-text {*
+text \<open>
Since @{term H} is nonempty, it contains some element @{term x}. Since
it is closed under inverse, it contains @{text "inv x"}. Since
it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.
-*}
+\<close>
lemma (in group) one_in_subset:
"[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |]
==> \<one> \<in> H"
by force
-text {* A characterization of subgroups: closed, non-empty subset. *}
+text \<open>A characterization of subgroups: closed, non-empty subset.\<close>
lemma (in group) subgroupI:
assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
@@ -513,7 +513,7 @@
*)
-subsection {* Direct Products *}
+subsection \<open>Direct Products\<close>
definition
DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
@@ -533,7 +533,7 @@
qed
-text{*Does not use the previous result because it's easier just to use auto.*}
+text\<open>Does not use the previous result because it's easier just to use auto.\<close>
lemma DirProd_group:
assumes "group G" and "group H"
shows "group (G \<times>\<times> H)"
@@ -571,7 +571,7 @@
qed
-subsection {* Homomorphisms and Isomorphisms *}
+subsection \<open>Homomorphisms and Isomorphisms\<close>
definition
hom :: "_ => _ => ('a => 'b) set" where
@@ -611,8 +611,8 @@
by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
-text{*Basis for homomorphism proofs: we assume two groups @{term G} and
- @{term H}, with a homomorphism @{term h} between them*}
+text\<open>Basis for homomorphism proofs: we assume two groups @{term G} and
+ @{term H}, with a homomorphism @{term h} between them\<close>
locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
fixes h
assumes homh: "h \<in> hom G H"
@@ -665,13 +665,13 @@
unfolding hom_def by (simp add: int_pow_mult)
-subsection {* Commutative Structures *}
+subsection \<open>Commutative Structures\<close>
-text {*
+text \<open>
Naming convention: multiplicative structures that are commutative
are called \emph{commutative}, additive structures are called
\emph{Abelian}.
-*}
+\<close>
locale comm_monoid = monoid +
assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
@@ -753,9 +753,9 @@
by (simp add: m_ac inv_mult_group)
-subsection {* The Lattice of Subgroups of a Group *}
+subsection \<open>The Lattice of Subgroups of a Group\<close>
-text_raw {* \label{sec:subgroup-lattice} *}
+text_raw \<open>\label{sec:subgroup-lattice}\<close>
theorem (in group) subgroups_partial_order:
"partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
--- a/src/HOL/Algebra/Ideal.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Ideal.thy Sat Oct 10 16:26:23 2015 +0200
@@ -6,11 +6,11 @@
imports Ring AbelCoset
begin
-section {* Ideals *}
+section \<open>Ideals\<close>
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
-subsubsection {* General definition *}
+subsubsection \<open>General definition\<close>
locale ideal = additive_subgroup I R + ring R for I and R (structure) +
assumes I_l_closed: "\<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
@@ -44,12 +44,12 @@
qed
-subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
+subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>
definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)
where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
-subsubsection {* Principal Ideals *}
+subsubsection \<open>Principal Ideals\<close>
locale principalideal = ideal +
assumes generate: "\<exists>i \<in> carrier R. I = Idl {i}"
@@ -70,7 +70,7 @@
qed
-subsubsection {* Maximal Ideals *}
+subsubsection \<open>Maximal Ideals\<close>
locale maximalideal = ideal +
assumes I_notcarr: "carrier R \<noteq> I"
@@ -93,7 +93,7 @@
qed
-subsubsection {* Prime Ideals *}
+subsubsection \<open>Prime Ideals\<close>
locale primeideal = ideal + cring +
assumes I_notcarr: "carrier R \<noteq> I"
@@ -140,7 +140,7 @@
qed
-subsection {* Special Ideals *}
+subsection \<open>Special Ideals\<close>
lemma (in ring) zeroideal: "ideal {\<zero>} R"
apply (intro idealI subgroup.intro)
@@ -166,7 +166,7 @@
qed
-subsection {* General Ideal Properies *}
+subsection \<open>General Ideal Properies\<close>
lemma (in ideal) one_imp_carrier:
assumes I_one_closed: "\<one> \<in> I"
@@ -187,10 +187,10 @@
using iI by (rule a_Hcarr)
-subsection {* Intersection of Ideals *}
+subsection \<open>Intersection of Ideals\<close>
-text {* \paragraph{Intersection of two ideals} The intersection of any
- two ideals is again an ideal in @{term R} *}
+text \<open>\paragraph{Intersection of two ideals} The intersection of any
+ two ideals is again an ideal in @{term R}\<close>
lemma (in ring) i_intersect:
assumes "ideal I R"
assumes "ideal J R"
@@ -212,8 +212,8 @@
done
qed
-text {* The intersection of any Number of Ideals is again
- an Ideal in @{term R} *}
+text \<open>The intersection of any Number of Ideals is again
+ an Ideal in @{term R}\<close>
lemma (in ring) i_Intersect:
assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"
and notempty: "S \<noteq> {}"
@@ -291,7 +291,7 @@
qed
-subsection {* Addition of Ideals *}
+subsection \<open>Addition of Ideals\<close>
lemma (in ring) add_ideals:
assumes idealI: "ideal I R"
@@ -335,9 +335,9 @@
qed
-subsection (in ring) {* Ideals generated by a subset of @{term "carrier R"} *}
+subsection (in ring) \<open>Ideals generated by a subset of @{term "carrier R"}\<close>
-text {* @{term genideal} generates an ideal *}
+text \<open>@{term genideal} generates an ideal\<close>
lemma (in ring) genideal_ideal:
assumes Scarr: "S \<subseteq> carrier R"
shows "ideal (Idl S) R"
@@ -360,14 +360,14 @@
then show "i \<in> Idl {i}" by fast
qed
-text {* @{term genideal} generates the minimal ideal *}
+text \<open>@{term genideal} generates the minimal ideal\<close>
lemma (in ring) genideal_minimal:
assumes a: "ideal I R"
and b: "S \<subseteq> I"
shows "Idl S \<subseteq> I"
unfolding genideal_def by rule (elim InterD, simp add: a b)
-text {* Generated ideals and subsets *}
+text \<open>Generated ideals and subsets\<close>
lemma (in ring) Idl_subset_ideal:
assumes Iideal: "ideal I R"
and Hcarr: "H \<subseteq> carrier R"
@@ -425,12 +425,12 @@
qed
-text {* Generation of Principal Ideals in Commutative Rings *}
+text \<open>Generation of Principal Ideals in Commutative Rings\<close>
definition cgenideal :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("PIdl\<index> _" [80] 79)
where "cgenideal R a = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
-text {* genhideal (?) really generates an ideal *}
+text \<open>genhideal (?) really generates an ideal\<close>
lemma (in cring) cgenideal_ideal:
assumes acarr: "a \<in> carrier R"
shows "ideal (PIdl a) R"
@@ -499,7 +499,7 @@
by fast
qed
-text {* @{const "cgenideal"} is minimal *}
+text \<open>@{const "cgenideal"} is minimal\<close>
lemma (in ring) cgenideal_minimal:
assumes "ideal J R"
@@ -544,7 +544,7 @@
qed
-subsection {* Union of Ideals *}
+subsection \<open>Union of Ideals\<close>
lemma (in ring) union_genideal:
assumes idealI: "ideal I R"
@@ -589,16 +589,16 @@
qed
-subsection {* Properties of Principal Ideals *}
+subsection \<open>Properties of Principal Ideals\<close>
-text {* @{text "\<zero>"} generates the zero ideal *}
+text \<open>@{text "\<zero>"} generates the zero ideal\<close>
lemma (in ring) zero_genideal: "Idl {\<zero>} = {\<zero>}"
apply rule
apply (simp add: genideal_minimal zeroideal)
apply (fast intro!: genideal_self)
done
-text {* @{text "\<one>"} generates the unit ideal *}
+text \<open>@{text "\<one>"} generates the unit ideal\<close>
lemma (in ring) one_genideal: "Idl {\<one>} = carrier R"
proof -
have "\<one> \<in> Idl {\<one>}"
@@ -608,14 +608,14 @@
qed
-text {* The zero ideal is a principal ideal *}
+text \<open>The zero ideal is a principal ideal\<close>
corollary (in ring) zeropideal: "principalideal {\<zero>} R"
apply (rule principalidealI)
apply (rule zeroideal)
apply (blast intro!: zero_genideal[symmetric])
done
-text {* The unit ideal is a principal ideal *}
+text \<open>The unit ideal is a principal ideal\<close>
corollary (in ring) onepideal: "principalideal (carrier R) R"
apply (rule principalidealI)
apply (rule oneideal)
@@ -623,7 +623,7 @@
done
-text {* Every principal ideal is a right coset of the carrier *}
+text \<open>Every principal ideal is a right coset of the carrier\<close>
lemma (in principalideal) rcos_generate:
assumes "cring R"
shows "\<exists>x\<in>I. I = carrier R #> x"
@@ -650,7 +650,7 @@
qed
-subsection {* Prime Ideals *}
+subsection \<open>Prime Ideals\<close>
lemma (in ideal) primeidealCD:
assumes "cring R"
@@ -683,7 +683,7 @@
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 *}
+text \<open>If @{text "{\<zero>}"} is a prime ideal of a commutative ring, the ring is a domain\<close>
lemma (in cring) zeroprimeideal_domainI:
assumes pi: "primeideal {\<zero>} R"
shows "domain R"
@@ -713,7 +713,7 @@
done
-subsection {* Maximal Ideals *}
+subsection \<open>Maximal Ideals\<close>
lemma (in ideal) helper_I_closed:
assumes carr: "a \<in> carrier R" "x \<in> carrier R" "y \<in> carrier R"
@@ -767,7 +767,7 @@
qed
qed
-text {* In a cring every maximal ideal is prime *}
+text \<open>In a cring every maximal ideal is prime\<close>
lemma (in cring) maximalideal_is_prime:
assumes "maximalideal I R"
shows "primeideal I R"
@@ -825,7 +825,7 @@
qed
-subsection {* Derived Theorems *}
+subsection \<open>Derived Theorems\<close>
--"A non-zero cring that has only the two trivial ideals is a field"
lemma (in cring) trivialideals_fieldI:
@@ -927,7 +927,7 @@
by (fast intro!: trivialideals_fieldI[OF carrnzero] field.all_ideals)
-text {* Like zeroprimeideal for domains *}
+text \<open>Like zeroprimeideal for domains\<close>
lemma (in field) zeromaximalideal: "maximalideal {\<zero>} R"
apply (rule maximalidealI)
apply (rule zeroideal)
--- a/src/HOL/Algebra/IntRing.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/IntRing.thy Sat Oct 10 16:26:23 2015 +0200
@@ -7,9 +7,9 @@
imports QuotRing Lattice Int "~~/src/HOL/Number_Theory/Primes"
begin
-section {* The Ring of Integers *}
+section \<open>The Ring of Integers\<close>
-subsection {* Some properties of @{typ int} *}
+subsection \<open>Some properties of @{typ int}\<close>
lemma dvds_eq_abseq:
fixes k :: int
@@ -20,7 +20,7 @@
done
-subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
+subsection \<open>@{text "\<Z>"}: The Set of Integers as Algebraic Structure\<close>
abbreviation int_ring :: "int ring" ("\<Z>")
where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
@@ -47,11 +47,11 @@
*)
-subsection {* Interpretations *}
+subsection \<open>Interpretations\<close>
-text {* Since definitions of derived operations are global, their
+text \<open>Since definitions of derived operations are global, their
interpretation needs to be done as early as possible --- that is,
- with as few assumptions as possible. *}
+ with as few assumptions as possible.\<close>
interpretation int: monoid \<Z>
where "carrier \<Z> = UNIV"
@@ -159,8 +159,8 @@
qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
-text {* Removal of occurrences of @{term UNIV} in interpretation result
- --- experimental. *}
+text \<open>Removal of occurrences of @{term UNIV} in interpretation result
+ --- experimental.\<close>
lemma UNIV:
"x \<in> UNIV \<longleftrightarrow> True"
@@ -218,7 +218,7 @@
by standard clarsimp
-subsection {* Generated Ideals of @{text "\<Z>"} *}
+subsection \<open>Generated Ideals of @{text "\<Z>"}\<close>
lemma int_Idl: "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp
@@ -255,7 +255,7 @@
qed
-subsection {* Ideals and Divisibility *}
+subsection \<open>Ideals and Divisibility\<close>
lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
by (rule int.Idl_subset_ideal') simp_all
@@ -287,7 +287,7 @@
done
-subsection {* Ideals and the Modulus *}
+subsection \<open>Ideals and the Modulus\<close>
definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set"
where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
@@ -370,7 +370,7 @@
done
-subsection {* Factorization *}
+subsection \<open>Factorization\<close>
definition ZFact :: "int \<Rightarrow> int set ring"
where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
--- a/src/HOL/Algebra/Lattice.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Lattice.thy Sat Oct 10 16:26:23 2015 +0200
@@ -9,9 +9,9 @@
imports Congruence
begin
-section {* Orders and Lattices *}
+section \<open>Orders and Lattices\<close>
-subsection {* Partial Orders *}
+subsection \<open>Partial Orders\<close>
record 'a gorder = "'a eq_object" +
le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
@@ -32,7 +32,7 @@
where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
-subsubsection {* The order relation *}
+subsubsection \<open>The order relation\<close>
context weak_partial_order
begin
@@ -103,7 +103,7 @@
using assms unfolding lless_def by (blast dest: le_trans intro: sym)
-subsubsection {* Upper and lower bounds of a set *}
+subsubsection \<open>Upper and lower bounds of a set\<close>
definition
Upper :: "[_, 'a set] => 'a set"
@@ -276,7 +276,7 @@
qed
-subsubsection {* Least and greatest, as predicate *}
+subsubsection \<open>Least and greatest, as predicate\<close>
definition
least :: "[_, 'a, 'a set] => bool"
@@ -286,8 +286,8 @@
greatest :: "[_, 'a, 'a set] => bool"
where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
-text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
- .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
+text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l
+ .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
lemma least_closed [intro, simp]:
"least L l A ==> l \<in> carrier L"
@@ -310,8 +310,8 @@
"[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
by (unfold least_def) (auto dest: sym)
-text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for
- @{term "A {.=} A'"} *}
+text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for
+ @{term "A {.=} A'"}\<close>
lemma (in weak_partial_order) least_Upper_cong_l:
assumes "x .= x'"
@@ -367,8 +367,8 @@
greatest L x A = greatest L x' A"
by (unfold greatest_def) (auto dest: sym)
-text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for
- @{term "A {.=} A'"} *}
+text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for
+ @{term "A {.=} A'"}\<close>
lemma (in weak_partial_order) greatest_Lower_cong_l:
assumes "x .= x'"
@@ -402,7 +402,7 @@
shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
by (unfold greatest_def) blast
-text {* Supremum and infimum *}
+text \<open>Supremum and infimum\<close>
definition
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
@@ -421,7 +421,7 @@
where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
-subsection {* Lattices *}
+subsection \<open>Lattices\<close>
locale weak_upper_semilattice = weak_partial_order +
assumes sup_of_two_exists:
@@ -434,7 +434,7 @@
locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
-subsubsection {* Supremum *}
+subsubsection \<open>Supremum\<close>
lemma (in weak_upper_semilattice) joinI:
"[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
@@ -507,7 +507,7 @@
unfolding sup_def
by (rule someI2) (auto intro: sup_of_singletonI)
-text {* Condition on @{text A}: supremum exists. *}
+text \<open>Condition on @{text A}: supremum exists.\<close>
lemma (in weak_upper_semilattice) sup_insertI:
"[| !!s. least L s (Upper L (insert x A)) ==> P s;
@@ -638,7 +638,7 @@
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
proof (rule finite_sup_insertI)
- -- {* The textbook argument in Jacobson I, p 457 *}
+ -- \<open>The textbook argument in Jacobson I, p 457\<close>
fix s
assume sup: "least L s (Upper L {x, y, z})"
show "x \<squnion> (y \<squnion> z) .= s"
@@ -652,7 +652,7 @@
qed (simp_all add: L least_closed [OF sup])
qed (simp_all add: L)
-text {* Commutativity holds for @{text "="}. *}
+text \<open>Commutativity holds for @{text "="}.\<close>
lemma join_comm:
fixes L (structure)
@@ -673,7 +673,7 @@
qed
-subsubsection {* Infimum *}
+subsubsection \<open>Infimum\<close>
lemma (in weak_lower_semilattice) meetI:
"[| !!i. greatest L i (Lower L {x, y}) ==> P i;
@@ -747,7 +747,7 @@
unfolding inf_def
by (rule someI2) (auto intro: inf_of_singletonI)
-text {* Condition on @{text A}: infimum exists. *}
+text \<open>Condition on @{text A}: infimum exists.\<close>
lemma (in weak_lower_semilattice) inf_insertI:
"[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
@@ -879,7 +879,7 @@
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
proof (rule finite_inf_insertI)
- txt {* The textbook argument in Jacobson I, p 457 *}
+ txt \<open>The textbook argument in Jacobson I, p 457\<close>
fix i
assume inf: "greatest L i (Lower L {x, y, z})"
show "x \<sqinter> (y \<sqinter> z) .= i"
@@ -911,19 +911,19 @@
qed
-subsection {* Total Orders *}
+subsection \<open>Total Orders\<close>
locale weak_total_order = weak_partial_order +
assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
-text {* Introduction rule: the usual definition of total order *}
+text \<open>Introduction rule: the usual definition of total order\<close>
lemma (in weak_partial_order) weak_total_orderI:
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
shows "weak_total_order L"
by standard (rule total)
-text {* Total orders are lattices. *}
+text \<open>Total orders are lattices.\<close>
sublocale weak_total_order < weak: weak_lattice
proof
@@ -969,7 +969,7 @@
qed
-subsection {* Complete Lattices *}
+subsection \<open>Complete Lattices\<close>
locale weak_complete_lattice = weak_lattice +
assumes sup_exists:
@@ -977,7 +977,7 @@
and inf_exists:
"[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
-text {* Introduction rule: the usual definition of complete lattice *}
+text \<open>Introduction rule: the usual definition of complete lattice\<close>
lemma (in weak_partial_order) weak_complete_latticeI:
assumes sup_exists:
@@ -1034,7 +1034,7 @@
"\<bottom> \<in> carrier L"
by (unfold bottom_def) simp
-text {* Jacobson: Theorem 8.1 *}
+text \<open>Jacobson: Theorem 8.1\<close>
lemma Lower_empty [simp]:
"Lower L {} = carrier L"
@@ -1090,7 +1090,7 @@
(* TODO: prove dual version *)
-subsection {* Orders and Lattices where @{text eq} is the Equality *}
+subsection \<open>Orders and Lattices where @{text eq} is the Equality\<close>
locale partial_order = weak_partial_order +
assumes eq_is_equal: "op .= = op ="
@@ -1115,7 +1115,7 @@
end
-text {* Least and greatest, as predicate *}
+text \<open>Least and greatest, as predicate\<close>
lemma (in partial_order) least_unique:
"[| least L x A; least L y A |] ==> x = y"
@@ -1126,7 +1126,7 @@
using weak_greatest_unique unfolding eq_is_equal .
-text {* Lattices *}
+text \<open>Lattices\<close>
locale upper_semilattice = partial_order +
assumes sup_of_two_exists:
@@ -1145,7 +1145,7 @@
locale lattice = upper_semilattice + lower_semilattice
-text {* Supremum *}
+text \<open>Supremum\<close>
declare (in partial_order) weak_sup_of_singleton [simp del]
@@ -1164,7 +1164,7 @@
using weak_join_assoc L unfolding eq_is_equal .
-text {* Infimum *}
+text \<open>Infimum\<close>
declare (in partial_order) weak_inf_of_singleton [simp del]
@@ -1172,7 +1172,7 @@
"x \<in> carrier L ==> \<Sqinter>{x} = x"
using weak_inf_of_singleton unfolding eq_is_equal .
-text {* Condition on @{text A}: infimum exists. *}
+text \<open>Condition on @{text A}: infimum exists.\<close>
lemma (in lower_semilattice) meet_assoc_lemma:
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
@@ -1185,7 +1185,7 @@
using weak_meet_assoc L unfolding eq_is_equal .
-text {* Total Orders *}
+text \<open>Total Orders\<close>
locale total_order = partial_order +
assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
@@ -1193,20 +1193,20 @@
sublocale total_order < weak: weak_total_order
by standard (rule total_order_total)
-text {* Introduction rule: the usual definition of total order *}
+text \<open>Introduction rule: the usual definition of total order\<close>
lemma (in partial_order) total_orderI:
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
shows "total_order L"
by standard (rule total)
-text {* Total orders are lattices. *}
+text \<open>Total orders are lattices.\<close>
sublocale total_order < weak: lattice
by standard (auto intro: sup_of_two_exists inf_of_two_exists)
-text {* Complete lattices *}
+text \<open>Complete lattices\<close>
locale complete_lattice = lattice +
assumes sup_exists:
@@ -1217,7 +1217,7 @@
sublocale complete_lattice < weak: weak_complete_lattice
by standard (auto intro: sup_exists inf_exists)
-text {* Introduction rule: the usual definition of complete lattice *}
+text \<open>Introduction rule: the usual definition of complete lattice\<close>
lemma (in partial_order) complete_latticeI:
assumes sup_exists:
@@ -1273,9 +1273,9 @@
(* TODO: prove dual version *)
-subsection {* Examples *}
+subsection \<open>Examples\<close>
-subsubsection {* The Powerset of a Set is a Complete Lattice *}
+subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
theorem powerset_is_complete_lattice:
"complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
@@ -1293,13 +1293,13 @@
fix B
assume "B \<subseteq> carrier ?L"
then have "greatest ?L (\<Inter>B \<inter> A) (Lower ?L B)"
- txt {* @{term "\<Inter>B"} is not the infimum of @{term B}:
- @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}! *}
+ txt \<open>@{term "\<Inter>B"} is not the infimum of @{term B}:
+ @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}!\<close>
by (fastforce intro!: greatest_LowerI simp: Lower_def)
then show "EX i. greatest ?L i (Lower ?L B)" ..
qed
-text {* An other example, that of the lattice of subgroups of a group,
- can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
+text \<open>An other example, that of the lattice of subgroups of a group,
+ can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
end
--- a/src/HOL/Algebra/Module.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Module.thy Sat Oct 10 16:26:23 2015 +0200
@@ -7,9 +7,9 @@
imports Ring
begin
-section {* Modules over an Abelian Group *}
+section \<open>Modules over an Abelian Group\<close>
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
record ('a, 'b) module = "'b ring" +
smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
@@ -103,7 +103,7 @@
smult_l_distr smult_r_distr smult_assoc1)
-subsection {* Basic Properties of Algebras *}
+subsection \<open>Basic Properties of Algebras\<close>
lemma (in algebra) smult_l_null [simp]:
"x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
--- a/src/HOL/Algebra/QuotRing.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/QuotRing.thy Sat Oct 10 16:26:23 2015 +0200
@@ -6,17 +6,17 @@
imports RingHom
begin
-section {* Quotient Rings *}
+section \<open>Quotient Rings\<close>
-subsection {* Multiplication on Cosets *}
+subsection \<open>Multiplication on Cosets\<close>
definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
where "rcoset_mult R I A B = (\<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b))"
-text {* @{const "rcoset_mult"} fulfils the properties required by
- congruences *}
+text \<open>@{const "rcoset_mult"} fulfils the properties required by
+ congruences\<close>
lemma (in ideal) rcoset_mult_add:
"x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> [mod I:] (I +> x) \<Otimes> (I +> y) = I +> (x \<otimes> y)"
apply rule
@@ -70,7 +70,7 @@
qed
-subsection {* Quotient Ring Definition *}
+subsection \<open>Quotient Ring Definition\<close>
definition FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"
(infixl "Quot" 65)
@@ -79,33 +79,33 @@
one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"
-subsection {* Factorization over General Ideals *}
+subsection \<open>Factorization over General Ideals\<close>
-text {* The quotient is a ring *}
+text \<open>The quotient is a ring\<close>
lemma (in ideal) quotient_is_ring: "ring (R Quot I)"
apply (rule ringI)
- --{* abelian group *}
+ --\<open>abelian group\<close>
apply (rule comm_group_abelian_groupI)
apply (simp add: FactRing_def)
apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def'])
- --{* mult monoid *}
+ --\<open>mult monoid\<close>
apply (rule monoidI)
apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def
a_r_coset_def[symmetric])
- --{* mult closed *}
+ --\<open>mult closed\<close>
apply (clarify)
apply (simp add: rcoset_mult_add, fast)
- --{* mult @{text one_closed} *}
+ --\<open>mult @{text one_closed}\<close>
apply force
- --{* mult assoc *}
+ --\<open>mult assoc\<close>
apply clarify
apply (simp add: rcoset_mult_add m_assoc)
- --{* mult one *}
+ --\<open>mult one\<close>
apply clarify
apply (simp add: rcoset_mult_add)
apply clarify
apply (simp add: rcoset_mult_add)
- --{* distr *}
+ --\<open>distr\<close>
apply clarify
apply (simp add: rcoset_mult_add a_rcos_sum l_distr)
apply clarify
@@ -113,7 +113,7 @@
done
-text {* This is a ring homomorphism *}
+text \<open>This is a ring homomorphism\<close>
lemma (in ideal) rcos_ring_hom: "(op +> I) \<in> ring_hom R (R Quot I)"
apply (rule ring_hom_memI)
@@ -132,7 +132,7 @@
apply (simp add: FactRing_def)
done
-text {* The quotient of a cring is also commutative *}
+text \<open>The quotient of a cring is also commutative\<close>
lemma (in ideal) quotient_is_cring:
assumes "cring R"
shows "cring (R Quot I)"
@@ -148,7 +148,7 @@
done
qed
-text {* Cosets as a ring homomorphism on crings *}
+text \<open>Cosets as a ring homomorphism on crings\<close>
lemma (in ideal) rcos_ring_hom_cring:
assumes "cring R"
shows "ring_hom_cring R (R Quot I) (op +> I)"
@@ -164,9 +164,9 @@
qed
-subsection {* Factorization over Prime Ideals *}
+subsection \<open>Factorization over Prime Ideals\<close>
-text {* The quotient ring generated by a prime ideal is a domain *}
+text \<open>The quotient ring generated by a prime ideal is a domain\<close>
lemma (in primeideal) quotient_is_domain: "domain (R Quot I)"
apply (rule domain.intro)
apply (rule quotient_is_cring, rule is_cring)
@@ -201,18 +201,18 @@
then show "I +> x = I" by (rule a_rcos_const)
qed
-text {* Generating right cosets of a prime ideal is a homomorphism
- on commutative rings *}
+text \<open>Generating right cosets of a prime ideal is a homomorphism
+ on commutative rings\<close>
lemma (in primeideal) rcos_ring_hom_cring: "ring_hom_cring R (R Quot I) (op +> I)"
by (rule rcos_ring_hom_cring) (rule is_cring)
-subsection {* Factorization over Maximal Ideals *}
+subsection \<open>Factorization over Maximal Ideals\<close>
-text {* In a commutative ring, the quotient ring over a maximal ideal
+text \<open>In a commutative ring, the quotient ring over a maximal ideal
is a field.
The proof follows ``W. Adkins, S. Weintraub: Algebra --
- An Approach via Module Theory'' *}
+ An Approach via Module Theory''\<close>
lemma (in maximalideal) quotient_is_field:
assumes "cring R"
shows "field (R Quot I)"
@@ -225,7 +225,7 @@
apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
apply (simp add: rcoset_mult_add) defer 1
proof (rule ccontr, simp)
- --{* Quotient is not empty *}
+ --\<open>Quotient is not empty\<close>
assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
then have II1: "I = I +> \<one>" by (simp add: FactRing_def)
from a_rcos_self[OF one_closed] have "\<one> \<in> I"
@@ -233,11 +233,11 @@
then have "I = carrier R" by (rule one_imp_carrier)
with I_notcarr show False by simp
next
- --{* Existence of Inverse *}
+ --\<open>Existence of Inverse\<close>
fix a
assume IanI: "I +> a \<noteq> I" and acarr: "a \<in> carrier R"
- --{* Helper ideal @{text "J"} *}
+ --\<open>Helper ideal @{text "J"}\<close>
def J \<equiv> "(carrier R #> a) <+> I :: 'a set"
have idealJ: "ideal J R"
apply (unfold J_def, rule add_ideals)
@@ -245,7 +245,7 @@
apply (rule is_ideal)
done
- --{* Showing @{term "J"} not smaller than @{term "I"} *}
+ --\<open>Showing @{term "J"} not smaller than @{term "I"}\<close>
have IinJ: "I \<subseteq> J"
proof (rule, simp add: J_def r_coset_def set_add_defs)
fix x
@@ -256,7 +256,7 @@
with Zcarr and xI show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
qed
- --{* Showing @{term "J \<noteq> I"} *}
+ --\<open>Showing @{term "J \<noteq> I"}\<close>
have anI: "a \<notin> I"
proof (rule ccontr, simp)
assume "a \<in> I"
@@ -274,7 +274,7 @@
from aJ and anI have JnI: "J \<noteq> I" by fast
- --{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *}
+ --\<open>Deducing @{term "J = carrier R"} because @{term "I"} is maximal\<close>
from idealJ and IinJ have "J = I \<or> J = carrier R"
proof (rule I_maximal, unfold J_def)
have "carrier R #> a \<subseteq> carrier R"
@@ -285,7 +285,7 @@
with JnI have Jcarr: "J = carrier R" by simp
- --{* Calculating an inverse for @{term "a"} *}
+ --\<open>Calculating an inverse for @{term "a"}\<close>
from one_closed[folded Jcarr]
have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
by (simp add: J_def r_coset_def set_add_defs)
@@ -294,7 +294,7 @@
from one and rcarr and acarr and iI[THEN a_Hcarr]
have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
- --{* Lifting to cosets *}
+ --\<open>Lifting to cosets\<close>
from iI have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
by (intro a_rcosI, simp, intro a_subset, simp)
with rai1 have "a \<otimes> r \<in> I +> \<one>" by simp
--- a/src/HOL/Algebra/Ring.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Ring.thy Sat Oct 10 16:26:23 2015 +0200
@@ -7,15 +7,15 @@
imports FiniteProduct
begin
-section {* The Algebraic Hierarchy of Rings *}
+section \<open>The Algebraic Hierarchy of Rings\<close>
-subsection {* Abelian Groups *}
+subsection \<open>Abelian Groups\<close>
record 'a ring = "'a monoid" +
zero :: 'a ("\<zero>\<index>")
add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
-text {* Derived operations. *}
+text \<open>Derived operations.\<close>
definition
a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
@@ -39,7 +39,7 @@
("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
translations
"\<Oplus>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finsum \<struct>\<index> (%i. b) A"
- -- {* Beware of argument permutation! *}
+ -- \<open>Beware of argument permutation!\<close>
locale abelian_group = abelian_monoid +
@@ -47,7 +47,7 @@
"comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-subsection {* Basic Properties *}
+subsection \<open>Basic Properties\<close>
lemma abelian_monoidI:
fixes R (structure)
@@ -91,7 +91,7 @@
lemmas monoid_record_simps = partial_object.simps monoid.simps
-text {* Transfer facts from multiplicative structures via interpretation. *}
+text \<open>Transfer facts from multiplicative structures via interpretation.\<close>
sublocale abelian_monoid <
add!: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
@@ -140,9 +140,9 @@
lemmas finsum_infinite = add.finprod_infinite
lemmas finsum_cong = add.finprod_cong
-text {*Usually, if this rule causes a failed congruence proof error,
+text \<open>Usually, if this rule causes a failed congruence proof error,
the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
- Adding @{thm [source] Pi_def} to the simpset is often useful. *}
+ Adding @{thm [source] Pi_def} to the simpset is often useful.\<close>
lemmas finsum_reindex = add.finprod_reindex
@@ -206,7 +206,7 @@
lemmas (in abelian_group) minus_add = add.inv_mult
-text {* Derive an @{text "abelian_group"} from a @{text "comm_group"} *}
+text \<open>Derive an @{text "abelian_group"} from a @{text "comm_group"}\<close>
lemma comm_group_abelian_groupI:
fixes G (structure)
@@ -219,7 +219,7 @@
qed
-subsection {* Rings: Basic Definitions *}
+subsection \<open>Rings: Basic Definitions\<close>
locale semiring = abelian_monoid R + monoid R for R (structure) +
assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
@@ -246,7 +246,7 @@
assumes field_Units: "Units R = carrier R - {\<zero>}"
-subsection {* Rings *}
+subsection \<open>Rings\<close>
lemma ringI:
fixes R (structure)
@@ -283,8 +283,8 @@
shows "cring R"
proof (intro cring.intro ring.intro)
show "ring_axioms R"
- -- {* Right-distributivity follows from left-distributivity and
- commutativity. *}
+ -- \<open>Right-distributivity follows from left-distributivity and
+ commutativity.\<close>
proof (rule ring_axioms.intro)
fix x y z
assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
@@ -312,7 +312,7 @@
"cring R" by (rule cring_axioms)
-subsubsection {* Normaliser for Rings *}
+subsubsection \<open>Normaliser for Rings\<close>
lemma (in abelian_group) r_neg2:
"[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> (\<ominus> x \<oplus> y) = y"
@@ -335,9 +335,9 @@
context ring begin
-text {*
+text \<open>
The following proofs are from Jacobson, Basic Algebra I, pp.~88--89.
-*}
+\<close>
sublocale semiring
proof -
@@ -387,20 +387,20 @@
"[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
by (simp only: a_minus_def)
-text {* Setup algebra method:
- compute distributive normal form in locale contexts *}
+text \<open>Setup algebra method:
+ compute distributive normal form in locale contexts\<close>
ML_file "ringsimp.ML"
-attribute_setup algebra = {*
+attribute_setup algebra = \<open>
Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
-- Scan.lift Args.name -- Scan.repeat Args.term
>> (fn ((b, n), ts) => if b then Ringsimp.add_struct (n, ts) else Ringsimp.del_struct (n, ts))
-*} "theorems controlling algebra method"
+\<close> "theorems controlling algebra method"
-method_setup algebra = {*
+method_setup algebra = \<open>
Scan.succeed (SIMPLE_METHOD' o Ringsimp.algebra_tac)
-*} "normalisation of algebraic structure"
+\<close> "normalisation of algebraic structure"
lemmas (in semiring) semiring_simprules
[algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
@@ -463,7 +463,7 @@
end
-text {* Two examples for use of method algebra *}
+text \<open>Two examples for use of method algebra\<close>
lemma
fixes R (structure) and S (structure)
@@ -487,7 +487,7 @@
qed
-subsubsection {* Sums over Finite Sets *}
+subsubsection \<open>Sums over Finite Sets\<close>
lemma (in semiring) finsum_ldistr:
"[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
@@ -508,7 +508,7 @@
qed
-subsection {* Integral Domains *}
+subsection \<open>Integral Domains\<close>
context "domain" begin
@@ -554,10 +554,10 @@
end
-subsection {* Fields *}
+subsection \<open>Fields\<close>
-text {* Field would not need to be derived from domain, the properties
- for domain follow from the assumptions of field *}
+text \<open>Field would not need to be derived from domain, the properties
+ for domain follow from the assumptions of field\<close>
lemma (in cring) cring_fieldI:
assumes field_Units: "Units R = carrier R - {\<zero>}"
shows "field R"
@@ -585,7 +585,7 @@
qed
qed (rule field_Units)
-text {* Another variant to show that something is a field *}
+text \<open>Another variant to show that something is a field\<close>
lemma (in cring) cring_fieldI2:
assumes notzero: "\<zero> \<noteq> \<one>"
and invex: "\<And>a. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>b\<in>carrier R. a \<otimes> b = \<one>"
@@ -604,7 +604,7 @@
qed
-subsection {* Morphisms *}
+subsection \<open>Morphisms\<close>
definition
ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
--- a/src/HOL/Algebra/RingHom.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/RingHom.thy Sat Oct 10 16:26:23 2015 +0200
@@ -6,9 +6,9 @@
imports Ideal
begin
-section {* Homomorphisms of Non-Commutative Rings *}
+section \<open>Homomorphisms of Non-Commutative Rings\<close>
-text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
+text \<open>Lifting existing lemmas in a @{text ring_hom_ring} locale\<close>
locale ring_hom_ring = R: ring R + S: ring S
for R (structure) and S (structure) +
fixes h
@@ -100,7 +100,7 @@
qed
-subsection {* The Kernel of a Ring Homomorphism *}
+subsection \<open>The Kernel of a Ring Homomorphism\<close>
--"the kernel of a ring homomorphism is an ideal"
lemma (in ring_hom_ring) kernel_is_ideal:
@@ -111,15 +111,15 @@
apply (unfold a_kernel_def', simp+)
done
-text {* Elements of the kernel are mapped to zero *}
+text \<open>Elements of the kernel are mapped to zero\<close>
lemma (in abelian_group_hom) kernel_zero [simp]:
"i \<in> a_kernel R S h \<Longrightarrow> h i = \<zero>\<^bsub>S\<^esub>"
by (simp add: a_kernel_defs)
-subsection {* Cosets *}
+subsection \<open>Cosets\<close>
-text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *}
+text \<open>Cosets of the kernel correspond to the elements of the image of the homomorphism\<close>
lemma (in ring_hom_ring) rcos_imp_homeq:
assumes acarr: "a \<in> carrier R"
and xrcos: "x \<in> a_kernel R S h +> a"
--- a/src/HOL/Algebra/Sylow.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/Sylow.thy Sat Oct 10 16:26:23 2015 +0200
@@ -6,11 +6,11 @@
imports Coset Exponent
begin
-text {*
+text \<open>
See also @{cite "Kammueller-Paulson:1999"}.
-*}
+\<close>
-text{*The combinatorial argument is in theory Exponent*}
+text\<open>The combinatorial argument is in theory Exponent\<close>
locale sylow = group +
fixes p and a and m and calM and RelM
@@ -49,7 +49,7 @@
done
-subsection{*Main Part of the Proof*}
+subsection\<open>Main Part of the Proof\<close>
locale sylow_central = sylow +
fixes H and M1 and M
@@ -107,7 +107,7 @@
qed
-subsection{*Discharging the Assumptions of @{text sylow_central}*}
+subsection\<open>Discharging the Assumptions of @{text sylow_central}\<close>
lemma (in sylow) EmptyNotInEquivSet: "{} \<notin> calM // RelM"
by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
@@ -155,7 +155,7 @@
done
-subsubsection{*Introduction and Destruct Rules for @{term H}*}
+subsubsection\<open>Introduction and Destruct Rules for @{term H}\<close>
lemma (in sylow_central) H_I: "[|g \<in> carrier G; M1 #> g = M1|] ==> g \<in> H"
by (simp add: H_def)
@@ -216,10 +216,10 @@
done
-subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*}
+subsection\<open>Equal Cardinalities of @{term M} and the Set of Cosets\<close>
-text{*Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that
- their cardinalities are equal.*}
+text\<open>Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that
+ their cardinalities are equal.\<close>
lemma ElemClassEquiv:
"[| equiv A r; C \<in> A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
@@ -259,7 +259,7 @@
done
-subsubsection{*The Opposite Injection*}
+subsubsection\<open>The Opposite Injection\<close>
lemma (in sylow_central) H_elem_map:
"H1 \<in> rcosets H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
@@ -278,7 +278,7 @@
intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
done
-text{*close to a duplicate of @{text inj_M_GmodH}*}
+text\<open>close to a duplicate of @{text inj_M_GmodH}\<close>
lemma (in sylow_central) inj_GmodH_M:
"\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)"
apply (rule bexI)
@@ -340,14 +340,14 @@
apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def)
done
-text{*Needed because the locale's automatic definition refers to
+text\<open>Needed because the locale's automatic definition refers to
@{term "semigroup G"} and @{term "group_axioms G"} rather than
- simply to @{term "group G"}.*}
+ simply to @{term "group G"}.\<close>
lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
by (simp add: sylow_def group_def)
-subsection {* Sylow's Theorem *}
+subsection \<open>Sylow's Theorem\<close>
theorem sylow_thm:
"[| prime p; group(G); order(G) = (p^a) * m; finite (carrier G)|]
--- a/src/HOL/Algebra/UnivPoly.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Sat Oct 10 16:26:23 2015 +0200
@@ -9,9 +9,9 @@
imports Module RingHom
begin
-section {* Univariate Polynomials *}
+section \<open>Univariate Polynomials\<close>
-text {*
+text \<open>
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
@@ -21,14 +21,14 @@
formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"},
which was implemented with axiomatic type classes. This was later
ported to Locales.
-*}
+\<close>
-subsection {* The Constructor for Univariate Polynomials *}
+subsection \<open>The Constructor for Univariate Polynomials\<close>
-text {*
+text \<open>
Functions with finite support.
-*}
+\<close>
locale bound =
fixes z :: 'a
@@ -67,9 +67,9 @@
monom = (%a:carrier R. %n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
coeff = (%p:up R. %n. p n)\<rparr>"
-text {*
+text \<open>
Properties of the set of polynomials @{term up}.
-*}
+\<close>
lemma mem_upI [intro]:
"[| !!n. f n \<in> carrier R; EX n. bound (zero R) n f |] ==> f \<in> up R"
@@ -168,7 +168,7 @@
end
-subsection {* Effect of Operations on Coefficients *}
+subsection \<open>Effect of Operations on Coefficients\<close>
locale UP =
fixes R (structure) and P (structure)
@@ -189,7 +189,7 @@
context UP
begin
-text {*Temporarily declare @{thm P_def} as simp rule.*}
+text \<open>Temporarily declare @{thm P_def} as simp rule.\<close>
declare P_def [simp]
@@ -240,12 +240,12 @@
end
-subsection {* Polynomials Form a Ring. *}
+subsection \<open>Polynomials Form a Ring.\<close>
context UP_ring
begin
-text {* Operations are closed over @{term P}. *}
+text \<open>Operations are closed over @{term P}.\<close>
lemma UP_mult_closed [simp]:
"[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_mult_closed)
@@ -269,7 +269,7 @@
declare (in UP) P_def [simp del]
-text {* Algebraic ring properties *}
+text \<open>Algebraic ring properties\<close>
context UP_ring
begin
@@ -398,7 +398,7 @@
end
-subsection {* Polynomials Form a Commutative Ring. *}
+subsection \<open>Polynomials Form a Commutative Ring.\<close>
context UP_cring
begin
@@ -428,7 +428,7 @@
qed (simp_all add: R1 R2)
-subsection {*Polynomials over a commutative ring for a commutative ring*}
+subsection \<open>Polynomials over a commutative ring for a commutative ring\<close>
theorem UP_cring:
"cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
@@ -461,7 +461,7 @@
sublocale UP_cring < P: cring P using UP_cring .
-subsection {* Polynomials Form an Algebra *}
+subsection \<open>Polynomials Form an Algebra\<close>
context UP_ring
begin
@@ -496,9 +496,9 @@
end
-text {*
+text \<open>
Interpretation of lemmas from @{term algebra}.
-*}
+\<close>
lemma (in cring) cring:
"cring R" ..
@@ -510,7 +510,7 @@
sublocale UP_cring < algebra R P using UP_algebra .
-subsection {* Further Lemmas Involving Monomials *}
+subsection \<open>Further Lemmas Involving Monomials\<close>
context UP_ring
begin
@@ -637,8 +637,8 @@
}
qed
-text{*The following corollary follows from lemmas @{thm "monom_one_Suc"}
- and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
+text\<open>The following corollary follows from lemmas @{thm "monom_one_Suc"}
+ and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}\<close>
corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..
@@ -709,7 +709,7 @@
end
-subsection {* The Degree Function *}
+subsection \<open>The Degree Function\<close>
definition
deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
@@ -743,19 +743,19 @@
assumes "deg R p < m" and "p \<in> carrier P"
shows "coeff P p m = \<zero>"
proof -
- from `p \<in> carrier P` obtain n where "bound \<zero> n (coeff P p)"
+ from \<open>p \<in> carrier P\<close> 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)
- from this and `deg R p < m` show ?thesis ..
+ from this and \<open>deg R p < m\<close> show ?thesis ..
qed
lemma 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
- @{thm [source] deg_aboveD} *}
+-- \<open>Logically, this is a slightly stronger version of
+ @{thm [source] deg_aboveD}\<close>
proof (cases "n=0")
case True then show ?thesis by simp
next
@@ -814,7 +814,7 @@
!!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
by (fast intro: le_antisym deg_aboveI deg_belowI)
-text {* Degree and polynomial operations *}
+text \<open>Degree and polynomial operations\<close>
lemma deg_add [simp]:
"p \<in> carrier P \<Longrightarrow> q \<in> carrier P \<Longrightarrow>
@@ -863,8 +863,8 @@
inj_on_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R)
qed
-text{*The following lemma is later \emph{overwritten} by the most
- specific one for domains, @{text deg_smult}.*}
+text\<open>The following lemma is later \emph{overwritten} by the most
+ specific one for domains, @{text deg_smult}.\<close>
lemma deg_smult_ring [simp]:
"[| a \<in> carrier R; p \<in> carrier P |] ==>
@@ -949,7 +949,7 @@
end
-text{*The following lemmas also can be lifted to @{term UP_ring}.*}
+text\<open>The following lemmas also can be lifted to @{term UP_ring}.\<close>
context UP_ring
begin
@@ -1013,7 +1013,7 @@
end
-subsection {* Polynomials over Integral Domains *}
+subsection \<open>Polynomials over Integral Domains\<close>
lemma domainI:
assumes cring: "cring R"
@@ -1071,15 +1071,15 @@
end
-text {*
+text \<open>
Interpretation of theorems from @{term domain}.
-*}
+\<close>
sublocale UP_domain < "domain" P
by intro_locales (rule domain.axioms UP_domain)+
-subsection {* The Evaluation Homomorphism and Universal Property*}
+subsection \<open>The Evaluation Homomorphism and Universal Property\<close>
(* alternative congruence rule (possibly more efficient)
lemma (in abelian_monoid) finsum_cong2:
@@ -1192,7 +1192,7 @@
end
-text {* The universal property of the polynomial ring *}
+text \<open>The universal property of the polynomial ring\<close>
locale UP_pre_univ_prop = ring_hom_cring + UP_cring
@@ -1203,9 +1203,9 @@
assumes indet_img_carrier [simp, intro]: "s \<in> carrier S"
defines Eval_def: "Eval == eval R S h s"
-text{*JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.*}
-text{*JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so
- maybe it is not that necessary.*}
+text\<open>JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.\<close>
+text\<open>JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so
+ maybe it is not that necessary.\<close>
lemma (in ring_hom_ring) hom_finsum [simp]:
"f \<in> A -> carrier R ==>
@@ -1296,18 +1296,18 @@
qed
qed
-text {*
+text \<open>
The following lemma could be proved in @{text UP_cring} with the additional
- assumption that @{text h} is closed. *}
+ assumption that @{text h} is closed.\<close>
lemma (in UP_pre_univ_prop) eval_const:
"[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
by (simp only: eval_on_carrier monom_closed) simp
-text {* Further properties of the evaluation homomorphism. *}
+text \<open>Further properties of the evaluation homomorphism.\<close>
-text {* The following proof is complicated by the fact that in arbitrary
- rings one might have @{term "one R = zero R"}. *}
+text \<open>The following proof is complicated by the fact that in arbitrary
+ rings one might have @{term "one R = zero R"}.\<close>
(* TODO: simplify by cases "one R = zero R" *)
@@ -1336,7 +1336,7 @@
end
-text {* Interpretation of ring homomorphism lemmas. *}
+text \<open>Interpretation of ring homomorphism lemmas.\<close>
sublocale UP_univ_prop < ring_hom_cring P S Eval
unfolding Eval_def
@@ -1442,7 +1442,7 @@
end
-text{*JE: The following lemma was added by me; it might be even lifted to a simpler locale*}
+text\<open>JE: The following lemma was added by me; it might be even lifted to a simpler locale\<close>
context monoid
begin
@@ -1461,7 +1461,7 @@
using lcoeff_nonzero [OF p_not_zero p_in_R] .
-subsection{*The long division algorithm: some previous facts.*}
+subsection\<open>The long division algorithm: some previous facts.\<close>
lemma coeff_minus [simp]:
assumes p: "p \<in> carrier P" and q: "q \<in> carrier P" shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n"
@@ -1538,7 +1538,7 @@
end
-subsection {* The long division proof for commutative rings *}
+subsection \<open>The long division proof for commutative rings\<close>
context UP_cring
begin
@@ -1547,7 +1547,7 @@
shows "\<exists> x y z. Pred x y z"
using exist by blast
-text {* Jacobson's Theorem 2.14 *}
+text \<open>Jacobson's Theorem 2.14\<close>
lemma long_div_theorem:
assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
@@ -1648,7 +1648,7 @@
end
-text {*The remainder theorem as corollary of the long division theorem.*}
+text \<open>The remainder theorem as corollary of the long division theorem.\<close>
context UP_cring
begin
@@ -1797,7 +1797,7 @@
end
-subsection {* Sample Application of Evaluation Homomorphism *}
+subsection \<open>Sample Application of Evaluation Homomorphism\<close>
lemma UP_pre_univ_propI:
assumes "cring R"
@@ -1820,11 +1820,11 @@
"UP_pre_univ_prop INTEG INTEG id"
by (fast intro: UP_pre_univ_propI INTEG_cring id_ring_hom)
-text {*
+text \<open>
Interpretation now enables to import all theorems and lemmas
valid in the context of homomorphisms between @{term INTEG} and @{term
"UP INTEG"} globally.
-*}
+\<close>
interpretation INTEG: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
using INTEG_id_eval by simp_all
--- a/src/HOL/Old_Number_Theory/BijectionRel.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/BijectionRel.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,18 +3,18 @@
Copyright 2000 University of Cambridge
*)
-section {* Bijections between sets *}
+section \<open>Bijections between sets\<close>
theory BijectionRel
imports Main
begin
-text {*
+text \<open>
Inductive definitions of bijections between two different sets and
between the same set. Theorem for relating the two definitions.
\bigskip
-*}
+\<close>
inductive_set
bijR :: "('a => 'b => bool) => ('a set * 'b set) set"
@@ -24,10 +24,10 @@
| insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
==> (insert a A, insert b B) \<in> bijR P"
-text {*
+text \<open>
Add extra condition to @{term insert}: @{term "\<forall>b \<in> B. \<not> P a b"}
(and similar for @{term A}).
-*}
+\<close>
definition
bijP :: "('a => 'a => bool) => 'a set => bool" where
@@ -51,7 +51,7 @@
==> insert a (insert b A) \<in> bijER P"
-text {* \medskip @{term bijR} *}
+text \<open>\medskip @{term bijR}\<close>
lemma fin_bijRl: "(A, B) \<in> bijR P ==> finite A"
apply (erule bijR.induct)
@@ -100,7 +100,7 @@
done
-text {* \medskip @{term bijER} *}
+text \<open>\medskip @{term bijER}\<close>
lemma fin_bijER: "A \<in> bijER P ==> finite A"
apply (erule bijER.induct)
--- a/src/HOL/Old_Number_Theory/Chinese.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Chinese.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,22 +3,22 @@
Copyright 2000 University of Cambridge
*)
-section {* The Chinese Remainder Theorem *}
+section \<open>The Chinese Remainder Theorem\<close>
theory Chinese
imports IntPrimes
begin
-text {*
+text \<open>
The Chinese Remainder Theorem for an arbitrary finite number of
equations. (The one-equation case is included in theory @{text
IntPrimes}. Uses functions for indexing.\footnote{Maybe @{term
funprod} and @{term funsum} should be based on general @{term fold}
on indices?}
-*}
+\<close>
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
primrec funprod :: "(nat => int) => nat => nat => int"
where
@@ -65,7 +65,7 @@
"x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
-text {* \medskip @{term funprod} and @{term funsum} *}
+text \<open>\medskip @{term funprod} and @{term funsum}\<close>
lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
by (induct n) auto
@@ -126,7 +126,7 @@
done
-subsection {* Chinese: uniqueness *}
+subsection \<open>Chinese: uniqueness\<close>
lemma zcong_funprod_aux:
"m_cond n mf ==> km_cond n kf mf
@@ -160,17 +160,17 @@
done
-subsection {* Chinese: existence *}
+subsection \<open>Chinese: existence\<close>
lemma unique_xi_sol:
"0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
apply (rule zcong_lineq_unique)
- apply (tactic {* stac @{context} @{thm zgcd_zmult_cancel} 2 *})
+ apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 2\<close>)
apply (unfold m_cond_def km_cond_def mhf_def)
apply (simp_all (no_asm_simp))
apply safe
- apply (tactic {* stac @{context} @{thm zgcd_zmult_cancel} 3 *})
+ apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 3\<close>)
apply (rule_tac [!] funprod_zgcd)
apply safe
apply simp_all
@@ -216,7 +216,7 @@
done
-subsection {* Chinese *}
+subsection \<open>Chinese\<close>
lemma chinese_remainder:
"0 < n ==> m_cond n mf ==> km_cond n kf mf
@@ -228,19 +228,19 @@
apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
apply (unfold lincong_sol_def)
apply safe
- apply (tactic {* stac @{context} @{thm zcong_zmod} 3 *})
- apply (tactic {* stac @{context} @{thm mod_mult_eq} 3 *})
- apply (tactic {* stac @{context} @{thm mod_mod_cancel} 3 *})
- apply (tactic {* stac @{context} @{thm x_sol_lin} 4 *})
- apply (tactic {* stac @{context} (@{thm mod_mult_eq} RS sym) 6 *})
- apply (tactic {* stac @{context} (@{thm zcong_zmod} RS sym) 6 *})
+ apply (tactic \<open>stac @{context} @{thm zcong_zmod} 3\<close>)
+ apply (tactic \<open>stac @{context} @{thm mod_mult_eq} 3\<close>)
+ apply (tactic \<open>stac @{context} @{thm mod_mod_cancel} 3\<close>)
+ apply (tactic \<open>stac @{context} @{thm x_sol_lin} 4\<close>)
+ apply (tactic \<open>stac @{context} (@{thm mod_mult_eq} RS sym) 6\<close>)
+ apply (tactic \<open>stac @{context} (@{thm zcong_zmod} RS sym) 6\<close>)
apply (subgoal_tac [6]
"0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
\<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
prefer 6
apply (simp add: ac_simps)
apply (unfold xilin_sol_def)
- apply (tactic {* asm_simp_tac @{context} 6 *})
+ apply (tactic \<open>asm_simp_tac @{context} 6\<close>)
apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
apply (rule_tac [6] unique_xi_sol)
apply (rule_tac [3] funprod_zdvd)
--- a/src/HOL/Old_Number_Theory/Euler.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy Sat Oct 10 16:26:23 2015 +0200
@@ -2,7 +2,7 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-section {* Euler's criterion *}
+section \<open>Euler's criterion\<close>
theory Euler
imports Residues EvenOdd
@@ -15,7 +15,7 @@
where "SetS a p = MultInvPair a p ` SRStar p"
-subsection {* Property for MultInvPair *}
+subsection \<open>Property for MultInvPair\<close>
lemma MultInvPair_prop1a:
"[| zprime p; 2 < p; ~([a = 0](mod p));
@@ -89,7 +89,7 @@
done
-subsection {* Properties of SetS *}
+subsection \<open>Properties of SetS\<close>
lemma SetS_finite: "2 < p ==> finite (SetS a p)"
by (auto simp add: SetS_def SRStar_finite [of p])
@@ -223,14 +223,14 @@
apply (auto simp add: Union_SetS_setprod_prop2)
done
-text {* \medskip Prove the first part of Euler's Criterion: *}
+text \<open>\medskip Prove the first part of Euler's Criterion:\<close>
lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p));
~(QuadRes p x) |] ==>
[x^(nat (((p) - 1) div 2)) = -1](mod p)"
by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)
-text {* \medskip Prove another part of Euler Criterion: *}
+text \<open>\medskip Prove another part of Euler Criterion:\<close>
lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
proof -
@@ -251,7 +251,7 @@
by (auto simp add: zEven_def zOdd_def)
then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
by (auto simp add: even_div_2_prop2)
- with `2 < p` have "1 < (p - 1)"
+ with \<open>2 < p\<close> have "1 < (p - 1)"
by auto
then have " 1 < (2 * ((p - 1) div 2))"
by (auto simp add: aux_1)
@@ -268,7 +268,7 @@
apply (frule zcong_zmult_prop1, auto)
done
-text {* \medskip Prove the final part of Euler's Criterion: *}
+text \<open>\medskip Prove the final part of Euler's Criterion:\<close>
lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)"
by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
@@ -291,7 +291,7 @@
done
-text {* \medskip Finally show Euler's Criterion: *}
+text \<open>\medskip Finally show Euler's Criterion:\<close>
theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
a^(nat (((p) - 1) div 2))] (mod p)"
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,20 +3,20 @@
Copyright 2000 University of Cambridge
*)
-section {* Fermat's Little Theorem extended to Euler's Totient function *}
+section \<open>Fermat's Little Theorem extended to Euler's Totient function\<close>
theory EulerFermat
imports BijectionRel IntFact
begin
-text {*
+text \<open>
Fermat's Little Theorem extended to Euler's Totient function. More
abstract approach than Boyer-Moore (which seems necessary to achieve
the extended version).
-*}
+\<close>
-subsection {* Definitions and lemmas *}
+subsection \<open>Definitions and lemmas\<close>
inductive_set RsetR :: "int => int set set" for m :: int
where
@@ -54,11 +54,11 @@
where "zcongm m = (\<lambda>a b. zcong a b m)"
lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
- -- {* LCP: not sure why this lemma is needed now *}
+ -- \<open>LCP: not sure why this lemma is needed now\<close>
by (auto simp add: abs_if)
-text {* \medskip @{text norRRset} *}
+text \<open>\medskip @{text norRRset}\<close>
declare BnorRset.simps [simp del]
@@ -146,7 +146,7 @@
done
-text {* \medskip @{term noXRRset} *}
+text \<open>\medskip @{term noXRRset}\<close>
lemma RRset_gcd [rule_format]:
"is_RRset A m ==> a \<in> A --> zgcd a m = 1"
@@ -249,7 +249,7 @@
\<Prod>(BnorRset a m) * x^card (BnorRset a m)"
apply (induct a m rule: BnorRset_induct)
prefer 2
- apply (simplesubst BnorRset.simps) --{*multiple redexes*}
+ apply (simplesubst BnorRset.simps) --\<open>multiple redexes\<close>
apply (unfold Let_def, auto)
apply (simp add: Bnor_fin Bnor_mem_zle_swap)
apply (subst setprod.insert)
@@ -259,7 +259,7 @@
done
-subsection {* Fermat *}
+subsection \<open>Fermat\<close>
lemma bijzcong_zcong_prod:
"(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Sat Oct 10 16:26:23 2015 +0200
@@ -2,7 +2,7 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-section {*Parity: Even and Odd Integers*}
+section \<open>Parity: Even and Odd Integers\<close>
theory EvenOdd
imports Int2
@@ -14,7 +14,7 @@
definition zEven :: "int set"
where "zEven = {x. \<exists>k. x = 2 * k}"
-subsection {* Some useful properties about even and odd *}
+subsection \<open>Some useful properties about even and odd\<close>
lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
@@ -167,11 +167,11 @@
lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1"
proof -
assume "x \<in> zEven" and "0 \<le> x"
- from `x \<in> zEven` obtain a where "x = 2 * a" ..
- with `0 \<le> x` have "0 \<le> a" by simp
- from `0 \<le> x` and `x = 2 * a` have "nat x = nat (2 * a)"
+ from \<open>x \<in> zEven\<close> obtain a where "x = 2 * a" ..
+ with \<open>0 \<le> x\<close> have "0 \<le> a" by simp
+ from \<open>0 \<le> x\<close> and \<open>x = 2 * a\<close> have "nat x = nat (2 * a)"
by simp
- also from `x = 2 * a` have "nat (2 * a) = 2 * nat a"
+ also from \<open>x = 2 * a\<close> have "nat (2 * a) = 2 * nat a"
by (simp add: nat_mult_distrib)
finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
by simp
@@ -186,9 +186,9 @@
lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1"
proof -
assume "x \<in> zOdd" and "0 \<le> x"
- from `x \<in> zOdd` obtain a where "x = 2 * a + 1" ..
- with `0 \<le> x` have a: "0 \<le> a" by simp
- with `0 \<le> x` and `x = 2 * a + 1` have "nat x = nat (2 * a + 1)"
+ from \<open>x \<in> zOdd\<close> obtain a where "x = 2 * a + 1" ..
+ with \<open>0 \<le> x\<close> have a: "0 \<le> a" by simp
+ with \<open>0 \<le> x\<close> and \<open>x = 2 * a + 1\<close> have "nat x = nat (2 * a + 1)"
by simp
also from a have "nat (2 * a + 1) = 2 * nat a + 1"
by (auto simp add: nat_mult_distrib nat_add_distrib)
@@ -214,8 +214,8 @@
lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2"
proof -
assume "y \<in> zEven" and "x < y"
- from `y \<in> zEven` obtain k where k: "y = 2 * k" ..
- with `x < y` have "x < 2 * k" by simp
+ from \<open>y \<in> zEven\<close> obtain k where k: "y = 2 * k" ..
+ with \<open>x < y\<close> have "x < 2 * k" by simp
then have "x div 2 < k" by (auto simp add: div_prop1)
also have "k = (2 * k) div 2" by simp
finally have "x div 2 < 2 * k div 2" by simp
--- a/src/HOL/Old_Number_Theory/Factorization.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Factorization.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,14 +3,14 @@
Copyright 2000 University of Cambridge
*)
-section {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
+section \<open>Fundamental Theorem of Arithmetic (unique factorization into primes)\<close>
theory Factorization
imports Primes "~~/src/HOL/Library/Permutation"
begin
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
definition primel :: "nat list => bool"
where "primel xs = (\<forall>p \<in> set xs. prime p)"
@@ -36,7 +36,7 @@
| "sort (x # xs) = oinsert x (sort xs)"
-subsection {* Arithmetic *}
+subsection \<open>Arithmetic\<close>
lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
apply (cases m)
@@ -64,7 +64,7 @@
done
-subsection {* Prime list and product *}
+subsection \<open>Prime list and product\<close>
lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"
apply (induct xs)
@@ -137,7 +137,7 @@
done
-subsection {* Sorting *}
+subsection \<open>Sorting\<close>
lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
apply (induct xs)
@@ -174,7 +174,7 @@
done
-subsection {* Permutation *}
+subsection \<open>Permutation\<close>
lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
apply (unfold primel_def)
@@ -212,7 +212,7 @@
done
-subsection {* Existence *}
+subsection \<open>Existence\<close>
lemma ex_nondec_lemma:
"primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs"
@@ -250,7 +250,7 @@
done
-subsection {* Uniqueness *}
+subsection \<open>Uniqueness\<close>
lemma prime_dvd_mult_list [rule_format]:
"prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"
--- a/src/HOL/Old_Number_Theory/Fib.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Fib.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,19 +3,19 @@
Copyright 1997 University of Cambridge
*)
-section {* The Fibonacci function *}
+section \<open>The Fibonacci function\<close>
theory Fib
imports Primes
begin
-text {*
+text \<open>
Fibonacci numbers: proofs of laws taken from:
R. L. Graham, D. E. Knuth, O. Patashnik. Concrete Mathematics.
(Addison-Wesley, 1989)
\bigskip
-*}
+\<close>
fun fib :: "nat \<Rightarrow> nat"
where
@@ -23,21 +23,21 @@
| "fib (Suc 0) = 1"
| fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)"
-text {*
+text \<open>
\medskip The difficulty in these proofs is to ensure that the
induction hypotheses are applied before the definition of @{term
fib}. Towards this end, the @{term fib} equations are not declared
to the Simplifier and are applied very selectively at first.
-*}
+\<close>
-text{*We disable @{text fib.fib_2fib_2} for simplification ...*}
+text\<open>We disable @{text fib.fib_2fib_2} for simplification ...\<close>
declare fib_2 [simp del]
-text{*...then prove a version that has a more restrictive pattern.*}
+text\<open>...then prove a version that has a more restrictive pattern.\<close>
lemma fib_Suc3: "fib (Suc (Suc (Suc n))) = fib (Suc n) + fib (Suc (Suc n))"
by (rule fib_2)
-text {* \medskip Concrete Mathematics, page 280 *}
+text \<open>\medskip Concrete Mathematics, page 280\<close>
lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
proof (induct n rule: fib.induct)
@@ -60,10 +60,10 @@
by (case_tac n, auto simp add: fib_Suc_gr_0)
-text {*
+text \<open>
\medskip Concrete Mathematics, page 278: Cassini's identity. The proof is
much easier using integers, not natural numbers!
-*}
+\<close>
lemma fib_Cassini_int:
"int (fib (Suc (Suc n)) * fib n) =
@@ -79,8 +79,8 @@
with "3.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2)
qed
-text{*We now obtain a version for the natural numbers via the coercion
- function @{term int}.*}
+text\<open>We now obtain a version for the natural numbers via the coercion
+ function @{term int}.\<close>
theorem fib_Cassini:
"fib (Suc (Suc n)) * fib n =
(if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1
@@ -92,7 +92,7 @@
done
-text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
+text \<open>\medskip Toward Law 6.111 of Concrete Mathematics\<close>
lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (Suc n)) = Suc 0"
apply (induct n rule: fib.induct)
@@ -135,7 +135,7 @@
qed
qed
-lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" -- {* Law 6.111 *}
+lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" -- \<open>Law 6.111\<close>
apply (induct m n rule: gcd_induct)
apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod)
done
--- a/src/HOL/Old_Number_Theory/Finite2.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy Sat Oct 10 16:26:23 2015 +0200
@@ -2,19 +2,19 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-section {*Finite Sets and Finite Sums*}
+section \<open>Finite Sets and Finite Sums\<close>
theory Finite2
imports IntFact "~~/src/HOL/Library/Infinite_Set"
begin
-text{*
+text\<open>
These are useful for combinatorial and number-theoretic counting
arguments.
-*}
+\<close>
-subsection {* Useful properties of sums and products *}
+subsection \<open>Useful properties of sums and products\<close>
lemma setsum_same_function_zcong:
assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
@@ -48,7 +48,7 @@
by (induct set: finite) (auto simp add: distrib_left)
-subsection {* Cardinality of explicit finite sets *}
+subsection \<open>Cardinality of explicit finite sets\<close>
lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
by (simp add: finite_subset)
@@ -104,7 +104,7 @@
also have "... = Suc (card {y. y < n})"
by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
finally show "card {y. y < Suc n} = Suc n"
- using `card {y. y < n} = n` by simp
+ using \<open>card {y. y < n} = n\<close> by simp
qed
lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
@@ -121,7 +121,7 @@
by (auto simp add: inj_on_def)
hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
by (rule card_image)
- also from `0 \<le> n` have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
+ also from \<open>0 \<le> n\<close> have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
apply (auto simp add: zless_nat_eq_int_zless image_def)
apply (rule_tac x = "nat x" in exI)
apply (auto simp add: nat_0_le)
@@ -150,7 +150,7 @@
hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
card {x. 0 \<le> x & x < n}"
by (rule card_image)
- also from `0 \<le> n` have "... = nat n"
+ also from \<open>0 \<le> n\<close> have "... = nat n"
by (rule card_bdd_int_set_l)
also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
apply (auto simp add: image_def)
--- a/src/HOL/Old_Number_Theory/Gauss.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Sat Oct 10 16:26:23 2015 +0200
@@ -2,7 +2,7 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-section {* Gauss' Lemma *}
+section \<open>Gauss' Lemma\<close>
theory Gauss
imports Euler
@@ -26,7 +26,7 @@
definition "F = (%x. (p - x)) ` E"
-subsection {* Basic properties of p *}
+subsection \<open>Basic properties of p\<close>
lemma p_odd: "p \<in> zOdd"
by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
@@ -64,7 +64,7 @@
done
-subsection {* Basic Properties of the Gauss Sets *}
+subsection \<open>Basic Properties of the Gauss Sets\<close>
lemma finite_A: "finite (A)"
by (auto simp add: A_def)
@@ -272,7 +272,7 @@
by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
-subsection {* Relationships Between Gauss Sets *}
+subsection \<open>Relationships Between Gauss Sets\<close>
lemma B_card_eq_A: "card B = card A"
using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
@@ -434,7 +434,7 @@
qed
-subsection {* Gauss' Lemma *}
+subsection \<open>Gauss' Lemma\<close>
lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
by (auto simp add: finite_E neg_one_special)
--- a/src/HOL/Old_Number_Theory/Int2.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy Sat Oct 10 16:26:23 2015 +0200
@@ -2,7 +2,7 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-section {*Integers: Divisibility and Congruences*}
+section \<open>Integers: Divisibility and Congruences\<close>
theory Int2
imports Finite2 WilsonRuss
@@ -12,7 +12,7 @@
where "MultInv p x = x ^ nat (p - 2)"
-subsection {* Useful lemmas about dvd and powers *}
+subsection \<open>Useful lemmas about dvd and powers\<close>
lemma zpower_zdvd_prop1:
"0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
@@ -47,12 +47,12 @@
assumes "0 < z" and "(x::int) < y * z"
shows "x div z < y"
proof -
- from `0 < z` have modth: "x mod z \<ge> 0" by simp
+ from \<open>0 < z\<close> have modth: "x mod z \<ge> 0" by simp
have "(x div z) * z \<le> (x div z) * z" by simp
then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith
also have "\<dots> = x"
by (auto simp add: zmod_zdiv_equality [symmetric] ac_simps)
- also note `x < y * z`
+ also note \<open>x < y * z\<close>
finally show ?thesis
apply (auto simp add: mult_less_cancel_right)
using assms apply arith
@@ -66,7 +66,7 @@
from assms have "x < (y + 1) * z" by (auto simp add: int_distrib)
then have "x div z < y + 1"
apply (rule_tac y = "y + 1" in div_prop1)
- apply (auto simp add: `0 < z`)
+ apply (auto simp add: \<open>0 < z\<close>)
done
then show ?thesis by auto
qed
@@ -79,7 +79,7 @@
qed
-subsection {* Useful properties of congruences *}
+subsection \<open>Useful properties of congruences\<close>
lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"
by (auto simp add: zcong_def)
@@ -142,7 +142,7 @@
by auto
then have "p dvd 2"
by (auto simp add: dvd_def zcong_def)
- with `2 < p` show False
+ with \<open>2 < p\<close> show False
by (auto simp add: zdvd_not_zless)
qed
@@ -174,7 +174,7 @@
by (induct set: finite) (auto simp add: zgcd_zgcd_zmult)
-subsection {* Some properties of MultInv *}
+subsection \<open>Some properties of MultInv\<close>
lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==>
[(MultInv p x) = (MultInv p y)] (mod p)"
--- a/src/HOL/Old_Number_Theory/IntFact.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/IntFact.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,19 +3,19 @@
Copyright 2000 University of Cambridge
*)
-section {* Factorial on integers *}
+section \<open>Factorial on integers\<close>
theory IntFact
imports IntPrimes
begin
-text {*
+text \<open>
Factorial on integers and recursively defined set including all
Integers from @{text 2} up to @{text a}. Plus definition of product
of finite set.
\bigskip
-*}
+\<close>
fun zfact :: "int => int"
where "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
@@ -24,10 +24,10 @@
where "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
-text {*
+text \<open>
\medskip @{term d22set} --- recursively defined set including all
integers from @{text 2} up to @{text a}
-*}
+\<close>
declare d22set.simps [simp del]
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,22 +3,22 @@
Copyright 2000 University of Cambridge
*)
-section {* Divisibility and prime numbers (on integers) *}
+section \<open>Divisibility and prime numbers (on integers)\<close>
theory IntPrimes
imports Primes
begin
-text {*
+text \<open>
The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,
congruences (all on the Integers). Comparable to theory @{text
Primes}, but @{text dvd} is included here as it is not present in
main HOL. Also includes extended GCD and congruences not present in
@{text Primes}.
-*}
+\<close>
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
fun xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
where
@@ -38,7 +38,7 @@
where "[a = b] (mod m) = (m dvd (a - b))"
-subsection {* Euclid's Algorithm and GCD *}
+subsection \<open>Euclid's Algorithm and GCD\<close>
lemma zrelprime_zdvd_zmult_aux:
@@ -55,8 +55,8 @@
lemma zgcd_geq_zero: "0 <= zgcd x y"
by (auto simp add: zgcd_def)
-text{*This is merely a sanity check on zprime, since the previous version
- denoted the empty set.*}
+text\<open>This is merely a sanity check on zprime, since the previous version
+ denoted the empty set.\<close>
lemma "zprime 2"
apply (auto simp add: zprime_def)
apply (frule zdvd_imp_le, simp)
@@ -109,7 +109,7 @@
-subsection {* Congruences *}
+subsection \<open>Congruences\<close>
lemma zcong_1 [simp]: "[a = b] (mod 1)"
by (unfold zcong_def, auto)
@@ -281,7 +281,7 @@
apply (simp add: linorder_neq_iff)
apply (erule disjE)
prefer 2 apply (simp add: zcong_zmod_eq)
- txt{*Remainding case: @{term "m<0"}*}
+ txt\<open>Remainding case: @{term "m<0"}\<close>
apply (rule_tac t = m in minus_minus [THEN subst])
apply (subst zcong_zminus)
apply (subst zcong_zmod_eq, arith)
@@ -289,14 +289,14 @@
apply (simp add: zmod_zminus2_eq_if del: neg_mod_bound)
done
-subsection {* Modulo *}
+subsection \<open>Modulo\<close>
lemma zmod_zdvd_zmod:
"0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
by (rule mod_mod_cancel)
-subsection {* Extended GCD *}
+subsection \<open>Extended GCD\<close>
declare xzgcda.simps [simp del]
@@ -336,7 +336,7 @@
done
-text {* \medskip @{term xzgcd} linear *}
+text \<open>\medskip @{term xzgcd} linear\<close>
lemma xzgcda_linear_aux1:
"(a - r * b) * m + (c - r * d) * (n::int) =
@@ -399,7 +399,7 @@
zgcd a n = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
apply auto
apply (rule_tac [2] zcong_zless_imp_eq)
- apply (tactic {* stac @{context} (@{thm zcong_cancel2} RS sym) 6 *})
+ apply (tactic \<open>stac @{context} (@{thm zcong_cancel2} RS sym) 6\<close>)
apply (rule_tac [8] zcong_trans)
apply (simp_all (no_asm_simp))
prefer 2
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,40 +3,40 @@
Copyright 1996 University of Cambridge
*)
-section {* The Greatest Common Divisor *}
+section \<open>The Greatest Common Divisor\<close>
theory Legacy_GCD
imports Main
begin
-text {*
+text \<open>
See @{cite davenport92}. \bigskip
-*}
+\<close>
-subsection {* Specification of GCD on nats *}
+subsection \<open>Specification of GCD on nats\<close>
definition
- is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
+ is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- \<open>@{term gcd} as a relation\<close>
"is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
(\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
-text {* Uniqueness *}
+text \<open>Uniqueness\<close>
lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
by (simp add: is_gcd_def) (blast intro: dvd_antisym)
-text {* Connection to divides relation *}
+text \<open>Connection to divides relation\<close>
lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
by (auto simp add: is_gcd_def)
-text {* Commutativity *}
+text \<open>Commutativity\<close>
lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
by (auto simp add: is_gcd_def)
-subsection {* GCD on nat by Euclid's algorithm *}
+subsection \<open>GCD on nat by Euclid's algorithm\<close>
fun gcd :: "nat => nat => nat"
where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
@@ -68,10 +68,10 @@
declare gcd.simps [simp del]
-text {*
+text \<open>
\medskip @{term "gcd m n"} divides @{text m} and @{text n}. The
conjunctions don't seem provable separately.
-*}
+\<close>
lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"
@@ -80,24 +80,24 @@
apply (blast dest: dvd_mod_imp_dvd)
done
-text {*
+text \<open>
\medskip Maximality: for all @{term m}, @{term n}, @{term k}
naturals, if @{term k} divides @{term m} and @{term k} divides
@{term n} then @{term k} divides @{term "gcd m n"}.
-*}
+\<close>
lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
-text {*
+text \<open>
\medskip Function gcd yields the Greatest Common Divisor.
-*}
+\<close>
lemma is_gcd: "is_gcd m n (gcd m n) "
by (simp add: is_gcd_def gcd_greatest)
-subsection {* Derived laws for GCD *}
+subsection \<open>Derived laws for GCD\<close>
lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
by (blast intro!: gcd_greatest intro: dvd_trans)
@@ -125,12 +125,12 @@
lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
unfolding One_nat_def by (rule gcd_1_left)
-text {*
+text \<open>
\medskip Multiplication laws
-*}
+\<close>
lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
- -- {* @{cite \<open>page 27\<close> davenport92} *}
+ -- \<open>@{cite \<open>page 27\<close> davenport92}\<close>
apply (induct m n rule: gcd_induct)
apply simp
apply (case_tac "k = 0")
@@ -165,7 +165,7 @@
done
-text {* \medskip Addition laws *}
+text \<open>\medskip Addition laws\<close>
lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
by (cases "n = 0") (auto simp add: gcd_non_0)
@@ -190,9 +190,9 @@
lemma gcd_dvd_prod: "gcd m n dvd m * n"
using mult_dvd_mono [of 1] by auto
-text {*
+text \<open>
\medskip Division by gcd yields rrelatively primes.
-*}
+\<close>
lemma div_gcd_relprime:
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
@@ -313,7 +313,7 @@
done
-text {* We can get a stronger version with a nonzeroness assumption. *}
+text \<open>We can get a stronger version with a nonzeroness assumption.\<close>
lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
@@ -449,7 +449,7 @@
qed
-subsection {* LCM defined by GCD *}
+subsection \<open>LCM defined by GCD\<close>
definition
@@ -562,7 +562,7 @@
done
-subsection {* GCD and LCM on integers *}
+subsection \<open>GCD and LCM on integers\<close>
definition
zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
@@ -595,7 +595,7 @@
proof -
assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
- from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
+ from \<open>i dvd k * j\<close> obtain h where h: "k*j = i*h" unfolding dvd_def by blast
have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
unfolding dvd_def
by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
@@ -620,7 +620,7 @@
let ?k' = "nat \<bar>k\<bar>"
let ?m' = "nat \<bar>m\<bar>"
let ?n' = "nat \<bar>n\<bar>"
- from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
+ from \<open>k dvd m\<close> and \<open>k dvd n\<close> have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
unfolding zgcd_def by (simp only: zdvd_int)
@@ -696,7 +696,7 @@
done
lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
- -- {* addition is an AC-operator *}
+ -- \<open>addition is an AC-operator\<close>
lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
by (simp del: minus_mult_right [symmetric]
@@ -728,7 +728,7 @@
lemma dvd_imp_dvd_zlcm1:
assumes "k dvd i" shows "k dvd (zlcm i j)"
proof -
- have "nat(abs k) dvd nat(abs i)" using `k dvd i`
+ have "nat(abs k) dvd nat(abs i)" using \<open>k dvd i\<close>
by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
qed
@@ -736,7 +736,7 @@
lemma dvd_imp_dvd_zlcm2:
assumes "k dvd j" shows "k dvd (zlcm i j)"
proof -
- have "nat(abs k) dvd nat(abs j)" using `k dvd j`
+ have "nat(abs k) dvd nat(abs j)" using \<open>k dvd j\<close>
by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
qed
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Sat Oct 10 16:26:23 2015 +0200
@@ -2,7 +2,7 @@
Author: Amine Chaieb
*)
-section {* Pocklington's Theorem for Primes *}
+section \<open>Pocklington's Theorem for Primes\<close>
theory Pocklington
imports Primes
--- a/src/HOL/Old_Number_Theory/Primes.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1996 University of Cambridge
*)
-section {* Primality on nat *}
+section \<open>Primality on nat\<close>
theory Primes
imports Complex_Main Legacy_GCD
@@ -27,11 +27,11 @@
apply (metis gcd_dvd1 gcd_dvd2)
done
-text {*
+text \<open>
This theorem leads immediately to a proof of the uniqueness of
factorization. If @{term p} divides a product of primes then it is
one of those primes.
-*}
+\<close>
lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
by (blast intro: relprime_dvd_mult prime_imp_relprime)
@@ -92,7 +92,7 @@
ultimately show ?thesis by blast
qed
-text {* Elementary theory of divisibility *}
+text \<open>Elementary theory of divisibility\<close>
lemma divides_ge: "(a::nat) dvd b \<Longrightarrow> b = 0 \<or> a \<le> b" unfolding dvd_def by auto
lemma divides_antisym: "(x::nat) dvd y \<and> y dvd x \<longleftrightarrow> x = y"
using dvd_antisym[of x y] by auto
@@ -176,7 +176,7 @@
lemma divides_rexp:
"x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" by (simp add: dvd_mult2[of x y])
-text {* Coprimality *}
+text \<open>Coprimality\<close>
lemma coprime: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
using gcd_unique[of 1 a b, simplified] by (auto simp add: coprime_def)
@@ -379,7 +379,7 @@
qed
-text {* A binary form of the Chinese Remainder Theorem. *}
+text \<open>A binary form of the Chinese Remainder Theorem.\<close>
lemma chinese_remainder: assumes ab: "coprime a b" and a:"a \<noteq> 0" and b:"b \<noteq> 0"
shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
@@ -397,9 +397,9 @@
thus ?thesis by blast
qed
-text {* Primality *}
+text \<open>Primality\<close>
-text {* A few useful theorems about primes *}
+text \<open>A few useful theorems about primes\<close>
lemma prime_0[simp]: "~prime 0" by (simp add: prime_def)
lemma prime_1[simp]: "~ prime 1" by (simp add: prime_def)
@@ -591,7 +591,7 @@
lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto
-text {* One property of coprimality is easier to prove via prime factors. *}
+text \<open>One property of coprimality is easier to prove via prime factors.\<close>
lemma prime_divprod_pow:
assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
@@ -714,7 +714,7 @@
ultimately show ?ths by blast
qed
-text {* More useful lemmas. *}
+text \<open>More useful lemmas.\<close>
lemma prime_product:
assumes "prime (p * q)"
shows "p = 1 \<or> q = 1"
@@ -722,7 +722,7 @@
from assms have
"1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
unfolding prime_def by auto
- from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
+ from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
have "p dvd p * q" by simp
then have "p = 1 \<or> p = p * q" by (rule P)
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sat Oct 10 16:26:23 2015 +0200
@@ -2,16 +2,16 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-section {* The law of Quadratic reciprocity *}
+section \<open>The law of Quadratic reciprocity\<close>
theory Quadratic_Reciprocity
imports Gauss
begin
-text {*
+text \<open>
Lemmas leading up to the proof of theorem 3.3 in Niven and
Zuckerman's presentation.
-*}
+\<close>
context GAUSS
begin
@@ -153,7 +153,7 @@
done
-subsection {* Stuff about S, S1 and S2 *}
+subsection \<open>Stuff about S, S1 and S2\<close>
locale QRTEMP =
fixes p :: "int"
--- a/src/HOL/Old_Number_Theory/Residues.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Residues.thy Sat Oct 10 16:26:23 2015 +0200
@@ -2,15 +2,15 @@
Authors: Jeremy Avigad, David Gray, and Adam Kramer
*)
-section {* Residue Sets *}
+section \<open>Residue Sets\<close>
theory Residues
imports Int2
begin
-text {*
+text \<open>
\medskip Define the residue of a set, the standard residue,
- quadratic residues, and prove some basic properties. *}
+ quadratic residues, and prove some basic properties.\<close>
definition ResSet :: "int => int set => bool"
where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
@@ -33,7 +33,7 @@
where "SRStar p = {x. (0 < x) & (x < p)}"
-subsection {* Some useful properties of StandardRes *}
+subsection \<open>Some useful properties of StandardRes\<close>
lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
by (auto simp add: StandardRes_def zcong_zmod)
@@ -61,7 +61,7 @@
by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def)
-subsection {* Relations between StandardRes, SRStar, and SR *}
+subsection \<open>Relations between StandardRes, SRStar, and SR\<close>
lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p"
by (auto simp add: SRStar_def SR_def)
@@ -115,7 +115,7 @@
by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
-subsection {* Properties relating ResSets with StandardRes *}
+subsection \<open>Properties relating ResSets with StandardRes\<close>
lemma aux: "x mod m = y mod m ==> [x = y] (mod m)"
apply (subgoal_tac "x = y ==> [x = y](mod m)")
@@ -158,7 +158,7 @@
by (auto simp add: ResSet_def)
-subsection {* Property for SRStar *}
+subsection \<open>Property for SRStar\<close>
lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"
by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,20 +3,20 @@
Copyright 2000 University of Cambridge
*)
-section {* Wilson's Theorem using a more abstract approach *}
+section \<open>Wilson's Theorem using a more abstract approach\<close>
theory WilsonBij
imports BijectionRel IntFact
begin
-text {*
+text \<open>
Wilson's Theorem using a more ``abstract'' approach based on
bijections between sets. Does not use Fermat's Little Theorem
(unlike Russinoff).
-*}
+\<close>
-subsection {* Definitions and lemmas *}
+subsection \<open>Definitions and lemmas\<close>
definition reciR :: "int => int => int => bool"
where "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
@@ -28,7 +28,7 @@
else 0)"
-text {* \medskip Inverse *}
+text \<open>\medskip Inverse\<close>
lemma inv_correct:
"zprime p ==> 0 < a ==> a < p
@@ -47,7 +47,7 @@
lemma inv_not_0:
"zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0"
- -- {* same as @{text WilsonRuss} *}
+ -- \<open>same as @{text WilsonRuss}\<close>
apply safe
apply (cut_tac a = a and p = p in inv_is_inv)
apply (unfold zcong_def)
@@ -56,7 +56,7 @@
lemma inv_not_1:
"zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 1"
- -- {* same as @{text WilsonRuss} *}
+ -- \<open>same as @{text WilsonRuss}\<close>
apply safe
apply (cut_tac a = a and p = p in inv_is_inv)
prefer 4
@@ -67,7 +67,7 @@
done
lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
- -- {* same as @{text WilsonRuss} *}
+ -- \<open>same as @{text WilsonRuss}\<close>
apply (unfold zcong_def)
apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
@@ -81,7 +81,7 @@
lemma inv_not_p_minus_1:
"zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> p - 1"
- -- {* same as @{text WilsonRuss} *}
+ -- \<open>same as @{text WilsonRuss}\<close>
apply safe
apply (cut_tac a = a and p = p in inv_is_inv)
apply auto
@@ -91,10 +91,10 @@
apply auto
done
-text {*
+text \<open>
Below is slightly different as we don't expand @{term [source] inv}
but use ``@{text correct}'' theorems.
-*}
+\<close>
lemma inv_g_1: "zprime p ==> 1 < a ==> a < p - 1 ==> 1 < inv p a"
apply (subgoal_tac "inv p a \<noteq> 1")
@@ -111,13 +111,13 @@
lemma inv_less_p_minus_1:
"zprime p ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1"
- -- {* ditto *}
+ -- \<open>ditto\<close>
apply (subst order_less_le)
apply (simp add: inv_not_p_minus_1 inv_less)
done
-text {* \medskip Bijection *}
+text \<open>\medskip Bijection\<close>
lemma aux1: "1 < x ==> 0 \<le> (x::int)"
apply auto
@@ -139,9 +139,9 @@
apply (unfold inj_on_def)
apply auto
apply (rule zcong_zless_imp_eq)
- apply (tactic {* stac @{context} (@{thm zcong_cancel} RS sym) 5 *})
+ apply (tactic \<open>stac @{context} (@{thm zcong_cancel} RS sym) 5\<close>)
apply (rule_tac [7] zcong_trans)
- apply (tactic {* stac @{context} @{thm zcong_sym} 8 *})
+ apply (tactic \<open>stac @{context} @{thm zcong_sym} 8\<close>)
apply (erule_tac [7] inv_is_inv)
apply (tactic "asm_simp_tac @{context} 9")
apply (erule_tac [9] inv_is_inv)
@@ -192,15 +192,15 @@
apply (unfold reciR_def uniqP_def)
apply auto
apply (rule zcong_zless_imp_eq)
- apply (tactic {* stac @{context} (@{thm zcong_cancel2} RS sym) 5 *})
+ apply (tactic \<open>stac @{context} (@{thm zcong_cancel2} RS sym) 5\<close>)
apply (rule_tac [7] zcong_trans)
- apply (tactic {* stac @{context} @{thm zcong_sym} 8 *})
+ apply (tactic \<open>stac @{context} @{thm zcong_sym} 8\<close>)
apply (rule_tac [6] zless_zprime_imp_zrelprime)
apply auto
apply (rule zcong_zless_imp_eq)
- apply (tactic {* stac @{context} (@{thm zcong_cancel} RS sym) 5 *})
+ apply (tactic \<open>stac @{context} (@{thm zcong_cancel} RS sym) 5\<close>)
apply (rule_tac [7] zcong_trans)
- apply (tactic {* stac @{context} @{thm zcong_sym} 8 *})
+ apply (tactic \<open>stac @{context} @{thm zcong_sym} 8\<close>)
apply (rule_tac [6] zless_zprime_imp_zrelprime)
apply auto
done
@@ -220,7 +220,7 @@
done
-subsection {* Wilson *}
+subsection \<open>Wilson\<close>
lemma bijER_zcong_prod_1:
"zprime p ==> A \<in> bijER (reciR p) ==> [\<Prod>A = 1] (mod p)"
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Sat Oct 10 16:21:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Sat Oct 10 16:26:23 2015 +0200
@@ -3,18 +3,18 @@
Copyright 2000 University of Cambridge
*)
-section {* Wilson's Theorem according to Russinoff *}
+section \<open>Wilson's Theorem according to Russinoff\<close>
theory WilsonRuss
imports EulerFermat
begin
-text {*
+text \<open>
Wilson's Theorem following quite closely Russinoff's approach
using Boyer-Moore (using finite sets instead of lists, though).
-*}
+\<close>
-subsection {* Definitions and lemmas *}
+subsection \<open>Definitions and lemmas\<close>
definition inv :: "int => int => int"
where "inv p a = (a^(nat (p - 2))) mod p"
@@ -26,7 +26,7 @@
in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
-text {* \medskip @{term [source] inv} *}
+text \<open>\medskip @{term [source] inv}\<close>
lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
by (subst int_int_eq [symmetric]) auto
@@ -149,7 +149,7 @@
done
-text {* \medskip @{term wset} *}
+text \<open>\medskip @{term wset}\<close>
declare wset.simps [simp del]
@@ -252,7 +252,7 @@
apply (subst wset.simps)
apply (auto, unfold Let_def, auto)
apply (subst setprod.insert)
- apply (tactic {* stac @{context} @{thm setprod.insert} 3 *})
+ apply (tactic \<open>stac @{context} @{thm setprod.insert} 3\<close>)
apply (subgoal_tac [5]
"zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
prefer 5
@@ -281,7 +281,7 @@
done
-subsection {* Wilson *}
+subsection \<open>Wilson\<close>
lemma prime_g_5: "zprime p \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
apply (unfold zprime_def dvd_def)