# HG changeset patch # User wenzelm # Date 1444487183 -7200 # Node ID efac889fccbcfa34f01aa605a92635382fe1d87b # Parent ddca85598c659453611448b647abde93fe767713 isabelle update_cartouches; diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/AbelCoset.thy --- 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 \More Lifting from Groups to Abelian Groups\ -subsubsection {* Definitions *} +subsubsection \Definitions\ -text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come - up with better syntax here *} +text \Hiding @{text "<+>"} from @{theory Sum_Type} until I come + up with better syntax here\ no_notation Sum_Type.Plus (infixr "<+>" 65) @@ -41,12 +41,12 @@ definition A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \ ('a set) monoid" (infixl "A'_Mod" 65) - --{*Actually defined for groups rather than monoids*} + --\Actually defined for groups rather than monoids\ where "A_FactGroup G H = FactGroup \carrier = carrier G, mult = add G, one = zero G\ H" definition a_kernel :: "('a, 'm) ring_scheme \ ('b, 'n) ring_scheme \ ('a \ 'b) \ 'a set" - --{*the kernel of a homomorphism (additive)*} + --\the kernel of a homomorphism (additive)\ where "a_kernel G H h = kernel \carrier = carrier G, mult = add G, one = zero G\ \carrier = carrier H, mult = add H, one = zero H\ h" @@ -103,7 +103,7 @@ by (fold a_inv_def) -subsubsection {* Cosets *} +subsubsection \Cosets\ lemma (in abelian_group) a_coset_add_assoc: "[| M \ carrier G; g \ carrier G; h \ 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\Really needed?\ lemma (in abelian_group) a_transpose_inv: "[| x \ y = z; x \ carrier G; y \ carrier G; z \ carrier G |] ==> (\ x) \ z = y" @@ -179,7 +179,7 @@ *) -subsubsection {* Subgroups *} +subsubsection \Subgroups\ 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 \Additive subgroups are normal\ -text {* Every subgroup of an @{text "abelian_group"} is normal *} +text \Every subgroup of an @{text "abelian_group"} is normal\ locale abelian_subgroup = additive_subgroup + abelian_group G + assumes a_normal: "normal H \carrier = carrier G, mult = add G, one = zero G\" @@ -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\Alternative characterization of normal subgroups\ lemma (in abelian_group) a_normal_inv_iff: "(N \ \carrier = carrier G, mult = add G, one = zero G\) = (subgroup N \carrier = carrier G, mult = add G, one = zero G\ & (\x \ carrier G. \h \ N. x \ h \ (\ x) \ N))" @@ -378,12 +378,12 @@ lemma (in abelian_subgroup) rcosets_add_eq: "M \ a_rcosets H \ H <+> M = M" - -- {* generalizes @{text subgroup_mult_id} *} + -- \generalizes @{text subgroup_mult_id}\ by (rule normal.rcosets_mult_eq [OF a_normal, folded set_add_def A_RCOSETS_def, simplified monoid_record_simps]) -subsubsection {* Congruence Relation *} +subsubsection \Congruence Relation\ 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 \Factorization\ 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 \Since the Factorization is based on an \emph{abelian} subgroup, is results in + a commutative group\ 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\The coset map is a homomorphism from @{term G} to the quotient group + @{term "G Mod H"}\ lemma (in abelian_subgroup) a_r_coset_hom_A_Mod: "(\a. H +> a) \ hom \carrier = carrier G, mult = add G, one = zero G\ (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 \The isomorphism theorems have been omitted from lifting, at + least for now\ -subsubsection{*The First Isomorphism Theorem*} +subsubsection\The First Isomorphism Theorem\ -text{*The quotient by the kernel of a homomorphism is isomorphic to the - range of that homomorphism.*} +text\The quotient by the kernel of a homomorphism is isomorphic to the + range of that homomorphism.\ 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 \Homomorphisms\ 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\The kernel of a homomorphism is an abelian subgroup\ 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\If the homomorphism @{term h} is onto @{term H}, then so is the +homomorphism from the quotient group\ lemma (in abelian_group_hom) A_FactGroup_onto: assumes h: "h ` carrier G = carrier H" shows "(\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\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}.\ theorem (in abelian_group_hom) A_FactGroup_iso: "h ` carrier G = carrier H \ (\X. the_elem (h`X)) \ (G A_Mod (a_kernel G H h)) \ @@ -641,9 +641,9 @@ folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) -subsubsection {* Cosets *} +subsubsection \Cosets\ -text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *} +text \Not eveything from \texttt{CosetExt.thy} is lifted here.\ lemma (in additive_subgroup) a_Hcarr [simp]: assumes hH: "h \ H" @@ -725,7 +725,7 @@ folded A_RCOSETS_def, simplified monoid_record_simps]) -subsubsection {* Addition of Subgroups *} +subsubsection \Addition of Subgroups\ lemma (in abelian_monoid) set_add_closed: assumes Acarr: "A \ carrier G" diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Bij.thy --- 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 \Bijections of a Set, Permutation and Automorphism Groups\ definition Bij :: "'a set \ ('a \ 'a) set" - --{*Only extensional functions, since otherwise we get too many.*} + --\Only extensional functions, since otherwise we get too many.\ where "Bij S = extensional S \ {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 \Bijections Form a Group\ lemma restrict_inv_into_Bij: "f \ Bij S \ (\x \ S. (inv_into S f) x) \ Bij S" by (simp add: Bij_def bij_betw_inv_into) @@ -57,7 +57,7 @@ done -subsection{*Automorphisms Form a Group*} +subsection\Automorphisms Form a Group\ lemma Bij_inv_into_mem: "\ f \ Bij S; x \ S\ \ inv_into S f x \ S" by (simp add: Bij_def bij_betw_def inv_into_into) diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Congruence.thy --- 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 \Objects\ -subsection {* Structure with Carrier Set. *} +subsection \Structure with Carrier Set.\ record 'a partial_object = carrier :: "'a set" -subsection {* Structure with Carrier and Equivalence Relation @{text eq} *} +subsection \Structure with Carrier and Equivalence Relation @{text eq}\ record 'a eq_object = "'a partial_object" + eq :: "'a \ 'a \ bool" (infixl ".=\" 50) diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Coset.thy --- 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 \Cosets and Quotient Groups\ definition r_coset :: "[_, 'a set, 'a] \ 'a set" (infixl "#>\" 60) @@ -39,7 +39,7 @@ "H \ G \ normal H G" -subsection {*Basic Properties of Cosets*} +subsection \Basic Properties of Cosets\ lemma (in group) coset_mult_assoc: "[| M \ carrier G; g \ carrier G; h \ carrier G |] @@ -85,7 +85,7 @@ lemma (in group) coset_join2: "\x \ carrier G; subgroup H G; x\H\ \ H #> x = H" - --{*Alternative proof is to put @{term "x=\"} in @{text repr_independence}.*} + --\Alternative proof is to put @{term "x=\"} in @{text repr_independence}.\ by (force simp add: subgroup.m_closed r_coset_def solve_equation) lemma (in monoid) r_coset_subset_G: @@ -100,7 +100,7 @@ "\H \ carrier G; x \ carrier G\ \ H #> x \ rcosets H" by (auto simp add: RCOSETS_def) -text{*Really needed?*} +text\Really needed?\ lemma (in group) transpose_inv: "[| x \ y = z; x \ carrier G; y \ carrier G; z \ carrier G |] ==> (inv x) \ z = y" @@ -112,7 +112,7 @@ subgroup.one_closed) done -text (in group) {* Opposite of @{thm [source] "repr_independence"} *} +text (in group) \Opposite of @{thm [source] "repr_independence"}\ lemma (in group) repr_independenceD: assumes "subgroup H G" assumes ycarr: "y \ carrier G" @@ -127,7 +127,7 @@ done qed -text {* Elements of a right coset are in the carrier *} +text \Elements of a right coset are in the carrier\ lemma (in subgroup) elemrcos_carrier: assumes "group G" assumes acarr: "a \ carrier G" @@ -171,7 +171,7 @@ qed qed -text {* Step one for lemma @{text "rcos_module"} *} +text \Step one for lemma @{text "rcos_module"}\ lemma (in subgroup) rcos_module_imp: assumes "group G" assumes xcarr: "x \ carrier G" @@ -211,7 +211,7 @@ show "x' \ (inv x) \ H" by simp qed -text {* Step two for lemma @{text "rcos_module"} *} +text \Step two for lemma @{text "rcos_module"}\ lemma (in subgroup) rcos_module_rev: assumes "group G" assumes carr: "x \ carrier G" "x' \ carrier G" @@ -243,7 +243,7 @@ by fast qed -text {* Module property of right cosets *} +text \Module property of right cosets\ lemma (in subgroup) rcos_module: assumes "group G" assumes carr: "x \ carrier G" "x' \ carrier G" @@ -262,7 +262,7 @@ qed qed -text {* Right cosets are subsets of the carrier. *} +text \Right cosets are subsets of the carrier.\ lemma (in subgroup) rcosets_carrier: assumes "group G" assumes XH: "X \ rcosets H" @@ -283,7 +283,7 @@ by (rule r_coset_subset_G) qed -text {* Multiplication of general subsets *} +text \Multiplication of general subsets\ lemma (in monoid) set_mult_closed: assumes Acarr: "A \ carrier G" and Bcarr: "B \ carrier G" @@ -381,7 +381,7 @@ qed -subsection {* Normal subgroups *} +subsection \Normal subgroups\ lemma normal_imp_subgroup: "H \ G \ 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\Alternative characterization of normal subgroups\ lemma (in group) normal_inv_iff: "(N \ G) = (subgroup N G & (\x \ carrier G. \h \ N. x \ h \ (inv x) \ N))" @@ -456,7 +456,7 @@ qed -subsection{*More Properties of Cosets*} +subsection\More Properties of Cosets\ lemma (in group) lcos_m_assoc: "[| M \ carrier G; g \ carrier G; h \ carrier G |] @@ -524,7 +524,7 @@ done -subsubsection {* Set of Inverses of an @{text r_coset}. *} +subsubsection \Set of Inverses of an @{text r_coset}.\ lemma (in normal) rcos_inv: assumes x: "x \ carrier G" @@ -549,7 +549,7 @@ qed -subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*} +subsubsection \Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.\ lemma (in group) setmult_rcos_assoc: "\H \ carrier G; K \ carrier G; x \ carrier G\ @@ -584,12 +584,12 @@ by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3) lemma (in normal) rcosets_mult_eq: "M \ rcosets H \ H <#> M = M" - -- {* generalizes @{text subgroup_mult_id} *} + -- \generalizes @{text subgroup_mult_id}\ by (auto simp add: RCOSETS_def subset setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms) -subsubsection{*An Equivalence Relation*} +subsubsection\An Equivalence Relation\ definition r_congruent :: "[('a,'b)monoid_scheme, 'a set] \ ('a*'a)set" ("rcong\ _") @@ -628,9 +628,9 @@ qed qed -text{*Equivalence classes of @{text rcong} correspond to left cosets. +text\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.\ (* 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\Two Distinct Right Cosets are Disjoint\ lemma (in group) rcos_equation: assumes "subgroup H G" @@ -679,9 +679,9 @@ qed -subsection {* Further lemmas for @{text "r_congruent"} *} +subsection \Further lemmas for @{text "r_congruent"}\ -text {* The relation is a congruence *} +text \The relation is a congruence\ lemma (in normal) congruent_rcong: shows "congruent2 (rcong H) (rcong H) (\a b. a \ b <# H)" @@ -753,7 +753,7 @@ qed -subsection {*Order of a Group and Lagrange's Theorem*} +subsection \Order of a Group and Lagrange's Theorem\ definition order :: "('a, 'b) monoid_scheme \ 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\The next two lemmas support the proof of @{text card_cosets_equal}.\ lemma (in group) inj_on_f: "\H \ carrier G; a \ carrier G\ \ inj_on (\y. y \ 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\The sets @{term "H #> a"} and @{term "H"} are finite.\ 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 \Quotient Groups: Factorization of a Group\ definition FactGroup :: "[('a,'b) monoid_scheme, 'a set] \ ('a set) monoid" (infixl "Mod" 65) - --{*Actually defined for groups rather than monoids*} + --\Actually defined for groups rather than monoids\ where "FactGroup G H = \carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\" 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\The coset map is a homomorphism from @{term G} to the quotient group + @{term "G Mod H"}\ lemma (in normal) r_coset_hom_Mod: "(\a. H #> a) \ 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\The First Isomorphism Theorem\ -text{*The quotient by the kernel of a homomorphism is isomorphic to the - range of that homomorphism.*} +text\The quotient by the kernel of a homomorphism is isomorphic to the + range of that homomorphism.\ definition kernel :: "('a, 'm) monoid_scheme \ ('b, 'n) monoid_scheme \ ('a \ 'b) \ 'a set" - --{*the kernel of a homomorphism*} + --\the kernel of a homomorphism\ where "kernel G H h = {x. x \ carrier G & h x = \\<^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\The kernel of a homomorphism is a normal subgroup\ lemma (in group_hom) normal_kernel: "(kernel G H h) \ 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\Lemma for the following injectivity result\ lemma (in group_hom) FactGroup_subset: "\g \ carrier G; g' \ carrier G; h g = h g'\ \ kernel G H h #> g \ 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\If the homomorphism @{term h} is onto @{term H}, then so is the +homomorphism from the quotient group\ lemma (in group_hom) FactGroup_onto: assumes h: "h ` carrier G = carrier H" shows "(\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\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}.\ theorem (in group_hom) FactGroup_iso: "h ` carrier G = carrier H \ (\X. the_elem (h`X)) \ (G Mod (kernel G H h)) \ H" diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Divisibility.thy --- 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 \Divisibility in monoids and rings\ theory Divisibility imports "~~/src/HOL/Library/Permutation" Coset Group begin -section {* Factorial Monoids *} - -subsection {* Monoids with Cancellation Law *} +section \Factorial Monoids\ + +subsection \Monoids with Cancellation Law\ locale monoid_cancel = monoid + assumes l_cancel: @@ -57,7 +57,7 @@ .. -subsection {* Products of Units in Monoids *} +subsection \Products of Units in Monoids\ lemma (in monoid) Units_m_closed[simp, intro]: assumes h1unit: "h1 \ Units G" and h2unit: "h2 \ Units G" @@ -144,9 +144,9 @@ qed -subsection {* Divisibility and Association *} - -subsubsection {* Function definitions *} +subsection \Divisibility and Association\ + +subsubsection \Function definitions\ definition factor :: "[_, 'a, 'a] \ bool" (infix "divides\" 65) @@ -174,7 +174,7 @@ (\a\carrier G. \b\carrier G. p divides\<^bsub>G\<^esub> (a \\<^bsub>G\<^esub> b) \ p divides\<^bsub>G\<^esub> a \ p divides\<^bsub>G\<^esub> b)" -subsubsection {* Divisibility *} +subsubsection \Divisibility\ lemma dividesI: fixes G (structure) @@ -309,7 +309,7 @@ by (fast dest: divides_unit intro: unit_divides) -subsubsection {* Association *} +subsubsection \Association\ lemma associatedI: fixes G (structure) @@ -449,7 +449,7 @@ done -subsubsection {* Division and associativity *} +subsubsection \Division and associativity\ lemma divides_antisym: fixes G (structure) @@ -497,7 +497,7 @@ done -subsubsection {* Multiplication and associativity *} +subsubsection \Multiplication and associativity\ lemma (in monoid_cancel) mult_cong_r: assumes "b \ b'" @@ -545,7 +545,7 @@ done -subsubsection {* Units *} +subsubsection \Units\ lemma (in monoid_cancel) assoc_unit_l [trans]: assumes asc: "a \ b" and bunit: "b \ Units G" @@ -604,7 +604,7 @@ done -subsubsection {* Proper factors *} +subsubsection \Proper factors\ 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 \Irreducible Elements and Primes\ + +subsubsection \Irreducible elements\ lemma irreducibleI: fixes G (structure) @@ -903,7 +903,7 @@ qed -subsubsection {* Prime elements *} +subsubsection \Prime elements\ 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 \Factorization and Factorial Monoids\ + +subsubsection \Function definitions\ definition factors :: "[_, 'a list, 'a] \ bool" @@ -972,9 +972,9 @@ set fs \ carrier G; set fs' \ carrier G\ \ essentially_equal G fs fs'" -subsubsection {* Comparing lists of elements *} - -text {* Association on lists *} +subsubsection \Comparing lists of elements\ + +text \Association on lists\ lemma (in monoid) listassoc_refl [simp, intro]: assumes "set as \ carrier G" @@ -1019,7 +1019,7 @@ done -text {* Permutations *} +text \Permutations\ lemma perm_map [intro]: assumes p: "a <~~> b" @@ -1077,7 +1077,7 @@ perm_setP[of _ _ "\as. \a\as. irreducible G a"] -text {* Essentially equal factorizations *} +text \Essentially equal factorizations\ lemma (in monoid) essentially_equalI: assumes ex: "fs1 <~~> fs1'" "fs1' [\] fs2" @@ -1149,9 +1149,9 @@ qed -subsubsection {* Properties of lists of elements *} - -text {* Multiplication of factors in a list *} +subsubsection \Properties of lists of elements\ + +text \Multiplication of factors in a list\ lemma (in monoid) multlist_closed [simp, intro]: assumes ascarr: "set fs \ carrier G" @@ -1224,7 +1224,7 @@ done -subsubsection {* Factorization in irreducible elements *} +subsubsection \Factorization in irreducible elements\ lemma wfactorsI: fixes G (structure) @@ -1328,7 +1328,7 @@ qed -text {* Comparing wfactors *} +text \Comparing wfactors\ 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 \Essentially equal factorizations\ lemma (in comm_monoid_cancel) unitfactor_ee: assumes uunit: "u \ Units G" @@ -1719,7 +1719,7 @@ qed -subsubsection {* Factorial monoids and wfactors *} +subsubsection \Factorial monoids and wfactors\ 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 \Factorizations as Multisets\ + +text \Gives useful operations like intersection\ (* FIXME: use class_of x instead of closure_of {x} *) @@ -1795,7 +1795,7 @@ "fmset G as = mset (map (\a. assocs G a) as)" -text {* Helper lemmas *} +text \Helper lemmas\ lemma (in monoid) assocs_repr_independence: assumes "y \ assocs G x" @@ -1834,7 +1834,7 @@ assocs_repr_independenceD[THEN assocs_assoc] -subsubsection {* Comparing multisets *} +subsubsection \Comparing multisets\ 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 \Interpreting multisets as factorizations\ lemma (in monoid) mset_fmsetEx: assumes elems: "\X. X \ set_mset Cs \ \x. P x \ X = assocs G x" @@ -2089,7 +2089,7 @@ qed -subsubsection {* Multiplication on multisets *} +subsubsection \Multiplication on multisets\ 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 \ b)" @@ -2131,7 +2131,7 @@ qed -subsubsection {* Divisibility on multisets *} +subsubsection \Divisibility on multisets\ 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 \Proper factors on multisets\ lemma (in factorial_monoid) fmset_properfactor: assumes asubb: "fmset G as \# fmset G bs" @@ -2250,7 +2250,7 @@ apply (metis assms divides_fmsubset fmsubset_divides) done -subsection {* Irreducible Elements are Prime *} +subsection \Irreducible Elements are Prime\ 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 \Greatest Common Divisors and Lowest Common Multiples\ + +subsubsection \Definitions\ definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \ bool" ("(_ gcdof\ _ _)" [81,81,81] 80) @@ -2529,7 +2529,7 @@ "wf {(x, y). x \ carrier G \ y \ carrier G \ properfactor G x y}" -subsubsection {* Connections to \texttt{Lattice.thy} *} +subsubsection \Connections to \texttt{Lattice.thy}\ lemma gcdof_greatestLower: fixes G (structure) @@ -2571,7 +2571,7 @@ by fast -subsubsection {* Existence of gcd and lcm *} +subsubsection \Existence of gcd and lcm\ lemma (in factorial_monoid) gcdof_exists: assumes acarr: "a \ carrier G" and bcarr: "b \ carrier G" @@ -2753,9 +2753,9 @@ qed -subsection {* Conditions for Factoriality *} - -subsubsection {* Gcd condition *} +subsection \Conditions for Factoriality\ + +subsubsection \Gcd condition\ 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 \Divisor chain condition\ lemma (in divisor_chain_condition_monoid) wfactors_exist: assumes acarr: "a \ carrier G" @@ -3243,7 +3243,7 @@ qed -subsubsection {* Primeness condition *} +subsubsection \Primeness condition\ lemma (in comm_monoid_cancel) multlist_prime_pos: assumes carr: "a \ carrier G" "set as \ carrier G" @@ -3481,9 +3481,9 @@ done -subsubsection {* Application to factorial monoids *} - -text {* Number of factors for wellfoundedness *} +subsubsection \Application to factorial monoids\ + +text \Number of factors for wellfoundedness\ definition factorcount :: "_ \ 'a \ nat" where @@ -3678,7 +3678,7 @@ qed -subsection {* Factoriality Theorems *} +subsection \Factoriality Theorems\ theorem factorial_condition_one: (* Jacobson theorem 2.21 *) shows "(divisor_chain_condition_monoid G \ primeness_condition_monoid G) = diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Exponent.thy --- 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 \Sylow's Theorem\ -subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*} +subsection \The Combinatorial Argument Underlying the First Sylow Theorem\ 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\Prime Theorems\ lemma prime_iff: "(prime p) = (Suc 0 < p & (\a b. p dvd a*b --> (p dvd a) | (p dvd b)))" @@ -100,7 +100,7 @@ done -text{*Exponent Theorems*} +text\Exponent Theorems\ lemma exponent_ge [rule_format]: "[|p^k dvd n; prime p; 0 k <= exponent p n" @@ -182,7 +182,7 @@ done -text{*Main Combinatorial Argument*} +text\Main Combinatorial Argument\ 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\Suc rules that we have to delete from the simpset\ 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\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.\ 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\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}.\ 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\one subgoal left!\ apply (auto simp: mult_ac) apply (subst times_binomial_minus1_eq, simp) apply (simp add: diff_le_mono exponent_mult_add) diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/FiniteProduct.thy --- 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 \Product Operator for Commutative Monoids\ -subsubsection {* Inductive Definition of a Relation for Products over Sets *} +subsubsection \Inductive Definition of a Relation for Products over Sets\ -text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not +text \Instantiation of locale @{text LC} of theory @{text Finite_Set} is not possible, because here we have explicit typing rules like @{text "x \ carrier G"}. We introduce an explicit argument for the domain - @{text D}. *} + @{text D}.\ inductive_set foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set" @@ -61,7 +61,7 @@ qed -text {* Left-Commutative Operations *} +text \Left-Commutative Operations\ 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 \force simplification of @{text "card A < card (insert ...)"}.\ 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 \ xb"}. *} + txt \case @{prop "xa \ xb"}.\ apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb \ Aa & xa \ 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. *} +-- \Delete rules to do with @{text foldSetD} relation.\ declare foldSetD_imp_finite [simp del] empty_foldSetDE [rule del] @@ -230,12 +230,12 @@ foldSetD_closed [rule del] -text {* Commutative Monoids *} +text \Commutative Monoids\ -text {* +text \ We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"} instead of @{text "'b => 'a => 'a"}. -*} +\ locale ACeD = fixes D :: "'a set" @@ -263,7 +263,7 @@ proof - assume "x \ D" then have "x \ e = x" by (rule ident) - with `x \ D` show ?thesis by (simp add: commute) + with \x \ D\ 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 \Products over Finite Sets\ definition finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" @@ -299,7 +299,7 @@ ("(3\__\_. _)" [1000, 0, 51, 10] 10) translations "\\i\A. b" \ "CONST finprod \\ (%i. b) A" - -- {* Beware of argument permutation! *} + -- \Beware of argument permutation!\ lemma (in comm_monoid) finprod_empty [simp]: "finprod G f {} = \" @@ -367,7 +367,7 @@ "[| finite A; finite B; g \ A -> carrier G; g \ B -> carrier G |] ==> finprod G g (A Un B) \ finprod G g (A Int B) = finprod G g A \ finprod G g B" --- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} +-- \The reversed orientation looks more natural, but LOOPS as a simprule!\ 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 \Usually, if this rule causes a failed congruence proof error, the reason is that the premise @{text "g \ 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. -*} +\ end @@ -497,7 +497,7 @@ case (infinite A) hence "\ finite (h ` A)" using finite_imageD by blast - with `\ finite A` show ?case by simp + with \\ finite A\ show ?case by simp qed (auto simp add: Pi_def) lemma finprod_const: diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Group.thy --- 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 \Monoids and Groups\ -subsection {* Definitions *} +subsection \Definitions\ -text {* +text \ Definitions follow @{cite "Jacobson:1985"}. -*} +\ record 'a monoid = "'a partial_object" + mult :: "['a, 'a] \ 'a" (infixl "\\" 70) @@ -26,7 +26,7 @@ definition Units :: "_ => 'a set" - --{*The set of invertible elements*} + --\The set of invertible elements\ where "Units G = {y. y \ carrier G & (\x \ carrier G. x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub> & y \\<^bsub>G\<^esub> x = \\<^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 \Power\ lemma (in monoid) nat_pow_closed [intro, simp]: "x \ carrier G ==> x (^) (n::nat) \ carrier G" @@ -218,11 +218,11 @@ (* Jacobson defines the order of a monoid here. *) -subsection {* Groups *} +subsection \Groups\ -text {* +text \ A group is a monoid all of whose elements are invertible. -*} +\ 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 \Cancellation Laws and Basic Properties\ lemma (in group) l_cancel [simp]: "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==> @@ -397,7 +397,7 @@ "\ a \ carrier G; b \ carrier G; c \ carrier G \ \ a = b \ inv c \ b = a \ c" by (metis inv_equality l_inv_ex l_one m_assoc r_inv) -text {* Power *} +text \Power\ 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 \Subgroups\ locale subgroup = fixes H and G (structure) @@ -469,18 +469,18 @@ done qed -text {* +text \ 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 \ inv x = \"}. -*} +\ lemma (in group) one_in_subset: "[| H \ carrier G; H \ {}; \a \ H. inv a \ H; \a\H. \b\H. a \ b \ H |] ==> \ \ H" by force -text {* A characterization of subgroups: closed, non-empty subset. *} +text \A characterization of subgroups: closed, non-empty subset.\ lemma (in group) subgroupI: assumes subset: "H \ carrier G" and non_empty: "H \ {}" @@ -513,7 +513,7 @@ *) -subsection {* Direct Products *} +subsection \Direct Products\ definition DirProd :: "_ \ _ \ ('a \ 'b) monoid" (infixr "\\" 80) where @@ -533,7 +533,7 @@ qed -text{*Does not use the previous result because it's easier just to use auto.*} +text\Does not use the previous result because it's easier just to use auto.\ lemma DirProd_group: assumes "group G" and "group H" shows "group (G \\ H)" @@ -571,7 +571,7 @@ qed -subsection {* Homomorphisms and Isomorphisms *} +subsection \Homomorphisms and Isomorphisms\ 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\Basis for homomorphism proofs: we assume two groups @{term G} and + @{term H}, with a homomorphism @{term h} between them\ locale group_hom = G: group G + H: group H for G (structure) and H (structure) + fixes h assumes homh: "h \ hom G H" @@ -665,13 +665,13 @@ unfolding hom_def by (simp add: int_pow_mult) -subsection {* Commutative Structures *} +subsection \Commutative Structures\ -text {* +text \ Naming convention: multiplicative structures that are commutative are called \emph{commutative}, additive structures are called \emph{Abelian}. -*} +\ locale comm_monoid = monoid + assumes m_comm: "\x \ carrier G; y \ carrier G\ \ x \ y = y \ x" @@ -753,9 +753,9 @@ by (simp add: m_ac inv_mult_group) -subsection {* The Lattice of Subgroups of a Group *} +subsection \The Lattice of Subgroups of a Group\ -text_raw {* \label{sec:subgroup-lattice} *} +text_raw \\label{sec:subgroup-lattice}\ theorem (in group) subgroups_partial_order: "partial_order \carrier = {H. subgroup H G}, eq = op =, le = op \\" diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Ideal.thy --- 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 \Ideals\ -subsection {* Definitions *} +subsection \Definitions\ -subsubsection {* General definition *} +subsubsection \General definition\ locale ideal = additive_subgroup I R + ring R for I and R (structure) + assumes I_l_closed: "\a \ I; x \ carrier R\ \ x \ a \ I" @@ -44,12 +44,12 @@ qed -subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *} +subsubsection (in ring) \Ideals Generated by a Subset of @{term "carrier R"}\ definition genideal :: "_ \ 'a set \ 'a set" ("Idl\ _" [80] 79) where "genideal R S = Inter {I. ideal I R \ S \ I}" -subsubsection {* Principal Ideals *} +subsubsection \Principal Ideals\ locale principalideal = ideal + assumes generate: "\i \ carrier R. I = Idl {i}" @@ -70,7 +70,7 @@ qed -subsubsection {* Maximal Ideals *} +subsubsection \Maximal Ideals\ locale maximalideal = ideal + assumes I_notcarr: "carrier R \ I" @@ -93,7 +93,7 @@ qed -subsubsection {* Prime Ideals *} +subsubsection \Prime Ideals\ locale primeideal = ideal + cring + assumes I_notcarr: "carrier R \ I" @@ -140,7 +140,7 @@ qed -subsection {* Special Ideals *} +subsection \Special Ideals\ lemma (in ring) zeroideal: "ideal {\} R" apply (intro idealI subgroup.intro) @@ -166,7 +166,7 @@ qed -subsection {* General Ideal Properies *} +subsection \General Ideal Properies\ lemma (in ideal) one_imp_carrier: assumes I_one_closed: "\ \ I" @@ -187,10 +187,10 @@ using iI by (rule a_Hcarr) -subsection {* Intersection of Ideals *} +subsection \Intersection of Ideals\ -text {* \paragraph{Intersection of two ideals} The intersection of any - two ideals is again an ideal in @{term R} *} +text \\paragraph{Intersection of two ideals} The intersection of any + two ideals is again an ideal in @{term R}\ 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 \The intersection of any Number of Ideals is again + an Ideal in @{term R}\ lemma (in ring) i_Intersect: assumes Sideals: "\I. I \ S \ ideal I R" and notempty: "S \ {}" @@ -291,7 +291,7 @@ qed -subsection {* Addition of Ideals *} +subsection \Addition of Ideals\ 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) \Ideals generated by a subset of @{term "carrier R"}\ -text {* @{term genideal} generates an ideal *} +text \@{term genideal} generates an ideal\ lemma (in ring) genideal_ideal: assumes Scarr: "S \ carrier R" shows "ideal (Idl S) R" @@ -360,14 +360,14 @@ then show "i \ Idl {i}" by fast qed -text {* @{term genideal} generates the minimal ideal *} +text \@{term genideal} generates the minimal ideal\ lemma (in ring) genideal_minimal: assumes a: "ideal I R" and b: "S \ I" shows "Idl S \ I" unfolding genideal_def by rule (elim InterD, simp add: a b) -text {* Generated ideals and subsets *} +text \Generated ideals and subsets\ lemma (in ring) Idl_subset_ideal: assumes Iideal: "ideal I R" and Hcarr: "H \ carrier R" @@ -425,12 +425,12 @@ qed -text {* Generation of Principal Ideals in Commutative Rings *} +text \Generation of Principal Ideals in Commutative Rings\ definition cgenideal :: "_ \ 'a \ 'a set" ("PIdl\ _" [80] 79) where "cgenideal R a = {x \\<^bsub>R\<^esub> a | x. x \ carrier R}" -text {* genhideal (?) really generates an ideal *} +text \genhideal (?) really generates an ideal\ lemma (in cring) cgenideal_ideal: assumes acarr: "a \ carrier R" shows "ideal (PIdl a) R" @@ -499,7 +499,7 @@ by fast qed -text {* @{const "cgenideal"} is minimal *} +text \@{const "cgenideal"} is minimal\ lemma (in ring) cgenideal_minimal: assumes "ideal J R" @@ -544,7 +544,7 @@ qed -subsection {* Union of Ideals *} +subsection \Union of Ideals\ lemma (in ring) union_genideal: assumes idealI: "ideal I R" @@ -589,16 +589,16 @@ qed -subsection {* Properties of Principal Ideals *} +subsection \Properties of Principal Ideals\ -text {* @{text "\"} generates the zero ideal *} +text \@{text "\"} generates the zero ideal\ lemma (in ring) zero_genideal: "Idl {\} = {\}" apply rule apply (simp add: genideal_minimal zeroideal) apply (fast intro!: genideal_self) done -text {* @{text "\"} generates the unit ideal *} +text \@{text "\"} generates the unit ideal\ lemma (in ring) one_genideal: "Idl {\} = carrier R" proof - have "\ \ Idl {\}" @@ -608,14 +608,14 @@ qed -text {* The zero ideal is a principal ideal *} +text \The zero ideal is a principal ideal\ corollary (in ring) zeropideal: "principalideal {\} R" apply (rule principalidealI) apply (rule zeroideal) apply (blast intro!: zero_genideal[symmetric]) done -text {* The unit ideal is a principal ideal *} +text \The unit ideal is a principal ideal\ 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 \Every principal ideal is a right coset of the carrier\ lemma (in principalideal) rcos_generate: assumes "cring R" shows "\x\I. I = carrier R #> x" @@ -650,7 +650,7 @@ qed -subsection {* Prime Ideals *} +subsection \Prime Ideals\ 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 "{\}"} is a prime ideal of a commutative ring, the ring is a domain *} +text \If @{text "{\}"} is a prime ideal of a commutative ring, the ring is a domain\ lemma (in cring) zeroprimeideal_domainI: assumes pi: "primeideal {\} R" shows "domain R" @@ -713,7 +713,7 @@ done -subsection {* Maximal Ideals *} +subsection \Maximal Ideals\ lemma (in ideal) helper_I_closed: assumes carr: "a \ carrier R" "x \ carrier R" "y \ carrier R" @@ -767,7 +767,7 @@ qed qed -text {* In a cring every maximal ideal is prime *} +text \In a cring every maximal ideal is prime\ lemma (in cring) maximalideal_is_prime: assumes "maximalideal I R" shows "primeideal I R" @@ -825,7 +825,7 @@ qed -subsection {* Derived Theorems *} +subsection \Derived Theorems\ --"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 \Like zeroprimeideal for domains\ lemma (in field) zeromaximalideal: "maximalideal {\} R" apply (rule maximalidealI) apply (rule zeroideal) diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/IntRing.thy --- 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 \The Ring of Integers\ -subsection {* Some properties of @{typ int} *} +subsection \Some properties of @{typ int}\ lemma dvds_eq_abseq: fixes k :: int @@ -20,7 +20,7 @@ done -subsection {* @{text "\"}: The Set of Integers as Algebraic Structure *} +subsection \@{text "\"}: The Set of Integers as Algebraic Structure\ abbreviation int_ring :: "int ring" ("\") where "int_ring \ \carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\" @@ -47,11 +47,11 @@ *) -subsection {* Interpretations *} +subsection \Interpretations\ -text {* Since definitions of derived operations are global, their +text \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.\ interpretation int: monoid \ where "carrier \ = 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 \Removal of occurrences of @{term UNIV} in interpretation result + --- experimental.\ lemma UNIV: "x \ UNIV \ True" @@ -218,7 +218,7 @@ by standard clarsimp -subsection {* Generated Ideals of @{text "\"} *} +subsection \Generated Ideals of @{text "\"}\ lemma int_Idl: "Idl\<^bsub>\\<^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 \Ideals and Divisibility\ lemma int_Idl_subset_ideal: "Idl\<^bsub>\\<^esub> {k} \ Idl\<^bsub>\\<^esub> {l} = (k \ Idl\<^bsub>\\<^esub> {l})" by (rule int.Idl_subset_ideal') simp_all @@ -287,7 +287,7 @@ done -subsection {* Ideals and the Modulus *} +subsection \Ideals and the Modulus\ definition ZMod :: "int \ int \ int set" where "ZMod k r = (Idl\<^bsub>\\<^esub> {k}) +>\<^bsub>\\<^esub> r" @@ -370,7 +370,7 @@ done -subsection {* Factorization *} +subsection \Factorization\ definition ZFact :: "int \ int set ring" where "ZFact k = \ Quot (Idl\<^bsub>\\<^esub> {k})" diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Lattice.thy --- 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 \Orders and Lattices\ -subsection {* Partial Orders *} +subsection \Partial Orders\ record 'a gorder = "'a eq_object" + le :: "['a, 'a] => bool" (infixl "\\" 50) @@ -32,7 +32,7 @@ where "x \\<^bsub>L\<^esub> y \ x \\<^bsub>L\<^esub> y & x .\\<^bsub>L\<^esub> y" -subsubsection {* The order relation *} +subsubsection \The order relation\ 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 \Upper and lower bounds of a set\ definition Upper :: "[_, 'a set] => 'a set" @@ -276,7 +276,7 @@ qed -subsubsection {* Least and greatest, as predicate *} +subsubsection \Least and greatest, as predicate\ definition least :: "[_, 'a, 'a set] => bool" @@ -286,8 +286,8 @@ greatest :: "[_, 'a, 'a set] => bool" where "greatest L g A \ A \ carrier L & g \ A & (ALL x : A. x \\<^bsub>L\<^esub> g)" -text (in weak_partial_order) {* Could weaken these to @{term "l \ carrier L \ l - .\ A"} and @{term "g \ carrier L \ g .\ A"}. *} +text (in weak_partial_order) \Could weaken these to @{term "l \ carrier L \ l + .\ A"} and @{term "g \ carrier L \ g .\ A"}.\ lemma least_closed [intro, simp]: "least L l A ==> l \ carrier L" @@ -310,8 +310,8 @@ "[| x .= x'; x \ carrier L; x' \ 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) \@{const least} is not congruent in the second parameter for + @{term "A {.=} A'"}\ 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) \@{const greatest} is not congruent in the second parameter for + @{term "A {.=} A'"}\ lemma (in weak_partial_order) greatest_Lower_cong_l: assumes "x .= x'" @@ -402,7 +402,7 @@ shows "[| greatest L i (Lower L A); x \ A; A \ carrier L |] ==> i \ x" by (unfold greatest_def) blast -text {* Supremum and infimum *} +text \Supremum and infimum\ definition sup :: "[_, 'a set] => 'a" ("\\_" [90] 90) @@ -421,7 +421,7 @@ where "x \\<^bsub>L\<^esub> y = \\<^bsub>L\<^esub>{x, y}" -subsection {* Lattices *} +subsection \Lattices\ 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 \Supremum\ lemma (in weak_upper_semilattice) joinI: "[| !!l. least L l (Upper L {x, y}) ==> P l; x \ carrier L; y \ 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 \Condition on @{text A}: supremum exists.\ 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 \ carrier L" "y \ carrier L" "z \ carrier L" shows "x \ (y \ z) .= \{x, y, z}" proof (rule finite_sup_insertI) - -- {* The textbook argument in Jacobson I, p 457 *} + -- \The textbook argument in Jacobson I, p 457\ fix s assume sup: "least L s (Upper L {x, y, z})" show "x \ (y \ 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 \Commutativity holds for @{text "="}.\ lemma join_comm: fixes L (structure) @@ -673,7 +673,7 @@ qed -subsubsection {* Infimum *} +subsubsection \Infimum\ 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 \Condition on @{text A}: infimum exists.\ 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 \ carrier L" "y \ carrier L" "z \ carrier L" shows "x \ (y \ z) .= \{x, y, z}" proof (rule finite_inf_insertI) - txt {* The textbook argument in Jacobson I, p 457 *} + txt \The textbook argument in Jacobson I, p 457\ fix i assume inf: "greatest L i (Lower L {x, y, z})" show "x \ (y \ z) .= i" @@ -911,19 +911,19 @@ qed -subsection {* Total Orders *} +subsection \Total Orders\ locale weak_total_order = weak_partial_order + assumes total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" -text {* Introduction rule: the usual definition of total order *} +text \Introduction rule: the usual definition of total order\ lemma (in weak_partial_order) weak_total_orderI: assumes total: "!!x y. [| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" shows "weak_total_order L" by standard (rule total) -text {* Total orders are lattices. *} +text \Total orders are lattices.\ sublocale weak_total_order < weak: weak_lattice proof @@ -969,7 +969,7 @@ qed -subsection {* Complete Lattices *} +subsection \Complete Lattices\ locale weak_complete_lattice = weak_lattice + assumes sup_exists: @@ -977,7 +977,7 @@ and inf_exists: "[| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" -text {* Introduction rule: the usual definition of complete lattice *} +text \Introduction rule: the usual definition of complete lattice\ lemma (in weak_partial_order) weak_complete_latticeI: assumes sup_exists: @@ -1034,7 +1034,7 @@ "\ \ carrier L" by (unfold bottom_def) simp -text {* Jacobson: Theorem 8.1 *} +text \Jacobson: Theorem 8.1\ 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 \Orders and Lattices where @{text eq} is the Equality\ locale partial_order = weak_partial_order + assumes eq_is_equal: "op .= = op =" @@ -1115,7 +1115,7 @@ end -text {* Least and greatest, as predicate *} +text \Least and greatest, as predicate\ 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 \Lattices\ locale upper_semilattice = partial_order + assumes sup_of_two_exists: @@ -1145,7 +1145,7 @@ locale lattice = upper_semilattice + lower_semilattice -text {* Supremum *} +text \Supremum\ 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 \Infimum\ declare (in partial_order) weak_inf_of_singleton [simp del] @@ -1172,7 +1172,7 @@ "x \ carrier L ==> \{x} = x" using weak_inf_of_singleton unfolding eq_is_equal . -text {* Condition on @{text A}: infimum exists. *} +text \Condition on @{text A}: infimum exists.\ lemma (in lower_semilattice) meet_assoc_lemma: assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L" @@ -1185,7 +1185,7 @@ using weak_meet_assoc L unfolding eq_is_equal . -text {* Total Orders *} +text \Total Orders\ locale total_order = partial_order + assumes total_order_total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ 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 \Introduction rule: the usual definition of total order\ lemma (in partial_order) total_orderI: assumes total: "!!x y. [| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" shows "total_order L" by standard (rule total) -text {* Total orders are lattices. *} +text \Total orders are lattices.\ sublocale total_order < weak: lattice by standard (auto intro: sup_of_two_exists inf_of_two_exists) -text {* Complete lattices *} +text \Complete lattices\ 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 \Introduction rule: the usual definition of complete lattice\ lemma (in partial_order) complete_latticeI: assumes sup_exists: @@ -1273,9 +1273,9 @@ (* TODO: prove dual version *) -subsection {* Examples *} +subsection \Examples\ -subsubsection {* The Powerset of a Set is a Complete Lattice *} +subsubsection \The Powerset of a Set is a Complete Lattice\ theorem powerset_is_complete_lattice: "complete_lattice \carrier = Pow A, eq = op =, le = op \\" @@ -1293,13 +1293,13 @@ fix B assume "B \ carrier ?L" then have "greatest ?L (\B \ A) (Lower ?L B)" - txt {* @{term "\B"} is not the infimum of @{term B}: - @{term "\{} = UNIV"} which is in general bigger than @{term "A"}! *} + txt \@{term "\B"} is not the infimum of @{term B}: + @{term "\{} = UNIV"} which is in general bigger than @{term "A"}!\ 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 \An other example, that of the lattice of subgroups of a group, + can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\ end diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Module.thy --- 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 \Modules over an Abelian Group\ -subsection {* Definitions *} +subsection \Definitions\ record ('a, 'b) module = "'b ring" + smult :: "['a, 'b] => 'b" (infixl "\\" 70) @@ -103,7 +103,7 @@ smult_l_distr smult_r_distr smult_assoc1) -subsection {* Basic Properties of Algebras *} +subsection \Basic Properties of Algebras\ lemma (in algebra) smult_l_null [simp]: "x \ carrier M ==> \ \\<^bsub>M\<^esub> x = \\<^bsub>M\<^esub>" diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/QuotRing.thy --- 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 \Quotient Rings\ -subsection {* Multiplication on Cosets *} +subsection \Multiplication on Cosets\ definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \ 'a set" ("[mod _:] _ \\ _" [81,81,81] 80) where "rcoset_mult R I A B = (\a\A. \b\B. I +>\<^bsub>R\<^esub> (a \\<^bsub>R\<^esub> b))" -text {* @{const "rcoset_mult"} fulfils the properties required by - congruences *} +text \@{const "rcoset_mult"} fulfils the properties required by + congruences\ lemma (in ideal) rcoset_mult_add: "x \ carrier R \ y \ carrier R \ [mod I:] (I +> x) \ (I +> y) = I +> (x \ y)" apply rule @@ -70,7 +70,7 @@ qed -subsection {* Quotient Ring Definition *} +subsection \Quotient Ring Definition\ definition FactRing :: "[('a,'b) ring_scheme, 'a set] \ ('a set) ring" (infixl "Quot" 65) @@ -79,33 +79,33 @@ one = (I +>\<^bsub>R\<^esub> \\<^bsub>R\<^esub>), zero = I, add = set_add R\" -subsection {* Factorization over General Ideals *} +subsection \Factorization over General Ideals\ -text {* The quotient is a ring *} +text \The quotient is a ring\ lemma (in ideal) quotient_is_ring: "ring (R Quot I)" apply (rule ringI) - --{* abelian group *} + --\abelian group\ apply (rule comm_group_abelian_groupI) apply (simp add: FactRing_def) apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def']) - --{* mult monoid *} + --\mult monoid\ apply (rule monoidI) apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def a_r_coset_def[symmetric]) - --{* mult closed *} + --\mult closed\ apply (clarify) apply (simp add: rcoset_mult_add, fast) - --{* mult @{text one_closed} *} + --\mult @{text one_closed}\ apply force - --{* mult assoc *} + --\mult assoc\ apply clarify apply (simp add: rcoset_mult_add m_assoc) - --{* mult one *} + --\mult one\ apply clarify apply (simp add: rcoset_mult_add) apply clarify apply (simp add: rcoset_mult_add) - --{* distr *} + --\distr\ 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 \This is a ring homomorphism\ lemma (in ideal) rcos_ring_hom: "(op +> I) \ 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 \The quotient of a cring is also commutative\ 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 \Cosets as a ring homomorphism on crings\ 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 \Factorization over Prime Ideals\ -text {* The quotient ring generated by a prime ideal is a domain *} +text \The quotient ring generated by a prime ideal is a domain\ 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 \Generating right cosets of a prime ideal is a homomorphism + on commutative rings\ 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 \Factorization over Maximal Ideals\ -text {* In a commutative ring, the quotient ring over a maximal ideal +text \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''\ 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 *} + --\Quotient is not empty\ assume "\\<^bsub>R Quot I\<^esub> = \\<^bsub>R Quot I\<^esub>" then have II1: "I = I +> \" by (simp add: FactRing_def) from a_rcos_self[OF one_closed] have "\ \ 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 *} + --\Existence of Inverse\ fix a assume IanI: "I +> a \ I" and acarr: "a \ carrier R" - --{* Helper ideal @{text "J"} *} + --\Helper ideal @{text "J"}\ def J \ "(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"} *} + --\Showing @{term "J"} not smaller than @{term "I"}\ have IinJ: "I \ J" proof (rule, simp add: J_def r_coset_def set_add_defs) fix x @@ -256,7 +256,7 @@ with Zcarr and xI show "\xa\carrier R. \k\I. x = xa \ a \ k" by fast qed - --{* Showing @{term "J \ I"} *} + --\Showing @{term "J \ I"}\ have anI: "a \ I" proof (rule ccontr, simp) assume "a \ I" @@ -274,7 +274,7 @@ from aJ and anI have JnI: "J \ I" by fast - --{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *} + --\Deducing @{term "J = carrier R"} because @{term "I"} is maximal\ from idealJ and IinJ have "J = I \ J = carrier R" proof (rule I_maximal, unfold J_def) have "carrier R #> a \ carrier R" @@ -285,7 +285,7 @@ with JnI have Jcarr: "J = carrier R" by simp - --{* Calculating an inverse for @{term "a"} *} + --\Calculating an inverse for @{term "a"}\ from one_closed[folded Jcarr] have "\r\carrier R. \i\I. \ = r \ a \ 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 \ r = \i \ \" by algebra - --{* Lifting to cosets *} + --\Lifting to cosets\ from iI have "\i \ \ \ I +> \" by (intro a_rcosI, simp, intro a_subset, simp) with rai1 have "a \ r \ I +> \" by simp diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Ring.thy --- 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 \The Algebraic Hierarchy of Rings\ -subsection {* Abelian Groups *} +subsection \Abelian Groups\ record 'a ring = "'a monoid" + zero :: 'a ("\\") add :: "['a, 'a] => 'a" (infixl "\\" 65) -text {* Derived operations. *} +text \Derived operations.\ definition a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\\ _" [81] 80) @@ -39,7 +39,7 @@ ("(3\__\_. _)" [1000, 0, 51, 10] 10) translations "\\i\A. b" \ "CONST finsum \\ (%i. b) A" - -- {* Beware of argument permutation! *} + -- \Beware of argument permutation!\ locale abelian_group = abelian_monoid + @@ -47,7 +47,7 @@ "comm_group \carrier = carrier G, mult = add G, one = zero G\" -subsection {* Basic Properties *} +subsection \Basic Properties\ 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 \Transfer facts from multiplicative structures via interpretation.\ sublocale abelian_monoid < add!: monoid "\carrier = carrier G, mult = add G, one = zero G\" @@ -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 \Usually, if this rule causes a failed congruence proof error, the reason is that the premise @{text "g \ 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.\ 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 \Derive an @{text "abelian_group"} from a @{text "comm_group"}\ lemma comm_group_abelian_groupI: fixes G (structure) @@ -219,7 +219,7 @@ qed -subsection {* Rings: Basic Definitions *} +subsection \Rings: Basic Definitions\ locale semiring = abelian_monoid R + monoid R for R (structure) + assumes l_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] @@ -246,7 +246,7 @@ assumes field_Units: "Units R = carrier R - {\}" -subsection {* Rings *} +subsection \Rings\ 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. *} + -- \Right-distributivity follows from left-distributivity and + commutativity.\ proof (rule ring_axioms.intro) fix x y z assume R: "x \ carrier R" "y \ carrier R" "z \ carrier R" @@ -312,7 +312,7 @@ "cring R" by (rule cring_axioms) -subsubsection {* Normaliser for Rings *} +subsubsection \Normaliser for Rings\ lemma (in abelian_group) r_neg2: "[| x \ carrier G; y \ carrier G |] ==> x \ (\ x \ y) = y" @@ -335,9 +335,9 @@ context ring begin -text {* +text \ The following proofs are from Jacobson, Basic Algebra I, pp.~88--89. -*} +\ sublocale semiring proof - @@ -387,20 +387,20 @@ "[| x \ carrier G; y \ carrier G |] ==> x \ y = x \ \ y" by (simp only: a_minus_def) -text {* Setup algebra method: - compute distributive normal form in locale contexts *} +text \Setup algebra method: + compute distributive normal form in locale contexts\ ML_file "ringsimp.ML" -attribute_setup algebra = {* +attribute_setup algebra = \ 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" +\ "theorems controlling algebra method" -method_setup algebra = {* +method_setup algebra = \ Scan.succeed (SIMPLE_METHOD' o Ringsimp.algebra_tac) -*} "normalisation of algebraic structure" +\ "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 \Two examples for use of method algebra\ lemma fixes R (structure) and S (structure) @@ -487,7 +487,7 @@ qed -subsubsection {* Sums over Finite Sets *} +subsubsection \Sums over Finite Sets\ lemma (in semiring) finsum_ldistr: "[| finite A; a \ carrier R; f \ A -> carrier R |] ==> @@ -508,7 +508,7 @@ qed -subsection {* Integral Domains *} +subsection \Integral Domains\ context "domain" begin @@ -554,10 +554,10 @@ end -subsection {* Fields *} +subsection \Fields\ -text {* Field would not need to be derived from domain, the properties - for domain follow from the assumptions of field *} +text \Field would not need to be derived from domain, the properties + for domain follow from the assumptions of field\ lemma (in cring) cring_fieldI: assumes field_Units: "Units R = carrier R - {\}" shows "field R" @@ -585,7 +585,7 @@ qed qed (rule field_Units) -text {* Another variant to show that something is a field *} +text \Another variant to show that something is a field\ lemma (in cring) cring_fieldI2: assumes notzero: "\ \ \" and invex: "\a. \a \ carrier R; a \ \\ \ \b\carrier R. a \ b = \" @@ -604,7 +604,7 @@ qed -subsection {* Morphisms *} +subsection \Morphisms\ definition ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set" diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/RingHom.thy --- 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 \Homomorphisms of Non-Commutative Rings\ -text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *} +text \Lifting existing lemmas in a @{text ring_hom_ring} locale\ 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 \The Kernel of a Ring Homomorphism\ --"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 \Elements of the kernel are mapped to zero\ lemma (in abelian_group_hom) kernel_zero [simp]: "i \ a_kernel R S h \ h i = \\<^bsub>S\<^esub>" by (simp add: a_kernel_defs) -subsection {* Cosets *} +subsection \Cosets\ -text {* Cosets of the kernel correspond to the elements of the image of the homomorphism *} +text \Cosets of the kernel correspond to the elements of the image of the homomorphism\ lemma (in ring_hom_ring) rcos_imp_homeq: assumes acarr: "a \ carrier R" and xrcos: "x \ a_kernel R S h +> a" diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/Sylow.thy --- 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 \ See also @{cite "Kammueller-Paulson:1999"}. -*} +\ -text{*The combinatorial argument is in theory Exponent*} +text\The combinatorial argument is in theory Exponent\ 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\Main Part of the Proof\ locale sylow_central = sylow + fixes H and M1 and M @@ -107,7 +107,7 @@ qed -subsection{*Discharging the Assumptions of @{text sylow_central}*} +subsection\Discharging the Assumptions of @{text sylow_central}\ lemma (in sylow) EmptyNotInEquivSet: "{} \ 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\Introduction and Destruct Rules for @{term H}\ lemma (in sylow_central) H_I: "[|g \ carrier G; M1 #> g = M1|] ==> g \ H" by (simp add: H_def) @@ -216,10 +216,10 @@ done -subsection{*Equal Cardinalities of @{term M} and the Set of Cosets*} +subsection\Equal Cardinalities of @{term M} and the Set of Cosets\ -text{*Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that - their cardinalities are equal.*} +text\Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that + their cardinalities are equal.\ lemma ElemClassEquiv: "[| equiv A r; C \ A // r |] ==> \x \ C. \y \ C. (x,y)\r" @@ -259,7 +259,7 @@ done -subsubsection{*The Opposite Injection*} +subsubsection\The Opposite Injection\ lemma (in sylow_central) H_elem_map: "H1 \ rcosets H ==> \g. g \ 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\close to a duplicate of @{text inj_M_GmodH}\ lemma (in sylow_central) inj_GmodH_M: "\g \ rcosets H\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\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"}.\ 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 \Sylow's Theorem\ theorem sylow_thm: "[| prime p; group(G); order(G) = (p^a) * m; finite (carrier G)|] diff -r ddca85598c65 -r efac889fccbc src/HOL/Algebra/UnivPoly.thy --- 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 \Univariate Polynomials\ -text {* +text \ Polynomials are formalised as modules with additional operations for extracting coefficients from polynomials and for obtaining monomials from coefficients and exponents (record @{text "up_ring"}). The @@ -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. -*} +\ -subsection {* The Constructor for Univariate Polynomials *} +subsection \The Constructor for Univariate Polynomials\ -text {* +text \ Functions with finite support. -*} +\ locale bound = fixes z :: 'a @@ -67,9 +67,9 @@ monom = (%a:carrier R. %n i. if i=n then a else \\<^bsub>R\<^esub>), coeff = (%p:up R. %n. p n)\" -text {* +text \ Properties of the set of polynomials @{term up}. -*} +\ lemma mem_upI [intro]: "[| !!n. f n \ carrier R; EX n. bound (zero R) n f |] ==> f \ up R" @@ -168,7 +168,7 @@ end -subsection {* Effect of Operations on Coefficients *} +subsection \Effect of Operations on Coefficients\ 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 \Temporarily declare @{thm P_def} as simp rule.\ declare P_def [simp] @@ -240,12 +240,12 @@ end -subsection {* Polynomials Form a Ring. *} +subsection \Polynomials Form a Ring.\ context UP_ring begin -text {* Operations are closed over @{term P}. *} +text \Operations are closed over @{term P}.\ lemma UP_mult_closed [simp]: "[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ 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 \Algebraic ring properties\ context UP_ring begin @@ -398,7 +398,7 @@ end -subsection {* Polynomials Form a Commutative Ring. *} +subsection \Polynomials Form a Commutative Ring.\ 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 \Polynomials over a commutative ring for a commutative ring\ 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 \Polynomials Form an Algebra\ context UP_ring begin @@ -496,9 +496,9 @@ end -text {* +text \ Interpretation of lemmas from @{term algebra}. -*} +\ 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 \Further Lemmas Involving Monomials\ 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\The following corollary follows from lemmas @{thm "monom_one_Suc"} + and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}\ corollary monom_one_comm: shows "monom P \ k \\<^bsub>P\<^esub> monom P \ 1 = monom P \ 1 \\<^bsub>P\<^esub> monom P \ k" unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] .. @@ -709,7 +709,7 @@ end -subsection {* The Degree Function *} +subsection \The Degree Function\ definition deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat" @@ -743,19 +743,19 @@ assumes "deg R p < m" and "p \ carrier P" shows "coeff P p m = \" proof - - from `p \ carrier P` obtain n where "bound \ n (coeff P p)" + from \p \ carrier P\ obtain n where "bound \ n (coeff P p)" by (auto simp add: UP_def P_def) then have "bound \ (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 \deg R p < m\ show ?thesis .. qed lemma deg_belowI: assumes non_zero: "n ~= 0 ==> coeff P p n ~= \" and R: "p \ carrier P" shows "n <= deg R p" --- {* Logically, this is a slightly stronger version of - @{thm [source] deg_aboveD} *} +-- \Logically, this is a slightly stronger version of + @{thm [source] deg_aboveD}\ proof (cases "n=0") case True then show ?thesis by simp next @@ -814,7 +814,7 @@ !!n. n ~= 0 ==> coeff P p n ~= \; p \ carrier P |] ==> deg R p = n" by (fast intro: le_antisym deg_aboveI deg_belowI) -text {* Degree and polynomial operations *} +text \Degree and polynomial operations\ lemma deg_add [simp]: "p \ carrier P \ q \ carrier P \ @@ -863,8 +863,8 @@ inj_on_iff [OF R.a_inv_inj, of _ "\", simplified] R) qed -text{*The following lemma is later \emph{overwritten} by the most - specific one for domains, @{text deg_smult}.*} +text\The following lemma is later \emph{overwritten} by the most + specific one for domains, @{text deg_smult}.\ lemma deg_smult_ring [simp]: "[| a \ carrier R; p \ carrier P |] ==> @@ -949,7 +949,7 @@ end -text{*The following lemmas also can be lifted to @{term UP_ring}.*} +text\The following lemmas also can be lifted to @{term UP_ring}.\ context UP_ring begin @@ -1013,7 +1013,7 @@ end -subsection {* Polynomials over Integral Domains *} +subsection \Polynomials over Integral Domains\ lemma domainI: assumes cring: "cring R" @@ -1071,15 +1071,15 @@ end -text {* +text \ Interpretation of theorems from @{term domain}. -*} +\ sublocale UP_domain < "domain" P by intro_locales (rule domain.axioms UP_domain)+ -subsection {* The Evaluation Homomorphism and Universal Property*} +subsection \The Evaluation Homomorphism and Universal Property\ (* 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 \The universal property of the polynomial ring\ locale UP_pre_univ_prop = ring_hom_cring + UP_cring @@ -1203,9 +1203,9 @@ assumes indet_img_carrier [simp, intro]: "s \ 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\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.\ lemma (in ring_hom_ring) hom_finsum [simp]: "f \ A -> carrier R ==> @@ -1296,18 +1296,18 @@ qed qed -text {* +text \ 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.\ lemma (in UP_pre_univ_prop) eval_const: "[| s \ carrier S; r \ 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 \Further properties of the evaluation homomorphism.\ -text {* The following proof is complicated by the fact that in arbitrary - rings one might have @{term "one R = zero R"}. *} +text \The following proof is complicated by the fact that in arbitrary + rings one might have @{term "one R = zero R"}.\ (* TODO: simplify by cases "one R = zero R" *) @@ -1336,7 +1336,7 @@ end -text {* Interpretation of ring homomorphism lemmas. *} +text \Interpretation of ring homomorphism lemmas.\ 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\JE: The following lemma was added by me; it might be even lifted to a simpler locale\ 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\The long division algorithm: some previous facts.\ lemma coeff_minus [simp]: assumes p: "p \ carrier P" and q: "q \ carrier P" shows "coeff P (p \\<^bsub>P\<^esub> q) n = coeff P p n \ coeff P q n" @@ -1538,7 +1538,7 @@ end -subsection {* The long division proof for commutative rings *} +subsection \The long division proof for commutative rings\ context UP_cring begin @@ -1547,7 +1547,7 @@ shows "\ x y z. Pred x y z" using exist by blast -text {* Jacobson's Theorem 2.14 *} +text \Jacobson's Theorem 2.14\ lemma long_div_theorem: assumes g_in_P [simp]: "g \ carrier P" and f_in_P [simp]: "f \ carrier P" @@ -1648,7 +1648,7 @@ end -text {*The remainder theorem as corollary of the long division theorem.*} +text \The remainder theorem as corollary of the long division theorem.\ context UP_cring begin @@ -1797,7 +1797,7 @@ end -subsection {* Sample Application of Evaluation Homomorphism *} +subsection \Sample Application of Evaluation Homomorphism\ 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 \ Interpretation now enables to import all theorems and lemmas valid in the context of homomorphisms between @{term INTEG} and @{term "UP INTEG"} globally. -*} +\ interpretation INTEG: UP_pre_univ_prop INTEG INTEG id "UP INTEG" using INTEG_id_eval by simp_all diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/BijectionRel.thy --- 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 \Bijections between sets\ theory BijectionRel imports Main begin -text {* +text \ Inductive definitions of bijections between two different sets and between the same set. Theorem for relating the two definitions. \bigskip -*} +\ inductive_set bijR :: "('a => 'b => bool) => ('a set * 'b set) set" @@ -24,10 +24,10 @@ | insert: "P a b ==> a \ A ==> b \ B ==> (A, B) \ bijR P ==> (insert a A, insert b B) \ bijR P" -text {* +text \ Add extra condition to @{term insert}: @{term "\b \ B. \ P a b"} (and similar for @{term A}). -*} +\ definition bijP :: "('a => 'a => bool) => 'a set => bool" where @@ -51,7 +51,7 @@ ==> insert a (insert b A) \ bijER P" -text {* \medskip @{term bijR} *} +text \\medskip @{term bijR}\ lemma fin_bijRl: "(A, B) \ bijR P ==> finite A" apply (erule bijR.induct) @@ -100,7 +100,7 @@ done -text {* \medskip @{term bijER} *} +text \\medskip @{term bijER}\ lemma fin_bijER: "A \ bijER P ==> finite A" apply (erule bijER.induct) diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Chinese.thy --- 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 \The Chinese Remainder Theorem\ theory Chinese imports IntPrimes begin -text {* +text \ 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?} -*} +\ -subsection {* Definitions *} +subsection \Definitions\ primrec funprod :: "(nat => int) => nat => nat => int" where @@ -65,7 +65,7 @@ "x_sol n kf bf mf = funsum (\i. xilin_sol i n kf bf mf * mhf mf n i) 0 n" -text {* \medskip @{term funprod} and @{term funsum} *} +text \\medskip @{term funprod} and @{term funsum}\ lemma funprod_pos: "(\i. i \ n --> 0 < mf i) ==> 0 < funprod mf 0 n" by (induct n) auto @@ -126,7 +126,7 @@ done -subsection {* Chinese: uniqueness *} +subsection \Chinese: uniqueness\ lemma zcong_funprod_aux: "m_cond n mf ==> km_cond n kf mf @@ -160,17 +160,17 @@ done -subsection {* Chinese: existence *} +subsection \Chinese: existence\ lemma unique_xi_sol: "0 < n ==> i \ n ==> m_cond n mf ==> km_cond n kf mf ==> \!x. 0 \ x \ x < mf i \ [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 \stac @{context} @{thm zgcd_zmult_cancel} 2\) 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 \stac @{context} @{thm zgcd_zmult_cancel} 3\) apply (rule_tac [!] funprod_zgcd) apply safe apply simp_all @@ -216,7 +216,7 @@ done -subsection {* Chinese *} +subsection \Chinese\ 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 \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 (subgoal_tac [6] "0 \ xilin_sol i n kf bf mf \ xilin_sol i n kf bf mf < mf i \ [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 \asm_simp_tac @{context} 6\) apply (rule_tac [6] ex1_implies_ex [THEN someI_ex]) apply (rule_tac [6] unique_xi_sol) apply (rule_tac [3] funprod_zdvd) diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Euler.thy --- 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 \Euler's criterion\ theory Euler imports Residues EvenOdd @@ -15,7 +15,7 @@ where "SetS a p = MultInvPair a p ` SRStar p" -subsection {* Property for MultInvPair *} +subsection \Property for MultInvPair\ lemma MultInvPair_prop1a: "[| zprime p; 2 < p; ~([a = 0](mod p)); @@ -89,7 +89,7 @@ done -subsection {* Properties of SetS *} +subsection \Properties of SetS\ 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 \\medskip Prove the first part of Euler's Criterion:\ 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 \\medskip Prove another part of Euler Criterion:\ 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 \2 < p\ 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 \\medskip Prove the final part of Euler's Criterion:\ 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 \\medskip Finally show Euler's Criterion:\ theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)" diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/EulerFermat.thy --- 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 \Fermat's Little Theorem extended to Euler's Totient function\ theory EulerFermat imports BijectionRel IntFact begin -text {* +text \ Fermat's Little Theorem extended to Euler's Totient function. More abstract approach than Boyer-Moore (which seems necessary to achieve the extended version). -*} +\ -subsection {* Definitions and lemmas *} +subsection \Definitions and lemmas\ inductive_set RsetR :: "int => int set set" for m :: int where @@ -54,11 +54,11 @@ where "zcongm m = (\a b. zcong a b m)" lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \ z = -1)" - -- {* LCP: not sure why this lemma is needed now *} + -- \LCP: not sure why this lemma is needed now\ by (auto simp add: abs_if) -text {* \medskip @{text norRRset} *} +text \\medskip @{text norRRset}\ declare BnorRset.simps [simp del] @@ -146,7 +146,7 @@ done -text {* \medskip @{term noXRRset} *} +text \\medskip @{term noXRRset}\ lemma RRset_gcd [rule_format]: "is_RRset A m ==> a \ A --> zgcd a m = 1" @@ -249,7 +249,7 @@ \(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) --\multiple redexes\ 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 \Fermat\ lemma bijzcong_zcong_prod: "(A, B) \ bijR (zcongm m) ==> [\A = \B] (mod m)" diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/EvenOdd.thy --- 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 \Parity: Even and Odd Integers\ theory EvenOdd imports Int2 @@ -14,7 +14,7 @@ definition zEven :: "int set" where "zEven = {x. \k. x = 2 * k}" -subsection {* Some useful properties about even and odd *} +subsection \Some useful properties about even and odd\ lemma zOddI [intro?]: "x = 2 * k + 1 \ x \ zOdd" and zOddE [elim?]: "x \ zOdd \ (!!k. x = 2 * k + 1 \ C) \ C" @@ -167,11 +167,11 @@ lemma neg_one_even_power: "[| x \ zEven; 0 \ x |] ==> (-1::int)^(nat x) = 1" proof - assume "x \ zEven" and "0 \ x" - from `x \ zEven` obtain a where "x = 2 * a" .. - with `0 \ x` have "0 \ a" by simp - from `0 \ x` and `x = 2 * a` have "nat x = nat (2 * a)" + from \x \ zEven\ obtain a where "x = 2 * a" .. + with \0 \ x\ have "0 \ a" by simp + from \0 \ x\ and \x = 2 * a\ have "nat x = nat (2 * a)" by simp - also from `x = 2 * a` have "nat (2 * a) = 2 * nat a" + also from \x = 2 * a\ 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 \ zOdd; 0 \ x |] ==> (-1::int)^(nat x) = -1" proof - assume "x \ zOdd" and "0 \ x" - from `x \ zOdd` obtain a where "x = 2 * a + 1" .. - with `0 \ x` have a: "0 \ a" by simp - with `0 \ x` and `x = 2 * a + 1` have "nat x = nat (2 * a + 1)" + from \x \ zOdd\ obtain a where "x = 2 * a + 1" .. + with \0 \ x\ have a: "0 \ a" by simp + with \0 \ x\ and \x = 2 * a + 1\ 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 \ zEven; x < y |] ==> x div 2 < y div 2" proof - assume "y \ zEven" and "x < y" - from `y \ zEven` obtain k where k: "y = 2 * k" .. - with `x < y` have "x < 2 * k" by simp + from \y \ zEven\ obtain k where k: "y = 2 * k" .. + with \x < y\ 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 diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Factorization.thy --- 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 \Fundamental Theorem of Arithmetic (unique factorization into primes)\ theory Factorization imports Primes "~~/src/HOL/Library/Permutation" begin -subsection {* Definitions *} +subsection \Definitions\ definition primel :: "nat list => bool" where "primel xs = (\p \ set xs. prime p)" @@ -36,7 +36,7 @@ | "sort (x # xs) = oinsert x (sort xs)" -subsection {* Arithmetic *} +subsection \Arithmetic\ lemma one_less_m: "(m::nat) \ m * k ==> m \ Suc 0 ==> Suc 0 < m" apply (cases m) @@ -64,7 +64,7 @@ done -subsection {* Prime list and product *} +subsection \Prime list and product\ lemma prod_append: "prod (xs @ ys) = prod xs * prod ys" apply (induct xs) @@ -137,7 +137,7 @@ done -subsection {* Sorting *} +subsection \Sorting\ lemma nondec_oinsert: "nondec xs \ nondec (oinsert x xs)" apply (induct xs) @@ -174,7 +174,7 @@ done -subsection {* Permutation *} +subsection \Permutation\ lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys" apply (unfold primel_def) @@ -212,7 +212,7 @@ done -subsection {* Existence *} +subsection \Existence\ lemma ex_nondec_lemma: "primel xs ==> \ys. primel ys \ nondec ys \ prod ys = prod xs" @@ -250,7 +250,7 @@ done -subsection {* Uniqueness *} +subsection \Uniqueness\ lemma prime_dvd_mult_list [rule_format]: "prime p ==> p dvd (prod xs) --> (\m. m:set xs \ p dvd m)" diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Fib.thy --- 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 \The Fibonacci function\ theory Fib imports Primes begin -text {* +text \ Fibonacci numbers: proofs of laws taken from: R. L. Graham, D. E. Knuth, O. Patashnik. Concrete Mathematics. (Addison-Wesley, 1989) \bigskip -*} +\ fun fib :: "nat \ nat" where @@ -23,21 +23,21 @@ | "fib (Suc 0) = 1" | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)" -text {* +text \ \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. -*} +\ -text{*We disable @{text fib.fib_2fib_2} for simplification ...*} +text\We disable @{text fib.fib_2fib_2} for simplification ...\ declare fib_2 [simp del] -text{*...then prove a version that has a more restrictive pattern.*} +text\...then prove a version that has a more restrictive pattern.\ 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 \\medskip Concrete Mathematics, page 280\ 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 \ \medskip Concrete Mathematics, page 278: Cassini's identity. The proof is much easier using integers, not natural numbers! -*} +\ 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\We now obtain a version for the natural numbers via the coercion + function @{term int}.\ 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 \\medskip Toward Law 6.111 of Concrete Mathematics\ 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)" -- \Law 6.111\ apply (induct m n rule: gcd_induct) apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod) done diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Finite2.thy --- 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 \Finite Sets and Finite Sums\ theory Finite2 imports IntFact "~~/src/HOL/Library/Infinite_Set" begin -text{* +text\ These are useful for combinatorial and number-theoretic counting arguments. -*} +\ -subsection {* Useful properties of sums and products *} +subsection \Useful properties of sums and products\ lemma setsum_same_function_zcong: assumes a: "\x \ 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 \Cardinality of explicit finite sets\ lemma finite_surjI: "[| B \ 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 \card {y. y < n} = n\ by simp qed lemma card_bdd_nat_set_le: "card { y::nat. y \ 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 \ n` have "int ` {y. y < nat n} = {y. 0 \ y & y < n}" + also from \0 \ n\ have "int ` {y. y < nat n} = {y. 0 \ 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 \ x & x < n}) = card {x. 0 \ x & x < n}" by (rule card_image) - also from `0 \ n` have "... = nat n" + also from \0 \ n\ have "... = nat n" by (rule card_bdd_int_set_l) also have "(%x. x + 1) ` {x. 0 \ x & x < n} = {x. 0 < x & x<= n}" apply (auto simp add: image_def) diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Gauss.thy --- 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 \Gauss' Lemma\ theory Gauss imports Euler @@ -26,7 +26,7 @@ definition "F = (%x. (p - x)) ` E" -subsection {* Basic properties of p *} +subsection \Basic properties of p\ lemma p_odd: "p \ 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 \Basic Properties of the Gauss Sets\ 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 \Relationships Between Gauss Sets\ 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 \Gauss' Lemma\ 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) diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Int2.thy --- 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 \Integers: Divisibility and Congruences\ 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 \Useful lemmas about dvd and powers\ lemma zpower_zdvd_prop1: "0 < n \ p dvd y \ 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 \ 0" by simp + from \0 < z\ have modth: "x mod z \ 0" by simp have "(x div z) * z \ (x div z) * z" by simp then have "(x div z) * z \ (x div z) * z + x mod z" using modth by arith also have "\ = x" by (auto simp add: zmod_zdiv_equality [symmetric] ac_simps) - also note `x < y * z` + also note \x < y * z\ 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: \0 < z\) done then show ?thesis by auto qed @@ -79,7 +79,7 @@ qed -subsection {* Useful properties of congruences *} +subsection \Useful properties of congruences\ 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 \2 < p\ 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 \Some properties of MultInv\ lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> [(MultInv p x) = (MultInv p y)] (mod p)" diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/IntFact.thy --- 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 \Factorial on integers\ theory IntFact imports IntPrimes begin -text {* +text \ 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 -*} +\ fun zfact :: "int => int" where "zfact n = (if n \ 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 \ \medskip @{term d22set} --- recursively defined set including all integers from @{text 2} up to @{text a} -*} +\ declare d22set.simps [simp del] diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/IntPrimes.thy --- 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 \Divisibility and prime numbers (on integers)\ theory IntPrimes imports Primes begin -text {* +text \ 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}. -*} +\ -subsection {* Definitions *} +subsection \Definitions\ fun xzgcda :: "int \ int \ int \ int \ int \ int \ int \ 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 \Euclid's Algorithm and GCD\ 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\This is merely a sanity check on zprime, since the previous version + denoted the empty set.\ lemma "zprime 2" apply (auto simp add: zprime_def) apply (frule zdvd_imp_le, simp) @@ -109,7 +109,7 @@ -subsection {* Congruences *} +subsection \Congruences\ 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\Remainding case: @{term "m<0"}\ 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 \Modulo\ 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 \Extended GCD\ declare xzgcda.simps [simp del] @@ -336,7 +336,7 @@ done -text {* \medskip @{term xzgcd} linear *} +text \\medskip @{term xzgcd} linear\ lemma xzgcda_linear_aux1: "(a - r * b) * m + (c - r * d) * (n::int) = @@ -399,7 +399,7 @@ zgcd a n = 1 ==> \!x. 0 \ x \ x < n \ [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 \stac @{context} (@{thm zcong_cancel2} RS sym) 6\) apply (rule_tac [8] zcong_trans) apply (simp_all (no_asm_simp)) prefer 2 diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Legacy_GCD.thy --- 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 \The Greatest Common Divisor\ theory Legacy_GCD imports Main begin -text {* +text \ See @{cite davenport92}. \bigskip -*} +\ -subsection {* Specification of GCD on nats *} +subsection \Specification of GCD on nats\ definition - is_gcd :: "nat \ nat \ nat \ bool" where -- {* @{term gcd} as a relation *} + is_gcd :: "nat \ nat \ nat \ bool" where -- \@{term gcd} as a relation\ "is_gcd m n p \ p dvd m \ p dvd n \ (\d. d dvd m \ d dvd n \ d dvd p)" -text {* Uniqueness *} +text \Uniqueness\ lemma is_gcd_unique: "is_gcd a b m \ is_gcd a b n \ m = n" by (simp add: is_gcd_def) (blast intro: dvd_antisym) -text {* Connection to divides relation *} +text \Connection to divides relation\ lemma is_gcd_dvd: "is_gcd a b m \ k dvd a \ k dvd b \ k dvd m" by (auto simp add: is_gcd_def) -text {* Commutativity *} +text \Commutativity\ 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 \GCD on nat by Euclid's algorithm\ 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 \ \medskip @{term "gcd m n"} divides @{text m} and @{text n}. The conjunctions don't seem provable separately. -*} +\ 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 \ \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"}. -*} +\ lemma gcd_greatest: "k dvd m \ k dvd n \ k dvd gcd m n" by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod) -text {* +text \ \medskip Function gcd yields the Greatest Common Divisor. -*} +\ lemma is_gcd: "is_gcd m n (gcd m n) " by (simp add: is_gcd_def gcd_greatest) -subsection {* Derived laws for GCD *} +subsection \Derived laws for GCD\ lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \ k dvd m \ 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 \ \medskip Multiplication laws -*} +\ lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)" - -- {* @{cite \page 27\ davenport92} *} + -- \@{cite \page 27\ davenport92}\ apply (induct m n rule: gcd_induct) apply simp apply (case_tac "k = 0") @@ -165,7 +165,7 @@ done -text {* \medskip Addition laws *} +text \\medskip Addition laws\ 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 \ \medskip Division by gcd yields rrelatively primes. -*} +\ lemma div_gcd_relprime: assumes nz: "a \ 0 \ b \ 0" @@ -313,7 +313,7 @@ done -text {* We can get a stronger version with a nonzeroness assumption. *} +text \We can get a stronger version with a nonzeroness assumption.\ lemma divides_le: "m dvd n ==> m <= n \ n = (0::nat)" by (auto simp add: dvd_def) lemma bezout_add_strong: assumes nz: "a \ (0::nat)" @@ -449,7 +449,7 @@ qed -subsection {* LCM defined by GCD *} +subsection \LCM defined by GCD\ definition @@ -562,7 +562,7 @@ done -subsection {* GCD and LCM on integers *} +subsection \GCD and LCM on integers\ definition zgcd :: "int \ int \ int" where @@ -595,7 +595,7 @@ proof - assume "int (gcd (nat \i\) (nat \j\)) = 1" "i dvd k * j" then have g: "gcd (nat \i\) (nat \j\) = 1" by simp - from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast + from \i dvd k * j\ obtain h where h: "k*j = i*h" unfolding dvd_def by blast have th: "nat \i\ dvd nat \k\ * nat \j\" unfolding dvd_def by (rule_tac x= "nat \h\" in exI, simp add: h nat_abs_mult_distrib [symmetric]) @@ -620,7 +620,7 @@ let ?k' = "nat \k\" let ?m' = "nat \m\" let ?n' = "nat \n\" - from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'" + from \k dvd m\ and \k dvd n\ 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 \k\) 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 *} + -- \addition is an AC-operator\ lemma zgcd_zmult_distrib2: "0 \ 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 \k dvd i\ 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 \k dvd j\ 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 diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Pocklington.thy --- 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 \Pocklington's Theorem for Primes\ theory Pocklington imports Primes diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Primes.thy --- 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 \Primality on nat\ theory Primes imports Complex_Main Legacy_GCD @@ -27,11 +27,11 @@ apply (metis gcd_dvd1 gcd_dvd2) done -text {* +text \ 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. -*} +\ lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \ 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 \Elementary theory of divisibility\ lemma divides_ge: "(a::nat) dvd b \ b = 0 \ a \ b" unfolding dvd_def by auto lemma divides_antisym: "(x::nat) dvd y \ y dvd x \ x = y" using dvd_antisym[of x y] by auto @@ -176,7 +176,7 @@ lemma divides_rexp: "x dvd y \ (x::nat) dvd (y^(Suc n))" by (simp add: dvd_mult2[of x y]) -text {* Coprimality *} +text \Coprimality\ lemma coprime: "coprime a b \ (\d. d dvd a \ d dvd b \ 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 \A binary form of the Chinese Remainder Theorem.\ lemma chinese_remainder: assumes ab: "coprime a b" and a:"a \ 0" and b:"b \ 0" shows "\x q1 q2. x = u + q1 * a \ x = v + q2 * b" @@ -397,9 +397,9 @@ thus ?thesis by blast qed -text {* Primality *} +text \Primality\ -text {* A few useful theorems about primes *} +text \A few useful theorems about primes\ 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 \ p = 2 \ odd p" unfolding prime_def by auto -text {* One property of coprimality is easier to prove via prime factors. *} +text \One property of coprimality is easier to prove via prime factors.\ 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 \More useful lemmas.\ lemma prime_product: assumes "prime (p * q)" shows "p = 1 \ q = 1" @@ -722,7 +722,7 @@ from assms have "1 < p * q" and P: "\m. m dvd p * q \ m = 1 \ m = p * q" unfolding prime_def by auto - from `1 < p * q` have "p \ 0" by (cases p) auto + from \1 < p * q\ have "p \ 0" by (cases p) auto then have Q: "p = p * q \ q = 1" by auto have "p dvd p * q" by simp then have "p = 1 \ p = p * q" by (rule P) diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy --- 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 \The law of Quadratic reciprocity\ theory Quadratic_Reciprocity imports Gauss begin -text {* +text \ Lemmas leading up to the proof of theorem 3.3 in Niven and Zuckerman's presentation. -*} +\ context GAUSS begin @@ -153,7 +153,7 @@ done -subsection {* Stuff about S, S1 and S2 *} +subsection \Stuff about S, S1 and S2\ locale QRTEMP = fixes p :: "int" diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/Residues.thy --- 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 \Residue Sets\ theory Residues imports Int2 begin -text {* +text \ \medskip Define the residue of a set, the standard residue, - quadratic residues, and prove some basic properties. *} + quadratic residues, and prove some basic properties.\ definition ResSet :: "int => int set => bool" where "ResSet m X = (\y1 y2. (y1 \ X & y2 \ 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 \Some useful properties of StandardRes\ 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 \Relations between StandardRes, SRStar, and SR\ lemma SRStar_SR_prop: "x \ SRStar p ==> x \ 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 \Properties relating ResSets with StandardRes\ 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 \Property for SRStar\ lemma ResSet_SRStar_prop: "ResSet p (SRStar p)" by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq) diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/WilsonBij.thy --- 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 \Wilson's Theorem using a more abstract approach\ theory WilsonBij imports BijectionRel IntFact begin -text {* +text \ Wilson's Theorem using a more ``abstract'' approach based on bijections between sets. Does not use Fermat's Little Theorem (unlike Russinoff). -*} +\ -subsection {* Definitions and lemmas *} +subsection \Definitions and lemmas\ definition reciR :: "int => int => int => bool" where "reciR p = (\a b. zcong (a * b) 1 p \ 1 < a \ a < p - 1 \ 1 < b \ b < p - 1)" @@ -28,7 +28,7 @@ else 0)" -text {* \medskip Inverse *} +text \\medskip Inverse\ 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 \ 0" - -- {* same as @{text WilsonRuss} *} + -- \same as @{text WilsonRuss}\ 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 \ 1" - -- {* same as @{text WilsonRuss} *} + -- \same as @{text WilsonRuss}\ 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} *} + -- \same as @{text WilsonRuss}\ 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 \ p - 1" - -- {* same as @{text WilsonRuss} *} + -- \same as @{text WilsonRuss}\ 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 \ Below is slightly different as we don't expand @{term [source] inv} but use ``@{text correct}'' theorems. -*} +\ lemma inv_g_1: "zprime p ==> 1 < a ==> a < p - 1 ==> 1 < inv p a" apply (subgoal_tac "inv p a \ 1") @@ -111,13 +111,13 @@ lemma inv_less_p_minus_1: "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1" - -- {* ditto *} + -- \ditto\ apply (subst order_less_le) apply (simp add: inv_not_p_minus_1 inv_less) done -text {* \medskip Bijection *} +text \\medskip Bijection\ lemma aux1: "1 < x ==> 0 \ (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 \stac @{context} (@{thm zcong_cancel} RS sym) 5\) apply (rule_tac [7] zcong_trans) - apply (tactic {* stac @{context} @{thm zcong_sym} 8 *}) + apply (tactic \stac @{context} @{thm zcong_sym} 8\) 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 \stac @{context} (@{thm zcong_cancel2} RS sym) 5\) apply (rule_tac [7] zcong_trans) - apply (tactic {* stac @{context} @{thm zcong_sym} 8 *}) + apply (tactic \stac @{context} @{thm zcong_sym} 8\) 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 \stac @{context} (@{thm zcong_cancel} RS sym) 5\) apply (rule_tac [7] zcong_trans) - apply (tactic {* stac @{context} @{thm zcong_sym} 8 *}) + apply (tactic \stac @{context} @{thm zcong_sym} 8\) apply (rule_tac [6] zless_zprime_imp_zrelprime) apply auto done @@ -220,7 +220,7 @@ done -subsection {* Wilson *} +subsection \Wilson\ lemma bijER_zcong_prod_1: "zprime p ==> A \ bijER (reciR p) ==> [\A = 1] (mod p)" diff -r ddca85598c65 -r efac889fccbc src/HOL/Old_Number_Theory/WilsonRuss.thy --- 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 \Wilson's Theorem according to Russinoff\ theory WilsonRuss imports EulerFermat begin -text {* +text \ Wilson's Theorem following quite closely Russinoff's approach using Boyer-Moore (using finite sets instead of lists, though). -*} +\ -subsection {* Definitions and lemmas *} +subsection \Definitions and lemmas\ definition inv :: "int => int => int" where "inv p a = (a^(nat (p - 2))) mod p" @@ -26,7 +26,7 @@ in (if a \ ws then ws else insert a (insert (inv p a) ws)) else {})" -text {* \medskip @{term [source] inv} *} +text \\medskip @{term [source] inv}\ 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 \\medskip @{term wset}\ 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 \stac @{context} @{thm setprod.insert} 3\) apply (subgoal_tac [5] "zcong (a * inv p a * (\x\wset (a - 1) p. x)) (1 * 1) p") prefer 5 @@ -281,7 +281,7 @@ done -subsection {* Wilson *} +subsection \Wilson\ lemma prime_g_5: "zprime p \ p \ 2 \ p \ 3 ==> 5 \ p" apply (unfold zprime_def dvd_def)