added power notation to group0 locale

IsarMathLib/FiniteSeq_ZF.thy

@@ -1046,6 +1046,20 @@ proof -
     using func1_1_L1 unfolding Prepend_def by simp
 qed
 
+text\<open>The tail of a list prepended by an element is equal to the list.\<close>
+
+lemma tail_prepend: assumes "n\<in>nat" "a:n\<rightarrow>X" "x\<in>X"
+  shows "Tail(Prepend(a,x)) = a"
+proof -
+  let ?b = "Prepend(a,x)"
+  from assms have "?b:(n #+ 1)\<rightarrow>X" using prepend_props(1) by simp
+  with assms(1) have "Tail(?b):n\<rightarrow>X" using tail_props(1) by simp
+  from assms \<open>?b:(n #+ 1)\<rightarrow>X\<close> have "\<forall>k\<in>n. Tail(?b)`(k) = a`(k)"
+    using tail_props2 prepend_val by simp
+  with assms(2) \<open>Tail(?b):n\<rightarrow>X\<close> show ?thesis using func_eq
+    by blast
+qed
+
 subsection\<open>Lists and cartesian products\<close>
 
 text\<open>Lists of length $n$ of elements of some set $X$ can be thought of as a 

IsarMathLib/Group_ZF.thy

@@ -2,7 +2,7 @@
 This file is a part of IsarMathLib - 
 a library of formalized mathematics for Isabelle/Isar.
 
-Copyright (C) 2005 - 2008  Slawomir Kolodynski
+Copyright (C) 2005 - 2024  Slawomir Kolodynski
 
 This program is free software; Redistribution and use in source and binary forms, 
 with or without modification, are permitted provided that the 
@@ -31,7 +31,7 @@ EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
 section \<open>Groups - introduction\<close>
 
-theory Group_ZF imports Monoid_ZF
+theory Group_ZF imports Monoid_ZF_1 Semigroup_ZF
 
 begin
 
@@ -60,8 +60,17 @@ text\<open>We define the group inverse as the set
 definition
   "GroupInv(G,f) \<equiv> {\<langle>x,y\<rangle> \<in> G\<times>G. f`\<langle>x,y\<rangle> = TheNeutralElement(G,f)}"
 
-text\<open>We will use the miltiplicative notation for groups. The neutral
-  element is denoted $1$.\<close>
+text\<open>Next we define the context \<open>group0\<close> in which groups will be discussed. 
+  The common assumption for all proposition proven in the context \<open>group0\<close> is that
+  fixed the pair $(G,P)$ is a group. We will use the multiplicative notation for groups. 
+  The neutral element is denoted $1$. \<open>x\<inverse>\<close>  will denote the inverse of $x$, i.e. the value
+  of the group inverse operation on $x$. We define the notation for product of a finite 
+  list of elements of $G$ using the notion of \<open>Fold\<close>, defined in the \<open>Fold_ZF\<close> theory.
+  Finally we define the notation \<open>pow(n,x)\<close> which is a product of the list
+  of length $n$ with value $x$ repeated $n$ times. Such list is a function that
+  assigns $x$ to every element of the set $n=\{0,1,...,n-1\}$ and is represented by a set of pairs
+  $\{\langle k,x\rangle : k\in n\}$, which is the same as the set $n\times\{ x\}$ 
+  (see lemma \<open>fun_def_alt1\<close> in the \<open>func1\<close> theory. \<close>
 
 locale group0 =
   fixes G 
@@ -77,16 +86,27 @@ locale group0 =
   fixes inv ("_\<inverse> " [90] 91)
   defines inv_def[simp]: "x\<inverse> \<equiv> GroupInv(G,P)`(x)"
 
+  fixes listprod ("\<Prod> _" 70)
+  defines listprod_def [simp]: "\<Prod>s \<equiv> Fold(P,\<one>,s)"
+
+  fixes pow
+  defines pow_def [simp]: "pow(n,x) \<equiv> \<Prod>{\<langle>k,x\<rangle>. k\<in>n}"
+
 text\<open>First we show a lemma that says that we can use theorems proven in
   the \<open>monoid0\<close> context (locale).\<close>
 
 lemma (in group0) group0_2_L1: shows "monoid0(G,P)"
   using groupAssum IsAgroup_def monoid0_def by simp
 
-text\<open>The theorems proven in the \<open>monoid\<close> context are valid in the \<open>group0\<close> context.\<close>
+text\<open>Assumptions of the \<open>monoid1\<close> context are satisfied in the \<open>group0\<close> context.\<close>
+
+lemma (in group0) monoid1_valid_in_group: shows "monoid1(G,P)"
+  using group0_2_L1 monoid1_def by simp 
 
-sublocale group0 < monoid: monoid0 G P groper
-  unfolding groper_def using group0_2_L1 by auto
+text\<open>The theorems proven in the \<open>monoid1\<close> context are valid in the \<open>group0\<close> context.\<close>
+
+sublocale group0 < monoid: monoid1 G P groper "\<one>" listprod pow
+  using monoid1_valid_in_group by auto
 
 text\<open>In some strange cases Isabelle has difficulties with applying
   the definition of a group. The next lemma defines a rule to be applied
@@ -1166,5 +1186,51 @@ proof -
   ultimately show "RightInv(G,P) = GroupInv(G,P)" using func_eq by blast  
 qed
 
+subsection\<open>Product of a list of group elements\<close>
+
+text\<open>The \<open>group0\<close> context defines notation for a product of a finite list of group elements. This
+  sections shows basic properties of that notation.\<close>
+
+text\<open>The assumptions of the \<open>semigr0\<close> context hold in the \<open>group0\<close> context.\<close>
+
+lemma (in group0) semigr0_valid_in_group0: shows "semigr0(G,P)"
+  using groupAssum IsAgroup_def IsAmonoid_def semigr0_def by simp
+
+text\<open>Since semigroups do not have a neutral element the product operator in the \<open>semigr0\<close>
+  is defined for nonempty lists only as \<open>Fold1(f,a)\<close>, where $f$ is the semigroup operation
+  and $a$ is a (nonempty) list. This is a bit different from the product of a finite
+  list in the \<open>group0\<close> context. The next lemma helps in translating between these two notations
+  by asserting that in the \<open>group0\<close> context the sum of a finite list $s$ is the same as \<open>Fold1(s\<^sub>1)\<close>
+  where $s_1$ is the list $s$ with the neutral element of the group prepended to it. \<close>
+
+lemma (in group0) list_prod_as_fold1: assumes "n\<in>nat" "s:n\<rightarrow>G"
+  shows "(\<Prod>s) = Fold1(P,Prepend(s,\<one>))"
+  using assms prepend_props group0_2_L2 tail_prepend
+  unfolding Fold1_def by simp
+
+text\<open>For nonempty lists the product is the the same as \<open>Fold1\<close> of the list with respect to the 
+  operation.\<close>
+
+lemma (in group0) nempty_list_prod_as_fold1: assumes "n\<in>nat" "s:(n #+ 1)\<rightarrow>G"
+  shows "(\<Prod>s) = Fold1(P,s)"
+  using assms group_oper_fun group0_2_L2 fold_detach_first
+    succ_add_one(6) apply_funtype
+  unfolding Fold1_def by simp
+
+text\<open>The product of a list is an element of the group.\<close>
+
+lemma (in group0) list_prod_in_group: assumes "n\<in>nat" "s:n\<rightarrow>G"
+  shows "(\<Prod>s) \<in> G"
+proof -
+  have "P:G\<times>G\<rightarrow>G" "\<one>\<in>G" "G\<noteq>\<emptyset>" using group_oper_fun group0_2_L2 by auto
+  with assms show "(\<Prod>s) \<in> G" using fold_props(2) by simp
+qed
+
+text\<open>Product of a singleton list is its only element.\<close>
+
+lemma (in group0) prod_singleton: assumes  "s:1\<rightarrow>G"
+  shows "(\<Prod>s) = s`(0)"
+  using assms nempty_list_prod_as_fold1 semigr0_valid_in_group0 semigr0.prod_of_1elem
+    by force
 
 end

IsarMathLib/Group_ZF_5.thy

@@ -319,6 +319,8 @@ sublocale abelian_group < endo_ring: ring0
      \<langle>TheNeutralElement (End(G, P), InEnd(Composition(G),G,P)),
       TheNeutralElement (End(G, P), InEnd(Composition(G),G,P))\<rangle>"
   "\<lambda>x. InEnd(Composition(G),G,P)`\<langle>x, x\<rangle>"
+  "\<lambda>s. Fold(InEnd(P {lifted to function space over} G,G,P), TheNeutralElement(End(G, P), InEnd(P {lifted to function space over} G,G,P)),s)"
+  "\<lambda>n x. Fold(InEnd(P {lifted to function space over} G,G,P), TheNeutralElement(End(G, P), InEnd(P {lifted to function space over} G,G,P)),{\<langle>k,x\<rangle>. k\<in>n})"
   using end_is_ring unfolding ring0_def by blast
 
 subsection\<open>First isomorphism theorem\<close>

IsarMathLib/IntModule_ZF.thy

@@ -1188,9 +1188,12 @@ locale abelian_group_int_action = abelian_group + int0
 text\<open>Under this assumptions, we have an action\<close>
 
 sublocale abelian_group_int_action < int_action:module0 ints IntegerAddition IntegerMultiplication 
-  ia iminus isub imult izero ione itwo "\<lambda>q. imult(q,q)" G P "{\<langle>$# n,{\<langle>x,Fold(P,neut,n\<times>{x})\<rangle>. x\<in>G}\<rangle>. n\<in>nat} \<union> {\<langle>$- $# n,GroupInv(G,P) O {\<langle>x,Fold(P,neut, n\<times>{x})\<rangle>. x\<in>G}\<rangle>. n\<in>nat}"
+  ia iminus isub imult izero ione itwo "\<lambda>q. imult(q,q)" 
+  "\<lambda> s. Fold(IntegerAddition,izero,s)"
+  "\<lambda> n x.  Fold(IntegerAddition,izero,{\<langle>k,x\<rangle>. k\<in>n})"
+  G P "{\<langle>$# n,{\<langle>x,Fold(P,neut,n\<times>{x})\<rangle>. x\<in>G}\<rangle>. n\<in>nat} \<union> {\<langle>$- $# n,GroupInv(G,P) O {\<langle>x,Fold(P,neut, n\<times>{x})\<rangle>. x\<in>G}\<rangle>. n\<in>nat}"
   neut groper "\<lambda>s g. ({\<langle>$# n,{\<langle>x,Fold(P,neut,n\<times>{x})\<rangle>. x\<in>G}\<rangle>. n\<in>nat} \<union> {\<langle>$- $# n,GroupInv(G,P) O {\<langle>x,Fold(P,neut, n\<times>{x})\<rangle>. x\<in>G}\<rangle>. n\<in>nat})`s`g" inv 
-  "\<lambda>g h. groper(g,inv(h))"
+  "\<lambda>g h. groper(g,inv(h))" 
   unfolding module0_def module0_axioms_def apply auto using Int_ZF_1_1_L2(3) apply simp
   using groupAssum apply simp using isAbelian apply simp using group_action_int
   unfolding IsLeftModule_def apply simp done
@@ -1203,11 +1206,11 @@ cannot be interpreted. First the unit integer.
 \<close>*)
 
 abbreviation (in abelian_group_int_action) zone ("\<one>\<^sub>\<int>") where
-"\<one>\<^sub>\<int> \<equiv> ione"
+  "\<one>\<^sub>\<int> \<equiv> ione"
 
 text\<open>Then, the unit in the abelian group\<close>
 
 abbreviation (in abelian_group_int_action) gone ("\<one>\<^sub>G") where
-"\<one>\<^sub>G \<equiv> neut"
+  "\<one>\<^sub>G \<equiv> neut"
 
 end

IsarMathLib/Module_ZF.thy

@@ -146,6 +146,7 @@ text\<open>Another way to state that theorems proven in the \<open>abelian_group
   can be used in the \<open>module0\<close> context:  \<close>
 
 sublocale module0 < mod_ab_gr: abelian_group "\<M>" "A\<^sub>M" "\<Theta>" vAdd negV
+  "\<lambda>s. Fold(A\<^sub>M, \<Theta>, s)" "\<lambda> n x. Fold(A\<^sub>M, \<Theta>, {\<langle>k, x\<rangle> . k \<in> n})"
   using abelian_group_valid_module0 by auto
 
 text\<open>Theorems proven in the \<open>ring_homo\<close> context are valid in the \<open>module0\<close> context, as

IsarMathLib/Real_ZF_2.thy

@@ -98,6 +98,12 @@ locale reals =
   defines inv_def[simp]: 
     "x\<inverse> \<equiv> GroupInv(\<real>\<^sub>0,restrict(Mul,\<real>\<^sub>0\<times>\<real>\<^sub>0))`(x)"
 
+  fixes listsum ("\<Sum> _" 70)
+  defines listsum_def[simp]: "\<Sum>s \<equiv> Fold(Add,\<zero>,s)"
+
+  fixes nat_mult (infix "\<nm>" 95)
+  defines nat_mult_def [simp]: "n\<nm>x \<equiv> \<Sum>{\<langle>k,x\<rangle>. k\<in>n}"
+
   fixes realsq ("_\<^sup>2" [96] 97)
   defines realsq_def [simp]: "x\<^sup>2 \<equiv> x\<rmu>x"
 
@@ -129,7 +135,8 @@ text\<open> We can use theorems proven in the  \<open>field1\<close> locale in t
   extension of \<open>ring0\<close> locale , this makes available also the theorems proven in 
   the \<open>ring1\<close> and \<open>ring0\<close> locales. \<close>
 
-sublocale reals < field1 Reals Add Mul realadd realminus realsub realmul zero one two realsq ROrd
+sublocale reals < field1 Reals Add Mul realadd realminus realsub realmul 
+  zero one two realsq listsum nat_mult ROrd
   using field1_is_valid by auto
 
 text\<open> The \<open>group3\<close> locale from the \<open>OrderedGroup_ZF\<close> theory defines context for theorems about 
@@ -142,7 +149,7 @@ sublocale reals < group3 Reals Add ROrd zero realadd realminus lesseq sless nonn
 text\<open>Since real numbers with addition form a group we can use the theorems proven in the  \<open>group0\<close> 
   locale defined in the \<open>Group_ZF\<close> theory in the \<open>reals\<close> locale. \<close>
 
-sublocale reals < group0 Reals Add zero realadd realminus 
+sublocale reals < group0 Reals Add zero realadd realminus listsum nat_mult
   unfolding group3_def using OrderedGroup_ZF_1_L1 by auto
 
 text\<open>Let's recall basic properties of the real line. \<close>