(*<*)theory Blatt6 = LittleFermat:(*>*)

text {* \subsection*{Pratts Primzahlregeln}

Von Vaughan Pratt gibt es ein Regelsystem, in dem die Primalit"at von
Zahlen beweisbar ist. Die Regeln arbeiten auf zweierlei Formeln:
*}

datatype form = Prime nat | Cand nat nat nat

text {* Formeln der Art @{text "Prime p"} deuten an, da"s @{text "p"} eine Primzahl ist, w"ahrend Formeln der Art @{text "Cand x q p"} Zwischenergebnisse festhalten.
*}

consts PrattSet::"form set"

inductive "PrattSet"
intros
Ax:"Cand p g 1 \<in> PrattSet"
R1:"\<lbrakk> Prime q \<in> PrattSet; Cand p g x \<in> PrattSet; 
     [g^((p - 1) div q) ~= 1] (mod p) \<rbrakk>
    \<Longrightarrow> Cand p g (x*q) \<in> PrattSet"
R2:"\<lbrakk> Cand p g (p - 1) \<in> PrattSet; [g^(p - 1) = 1] (mod p) \<rbrakk> 
    \<Longrightarrow> Prime p \<in> PrattSet"

(* Natural numbers in successor represenation are handier for the simplifier. *)
(*<*)
lemma Ax': "Cand p g (Suc 0) \<in> PrattSet"
by (simp add: Ax[simplified])

lemma R1': "\<lbrakk> Prime q \<in> PrattSet; Cand p g x \<in> PrattSet; 
     [g^((p - (Suc 0)) div q) ~= (Suc 0)] (mod p) \<rbrakk>
    \<Longrightarrow> Cand p g (x*q) \<in> PrattSet"
by (simp add: R1[simplified])

lemma R2': "\<lbrakk> Cand p g (p - (Suc 0)) \<in> PrattSet; [g^(p - (Suc 0)) = (Suc 0)] (mod p) \<rbrakk> 
    \<Longrightarrow> Prime p \<in> PrattSet"
by (simp add: R2[simplified])
(*>*)


text {* \subsection*{Kennenlernen der Regeln}

Machen Sie sich mit den Regeln vertraut, indem Sie folgende Lemmas
beweisen. 

*} 

lemma Prime3_in_PrattSet: "Prime 2 \<in> PrattSet"
(*<*)  sorry (*>*)

lemma Prime0_notin_PrattSet: "Prime 0 \<notin> PrattSet"
(*<*)  sorry (*>*)



text {* \subsection*{Erkl"arung der Regeln} 

Unser gro"ses Ziel ist zu beweisen, da"s die Pratt Regeln genau
die Menge aller Primzahlen @{text "prime"}, die
in @{text "HOL/Library/Primes.thy"} definiert wird, erzeugt. *}

theorem Pratt: "prime = {p. Prime p \<in> PrattSet}" 
(*<*) oops (*>*) 

text {* Um diesen Satz zu beweisen sind zahlentheoretische S"atze aus dem Grundstudium ({\it Diskrete Strukturen I})
 sehr hilfreich. Wir wiederholen hier kurz ein paar Begriffe und S"atze, die Sie in Ihrem Beweis gerne "ubernehmen
d"urfen.  

Wir repr"asentieren den Restklassenring @{text "\<int>\<^sub>p"} durch seine Standardvertreter @{text "{0,\<dots>,p-1}"}. *}

lemma Z_def:  "Z p \<equiv> set (upt 0 p)"
(*<*) by (simp add: Z_def) (*>*)

lemma modeq_def: "[a = b] (mod p) \<equiv> ((a mod p) = (b mod p))"
(*<*) by (simp add: modeq_def) (*>*)

lemma modneq_def: "[a ~= b] (mod p) \<equiv> ((a mod p) ~= (b mod p))"
(*<*) by (simp add: modneq_def) (*>*)

text {* 

In dieser Struktur spielt der kleine Satz von Fermat eine wichtige Rolle: *}

theorem Little_Fermat: 
"p \<in> prime = (\<forall>x \<in> (Z p - {0}). [x^(p - 1) = 1] (mod p))"
(*<*) by (rule Little_Fermat) (*>*)

text {*
Elemente einer Menge @{text "M"}, die durch iterierte Multiplikation alle anderen Elemente erzeugen,
nennt man Generatoren von @{text "M"}. *}

lemma generators_def: "generators M p = 
                       {g.  g \<in> M \<and> (\<forall>x \<in> M. \<exists> k. [x = g^k] (mod p))}"
(*<*) by (simp add: generators_def) (*>*)

text {*

Man kann beweisen, da"s @{text "Z p - {0}"} einen Generator hat, wenn @{text "p"} prim ist. *}

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

text {*
Um zu testen, ob man es mit einem Generator zu tun hat, kann man durch Ausrechnen von Potenzen
sicherstellen, da"s es sich um ein Element der Ordnung @{text "p - 1"} handelt. Die Ordnung eines
Elementes @{text "a"} ist dabei der kleinste Exponent @{text "k > 0"}, f"ur den @{text "[a ^ k = 1] mod p"}
gilt. *}

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)"
(*<*) by (rule generator_check) (*>*)

text {*
Anstatt alle Exponenten kleiner @{text "p - 1"} durchzuprobieren, reicht es f"ur alle Primfaktoren @{text "q"}
von @{text "p - 1"} Exponenten der Form @{text "p - 1 / q"} zu "uberpr"ufen. Dieser nicht offensichtliche Zusammenhang
stellt das R"uckgrat der Pratt Regeln dar und ist der Grund, warum man Primzahlen effizient nachweisen kann. Um dies
zu formalisieren, verwenden wir die Funktion @{text "primefactors"}, die f"ur eine gegebene Zahl die Liste aller
Primfaktoren in aufsteigender Reihenfolge liefert. *}

lemma fast_generator_check: "1 < p \<Longrightarrow> g \<in> generators (Z p - {0}) p =
((\<forall> q \<in> set (primefactors (p - 1)). [(g^((p - 1) div q)) ~= 1] (mod p)) \<and> [(g^(p - 1)) = 1] (mod p))"
(*<*) sorry (*>*)

text {* 
Die Pratt Regeln sind so gestaltet, da"s man @{text "Prime p"} nur dann ableiten kann, wenn
@{text "p"} eine Primzahl ist. Dazu braucht man einen Generator @{text "g"} von @{text "Z p"}.
Man startet mit @{text "Cand p g 1"}. Dann multipliziert man schrittweise alle Primfaktoren
von @{text "p - 1"} an das dritte Argument von @{text "Cand"} mit Hilfe der Regel @{text "R2"}.
Man erh"alt schlie"slich @{text "Cand p g (p-1)"} und kann mit Hilfe von @{text "R3"} die
Formel @{text "Prime p"} ableiten. Die Seitenbedingungen von @{text "R1"} und @{text "R2"}
garantieren, da"s @{text "g"} tats"achlich ein Generator von @{text "Z p"} ist. Damit ist
"uber den kleinen Satz von Fermat sichergestellt, da"s @{text "p"} eine Primzahl ist. \\

N"ahere Informationen zu den Pratt Regeln finden Sie in den Seminarausarbeitungen von 
Alexander Fischer und Maksym Marchenko, die auf der Praktikumsseite 
{\bf http://www4.in.tum.de/lehre/praktika/psv/psv2005/ } verlinkt sind. F"ur die folgenden Beweisarbeiten
d"urfen Sie auf oben genannte Lemmas zur"uckgreifen. F"ur die induktiv definierte Menge @{text "PrattSet"} 
liefert Isabelle automatisch Theoreme. Diese k"onnen Sie sich mit @{text "thm PrattSet.intros"}, @{text "thm PrattSet.elims"} und 
@{text "thm PrattSet.induct"} anzeigen lassen. Beachten Sie, da"s in den Theorien @{text "Primefactors.thy"}
und  @{text "LittleFermat.thy"}, die dieser Aufgabe beiliegen, auch n"utzliche Theoreme und Definitionen vorhanden sind. Au"serdem
d"urfen wie "ublich alle Theoreme aus der Isabelle Library verwendet werden. Um Ihnen das Suchen zu erleichtern, 
listen wir im Anhang ein paar Kandidaten auf. *}

text {* \subsection*{Korrektheit (1. Woche)} 

Beweisen Sie die Korrektheit der Pratt Regeln: *}

theorem Pratt_correct: "Prime p \<in> PrattSet \<Longrightarrow> p \<in> prime"
(*<*) sorry (*>*)

text {* 
Tip: Finden Sie eine geeignete Invariante @{text "PrattInv"} und zeigen Sie
folgende Lemmas. *}

lemma PrattInv_prime: "PrattInv (Prime p) \<Longrightarrow> p \<in> prime"
(*<*) sorry (*>*)


lemma PrattInv_covers_PrattSet "f \<in> PrattSet \<Longrightarrow> PrattInv f"
(*<*) sorry (*>*)

text {* \subsection*{Vollst"andigkeit (2. Woche)} 

Zeigen Sie die Vollst"andigkeit der Regeln. *}

theorem Pratt_complete: "p \<in> prime \<Longrightarrow> Prime p \<in> PrattSet"
(*<*) sorry (*>*)

text {*
Tip: Finden Sie eine Formel @{text "PrattInv2"}, die folgende
Lemmas erf"ullt. *}

lemma prime_PrattInv2: "p \<in> prime \<Longrightarrow> PrattInv2 (Prime p)"
(*<*) sorry (*>*)

lemma PrattSet_covers_PrattInv2: "PrattInv2 f \<Longrightarrow> f \<in> PrattSet"
(*<*) sorry (*>*)


text {* \subsection*{ Schneller Generator Nachweis (3. Woche)} 

Beweisen Sie das Lemma @{thm[source]fast_generator_check} von vorhin. 

*}

text {* \subsection*{ Anhang: N"utzliche Theoreme } *}


text {*
@{thm[source]dvd_imp_le}:@{thm[break]dvd_imp_le[no_vars]}

@{thm[source]le_div_geq}:@{thm[break]le_div_geq[no_vars]}

@{thm[source]div_less_dividend}:@{thm[break]div_less_dividend[no_vars]}

@{thm[source]mod_mult_distrib_mod}:@{thm[break]mod_mult_distrib_mod[no_vars]}

@{thm[source]dvd_eq_mod_eq_0}:@{thm[break]dvd_eq_mod_eq_0[no_vars]}

@{thm[source]power_one}:@{thm[break]power_one[no_vars]}

@{thm[source]power_add}:@{thm[break]power_add[no_vars]}

@{thm[source]power_mult}: @{thm[break]power_mult[no_vars]}

@{thm[source]mod_less}: @{thm[break]mod_less[no_vars]}

@{thm[source]prime_g_one}: @{thm[break]prime_g_one[no_vars]}

@{thm[source]primefactors_upper_bound}: @{thm[break]primefactors_upper_bound [no_vars]}

@{thm[source]primefactors_are_prime}: @{thm[break]primefactors_are_prime [no_vars]}

@{thm[source]primefactors_are_factors}: @{thm[break]primefactors_are_factors [no_vars]}

@{thm[source]prime_primefactors}: @{thm[break]prime_primefactors [no_vars]}

@{thm[source]primefactors_mult}: @{thm[break]primefactors_mult [no_vars]}

@{thm[source]primefactors_exist}: @{thm[break]primefactors_exist [no_vars]}

@{thm[source]no_primefactors}: @{thm[break]no_primefactors [no_vars]}

@{thm[source]primefactors_complete}: @{thm[break]primefactors_complete [no_vars]}

@{thm[source]common_primefactors}: @{thm[break]common_primefactors [no_vars]}

@{thm[source]onelogs_def}: @{thm[break]onelogs_def [no_vars]}

@{thm[source]order_is_onelog}: @{thm[break]order_is_onelog [no_vars]}

@{thm[source]order_l_p}: @{thm[break]order_l_p [no_vars]}

@{thm[source]order_g_0}: @{thm[break]order_g_0 [no_vars]}

@{thm[source]order_minimal}: @{thm[break]order_minimal [no_vars]}

@{thm[source]below_order_pow}: @{thm[break]below_order_pow [no_vars]}

@{thm[source]generator_Zp_pow}: @{thm[break]generator_Zp_pow [no_vars]}

@{thm[source]generator_exists}: @{thm[break]generator_exists [no_vars]}

*}


(*<*)end(*>*)