From 7297867d2f6c7145e6d7b54156dbb2ed4891c035 Mon Sep 17 00:00:00 2001 From: SKolodynski Date: Tue, 30 Jan 2024 18:48:04 +0100 Subject: [PATCH] fixed parsing Ring_ZF_2 --- IsarMathLib/Ring_ZF_2.thy | 55 +++++++++++--------- IsarMathLib/Ring_ZF_3.thy | 13 +++-- isar2html2.0/src/isar2html/Export2Html.fs | 7 +-- isar2html2.0/src/isar2html/IMLP_datatypes.fs | 1 + isar2html2.0/src/isar2html/IMLParser.fs | 7 +-- isar2html2.0/test/isar2htmlTest/Tests.fs | 3 +- 6 files changed, 50 insertions(+), 36 deletions(-) diff --git a/IsarMathLib/Ring_ZF_2.thy b/IsarMathLib/Ring_ZF_2.thy index 9a87603..f5592d7 100644 --- a/IsarMathLib/Ring_ZF_2.thy +++ b/IsarMathLib/Ring_ZF_2.thy @@ -34,13 +34,18 @@ theory Ring_ZF_2 imports Ring_ZF Group_ZF_2 Finite_ZF Finite1 Cardinal_ZF Semigr begin -text \This section defines the concept of a ring ideal, and +text\This section defines the concept of a ring ideal, and defines some basic concepts and types, finishing with the theorem that shows that the quotient of the additive group by the ideal is actually a full ring.\ +subsection\Ideals\ + +text\In ring theory ideals are special subsets of a ring that play a similar role + as normal subgroups in the group theory. \ + text\An ideal is a subgroup of the additive group of the ring, which -is closed by left and right multiplication by any ring element.\ + is closed by left and right multiplication by any ring element.\ definition (in ring0) Ideal ("_\R") where "I \R \ (\x\I. \y\R. y\x\I \ x\y\I) \ IsAsubgroup(I,A)" @@ -67,7 +72,8 @@ text\An ideal is s subset of the the ring.\ lemma (in ring0) ideal_dest_subset: assumes "I \R" - shows "I \ R" using assms unfolding Ideal_def using add_group.group0_3_L2 by auto + shows "I \ R" using assms add_group.group0_3_L2 + unfolding Ideal_def by auto text\Ideals are closed with respect to the ring addition.\ @@ -86,15 +92,15 @@ text\Ideals are closed with respect to taking the opposite in the ring.\R" "x\I" - shows "(\x) \ I" using assms unfolding Ideal_def using - add_group.group0_3_T3A by auto + shows "(\x) \ I" + using assms add_group.group0_3_T3A unfolding Ideal_def by auto text\Every ideals contains zero.\ lemma (in ring0) ideal_dest_zero: assumes "I \R" - shows "\ \ I" using assms unfolding Ideal_def using - add_group.group0_3_L5 by auto + shows "\ \ I" + using assms add_group.group0_3_L5 unfolding Ideal_def by auto text\The simplest way to obtain an ideal from others is the intersection, since the intersection of arbitrary collection of ideals is an ideal.\ @@ -137,13 +143,12 @@ text\The ideal generated by a set is contained in any ideal containing the corollary (in ring0) generated_ideal_small: assumes "X\I" "I \R" shows "\X\\<^sub>I \ I" -proof- - have "I\{J\Pow(R). J \R \ X\J}" using assms(2,1) - ideal_dest_subset by auto - then have "\{J\Pow(R). J \R \ X\J} \ I" by auto moreover - from assms have "X\ R" using ideal_dest_subset by auto - ultimately show "\X\\<^sub>I \ I" using generatedIdeal_def[of X] - by auto +proof - + from assms have "I\{J\Pow(R). J \R \ X\J}" + using ideal_dest_subset by auto + then have "\{J\Pow(R). J \R \ X\J} \ I" by auto + moreover from assms have "X\ R" using ideal_dest_subset by auto + ultimately show "\X\\<^sub>I \ I" using generatedIdeal_def by auto qed text\The ideal generated by a set contains the set.\ @@ -442,7 +447,7 @@ proof - ultimately have "x\y \ A``(I\J)" using ij add_group.group_oper_fun func_imagedef by auto - } hence "A``(I \ J) {is closed under} A" + } then have "A``(I \ J) {is closed under} A" unfolding IsOpClosed_def by auto moreover { fix x assume "x \ A``(I \ J)" @@ -522,9 +527,9 @@ text\Any maximal ideal is a prime ideal.\ theorem (in ring0) maximal_is_prime: assumes "Q\\<^sub>mR" shows "Q\\<^sub>pR" proof - - have "Q\\" using assms unfolding maximalIdeal_def - using ideal_dest_subset by auto - { fix I J assume "I\\" "J\\" "I \\<^sub>I J \ Q" + have "Q\\" using assms ideal_dest_subset + unfolding maximalIdeal_def by auto + { fix I J assume "I\\" "J\\" "I\\<^sub>IJ \ Q" { assume K: "\(I\Q)" "\(J\Q)" from \\(I\Q)\ obtain x where "x\I-Q" by auto with \I\\\ have "x\R" using ideal_dest_subset by auto @@ -538,7 +543,7 @@ proof - using ideal_dest_subset generated_ideal_is_ideal by blast with assms \Q\?K\ \?K\Q\ have "?K=R" unfolding maximalIdeal_def by auto - let ?P="Q+\<^sub>II" + let ?P = "Q+\<^sub>II" from \Q\\\ \I\\\ \x\I-Q\ have "Q\{x} \ Q+\<^sub>II" using comp_in_sum_ideals(3) by auto with \Q\\\ \I\\\ have "?K \ Q+\<^sub>II" "Q+\<^sub>II \ R" @@ -617,8 +622,8 @@ lemma (in ring0) zero_prime_ideal_prime_ring: shows "[R,A,M]{is a prime ring}" proof - { fix x y z assume "x\R" "y\R" "\z\R. x\z\y = \" - let ?X="\{x}\\<^sub>I" - let ?Y="\{y}\\<^sub>I" + let ?X = "\{x}\\<^sub>I" + let ?Y = "\{y}\\<^sub>I" from \x\R\ \y\R\ have "?X\?Y \ R\R" using generated_ideal_is_ideal ideal_dest_subset by auto @@ -697,8 +702,8 @@ theorem (in ring0) equivalent_prime_ideal: shows "\x\R. \y\R. (\z\R. x\z\y\P) \ x\P \ y\P" proof - { fix x y assume "x\R" "y\R" "\z\R. x\z\y\P" "y\P" - let ?X="\{x}\\<^sub>I" - let ?Y="\{y}\\<^sub>I" + let ?X = "\{x}\\<^sub>I" + let ?Y = "\{y}\\<^sub>I" from \y\R\ have "{y}\0" and "{y}\R" by auto moreover have "\y\<^sub>a\R. \z\R. \q\\{y}\\<^sub>I. (\t\\{x}\\<^sub>I. \u\R. t\u\q \ P) \ @@ -823,8 +828,8 @@ text\Any ideal is a normal subgroup.\ lemma (in ring0) ideal_normal_add_subgroup: assumes "I\R" shows "IsAnormalSubgroup(R,A,I)" - using Group_ZF_2_4_L6(1) using ringAssum - unfolding IsAring_def using assms unfolding Ideal_def by auto + using ringAssum assms Group_ZF_2_4_L6(1) + unfolding IsAring_def Ideal_def by auto text\ Each ring $R$ is a group with respect to its addition operation. By the lemma \ideal_normal_add_subgroup\ above an ideal $I\subseteq R$ is a normal subgroup of that group. diff --git a/IsarMathLib/Ring_ZF_3.thy b/IsarMathLib/Ring_ZF_3.thy index b2adfd2..3f5512d 100644 --- a/IsarMathLib/Ring_ZF_3.thy +++ b/IsarMathLib/Ring_ZF_3.thy @@ -34,10 +34,15 @@ theory Ring_ZF_3 imports Ring_ZF_2 Group_ZF_5 begin -text \This section studies the ideals of quotient rings, +text\This section studies the ideals of quotient rings, and defines ring homomorphisms.\ -text\A ring homomorphism is a function between rings that which has the +subsection\Ring homomorphisms\ + +text\Morphisms in general are structure preserving functions between algebraic + structures. In this section we study ring homomorphisms.\ + +text\A ring homomorphism is a function between rings which has the morphism property with respect to both addition and multiplication operation, and maps one (the neutral element of multiplication) in the first ring to one in the second ring. \ @@ -385,7 +390,7 @@ proof - by (rule origin_ring.equivalent_prime_ideal_2) qed -section\Quotient ring with quotient map\ +subsection\Quotient ring with quotient map\ text\The notion of a quotient ring (a.k.a factor ring, difference ring or residue class) is analogous to the notion of quotient group from the group theory. \ @@ -1032,4 +1037,4 @@ proof - ultimately show ?thesis by auto qed -end \ No newline at end of file +end diff --git a/isar2html2.0/src/isar2html/Export2Html.fs b/isar2html2.0/src/isar2html/Export2Html.fs index 1673f82..31af167 100644 --- a/isar2html2.0/src/isar2html/Export2Html.fs +++ b/isar2html2.0/src/isar2html/Export2Html.fs @@ -365,10 +365,11 @@ namespace iml /// exports formal items let exportFormalItem (repls:(string*string) list) (mfii:Map) (fit:FormalItem) = match fit with - | Abbr abbr -> (bf "abbreviation" |> par) + (isar2latex repls abbr.abbspec |> par) + | Abbr abbr -> ((bf "abbreviation") + (if abbr.abbcontext.Length=0 then "\n" else " (in " + abbr.abbcontext + ")") + "\n" |> par) + + (isar2latex repls abbr.abbspec |> par) |> mkformal "" - | Def def -> ((bf "definition ") + (if def.defcontext.Length=0 then "\n" else " (in " + def.defcontext + ")") + "\n" |> par) - + (isar2latex repls def.def |> par) + | Def def -> ((bf "definition ") + (if def.defcontext.Length=0 then "\n" else " (in " + def.defcontext + ")") + "\n" |> par) + + (isar2latex repls def.def |> par) |> mkformal "" | Loc loc -> let (parent,vars) = loc.inheritsFrom ((bf "locale ") + loc.localename diff --git a/isar2html2.0/src/isar2html/IMLP_datatypes.fs b/isar2html2.0/src/isar2html/IMLP_datatypes.fs index c9b2895..2c1959a 100644 --- a/isar2html2.0/src/isar2html/IMLP_datatypes.fs +++ b/isar2html2.0/src/isar2html/IMLP_datatypes.fs @@ -32,6 +32,7 @@ module IMLP_datatypes = } type Abbreviation = { abbname: string; + abbcontext: string; // an optional locale abbnotation: string; // string defining notation, like "_ ->F _ {in} _" abbspec: string // the actual abbreviation (after the "where" keyword) } diff --git a/isar2html2.0/src/isar2html/IMLParser.fs b/isar2html2.0/src/isar2html/IMLParser.fs index c2c2555..537b08c 100644 --- a/isar2html2.0/src/isar2html/IMLParser.fs +++ b/isar2html2.0/src/isar2html/IMLParser.fs @@ -189,11 +189,12 @@ module IMLParser = /// parses abbreviations let abbreviation : Parser = - pipe3 - (pstring "abbreviation" >>. whiteSpace >>. pureItemName) + pipe4 + (pstring "abbreviation" >>. whiteSpace >>. poption "" incontext) + (whiteSpace >>. pureItemName) (whiteSpace >>. textBetween "(\"" "\")") (whiteSpace >>. pstring "where" >>. whiteSpace >>. innerText) - (fun nm nt d -> Abbr { abbname = nm; abbnotation = nt; abbspec = d }) + (fun contxt nm nt d -> Abbr { abbname = nm; abbcontext = contxt; abbnotation = nt; abbspec = d }) /// parses definitions. Note we require a space before \ in the definition let definition : Parser = diff --git a/isar2html2.0/test/isar2htmlTest/Tests.fs b/isar2html2.0/test/isar2htmlTest/Tests.fs index 99ea68d..370c967 100644 --- a/isar2html2.0/test/isar2htmlTest/Tests.fs +++ b/isar2html2.0/test/isar2htmlTest/Tests.fs @@ -177,7 +177,8 @@ let ``test labelsimp`` () = let ``test abbreviation`` () = let teststr = "abbreviation FilConvTop(\"_ \\\\<^sub>F _ {in} _\")\n\ where \"\\ \\\\<^sub>F x {in} T \\ topology0.FilterConverges(T,\\,x)\"" - let parsed = Abbr { abbname = "FilConvTop"; + let parsed = Abbr { abbname = "FilConvTop"; + abbcontext = ""; abbnotation = "_ \\\\<^sub>F _ {in} _"; abbspec = "\\ \\\\<^sub>F x {in} T \\ topology0.FilterConverges(T,\\,x)" } test1 abbreviation teststr parsed