integer power commutes with group operation in abelian groups

IsarMathLib/Group_ZF.thy

@@ -462,6 +462,17 @@ proof -
   with A1 show "a=b" using group_inv_of_inv by simp
 qed
 
+text\<open>Inverses of different group elements are different.\<close>
+
+lemma (in group0) el_neq_inv_neq: assumes "a\<in>G"  "b\<in>G" "a\<noteq>b"
+  shows "a\<inverse> \<noteq> b\<inverse>"
+proof -
+  { assume "a\<inverse> = b\<inverse>"
+    hence "(a\<inverse>)\<inverse> = (b\<inverse>)\<inverse>" by simp
+    with assms have False using group_inv_of_inv by simp
+  } thus "a\<inverse> \<noteq> b\<inverse>" by auto
+qed
+
 text\<open>If if the inverse of $b$ is different than $a$, then the
   inverse of $a$ is different than $b$.\<close>
 

IsarMathLib/IntGroup_ZF.thy

@@ -199,6 +199,14 @@ text\<open>An integer power of a group element is in the group.\<close>
 lemma (in group_int0) powz_type: assumes "z\<in>\<int>" "x\<in>G" shows "powz(z,x) \<in> G"
   using assms zmagnitude_type monoid.nat_mult_type inverse_in_group by simp
 
+text\<open>A group element raised to (integer) zero'th power is equal to the group's neutral element. 
+  An element raised to (integer) power one is the same element. \<close>
+
+lemma (in group_int0) int_power_zero_one: assumes "x\<in>G"
+  shows "powz(\<zero>,x) = \<one>" and "powz(\<one>\<^sub>Z,x) = x"
+  using assms int0.Int_ZF_1_L8A(1) int0.int_ord_is_refl1 int0.zmag_zero_one 
+    monoid.nat_mult_zero int0.Int_ZF_2_L16A(1) monoid.nat_mult_one by auto
+
 text\<open>If $x$ is an element of the group and $z_1,z_2$ are nonnegative integers then
   $x^{z_1+z_2}=x^{z_1}\cdot x^{z_2}$, i.e. the power homomorphism property holds.\<close>
 
@@ -287,14 +295,6 @@ proof -
     by blast
 qed
 
-text\<open>A group element raised to (integer) zero'th power is equal to the group's neutral element. 
-  An element raised to (integer) power one is the same element. \<close>
-
-lemma (in group_int0) int_power_zero_one: assumes "x\<in>G"
-  shows "powz(\<zero>,x) = \<one>" and "powz(\<one>\<^sub>Z,x) = x"
-  using assms int0.Int_ZF_1_L8A(1) int0.int_ord_is_refl1 int0.zmag_zero_one 
-    monoid.nat_mult_zero int0.Int_ZF_2_L16A(1) monoid.nat_mult_one by auto
-
 text\<open>A group element raised to power $-1$ is the inverse of that group element.\<close>
 
 lemma (in group_int0) inpt_power_neg_one: assumes "x\<in>G"
@@ -310,4 +310,94 @@ lemma (in group_int0) int_power_add_one: assumes "z\<in>\<int>" "x\<in>G"
   using assms int0.Int_ZF_1_L8A(2) powz_hom_prop int_power_zero_one(2)
   by simp
 
+text\<open>For integer power taking a negative of the exponent is the same as taking inverse of the 
+  group element. \<close>
+
+lemma (in group_int0) minus_exp_inv_base: assumes "z\<in>\<int>" "x\<in>G"
+  shows "powz(\<rm>z,x) = powz(z,x\<inverse>)"
+proof -
+  from assms(1) have "\<zero>\<ls>z \<or> z=\<zero> \<or> z\<ls>\<zero>"
+    using int0.int_neg_zero_pos by simp
+  moreover from assms(1) have "\<zero>\<ls>z \<longrightarrow> powz(\<rm>z,x) = powz(z,x\<inverse>)"
+    using int0.neg_pos_int_neg int0.neg_not_nonneg int0.zmag_opposite_same(2) 
+    by simp
+  moreover from assms(2) have "z=\<zero> \<longrightarrow> powz(\<rm>z,x) = powz(z,x\<inverse>)"
+    using int0.Int_ZF_1_L11 int_power_zero_one(1) inverse_in_group by simp
+  moreover from assms have "z\<ls>\<zero> \<longrightarrow> powz(\<rm>z,x) = powz(z,x\<inverse>)"
+    using int0.neg_not_nonneg int0.neg_neg_int_pos group_inv_of_inv 
+        int0.zmag_opposite_same(2) by simp
+  ultimately show "powz(\<rm>z,x) = powz(z,x\<inverse>)" by auto
+qed
+
+text\<open>Integer power of a group element is the same as the inverse of the element
+  raised to negative of the exponent. \<close>
+
+lemma (in group_int0) minus_exp_inv_base1: assumes "z\<in>\<int>" "x\<in>G"
+  shows "powz(z,x) = powz(\<rm>z,x\<inverse>)"
+proof -
+  from assms(1) have "(\<rm>z)\<in>\<int>" using int0.int_neg_type by simp
+  with assms show ?thesis using minus_exp_inv_base int0.neg_neg_noop
+    by force
+qed
+
+text\<open>The next context is like \<open>group_int0\<close> but adds the assumption that the group 
+  operation is commutative (i.e. the group is abelian). \<close>
+
+locale abgroup_int0 = group_int0 +
+  assumes isAbelian: "P {is commutative on} G"
+
+text\<open>In abelian groups taking a nonnegative integer power commutes with the group operation.
+  Unfortunately we have to drop to raw set theory notation in the proof to be able to use 
+  \<open>int0.Induction_on_int\<close> from the \<open>abgroup_int0\<close> context.\<close>
+
+lemma (in abgroup_int0) powz_groupop_commute0: assumes "\<zero>\<lsq>k" "x\<in>G" "y\<in>G"
+  shows "powz(k,x\<cdot>y) = powz(k,x)\<cdot>powz(k,y)"
+proof -
+  from assms(1) have "\<langle>\<zero>,k\<rangle> \<in> IntegerOrder" by simp
+  moreover 
+  from assms(2,3) have "powz(\<zero>,x\<cdot>y) = powz(\<zero>,x)\<cdot>powz(\<zero>,y)"
+    using group_op_closed int_power_zero_one(1) group0_2_L2
+    by simp
+  moreover
+  { fix m assume "\<zero>\<lsq>m" and I: "powz(m,x\<cdot>y) = powz(m,x)\<cdot>powz(m,y)"
+    from assms(2,3) \<open>\<zero>\<lsq>m\<close> have  "m\<in>\<int>" and "x\<cdot>y \<in> G"  
+      using int0.Int_ZF_2_L1A(3) group_op_closed by simp_all
+    with isAbelian assms(2,3) I have "powz(m\<ra>\<one>\<^sub>Z,x\<cdot>y) = powz(m\<ra>\<one>\<^sub>Z,x)\<cdot>powz(m\<ra>\<one>\<^sub>Z,y)"
+      using int_power_add_one group0_4_L8(3) powz_type by simp
+  } hence "\<forall>m. \<zero>\<lsq>m \<and> powz(m,x\<cdot>y) = powz(m,x)\<cdot>powz(m,y) \<longrightarrow>
+     powz(m\<ra>\<one>\<^sub>Z,x\<cdot>y) = powz(m\<ra>\<one>\<^sub>Z,x)\<cdot>powz(m\<ra>\<one>\<^sub>Z,y)" by simp
+  hence "\<forall>m. \<langle>\<zero>, m\<rangle> \<in> IntegerOrder \<and> powz(m,x\<cdot>y) = powz(m,x)\<cdot>powz(m,y) \<longrightarrow> 
+    powz(IntegerAddition`\<langle>m,TheNeutralElement(int,IntegerMultiplication)\<rangle>,x\<cdot>y) = 
+    powz(IntegerAddition`\<langle>m,TheNeutralElement(int,IntegerMultiplication)\<rangle>,x)\<cdot>
+    powz(IntegerAddition`\<langle>m,TheNeutralElement(int,IntegerMultiplication)\<rangle>,y)"
+    by simp
+  ultimately show "powz(k,x\<cdot>y) = powz(k,x)\<cdot>powz(k,y)" by (rule int0.Induction_on_int)
+qed
+
+text\<open>In abelian groups taking a nonpositive integer power commutes with the group operation.
+  We could use backwards induction in the proof but it is shorter to use the nonnegative 
+  case from \<open>powz_groupop_commute0\<close>. \<close>
+
+lemma (in abgroup_int0) powz_groupop_commute1: assumes "k\<lsq>\<zero>" "x\<in>G" "y\<in>G"
+  shows "powz(k,x\<cdot>y) = powz(k,x)\<cdot>powz(k,y)"
+proof -
+  from isAbelian assms have "powz(k,x\<cdot>y) = powz(\<rm>k,x\<inverse>\<cdot>y\<inverse>)"
+    using int0.Int_ZF_2_L1A(2) group_op_closed minus_exp_inv_base1 group_inv_of_two
+    unfolding IsCommutative_def by simp
+  with assms show ?thesis
+    using int0.Int_ZF_2_L10A inverse_in_group powz_groupop_commute0 
+      int0.Int_ZF_2_L1A(2) minus_exp_inv_base1 by simp
+qed
+
+text\<open>In abelian groups taking an integer power commutes with the group operation.\<close>
+
+theorem (in abgroup_int0) powz_groupop_commute: assumes "z\<in>\<int>" "x\<in>G" "y\<in>G"
+  shows "powz(z,x\<cdot>y) = powz(z,x)\<cdot>powz(z,y)"
+proof -
+  from assms(1) have "\<zero>\<lsq>z \<or> z\<lsq>\<zero>" using int0.int_nonneg_or_nonpos
+    by auto
+  with assms(2,3) show ?thesis using powz_groupop_commute0 powz_groupop_commute1
+    by blast
+qed
+
 end

IsarMathLib/Int_ZF_IML.thy

@@ -330,6 +330,16 @@ theorem Int_ZF_1_T2: shows
   using int0.Int_ZF_1_T1 int0.Int_ZF_1_L9 IsAgroup_def
   group0_def int0.Int_ZF_1_L4 IsCommutative_def by auto
 
+text\<open>Negative of an integer is an integer.\<close>
+
+lemma (in int0) int_neg_type: assumes "m\<in>\<int>" shows "(\<rm>m) \<in> \<int>"
+  using assms Int_ZF_1_T2(3) group0.inverse_in_group by simp
+
+text\<open>Taking a negative twice we get back the same integer. \<close>
+
+lemma (in int0) neg_neg_noop: assumes "m\<in>\<int>" shows "(\<rm>(\<rm>m)) = m"
+  using assms Int_ZF_1_T2(3) group0.group_inv_of_inv by simp
+
 text\<open>What is the additive group inverse in the group of integers?\<close>
 
 lemma (in int0) Int_ZF_1_L9A: assumes A1: "m\<in>\<int>" 
@@ -593,12 +603,33 @@ text\<open>Negative numbers are not nonnegative. This is a special case of \<ope
 corollary (in int0) neg_not_nonneg: assumes "m\<ls>\<zero>" shows "\<not>(\<zero>\<lsq>m)"
   using assms ls_not_leq by simp
 
+text\<open>Negative of a positive integer is negative.\<close>
+
+lemma (in int0) neg_pos_int_neg: assumes "\<zero>\<ls>z" shows "(\<rm>z)\<ls>\<zero>"
+  using assms inv_both_strict_ineq Int_ZF_1_L11 by force
+
+text\<open>Negative of a negative integer is positive.\<close>
+
+lemma (in int0) neg_neg_int_pos: assumes "z\<ls>\<zero>" shows "\<zero>\<ls>(\<rm>z)"
+  using assms inv_both_strict_ineq Int_ZF_1_L11 by force
+
 text\<open>An integer is nonnegative or negative. This is a special case of \<open>OrdGroup_2cases\<close>
   from \<open>OrderedGroup_ZF\<close> theory and useful for splitting proofs into cases.\<close>
 
 lemma (in int0) int_nonneg_or_neg: assumes "z\<in>\<int>" shows "\<zero>\<lsq>z \<or> z\<ls>\<zero>"
   using assms OrdGroup_2cases Int_ZF_1_L8A(1) Int_ZF_2_T1(2) by simp
 
+text\<open>Slightly weaker assertion than \<open>int_nonneg_or_neg\<close> with overlap at zero:
+ an integer is nonnegative or nonpositive. \<close>
+
+corollary (in int0) int_nonneg_or_nonpos: assumes "z\<in>\<int>" shows "\<zero>\<lsq>z \<or> z\<lsq>\<zero>"
+  using assms int_nonneg_or_neg by auto
+
+text\<open>Another variant of splitting into cases: an integer is positive, zero or negative.\<close>
+
+lemma (in int0) int_neg_zero_pos: assumes "z\<in>\<int>" shows "\<zero>\<ls>z \<or> z=\<zero> \<or> z\<ls>\<zero>"
+  using assms OrdGroup_3cases Int_ZF_1_L8A(1) Int_ZF_2_T1(2) by auto
+
 text\<open>If a pair $(i,m)$ belongs to the order relation on integers and
   $i\neq m$, then $i$ is smaller that $m$ in the sense of defined in the standard Isabelle's 
   \<open>Int.thy\<close>.\<close>
@@ -910,7 +941,9 @@ proof -
     by simp
 qed
 
-text\<open>Integers greater or equal one are greater or equal zero.\<close>
+text\<open>Assume an integer is greater or equal one. Then it is greater or equal than zero,
+  is not equal zero, if we add one to it then it is greater or equal one, two and zero.  
+  Two is .\<close>
 
 lemma (in int0) Int_ZF_2_L16C: 
   assumes A1: "\<one>\<lsq>a" shows 
@@ -932,6 +965,17 @@ proof -
     Int_ZF_2_L16A Int_ZF_2_L3 int_zero_not_one by auto 
 qed
 
+text\<open>If we add one to a nonnegative integer, the result is greater than zero.\<close>
+
+lemma (in int0) nneg_add_one: assumes "\<zero>\<lsq>a"
+  shows "\<zero>\<ls>a\<ra>\<one>"
+proof -
+  from assms have "\<zero>\<ra>\<zero> \<ls> a\<ra>\<one>"
+    using Int_ZF_2_L16A(2) OrderedGroup_ZF_1_L12D by simp
+  then show "\<zero>\<ls>a\<ra>\<one>" using OrderedGroup_ZF_1_L1 group0.group0_2_L2
+    by simp
+qed
+
 text\<open>Absolute value is the same for an integer and its opposite.\<close>
 
 lemma (in int0) Int_ZF_2_L17: 

IsarMathLib/OrderedGroup_ZF.thy

@@ -1,7 +1,7 @@
 (*    This file is a part of IsarMathLib - 
     a library of formalized mathematics for Isabelle/Isar.
 
-    Copyright (C) 2005, 2006  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 following conditions are met:
@@ -351,7 +351,18 @@ proof -
     group0.group0_2_L6 by simp
 qed
 
-text\<open>If an element is nonnegative, then its inverse is less or equal than the unit.\<close>
+text\<open>Taking the inverse on both sides reverses the strict inequality.\<close>
+
+lemma (in group3) inv_both_strict_ineq:
+  assumes "a\<ls>b" shows "b\<inverse>\<ls>a\<inverse>"
+proof -
+  from assms have "b\<inverse>\<lsq>a\<inverse>" using OrderedGroup_ZF_1_L5 by simp
+  from assms have "a\<in>G" "b\<in>G" "a\<noteq>b" using less_are_members by simp_all
+  with \<open>b\<inverse>\<lsq>a\<inverse>\<close> show "b\<inverse>\<ls>a\<inverse>"
+    using OrderedGroup_ZF_1_L1 group0.el_neq_inv_neq by auto
+qed
+
+text\<open>If an element is less or equal than the unit, then its inverse is nonnegative.\<close>
 
 lemma (in group3) OrderedGroup_ZF_1_L5A: 
   assumes A1: "a\<lsq>\<one>" shows "\<one>\<lsq>a\<inverse>"
@@ -730,12 +741,19 @@ proof -
 qed
 
 text\<open>If $a,b$ are an elements of an ordered group where the order is total, then
-  $a\leq b$ or $b<a$.  \<close>
+  $a\leq b$ or $b < a$.  \<close>
 
 lemma (in group3) OrdGroup_2cases: assumes "r {is total on} G" "a\<in>G"  "b\<in>G"
   shows "a\<lsq>b \<or> b\<ls>a"
   using assms IsTotal_def by auto
 
+text\<open>If $a,b$ are an elements of an ordered group where the order is total, then
+  $a < b$ or $a=b$ or $b\leq a$. \<close>
+
+lemma (in group3) OrdGroup_3cases: assumes "r {is total on} G" "a\<in>G"  "b\<in>G"
+  shows "a\<ls>b \<or> a=b \<or> b\<ls>a"
+  using assms assms IsTotal_def by auto
+
 text\<open>A lemma about splitting the ordered group "plane" into 6 subsets. Useful
   for proofs by cases.\<close>