Theory Primitives

theory Primitives

imports Pairing  
begin

section ‹Mathematical Primitives›

text ‹We define the mathematical primitives used throughout our formalization as well as some
useful lemmas (mostly identities).›
locale math_primitives = pairing G⇩p  G⇩T p e
  for G⇩p :: "('a, 'b) cyclic_group_scheme" (structure)
  and G⇩T:: "('c, 'd) cyclic_group_scheme"  (structure)
  and p::int
  and e::"'a ⇒ 'a ⇒ 'c"
+ 
fixes "type_q" :: "('q :: prime_card) itself"
and max_deg::nat
assumes
p_gr_two: "p > 2" and
d_pos: "max_deg > 0" and
CARD_q: "int (CARD('q)) = p" and
d_l_p: "max_deg < p"
begin

abbreviation pow_mod_ring (infixr "^ı" 75)
  where "x ^ı y ≡  x [^]ı (to_int_mod_ring (y::'q mod_ring))"

abbreviation div_in_grp (infixr "÷ı" 70)
  where "x ÷ı y ≡ x ⊗ı invı y"

subsubsection ‹mod\_ring operations on pow of Gp›

lemma carrier_pow_mod_order_G⇩p: 
  assumes "g ∈ carrier G⇩p"
  shows "g [^]⇘G⇩p⇙ x = g [^]⇘G⇩p⇙ (x mod p)"
proof -
  have "p=(order G⇩p)" by (simp add: CARD_G⇩p)
  also have "g [^]⇘G⇩p⇙ x = g [^]⇘G⇩p⇙ (x mod order G⇩p)"
  proof -
    have "g [^]⇘G⇩p⇙ x ∈ carrier G⇩p" by (simp add: assms)
    let ?d = "x div (order G⇩p)"
    have "g [^]⇘G⇩p⇙ x = g [^]⇘G⇩p⇙ (?d * order G⇩p + x mod order G⇩p)" 
      using div_mult_mod_eq by presburger
    also have "…= g [^]⇘G⇩p⇙ (?d * order G⇩p) ⊗⇘G⇩p⇙  g [^]⇘G⇩p⇙ (x mod order G⇩p)"
      using G⇩p.int_pow_mult assms by blast
    also have "…=𝟭⇘G⇩p⇙ ⊗⇘G⇩p⇙ g [^]⇘G⇩p⇙ (x mod order G⇩p)"
      by (metis G⇩p.int_pow_closed G⇩p.int_pow_pow G⇩p.pow_order_eq_1 assms int_pow_int)
    finally show "g [^]⇘G⇩p⇙ x = g [^]⇘G⇩p⇙ (x mod order G⇩p)"
      using assms by fastforce
  qed
  finally show "g [^]⇘G⇩p⇙ x = g [^]⇘G⇩p⇙ (x mod p)" .
qed

lemma pow_mod_order_G⇩p: "❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ x = ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (x mod p)"
  using carrier_pow_mod_order_G⇩p by blast

lemma mod_ring_pow_mult_inv_G⇩p[symmetric]:" (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring (a::'q mod_ring))) ⊗⇘G⇩p⇙ inv⇘G⇩p⇙ (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring b)) 
  =  ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring (a-b))"
proof -
  have "(❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring (a::'q mod_ring))) ⊗⇘G⇩p⇙ inv⇘G⇩p⇙ (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring b)) 
        = (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring (a::'q mod_ring))) ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (- to_int_mod_ring b))"
    by (simp add: G⇩p.int_pow_neg)
  also have "…=(❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ ((to_int_mod_ring a + -to_int_mod_ring b) mod CARD ('q)))"
    using pow_mod_order_G⇩p CARD_q G⇩p.generator_closed G⇩p.int_pow_mult by presburger
  also have "…=(❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ ((to_int_mod_ring a - to_int_mod_ring b) mod CARD ('q)))"
    by fastforce
  also have "…=  ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring (a - b)"
    by (simp add: minus_mod_ring.rep_eq to_int_mod_ring.rep_eq)
  finally show "❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring a ⊗⇘G⇩p⇙ inv⇘G⇩p⇙ (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring b) = ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring (a - b)" .
qed

lemma mod_ring_pow_mult_G⇩p[symmetric]:" (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring (a::'q mod_ring))) ⊗⇘G⇩p⇙ (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring b)) 
  =  ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring (a+b))"
proof -
  have "❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring a ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring b =  ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring a + to_int_mod_ring b)"
    by (simp add: G⇩p.int_pow_mult)
  also have "…=  ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ ((to_int_mod_ring a + to_int_mod_ring b) mod (CARD ('q)))" 
    using pow_mod_order_G⇩p CARD_q by blast
  also have "…=  ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring (a + b)"
    by (simp add: plus_mod_ring.rep_eq to_int_mod_ring.rep_eq)
  finally show "❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring a ⊗⇘G⇩p⇙ ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring b = ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring (a + b)" .
qed

lemma mod_ring_pow_pow_G⇩p[symmetric]: "(❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring (a::'q mod_ring))) [^]⇘G⇩p⇙ (to_int_mod_ring (b::'q mod_ring)) 
                       = ❙g⇘G⇩p⇙[^]⇘G⇩p⇙ (to_int_mod_ring (a*b::'q mod_ring))"
proof -
  have "(❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring a) [^]⇘G⇩p⇙ to_int_mod_ring b = (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ (to_int_mod_ring a * to_int_mod_ring b))"
    using G⇩p.int_pow_pow by auto
  also have "… = (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ ((to_int_mod_ring a * to_int_mod_ring b) mod CARD ('q)))"
    using CARD_q pow_mod_order_G⇩p by blast
  also have "…=  ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring (a * b)"
    by (simp add: times_mod_ring.rep_eq to_int_mod_ring.rep_eq)
  finally show "(❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring a) [^]⇘G⇩p⇙ to_int_mod_ring b 
               = ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring (a * b)" .
qed

lemma to_int_mod_ring_ge_0: "to_int_mod_ring x ≥ 0" 
  using range_to_int_mod_ring by fastforce

lemma pow_on_eq_card: "(❙g⇘G⇩p⇙ ^⇘G⇩p⇙ x = ❙g⇘G⇩p⇙ ^⇘G⇩p⇙ y) = (x=y)"
proof 
  assume assm: "❙g ^⇘G⇩p⇙ x = ❙g ^⇘G⇩p⇙ y"
  then have "❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring x = ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ to_int_mod_ring y"
    using assm by blast
  then have "❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ nat (to_int_mod_ring x) = ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ nat (to_int_mod_ring y)" 
    using to_int_mod_ring_ge_0[of "x"] to_int_mod_ring_ge_0[of "y"] by fastforce
  then have "[nat (to_int_mod_ring x) = nat (to_int_mod_ring y)] (mod order G⇩p)"
    using G⇩p.pow_generator_eq_iff_cong G⇩p.finite_carrier by fast
  then have "[to_int_mod_ring x = to_int_mod_ring y] (mod order G⇩p)" 
    using to_int_mod_ring_ge_0[of "x"] to_int_mod_ring_ge_0[of "y"]
    by (metis cong_int_iff int_nat_eq)
  then have "[to_int_mod_ring x = to_int_mod_ring y] (mod p)" 
    using CARD_G⇩p by fast
  then have "to_int_mod_ring x = to_int_mod_ring y"
    by (metis Rep_mod_ring_mod to_int_mod_ring.rep_eq unique_euclidean_semiring_class.cong_def 
        CARD_q)
  then show "x = y" by force
next 
  assume "x = y"
  then show "❙g ^⇘G⇩p⇙ x = ❙g ^⇘G⇩p⇙ y" by fast
qed

lemma g_pow_to_int_mod_ring_of_int_mod_ring: " ❙g ^⇘G⇩p⇙ of_int_mod_ring x =  ❙g [^] x"
proof -
  have "❙g ^⇘G⇩p⇙ of_int_mod_ring x =  ❙g [^] (x mod p)"
    by (simp add: CARD_q of_int_mod_ring.rep_eq to_int_mod_ring.rep_eq)
  also have "…= ❙g [^] x" using CARD_G⇩p G⇩p.pow_generator_mod_int by presburger
  finally show ?thesis .
qed

lemma g_pow_to_int_mod_ring_of_int_mod_ring_pow_t: "❙g ^⇘G⇩p⇙ of_int_mod_ring x ^ (t::nat) =  ❙g [^] x ^ t"
  by (metis g_pow_to_int_mod_ring_of_int_mod_ring of_int_of_int_mod_ring of_int_power)

lemma carrier_inj_on_multc: "c ≠ 0 ⟹ inj_on (λx. x ^⇘G⇩p⇙ c) (carrier G⇩p)"
proof 
  fix x y
  assume c: "c ≠ 0"
  assume x: " x ∈ carrier G⇩p"
  assume y: " y ∈ carrier G⇩p"
  assume asm: "x ^ c = y ^ c"
  obtain x_pow where x_pow: "❙g ^⇘G⇩p⇙ x_pow = x"
    using x 
    by (metis G⇩p.generatorE g_pow_to_int_mod_ring_of_int_mod_ring int_pow_int)
  obtain y_pow where y_pow: "❙g ^⇘G⇩p⇙ y_pow = y"
    using y 
    by (metis G⇩p.generatorE g_pow_to_int_mod_ring_of_int_mod_ring int_pow_int)
  then have "(❙g ^⇘G⇩p⇙ x_pow) ^⇘G⇩p⇙ c = (❙g ^⇘G⇩p⇙ y_pow) ^⇘G⇩p⇙ c"
    using asm x_pow y_pow by blast
  then have "(❙g ^⇘G⇩p⇙ (x_pow*c))= (❙g ^⇘G⇩p⇙ (y_pow*c))"
    using mod_ring_pow_pow_G⇩p by presburger
  then have "x_pow * c = y_pow*c"
    using pow_on_eq_card by force
  then have "x_pow = y_pow"
    using c by simp
  then show "x=y"
    using x_pow y_pow by blast
qed

subsubsection‹mod\_ring operations on pow of GT›

lemma pow_mod_order_G⇩T: "g ∈ carrier G⇩T ⟹ g [^]⇘G⇩T⇙ x = g [^]⇘G⇩T⇙ (x mod p)" 
proof -
  assume asmpt: "g ∈ carrier G⇩T"
  have "p=(order G⇩T)" by (simp add: CARD_G⇩T)
  also have "g[^]⇘G⇩T⇙ x = g [^]⇘G⇩T⇙ (x mod order G⇩T)"
  proof -
    have "g [^]⇘G⇩T⇙ x ∈ carrier G⇩T" using asmpt by simp
    let ?d = "x div (order G⇩T)"
    have "g [^]⇘G⇩T⇙ x = g [^]⇘G⇩T⇙ (?d * order G⇩T + x mod order G⇩T)" 
      using div_mult_mod_eq by presburger
    also have "…=g [^]⇘G⇩T⇙ (?d * order G⇩T) ⊗⇘G⇩T⇙  g [^]⇘G⇩T⇙ (x mod order G⇩T)"
      using G⇩T.int_pow_mult asmpt by fast
    also have "…=𝟭⇘G⇩T⇙ ⊗⇘G⇩T⇙ g [^]⇘G⇩T⇙ (x mod order G⇩T)"
      by (metis G⇩T.int_pow_one G⇩T.int_pow_pow G⇩T.pow_order_eq_1 int_pow_int mult.commute asmpt)
    finally show "g [^]⇘G⇩T⇙ x = g [^]⇘G⇩T⇙ (x mod order G⇩T)"
      using asmpt by fastforce
  qed
  finally show "g [^]⇘G⇩T⇙ x = g [^]⇘G⇩T⇙ (x mod p)" .
qed


lemma mod_ring_pow_mult_G⇩T[symmetric]:" x ∈ carrier G⇩T ⟹ (x [^]⇘G⇩T⇙ (to_int_mod_ring (a::'q mod_ring))) ⊗⇘G⇩T⇙ (x [^]⇘G⇩T⇙ (to_int_mod_ring b)) 
  =  x [^]⇘G⇩T⇙ (to_int_mod_ring (a+b))"
proof -
  assume asmpt: "x ∈ carrier G⇩T"
  have "x [^]⇘G⇩T⇙ to_int_mod_ring a ⊗⇘G⇩T⇙ x [^]⇘G⇩T⇙ to_int_mod_ring b =  x [^]⇘G⇩T⇙ (to_int_mod_ring a + to_int_mod_ring b)"
    by (simp add: G⇩T.int_pow_mult asmpt)
  also have "…=  x [^]⇘G⇩T⇙ ((to_int_mod_ring a + to_int_mod_ring b) mod (CARD ('q)))" 
    using pow_mod_order_G⇩T CARD_q asmpt by blast
  also have "…=  x [^]⇘G⇩T⇙ to_int_mod_ring (a + b)"
    by (simp add: plus_mod_ring.rep_eq to_int_mod_ring.rep_eq)
  finally show "x [^]⇘G⇩T⇙ to_int_mod_ring a ⊗⇘G⇩T⇙ x [^]⇘G⇩T⇙ to_int_mod_ring b = x [^]⇘G⇩T⇙ to_int_mod_ring (a + b)" .
qed

subsubsection ‹bilinearity operations for mod\_ring elements›

lemma e_bilinear[simp]: "P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p ⟹ 
   e (P [^]⇘G⇩p⇙ (to_int_mod_ring (a::'q mod_ring))) (Q [^]⇘G⇩p⇙ (to_int_mod_ring b)) 
= (e P Q) [^]⇘G⇩T⇙ (to_int_mod_ring (a*b))"
proof -
  assume asm: "P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p"
  then have "e (P [^] to_int_mod_ring a) (Q [^] to_int_mod_ring b) = e P Q [^]⇘G⇩T⇙ (to_int_mod_ring a * to_int_mod_ring b)"
    by simp
   also have "… = (e P Q [^]⇘G⇩T⇙ ((to_int_mod_ring a * to_int_mod_ring b) mod CARD ('q)))"
     using CARD_q pow_mod_order_G⇩T asm e_symmetric by blast
   also have "…= e P Q [^]⇘G⇩T⇙ to_int_mod_ring (a * b)"
     by (simp add: times_mod_ring.rep_eq to_int_mod_ring.rep_eq)
   finally  show "e (P [^] to_int_mod_ring a) (Q [^] to_int_mod_ring b) = e P Q [^]⇘G⇩T⇙ to_int_mod_ring (a * b)"
     .
qed

lemma e_linear_in_fst: 
  assumes "P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p"
  shows "e (P [^]⇘G⇩p⇙ (to_int_mod_ring (a::'q mod_ring))) (Q) = (e P Q) [^]⇘G⇩T⇙ (to_int_mod_ring a)"
proof -
  have "e (P [^]⇘G⇩p⇙ to_int_mod_ring a) Q = e (P [^]⇘G⇩p⇙ to_int_mod_ring a) (Q [^]⇘G⇩p⇙ to_int_mod_ring (1::'q mod_ring))" using assms by simp
  also have "... = (e P Q) [^]⇘G⇩T⇙ (to_int_mod_ring (a*(1::'q mod_ring)))" using assms e_bilinear by fast
  also have "…=(e P Q) [^]⇘G⇩T⇙ (to_int_mod_ring a)" by simp
  finally show "e (P [^]⇘G⇩p⇙ (to_int_mod_ring a)) Q = (e P Q) [^]⇘G⇩T⇙ (to_int_mod_ring a)" .
qed

lemma e_linear_in_snd: 
assumes "P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p"
shows "e (P) (Q [^]⇘G⇩p⇙ (to_int_mod_ring (a::'q mod_ring))) = (e P Q) [^]⇘G⇩T⇙ (to_int_mod_ring a)"
proof -
have "e P (Q [^]⇘G⇩p⇙ to_int_mod_ring a) = e (P [^]⇘G⇩p⇙ to_int_mod_ring (1::'q mod_ring)) (Q [^]⇘G⇩p⇙ to_int_mod_ring a)" using assms by simp
  also have "... = (e P Q) [^]⇘G⇩T⇙ (to_int_mod_ring ((1::'q mod_ring)*a))" using assms e_bilinear by fast
  also have "…=(e P Q) [^]⇘G⇩T⇙ (to_int_mod_ring a)" by simp
  finally show "e P (Q [^]⇘G⇩p⇙ to_int_mod_ring a) = e P Q [^]⇘G⇩T⇙ to_int_mod_ring a" .
qed

lemma addition_in_exponents_on_e[simp]: 
  assumes "x ∈ carrier G⇩p ∧ y ∈ carrier G⇩p "
  shows "(e x y) ^⇘G⇩T⇙ a ⊗⇘G⇩T⇙ (e x y) ^⇘G⇩T⇙ b = (e x y) ^⇘G⇩T⇙ (a+b)"
  using assms
  by (metis PiE e_symmetric mod_ring_pow_mult_G⇩T)

lemma e_from_generators_ne_1: "e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ ≠ 𝟭⇘G⇩T⇙"
proof 
  assume asm: "e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ = 𝟭⇘G⇩T⇙"
  have "∀P Q. P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p ⟶ e P Q = 𝟭⇘G⇩T⇙" 
  proof(intro allI)
    fix P Q
    show "P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p ⟶ e P Q = 𝟭⇘G⇩T⇙ "
    proof 
      assume "P ∈ carrier G⇩p ∧ Q ∈ carrier G⇩p"
      then obtain p q::int where "❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ p = P ∧ ❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ q = Q"
        by (metis G⇩p.generatorE int_pow_int)
      then have "e P Q = e (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ p) (❙g⇘G⇩p⇙ [^]⇘G⇩p⇙ q)"
        by blast
      also have "… = e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙ [^]⇘G⇩T⇙ (p*q)"
        by force
      also have "… =  𝟭⇘G⇩T⇙ [^]⇘G⇩T⇙ (p*q)"
        using asm by argo
      also have "… =  𝟭⇘G⇩T⇙"
        by fastforce
      finally show "e P Q = 𝟭⇘G⇩T⇙" .
    qed
  qed
  then show "False" using e_non_degeneracy by blast
qed

lemma pow_on_eq_card_GT[simp]: "(❙g⇘G⇩T⇙ ^⇘G⇩T⇙ x = ❙g⇘G⇩T⇙ ^⇘G⇩T⇙ y) = (x=y)"
proof
  assume assm: "❙g⇘G⇩T⇙ ^⇘G⇩T⇙ x = ❙g⇘G⇩T⇙ ^⇘G⇩T⇙ y"
  then have "❙g⇘G⇩T⇙ [^]⇘G⇩T⇙ to_int_mod_ring x = ❙g⇘G⇩T⇙ [^]⇘G⇩T⇙ to_int_mod_ring y"
    using assm by blast
  then have "❙g⇘G⇩T⇙ [^]⇘G⇩T⇙ nat (to_int_mod_ring x) = ❙g⇘G⇩T⇙ [^]⇘G⇩T⇙ nat (to_int_mod_ring y)" 
    using to_int_mod_ring_ge_0[of "x"] to_int_mod_ring_ge_0[of "y"] by fastforce
  then have "[nat (to_int_mod_ring x) = nat (to_int_mod_ring y)] (mod order G⇩T)"
    using G⇩T.pow_generator_eq_iff_cong G⇩T.finite_carrier by fast
  then have "[to_int_mod_ring x = to_int_mod_ring y] (mod order G⇩T)" 
    using to_int_mod_ring_ge_0[of "x"] to_int_mod_ring_ge_0[of "y"]
    by (metis cong_int_iff int_nat_eq)
  then have "[to_int_mod_ring x = to_int_mod_ring y] (mod p)" 
    using CARD_G⇩T by fast
  then have "to_int_mod_ring x = to_int_mod_ring y"
    by (metis arith_simps(49) to_int_mod_ring_add to_int_mod_ring_hom.hom_0_iff
        unique_euclidean_semiring_class.cong_def CARD_q)
  then show "x = y" by force
next 
  assume "x = y"
  then show "❙g⇘G⇩T⇙ ^⇘G⇩T⇙ x = ❙g⇘G⇩T⇙ ^⇘G⇩T⇙ y" by fast
qed

lemma pow_on_eq_card_GT_carrier_ext'[simp]: 
  "((e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙))^⇘G⇩T⇙ x = ((e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙))^⇘G⇩T⇙ y ⟷ x=y"
proof 
  assume g_pow_x_eq_g_pow_y: "e ❙g ❙g ^⇘G⇩T⇙ x = e ❙g ❙g ^⇘G⇩T⇙ y"
  obtain g_exp::nat where "e ❙g ❙g = ❙g⇘G⇩T⇙ [^]⇘G⇩T⇙ g_exp"
    using G⇩T.generatorE e_g_g_in_carrier_GT by blast
  then have g_exp: "e ❙g ❙g = ❙g⇘G⇩T⇙ ^⇘G⇩T⇙ (of_int_mod_ring (int g_exp))"
    by (metis CARD_G⇩T G⇩T.pow_generator_mod_int math_primitives.CARD_q math_primitives_axioms int_pow_int of_int_mod_ring.rep_eq to_int_mod_ring.rep_eq)
  let ?g_exp = "of_int_mod_ring (int g_exp)"
  have "(e ❙g ❙g)^⇘G⇩T⇙ x =  ❙g⇘G⇩T⇙ ^⇘G⇩T⇙ (of_int_mod_ring (int g_exp) * x)"
    using g_exp
    by (metis CARD_G⇩T G⇩T.generator_closed G⇩T.int_pow_pow G⇩T.pow_generator_mod_int math_primitives.CARD_q math_primitives_axioms times_mod_ring.rep_eq to_int_mod_ring.rep_eq)
  moreover have "(e ❙g ❙g)^⇘G⇩T⇙ y = ❙g⇘G⇩T⇙ ^⇘G⇩T⇙ (of_int_mod_ring (int g_exp) * y)"
    using g_exp
    by (metis CARD_G⇩T G⇩T.generator_closed G⇩T.int_pow_pow G⇩T.pow_generator_mod_int math_primitives.CARD_q math_primitives_axioms times_mod_ring.rep_eq to_int_mod_ring.rep_eq)
  ultimately show "x =y"
    using g_pow_x_eq_g_pow_y pow_on_eq_card_GT e_from_generators_ne_1 g_exp by force
next 
    assume "x = y"
    then show "(e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙) ^⇘G⇩T⇙ x = (e ❙g⇘G⇩p⇙ ❙g⇘G⇩p⇙) ^⇘G⇩T⇙ y" 
      by blast
  qed

end

end