fixed parsing Ring_ZF_2

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 \<open>This section defines the concept of a ring ideal, and
+text\<open>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.\<close>
 
+subsection\<open>Ideals\<close>
+
+text\<open>In ring theory ideals are special subsets of a ring that play a similar role 
+  as normal subgroups in the group theory. \<close>
+
 text\<open>An ideal is a subgroup of the additive group of the ring, which
-is closed by left and right multiplication by any ring element.\<close>
+  is closed by left and right multiplication by any ring element.\<close>
 
 definition (in ring0) Ideal ("_\<triangleleft>R") where
   "I \<triangleleft>R \<equiv> (\<forall>x\<in>I. \<forall>y\<in>R. y\<cdot>x\<in>I \<and> x\<cdot>y\<in>I) \<and> IsAsubgroup(I,A)"
@@ -67,7 +72,8 @@ text\<open>An ideal is s subset of the the ring.\<close>
 
 lemma (in ring0) ideal_dest_subset:
   assumes "I \<triangleleft>R" 
-  shows "I \<subseteq> R" using assms unfolding Ideal_def using add_group.group0_3_L2  by auto
+  shows "I \<subseteq> R" using assms add_group.group0_3_L2 
+  unfolding Ideal_def by auto
 
 text\<open>Ideals are closed with respect to the ring addition.\<close>
 
@@ -86,15 +92,15 @@ text\<open>Ideals are closed with respect to taking the opposite in the ring.\<c
 
 lemma (in ring0) ideal_dest_minus:
   assumes "I \<triangleleft>R" "x\<in>I"
-  shows "(\<rm>x) \<in> I" using assms unfolding Ideal_def using
-    add_group.group0_3_T3A by auto
+  shows "(\<rm>x) \<in> I" 
+  using assms add_group.group0_3_T3A unfolding Ideal_def by auto
 
 text\<open>Every ideals contains zero.\<close>
 
 lemma (in ring0) ideal_dest_zero:
   assumes "I \<triangleleft>R"
-  shows "\<zero> \<in> I" using assms unfolding Ideal_def using
-    add_group.group0_3_L5 by auto
+  shows "\<zero> \<in> I" 
+  using assms add_group.group0_3_L5 unfolding Ideal_def by auto
 
 text\<open>The simplest way to obtain an ideal from others is the intersection,
   since the intersection of arbitrary collection of ideals is an ideal.\<close>
@@ -137,13 +143,12 @@ text\<open>The ideal generated by a set is contained in any ideal containing the
 corollary (in ring0) generated_ideal_small:
   assumes "X\<subseteq>I" "I \<triangleleft>R"
   shows "\<langle>X\<rangle>\<^sub>I \<subseteq> I"
-proof-
-  have "I\<in>{J\<in>Pow(R). J \<triangleleft>R \<and> X\<subseteq>J}" using assms(2,1)
-    ideal_dest_subset by auto
-  then have "\<Inter>{J\<in>Pow(R). J \<triangleleft>R \<and> X\<subseteq>J} \<subseteq> I" by auto moreover
-  from assms have "X\<subseteq> R" using ideal_dest_subset by auto
-  ultimately show "\<langle>X\<rangle>\<^sub>I \<subseteq> I" using generatedIdeal_def[of X]
-    by auto
+proof -
+  from assms have "I\<in>{J\<in>Pow(R). J \<triangleleft>R \<and> X\<subseteq>J}" 
+    using ideal_dest_subset by auto
+  then have "\<Inter>{J\<in>Pow(R). J \<triangleleft>R \<and> X\<subseteq>J} \<subseteq> I" by auto 
+  moreover from assms have "X\<subseteq> R" using ideal_dest_subset by auto
+  ultimately show "\<langle>X\<rangle>\<^sub>I \<subseteq> I" using generatedIdeal_def by auto
 qed
 
 text\<open>The ideal generated by a set contains the set.\<close>
@@ -442,7 +447,7 @@ proof -
       ultimately have "x\<ra>y \<in> A``(I\<times>J)" 
         using ij add_group.group_oper_fun func_imagedef 
         by auto
-    } hence "A``(I \<times> J) {is closed under} A" 
+    } then have "A``(I \<times> J) {is closed under} A" 
       unfolding IsOpClosed_def by auto
     moreover
     { fix x assume "x \<in> A``(I \<times> J)"
@@ -522,9 +527,9 @@ text\<open>Any maximal ideal is a prime ideal.\<close>
 theorem (in ring0) maximal_is_prime:
   assumes "Q\<triangleleft>\<^sub>mR" shows "Q\<triangleleft>\<^sub>pR"
 proof -
-  have "Q\<in>\<I>" using assms unfolding maximalIdeal_def
-    using ideal_dest_subset by auto
-  { fix I J assume "I\<in>\<I>" "J\<in>\<I>" "I \<cdot>\<^sub>I J \<subseteq> Q"
+  have "Q\<in>\<I>" using assms ideal_dest_subset 
+    unfolding maximalIdeal_def by auto
+  { fix I J assume "I\<in>\<I>" "J\<in>\<I>" "I\<cdot>\<^sub>IJ \<subseteq> Q"
     { assume K: "\<not>(I\<subseteq>Q)" "\<not>(J\<subseteq>Q)"
       from \<open>\<not>(I\<subseteq>Q)\<close> obtain x where "x\<in>I-Q" by auto
       with \<open>I\<in>\<I>\<close> have "x\<in>R" using ideal_dest_subset by auto
@@ -538,7 +543,7 @@ proof -
         using ideal_dest_subset generated_ideal_is_ideal by blast
       with assms \<open>Q\<subseteq>?K\<close> \<open>?K\<noteq>Q\<close> have "?K=R" unfolding maximalIdeal_def
         by auto
-      let ?P="Q+\<^sub>II"
+      let ?P = "Q+\<^sub>II"
       from \<open>Q\<in>\<I>\<close> \<open>I\<in>\<I>\<close> \<open>x\<in>I-Q\<close> have "Q\<union>{x} \<subseteq> Q+\<^sub>II"
         using comp_in_sum_ideals(3) by auto
       with \<open>Q\<in>\<I>\<close> \<open>I\<in>\<I>\<close> have "?K \<subseteq> Q+\<^sub>II" "Q+\<^sub>II \<subseteq> 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\<in>R" "y\<in>R" "\<forall>z\<in>R. x\<cdot>z\<cdot>y = \<zero>"
-    let ?X="\<langle>{x}\<rangle>\<^sub>I"
-    let ?Y="\<langle>{y}\<rangle>\<^sub>I"
+    let ?X = "\<langle>{x}\<rangle>\<^sub>I"
+    let ?Y = "\<langle>{y}\<rangle>\<^sub>I"
     from \<open>x\<in>R\<close> \<open>y\<in>R\<close> have "?X\<times>?Y \<subseteq> R\<times>R"
       using generated_ideal_is_ideal ideal_dest_subset 
       by auto
@@ -697,8 +702,8 @@ theorem (in ring0) equivalent_prime_ideal:
   shows "\<forall>x\<in>R. \<forall>y\<in>R. (\<forall>z\<in>R. x\<cdot>z\<cdot>y\<in>P) \<longrightarrow> x\<in>P \<or> y\<in>P"
 proof -
   { fix x y assume "x\<in>R" "y\<in>R" "\<forall>z\<in>R. x\<cdot>z\<cdot>y\<in>P" "y\<notin>P"
-    let ?X="\<langle>{x}\<rangle>\<^sub>I"
-    let ?Y="\<langle>{y}\<rangle>\<^sub>I"
+    let ?X = "\<langle>{x}\<rangle>\<^sub>I"
+    let ?Y = "\<langle>{y}\<rangle>\<^sub>I"
     from \<open>y\<in>R\<close> have "{y}\<noteq>0" and "{y}\<subseteq>R" by auto
     moreover have "\<forall>y\<^sub>a\<in>R.
        \<forall>z\<in>R. \<forall>q\<in>\<langle>{y}\<rangle>\<^sub>I. (\<forall>t\<in>\<langle>{x}\<rangle>\<^sub>I. \<forall>u\<in>R. t\<cdot>u\<cdot>q \<in> P) \<longrightarrow>
@@ -823,8 +828,8 @@ text\<open>Any ideal is a normal subgroup.\<close>
 lemma (in ring0) ideal_normal_add_subgroup:
   assumes "I\<triangleleft>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\<open> Each ring $R$ is a group with respect to its addition operation.
   By the lemma \<open>ideal_normal_add_subgroup\<close> above an ideal $I\subseteq R$ is a normal subgroup of that group.

IsarMathLib/Ring_ZF_3.thy

@@ -34,10 +34,15 @@ theory Ring_ZF_3 imports Ring_ZF_2 Group_ZF_5
 
 begin
 
-text \<open>This section studies the ideals of quotient rings,
+text\<open>This section studies the ideals of quotient rings,
   and defines ring homomorphisms.\<close>
 
-text\<open>A ring homomorphism is a function between rings that which has the
+subsection\<open>Ring homomorphisms\<close>
+
+text\<open>Morphisms in general are structure preserving functions between algebraic
+  structures. In this section we study ring homomorphisms.\<close>
+
+text\<open>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. \<close>
@@ -385,7 +390,7 @@ proof -
     by (rule origin_ring.equivalent_prime_ideal_2)
 qed
 
-section\<open>Quotient ring with quotient map\<close>
+subsection\<open>Quotient ring with quotient map\<close>
 
 text\<open>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. \<close>
@@ -1032,4 +1037,4 @@ proof -
   ultimately show ?thesis by auto
 qed
 
-end
+end

isar2html2.0/src/isar2html/Export2Html.fs

@@ -365,10 +365,11 @@ namespace iml
         /// exports formal items
         let exportFormalItem (repls:(string*string) list) (mfii:Map<string,string>) (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 

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)
                             }

isar2html2.0/src/isar2html/IMLParser.fs

@@ -189,11 +189,12 @@ module IMLParser =
 
     /// parses abbreviations
     let abbreviation : Parser<FormalItem,unit> =
-        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 \<equiv> in the definition
     let definition : Parser<FormalItem,unit> =  

isar2html2.0/test/isar2htmlTest/Tests.fs

@@ -177,7 +177,8 @@ let ``test labelsimp`` () =
 let ``test abbreviation`` () =
     let teststr = "abbreviation FilConvTop(\"_ \\<rightarrow>\\<^sub>F _ {in} _\")\n\
                     where \"\\<FF> \\<rightarrow>\\<^sub>F x {in} T \\<equiv> topology0.FilterConverges(T,\\<FF>,x)\""
-    let parsed =  Abbr { abbname = "FilConvTop"; 
+    let parsed =  Abbr { abbname = "FilConvTop";
+                         abbcontext = "";
                             abbnotation = "_ \\<rightarrow>\\<^sub>F _ {in} _";
                             abbspec = "\\<FF> \\<rightarrow>\\<^sub>F x {in} T \\<equiv> topology0.FilterConverges(T,\\<FF>,x)" }            
     test1 abbreviation teststr parsed