--- a/src/HOL/NumberTheory/WilsonRuss.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Wed May 17 01:23:41 2006 +0200
@@ -15,13 +15,13 @@
subsection {* Definitions and lemmas *}
+definition
+ inv :: "int => int => int"
+ "inv p a = (a^(nat (p - 2))) mod p"
+
consts
- inv :: "int => int => int"
wset :: "int * int => int set"
-defs
- inv_def: "inv p a == (a^(nat (p - 2))) mod p"
-
recdef wset
"measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
"wset (a, p) =
@@ -81,7 +81,8 @@
apply (rule_tac [2] zcong_zless_imp_eq, auto)
done
-lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
+lemma inv_not_p_minus_1_aux:
+ "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
apply (unfold zcong_def)
apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
@@ -163,7 +164,8 @@
lemma wset_induct:
assumes "!!a p. P {} a p"
- and "!!a p. 1 < (a::int) \<Longrightarrow> P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
+ and "!!a p. 1 < (a::int) \<Longrightarrow>
+ P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
shows "P (wset (u, v)) u v"
apply (rule wset.induct, safe)
prefer 2