more properties of integer powers of group elements

IsarMathLib/IntGroup_ZF.thy

@@ -119,7 +119,7 @@ text\<open>If $k\leq n$ are natural numbers and $x$ an element of the group, the
 lemma (in group0) nat_pow_cancel_more: assumes "n\<in>nat" "k\<le>n" "x\<in>G"
   shows "pow(k,x\<inverse>)\<cdot>pow(n,x) = pow(n #- k,x)"
 proof -
-  from assms have 
+  from assms have
     "k\<in>nat" "n #- k \<in> nat" "pow((n #- k),x) \<in> G" "pow(k,x) \<in> G" "pow(k,x\<inverse>) \<in> G"
     using leq_nat_is_nat diff_type monoid.nat_mult_type inverse_in_group 
       by simp_all
@@ -157,7 +157,8 @@ text\<open>We extend the \<open>group0\<close> context with some notation from \
   that we can use to convert one into the other. 
   Hence, we define the integer power \<open>powz(z,x)\<close> as $x$ raised to the corresponding
   natural power if $z$ is a nonnegative and  $x^{-1}$ raised to natural power corresponding
-  to $-z$ otherwise.   \<close>
+  to $-z$ otherwise. Since we inherit the multiplicative notation from the \<open>group0\<close> context
+  the integer "one" is denoted \<open>\<one>\<^sub>Z\<close> rather than just \<open>\<one>\<close> (which is the group's neutral element). \<close>
 
 locale group_int0 = group0 +
 
@@ -176,6 +177,9 @@ locale group_int0 = group0 +
   fixes izero ("\<zero>")
   defines izero_def [simp]: "\<zero> \<equiv> TheNeutralElement(\<int>,IntegerAddition)"
 
+  fixes ione ("\<one>\<^sub>Z")
+  defines ione_def [simp]: "\<one>\<^sub>Z \<equiv> TheNeutralElement(\<int>,IntegerMultiplication)"
+
   fixes nonnegative ("\<int>\<^sup>+")
   defines nonnegative_def [simp]: 
     "\<int>\<^sup>+ \<equiv> Nonnegative(\<int>,IntegerAddition,IntegerOrder)"
@@ -279,4 +283,27 @@ 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"
+  shows "powz(\<rm>\<one>\<^sub>Z,x) = x\<inverse>"
+  using assms int0.neg_not_nonneg int0.neg_one_less_zero int0.zmag_opposite_same(2) 
+    int0.Int_ZF_1_L8A(2) int0.zmag_zero_one(2) inverse_in_group monoid.nat_mult_one 
+  by simp
+
+text\<open>Increasing the (integer) power by one is the same as multiplying by the group element.\<close>
+
+lemma (in group_int0) int_power_add_one: assumes "z\<in>\<int>" "x\<in>G"
+  shows "powz(z\<ra>\<one>\<^sub>Z,x) = powz(z,x)\<cdot>x"
+  using assms int0.Int_ZF_1_L8A(2) powz_hom_prop int_power_zero_one(2)
+  by simp
+
 end

IsarMathLib/Int_ZF_IML.thy

@@ -470,6 +470,12 @@ text\<open>The order on integers is reflexive.\<close>
 lemma (in int0) int_ord_is_refl: shows "refl(\<int>,IntegerOrder)"
   using Int_ZF_2_L1 zle_refl refl_def by auto
 
+text\<open>A more explicit version of "integer order is reflexive" claim\<close>
+
+lemma (in int0) int_ord_is_refl1: assumes "z\<in>\<int>"
+  shows "z\<lsq>z"
+  using assms int_ord_is_refl unfolding refl_def by simp
+
 text\<open>The essential condition to show antisymmetry of the order on integers.\<close>
 
 lemma (in int0) Int_ZF_2_L3: 
@@ -876,17 +882,24 @@ lemma (in int0) Int_ZF_2_L16:
 
 text\<open>$0\leq 1$, so $|1| = 1$.\<close>
 
-lemma (in int0) Int_ZF_2_L16A: shows "\<zero>\<lsq>\<one>" and "abs(\<one>) = \<one>"
+lemma (in int0) Int_ZF_2_L16A: 
+  shows "\<zero>\<lsq>\<one>" "\<zero>\<ls>\<one>" "abs(\<one>) = \<one>"
 proof -
   have "($# 0) \<in> \<int>" "($# 1)\<in> \<int>" by auto
   then have "\<zero>\<lsq>\<zero>" and T1: "\<one>\<in>\<int>" 
     using Int_ZF_1_L8 int_ord_is_refl refl_def by auto
   then have "\<zero>\<lsq>\<zero>\<ra>\<one>" using Int_ZF_2_L12A by simp
   with T1 show "\<zero>\<lsq>\<one>" using Int_ZF_1_T2 group0.group0_2_L2
     by simp
-  then show "abs(\<one>) = \<one>" using Int_ZF_2_L16 by simp
+  then show "abs(\<one>) = \<one>" and "\<zero>\<ls>\<one>" 
+    using Int_ZF_2_L16 int_zero_not_one by simp_all
 qed
 
+text\<open>Negative one is smaller than zero.\<close>
+
+lemma (in int0) neg_one_less_zero: shows "(\<rm>\<one>)\<ls>\<zero>"
+  using Int_ZF_2_L16A(2) pos_inv_neg by simp
+
 text\<open>$1\leq 2$.\<close>
 
 lemma (in int0) Int_ZF_2_L16B: shows "\<one>\<lsq>\<two>"
@@ -1514,16 +1527,32 @@ text\<open>The next lemma shows that \<open>zmagnitude\<close> of an integer is
   of its opposite. \<close>
 
 lemma (in int0) zmag_opposite_same: assumes "z\<in>\<int>" 
-  shows "zmagnitude(z) = zmagnitude($-z)"
+  shows 
+    "zmagnitude(z) = zmagnitude($-z)"
+    "zmagnitude(z) = zmagnitude(\<rm>z)"
 proof -
   from assms obtain n where "n\<in>nat" and "z=$#n \<or> z=$-($# succ(n))"
     using int_cases by auto
-  then show ?thesis using zmagnitude_int_of zmagnitude_zminus_int_of
+  then show "zmagnitude(z) = zmagnitude($-z)" using zmagnitude_int_of 
     by auto
+  with assms show "zmagnitude(z) = zmagnitude(\<rm>z)" using Int_ZF_1_L9A
+    by simp
+qed
+
+text\<open>The magnitude of zero (the integer) is zero (the natural number)
+  and the magnitude of one (the integer) is one (the natural number).\<close>
+
+lemma (in int0) zmag_zero_one: shows "zmagnitude(\<zero>) = 0" and "zmagnitude(\<one>) = 1"
+proof -
+  have "zmagnitude(\<zero>) = zmagnitude($#0)" and "zmagnitude(\<one>) = zmagnitude($#1)" 
+    using Int_ZF_1_L8 by simp_all
+  then show "zmagnitude(\<zero>) = 0" and "zmagnitude(\<one>) = 1" using zmagnitude_int_of
+    by simp_all
 qed
 
 text\<open>If $z_1,z_1$ is a pair of integers then (at least) one of the following six cases holds:
   
+  
   1. Both integers are nonnegative.
 
   2. Both integers are negative.

IsarMathLib/OrderedGroup_ZF.thy

@@ -351,7 +351,7 @@ proof -
     group0.group0_2_L6 by simp
 qed
 
-text\<open>If an element is smaller that the unit, then its inverse is greater.\<close>
+text\<open>If an element is nonnegative, then its inverse is less or equal than the unit.\<close>
 
 lemma (in group3) OrderedGroup_ZF_1_L5A: 
   assumes A1: "a\<lsq>\<one>" shows "\<one>\<lsq>a\<inverse>"
@@ -393,6 +393,18 @@ proof -
   } then show "\<not>(a\<lsq>\<one> \<and> a\<noteq>\<one>)" by auto
 qed
 
+text\<open>If an element is positive, then its inverse is negative.\<close>
+
+lemma (in group3) pos_inv_neg: assumes  "\<one>\<ls>a"
+  shows "a\<inverse>\<ls>\<one>"
+proof -
+  from assms have "a\<in>G" and "a\<noteq>\<one>"
+    using less_are_members(2) by auto
+  with assms show "a\<inverse>\<ls>\<one>"
+    using OrderedGroup_ZF_1_L1 group0.group0_2_L8B OrderedGroup_ZF_1_L5AB(1)
+    by simp
+qed
+
 text\<open>If two elements are greater or equal than the unit, then the inverse
   of one is not greater than the other.\<close>
 

isar2html2.0/isarhtml/index.html

@@ -187,7 +187,7 @@ <h3>About this site</h3>
 
 <p><a href="Int_ZF_3.html">Int_ZF_3</a></p>
 
-<p><a href="IntGroup_ZF.html">Int_ZF_3</a></p>
+<p><a href="IntGroup_ZF.html">IntGroup_ZF</a></p>
 
 <p><a href="Real_ZF.html">Real_ZF</a></p>