theory LittleFermat
imports "Primefactors"
begin

section {* Group Zp *}

constdefs Z::"nat \<Rightarrow> nat set"
"Z p \<equiv> set (upt 0 p)"

constdefs modeq:: "nat => nat => nat => bool"    ("(1[_ = _] '(mod _'))")
"[a = b] (mod p) == ((a mod p) = (b mod p))"

constdefs modneq:: "nat => nat => nat => bool"    ("(1[_ ~= _] '(mod _'))")
"[a ~= b] (mod p) == ((a mod p) ~= (b mod p))"

lemma modeq_trans:
"\<lbrakk> [a = b] (mod p); [b = c] (mod p) \<rbrakk> \<Longrightarrow> [a = c] (mod p)"
by (simp add:modeq_def)

lemma in_Zp_upper_bound:
"x \<in> Z p \<Longrightarrow> x < p"
by (simp add:Z_def)

(* FIME: Move to standard library? *)
lemma mod_mult:
"\<lbrakk> (a::nat) mod p = b mod p; a' mod p = b' mod p \<rbrakk> \<Longrightarrow> (a * a') mod p = (b * b') mod p"
apply (subgoal_tac "a * a' mod p = a mod p * (a' mod p) mod p")
 prefer 2
 apply (rule mod_mult_distrib_mod)
apply(subgoal_tac "b * b' mod p = b mod p * (b' mod p) mod p")
 prefer 2
 apply (rule mod_mult_distrib_mod)
apply simp
done

lemma modeq_pow:
"[a = b] (mod p) \<Longrightarrow> [a^k = b^k] (mod p)"
apply (induct k)
apply (simp add: modeq_def)

apply (simp add: modeq_def)
apply (rule mod_mult)
apply simp
apply simp
done

lemma finite_Zp: "finite (Z p)"
apply (induct p)
apply (simp add: Z_def)
apply (simp add: Z_def)
done

lemma card_Zp: "card (Z p) = p"
apply (induct p)
apply (simp add: Z_def)

apply (subgoal_tac "finite (Z p)")
 prefer 2
 apply (rule finite_Zp)

apply (simp add: Z_def)
done

lemma card_Zp_0: "card (Z p - {0}) = p - 1"
apply (induct p)
apply (simp add: Z_def)

apply (subgoal_tac "finite (Z p - {0})")
 prefer 2
 apply (subgoal_tac "finite (Z p)")
  prefer 2
  apply (rule finite_Zp)
 apply simp

apply (simp add: Z_def)
apply (case_tac "p = 0")
apply simp

apply (subgoal_tac "insert p {k. k < p} - {0} = insert p ({k. k < p} - {0})")
 prefer 2
 apply (rule sym)
 apply blast

apply simp
done

lemma Little_Fermat_l2r:
"p \<in> prime \<Longrightarrow> (\<forall>x \<in> (Z p - {0}). [x^(p - 1) = 1] (mod p))"
sorry

lemma Little_Fermat_r2l:
"(\<forall>x \<in> (Z p - {0}). [x^(p - 1) = 1] (mod p)) \<Longrightarrow> p \<in> prime"
sorry

theorem Little_Fermat:
"p \<in> prime = (\<forall>x \<in> (Z p - {0}). [x^(p - 1) = 1] (mod p))"
apply (rule iffI)
apply (rule Little_Fermat_l2r, assumption)
apply (rule Little_Fermat_r2l, assumption)
done

section {* Generators *}

constdefs generators::"nat set \<Rightarrow> nat \<Rightarrow> nat set"
"generators Zp p \<equiv> {g.  g \<in> Zp \<and> (\<forall>x \<in> Zp. \<exists> k. [x = g^k] (mod p))}"

lemma generator_check:
"1 < p \<Longrightarrow> 
 g \<in> generators (Z p - {0}) p = (\<forall> k. 0 < k \<and> k < (p - 1) \<longrightarrow> [g^k ~= 1] (mod p)) \<and> [g ^ (p - 1) = 1] (mod p)"
sorry

constdefs onelogs::"nat \<Rightarrow> nat \<Rightarrow> nat set"
"onelogs x p \<equiv> {i. 0 < i \<and> [x^i = 1] (mod p)}"

constdefs minN:: "nat set \<Rightarrow> nat"
"minN S \<equiv> LeastM (\<lambda> x. x) (\<lambda> x. x \<in> S)"

lemma minN_in:
"S \<noteq> {} \<Longrightarrow> minN S \<in> S"
apply (subgoal_tac "\<exists> x. x \<in> S")
 prefer 2
 apply blast
apply (erule exE)
apply (simp only: minN_def)
apply (drule_tac P="\<lambda> x. x \<in> S" and k="x" and m="\<lambda> x. x" in LeastM_natI)
apply simp
done

lemma minN_least:
"\<forall> x \<in> S. minN S \<le> x"
apply (rule ballI)
apply (drule_tac P="\<lambda> x. x \<in> S"  and m="\<lambda> x. x" in LeastM_nat_le)
apply (simp add: minN_def)
done

constdefs order::"nat \<Rightarrow> nat \<Rightarrow> nat"
"order x p \<equiv> minN (onelogs x p)"


lemma onelogs_exist:
"0 < x \<and> 0 < p \<and> gcd (x,p) = 1 \<Longrightarrow> onelogs x p \<noteq> {}"
sorry

lemma order_l_p:
"onelogs x p \<noteq> {} \<Longrightarrow> order x p < p"
sorry

lemma order_g_0:
"onelogs x p \<noteq> {} \<Longrightarrow> 0 < order x p"
apply (simp add: order_def)
apply (subgoal_tac "minN (onelogs x p) \<in> onelogs x p")
 prefer 2
 apply (rule minN_in)
 apply assumption
apply (simp add:onelogs_def)
done

lemma order_is_onelog:
"onelogs x p \<noteq> {} \<Longrightarrow> [x^(order x p) = 1] (mod p)"
apply (subgoal_tac "minN (onelogs x p) \<in> onelogs x p")
 prefer 2
 apply (rule minN_in)
 apply assumption
apply (simp add: onelogs_def order_def)
done

lemma order_minimal:
"a \<in> onelogs x p \<Longrightarrow> order x p \<le> a"
apply (subgoal_tac "\<forall> a \<in> (onelogs x p). minN (onelogs x p) \<le> a")
 prefer 2
 apply (rule minN_least)
apply (erule_tac x="a" in ballE)
 prefer 2
 apply simp
apply (simp only: order_def)
done

lemma generator_Zp_pow: "g \<in> (generators (Z p - {0}) p) \<Longrightarrow> [g^(p - 1) = 1] (mod p)"
apply (case_tac "1 < p")
apply (drule_tac g="g" in generator_check)
apply simp

apply (case_tac "p = 0")
apply (simp add: generators_def Z_def)

apply (subgoal_tac "p = 1")
 prefer 2
 apply simp
apply (simp add: modeq_def)
done

lemma below_order_pow: "\<lbrakk> 0 < k; k < order x p \<rbrakk> \<Longrightarrow> [x^k ~= 1] (mod p)"
sorry

lemma generator_exists:
"p \<in> prime \<Longrightarrow> \<exists> g. g \<in> generators (Z p - {0}) p"
sorry 



end