Theory Cyclic_Group_Ext

theory Cyclic_Group_Ext imports
  CryptHOL.CryptHOL
  "HOL-Number_Theory.Cong"
begin

context cyclic_group begin

lemma generator_pow_order: "❙g [^] order G = 𝟭"
proof(cases "order G > 0")
  case True
  hence fin: "finite (carrier G)" by(simp add: order_gt_0_iff_finite)
  then have [symmetric]: "(λx. x ⊗ ❙g) ` carrier G = carrier G"
    by(rule endo_inj_surj)(auto simp add: inj_on_multc)
  then have "carrier G = (λ n. ❙g [^] Suc n) ` {..<order G}" 
    using fin by(simp add: carrier_conv_generator image_image)
  then obtain n where n: "𝟭 = ❙g [^] Suc n" "n < order G" by auto
  have "n = order G - 1" using n inj_onD[OF inj_on_generator, of 0 "Suc n"] by fastforce
  with True n show ?thesis by auto
qed simp
                        
lemma pow_generator_mod: "❙g [^] (k mod order G) = ❙g [^] k"
proof(cases "order G > 0")
  case True
  obtain n where n: "k = n * order G + k mod order G" by (metis div_mult_mod_eq)
  have "❙g [^] k = (❙g [^] order G) [^] n ⊗ ❙g [^] (k mod order G)" 
    by(subst n)(simp add: nat_pow_mult nat_pow_pow mult_ac)
  then show ?thesis by(simp add: generator_pow_order)
qed simp

lemma int_nat_pow: 
  assumes "a ≥ 0" 
  shows "(❙g [^] (int (a ::nat))) [^] (b::int)  = ❙g [^] (a*b)"
  using assms 
proof(cases "a > 0")
  case True 
  show ?thesis
    using int_pow_pow by blast
next case False
  have "(❙g [^] (int (a ::nat))) [^] (b::int) = 𝟭" using False by simp
  also have "❙g [^] (a*b) = 𝟭" using False by simp
  ultimately show ?thesis by simp
qed

lemma pow_generator_mod_int: "❙g [^] ((k :: int) mod order G) = ❙g [^] k"
proof(cases "order G > 0")
  case True
  obtain n :: int where n: "k = order G * n + k mod order G" 
    by (metis div_mult_mod_eq mult.commute)
  then have "❙g [^] k = ❙g [^] (order G * n) ⊗ ❙g [^] (k mod order G)" 
    using int_pow_mult nat_pow_mult by (metis generator_closed)
  then have "❙g [^] k = (❙g [^] order G) [^] n ⊗ ❙g [^] (k mod order G)"
    using int_nat_pow by (simp add: int_pow_int)
  then show ?thesis by(simp add: generator_pow_order)
qed simp

lemma pow_gen_mod_mult:
  shows"(❙g [^] (a::nat) ⊗ ❙g [^] (b::nat)) [^] ((c::int)* int (d::nat)) = (❙g [^] a ⊗ ❙g [^] b) [^] ((c*int d) mod (order G))"
proof-
  have "(❙g [^] (a::nat) ⊗ ❙g [^] (b::nat)) ∈ carrier G" by simp
  then obtain n :: nat where n: "❙g [^] n = (❙g [^] (a::nat) ⊗ ❙g [^] (b::nat))" 
    by (simp add: monoid.nat_pow_mult)
  also obtain r where r: "r = c*int d" by simp
  have "(❙g [^] (a::nat) ⊗ ❙g [^] (b::nat)) [^] ((c::int)*int (d::nat)) = (❙g [^] n) [^] r" using n r by simp
  moreover have"... = (❙g [^] n) [^] (r mod (order G))" using pow_generator_mod_int pow_generator_mod 
    by (metis int_nat_pow int_pow_int mod_mult_right_eq zero_le)
  moreover have "... =  (❙g [^] a ⊗ ❙g [^] b) [^] ((c*int d) mod (order G))" using r n by simp
  ultimately show ?thesis by simp
qed

lemma pow_generator_eq_iff_cong:
  "finite (carrier G) ⟹ ❙g [^] x = ❙g [^] y ⟷ [x = y] (mod order G)"
  by(subst (1 2) pow_generator_mod[symmetric])(auto simp add: cong_def order_gt_0_iff_finite intro: inj_onD[OF inj_on_generator])

lemma cyclic_group_commute: 
  assumes "a ∈ carrier G" "b ∈ carrier G" 
  shows "a ⊗ b = b ⊗ a"
(is "?lhs = ?rhs")
proof-
  obtain n :: nat where n: "a = ❙g [^] n" using generatorE assms by auto
  also  obtain k :: nat where k: "b = ❙g [^] k" using generatorE assms by auto
  ultimately have "?lhs =  ❙g [^] n ⊗ ❙g [^] k" by simp
  then have "... = ❙g [^] (n + k)" by(simp add: nat_pow_mult)
  then have "... = ❙g [^] (k + n)" by(simp add: add.commute)
  then show ?thesis by(simp add: nat_pow_mult n k)
qed

lemma cyclic_group_assoc: 
  assumes "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
  shows "(a ⊗ b) ⊗ c = a ⊗ (b ⊗ c)"
(is "?lhs = ?rhs")
proof-
  obtain n :: nat where n: "a = ❙g [^] n" using generatorE assms by auto
  obtain k :: nat where k: "b = ❙g [^] k" using generatorE assms by auto
  obtain j :: nat where j: "c = ❙g [^] j" using generatorE assms by auto 
  have "?lhs = (❙g [^] n ⊗ ❙g [^] k) ⊗ ❙g [^] j" using n k j by simp
  then have "... = ❙g [^] (n + (k + j))" by(simp add: nat_pow_mult add.assoc)
  then show ?thesis by(simp add: nat_pow_mult n k j)
qed
 
lemma l_cancel_inv: 
  assumes "h ∈ carrier G" 
  shows "(❙g [^] (a :: nat) ⊗ inv (❙g [^] a)) ⊗ h = h"
(is "?lhs = ?rhs")
proof-
  have "?lhs = (❙g [^] int a ⊗ inv (❙g [^] int a)) ⊗ h" by simp
  then have "... = (❙g [^] int a ⊗ (❙g [^] (- a))) ⊗ h" using int_pow_neg[symmetric] by simp
  then have "... = ❙g [^] (int a - a)  ⊗ h" by(simp add: int_pow_mult)
  then have "... = ❙g [^] ((0:: int)) ⊗ h" by simp
  then show ?thesis by (simp add: assms)
qed

lemma inverse_split: 
  assumes "a ∈ carrier G" and "b ∈ carrier G"
  shows "inv (a ⊗ b) = inv a ⊗ inv b"
  by (simp add:  assms comm_group.inv_mult cyclic_group_commute group_comm_groupI)

lemma inverse_pow_pow:
  assumes "a ∈ carrier G"
  shows "inv (a [^] (r::nat)) = (inv a) [^] r"
proof -
  have "a [^] r ∈ carrier G"
    using assms by blast
  then show ?thesis
    by (simp add: assms nat_pow_inv)
qed

lemma l_neq_1_exp_neq_0:
  assumes "l ∈ carrier G" 
    and "l ≠ 𝟭" 
    and "l = ❙g [^] (t::nat)" 
  shows "t ≠ 0"
proof(rule ccontr)
  assume "¬ (t ≠ 0)"
  hence "t = 0" by simp
  hence "❙g [^] t = 𝟭" by simp
  then show "False" using assms by simp
qed

lemma order_gt_1_gen_not_1:
  assumes "order G > 1"
  shows "❙g ≠ 𝟭"
proof(rule ccontr)
  assume "¬ ❙g ≠ 𝟭"
  hence "❙g = 𝟭" by simp
  hence g_pow_eq_1: "❙g [^] n = 𝟭" for n :: nat by simp
  hence "range (λn :: nat. ❙g [^] n) = {𝟭}" by auto
  hence "carrier G ⊆ {𝟭}" using generator by auto
  hence "order G < 1" 
    by (metis One_nat_def assms g_pow_eq_1 inj_onD inj_on_generator lessThan_iff not_gr_zero zero_less_Suc)
  with assms show "False" by simp
qed

lemma power_swap: "((❙g [^] (α0::nat)) [^] (r::nat)) = ((❙g [^] r) [^] α0)"
(is "?lhs = ?rhs")
proof-
  have "?lhs = ❙g [^] (α0 * r)" 
    using nat_pow_pow mult.commute by auto
  hence "... = ❙g [^] (r * α0)" 
    by(metis mult.commute)
  thus ?thesis using nat_pow_pow by auto
qed

end 

end