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 generator_pow_mult_order: "❙g [^] (order G * order G) = 𝟭"
  using generator_pow_order 
  by (metis generator_closed nat_pow_one nat_pow_pow)

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 pow_carrier_mod: 
  assumes "g ∈ carrier G"
  shows "g [^] (k mod order G) = g [^] k"
  using assms pow_generator_mod 
  by (metis generatorE generator_closed mod_mult_right_eq nat_pow_pow)

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 = 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)" 
    apply(subst n)apply(simp add: int_pow_mult int_pow_pow mult_ac)
    by (metis generator_closed int_pow_int int_pow_pow mult.commute)
  then show ?thesis by(simp add: generator_pow_order)
qed simp

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

lemma power_distrib: 
  assumes "h ∈ carrier G" 
  shows "❙g [^] (e :: nat) ⊗ h [^] e = (❙g ⊗ h ) [^] e"
(is "?lhs = ?rhs")
proof-
  obtain x :: nat where x: "h = ❙g [^] x" 
    using assms generatorE by blast
  hence "?lhs = ❙g [^] (e * (1 + x))" 
    by (simp add: nat_pow_mult mult.commute nat_pow_pow)
  also have "... = (❙g [^] (1 + x)) [^] e" 
    by (metis generator_closed mult.commute nat_pow_pow)
  ultimately show ?thesis 
    by (metis x One_nat_def generator_closed l_one monoid.nat_pow_Suc monoid_axioms nat_pow_0 nat_pow_mult)
qed

lemma neg_power_inverse:
  assumes "g ∈ carrier G" 
    and "x < order G"
  shows "g [^] (order G - (x :: nat)) = inv (g [^] x)"
proof-
  have "inv (g [^] x) = g [^] (- int x)"  
    by (simp add: int_pow_int int_pow_neg assms)
  moreover have "g [^] (order G - (x :: nat)) = g [^] (- int x)"
  proof-
    have "g [^] ((order G - (x :: nat)) mod (order G)) = g [^] ((- int x) mod (order G))" 
    proof-
      have "(order G - (x :: nat)) mod (order G) = (- int x) mod (order G)" 
        using assms(2) zmod_zminus1_eq_if by auto
      thus ?thesis 
        by (metis int_pow_int)
    qed
    thus ?thesis 
    proof -
      have f1: "∀a. a [^] int 0 = 𝟭"
        by simp
      have f2: "∀n na. ((na::nat) + n) mod na = n mod na"
        by simp
        have f3: "∀a aa. aa ⊗ a [^] int 0 = aa ∨ aa ∉ carrier G"
          by force
        have f4: "∀i a aa. a [^] int 0 ⊗ aa [^] i = aa [^] (int 0 + i) ∨ aa ∉ carrier G"
          by force
        have "∀n a. a [^] int (n * 0) = a [^] (int 0 + int 0) ∨ a ∉ carrier G"
          by simp
        then have f5: "∀a aa. aa [^] int (order G) = a [^] int 0 ∨ aa ∉ carrier G"
          using f4 f3 f2 f1 by (metis int_pow_closed int_pow_int mod_mult_self2 pow_carrier_mod)
        have "∀n na. int (n - na) = - int na + int n ∨ ¬ na ≤ n"
          by auto
        then show ?thesis
          using f5 f3 by (metis assms(1) assms(2) int_pow_closed int_pow_int int_pow_mult less_imp_le_nat)
      qed
    qed
  ultimately show ?thesis by simp
qed

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_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 1: "(❙g [^] (a::nat) ⊗ ❙g [^] (b::nat)) [^] ((c::int)*int (d::nat)) = (❙g [^] n) [^] r" using n r by simp
  also have 2:"... = (❙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)
  also have 3:"... =  (❙g [^] a ⊗ ❙g [^] b) [^] ((c*int d) mod (order G))" using r n by simp
  ultimately show ?thesis using 1 2 3 by simp
qed

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 inj_onD inj_on_generator lessThan_iff g_pow_eq_1 assms less_one neq0_conv)
  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

lemma gen_power_0:
  fixes r :: nat 
  assumes "❙g [^] r = 𝟭" 
    and "r < order G"
  shows "r = 0" 
  using assms inj_onD inj_on_generator by fastforce

lemma group_eq_pow_eq_mod: 
  fixes a b :: nat 
  assumes "❙g [^] a = ❙g [^] b" 
    and "order G > 0"
  shows "[a = b] (mod order G)"
proof(cases "a > b")
  case True
  have "❙g [^] a ⊗ inv (❙g [^] b) = 𝟭"
    using assms by simp
  hence "❙g [^] (a - b) = 𝟭" 
    by (smt True add_Suc_right assms diff_add_inverse generator_closed group.l_cancel_one' group_l_invI l_inv_ex less_imp_Suc_add nat_pow_closed nat_pow_mult)
  hence "❙g [^] ((a - b) mod (order G)) = 𝟭" using pow_generator_mod by auto
  thus ?thesis using gen_power_0 
    using assms(1) assms(2) order_gt_0_iff_finite pow_generator_eq_iff_cong by blast
next
  case False
  have "❙g [^] a ⊗ inv (❙g [^] b) = 𝟭"
    using assms by simp
  hence "❙g [^] (b - a) = 𝟭" 
    by (metis (no_types, lifting) False Group.group.axioms(1) Units_eq add_diff_inverse_nat assms(1) generator_closed group_l_invI l_inv_ex l_neq_1_exp_neq_0 monoid.Units_l_cancel nat_pow_closed nat_pow_mult r_one)
  hence "❙g [^] ((b - a) mod (order G)) = 𝟭" using pow_generator_mod by simp
  thus ?thesis using gen_power_0 
    using assms(1) assms(2) order_gt_0_iff_finite pow_generator_eq_iff_cong by blast
qed


end 

end