src/HOL/NumberTheory/WilsonRuss.thy

 
 lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
 by (subst int_int_eq [symmetric], auto)
 
 lemma inv_is_inv:
-    "p \<in> zprime \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
+    "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
   apply (unfold inv_def)
   apply (subst zcong_zmod)
   apply (subst zmod_zmult1_eq [symmetric])
   apply (subst zcong_zmod [symmetric])
   apply (subst power_Suc [symmetric])

    apply (erule_tac [2] zdvd_not_zless)
    apply (unfold zprime_def, auto)
   done
 
 lemma inv_distinct:
-    "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> a \<noteq> inv p a"
+    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> a \<noteq> inv p a"
   apply safe
   apply (cut_tac a = a and p = p in zcong_square)
      apply (cut_tac [3] a = a and p = p in inv_is_inv, auto)
    apply (subgoal_tac "a = 1")
     apply (rule_tac [2] m = p in zcong_zless_imp_eq)
         apply (subgoal_tac [7] "a = p - 1")
          apply (rule_tac [8] m = p in zcong_zless_imp_eq, auto)
   done
 
 lemma inv_not_0:
-    "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 0"
+    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 0"
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      apply (unfold zcong_def, auto)
   apply (subgoal_tac "\<not> p dvd 1")
    apply (rule_tac [2] zdvd_not_zless)

      prefer 2
      apply (subst zdvd_zminus_iff [symmetric], auto)
   done
 
 lemma inv_not_1:
-    "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 1"
+    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 1"
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      prefer 4
      apply simp
      apply (subgoal_tac "a = 1")

   apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
    apply (subst zdvd_reduce, auto)
   done
 
 lemma inv_not_p_minus_1:
-    "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> p - 1"
+    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> p - 1"
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv, auto)
   apply (simp add: inv_not_p_minus_1_aux)
   apply (subgoal_tac "a = p - 1")
    apply (rule_tac [2] zcong_zless_imp_eq, auto)
   done
 
 lemma inv_g_1:
-    "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> 1 < inv p a"
+    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> 1 < inv p a"
   apply (case_tac "0\<le> inv p a")
    apply (subgoal_tac "inv p a \<noteq> 1")
     apply (subgoal_tac "inv p a \<noteq> 0")
      apply (subst order_less_le)
      apply (subst zle_add1_eq_le [symmetric])

        apply (rule_tac [5] inv_not_1, auto)
   apply (unfold inv_def zprime_def, simp)
   done
 
 lemma inv_less_p_minus_1:
-    "p \<in> zprime \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a < p - 1"
+    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a < p - 1"
   apply (case_tac "inv p a < p")
    apply (subst order_less_le)
    apply (simp add: inv_not_p_minus_1, auto)
   apply (unfold inv_def zprime_def, simp)
   done

    apply (auto simp add: zpower_zadd_distrib)
   apply (subgoal_tac "zcong (x^y * x^(y * z)) (1 * 1) p")
    apply (rule_tac [2] zcong_zmult, simp_all)
   done
 
-lemma inv_inv: "p \<in> zprime \<Longrightarrow>
+lemma inv_inv: "zprime p \<Longrightarrow>
     5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
   apply (unfold inv_def)
   apply (subst zpower_zmod)
   apply (subst zpower_zpower)
   apply (rule zcong_zless_imp_eq)

   apply (subst wset.simps)
   apply (unfold Let_def, auto)
   done
 
 lemma wset_g_1 [rule_format]:
-    "p \<in> zprime --> a < p - 1 --> b \<in> wset (a, p) --> 1 < b"
+    "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> 1 < b"
   apply (induct a p rule: wset_induct, auto)
   apply (case_tac "b = a")
    apply (case_tac [2] "b = inv p a")
     apply (subgoal_tac [3] "b = a \<or> b = inv p a")
      apply (rule_tac [4] wset_mem_imp_or)

        apply simp
        apply (rule inv_g_1, auto)
   done
 
 lemma wset_less [rule_format]:
-    "p \<in> zprime --> a < p - 1 --> b \<in> wset (a, p) --> b < p - 1"
+    "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> b < p - 1"
   apply (induct a p rule: wset_induct, auto)
   apply (case_tac "b = a")
    apply (case_tac [2] "b = inv p a")
     apply (subgoal_tac [3] "b = a \<or> b = inv p a")
      apply (rule_tac [4] wset_mem_imp_or)

        apply simp
        apply (rule inv_less_p_minus_1, auto)
   done
 
 lemma wset_mem [rule_format]:
-  "p \<in> zprime -->
+  "zprime p -->
     a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset (a, p)"
   apply (induct a p rule: wset.induct, auto)
   apply (rule_tac wset_subset)
   apply (simp (no_asm_simp))
   apply auto
   done
 
 lemma wset_mem_inv_mem [rule_format]:
-  "p \<in> zprime --> 5 \<le> p --> a < p - 1 --> b \<in> wset (a, p)
+  "zprime p --> 5 \<le> p --> a < p - 1 --> b \<in> wset (a, p)
     --> inv p b \<in> wset (a, p)"
   apply (induct a p rule: wset_induct, auto)
    apply (case_tac "b = a")
     apply (subst wset.simps)
     apply (unfold Let_def)

        apply (subgoal_tac [6] "b = a \<or> b = inv p a")
         apply (rule_tac [7] wset_mem_imp_or, auto)
   done
 
 lemma wset_inv_mem_mem:
-  "p \<in> zprime \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - 1 \<Longrightarrow> 1 < b \<Longrightarrow> b < p - 1
+  "zprime p \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - 1 \<Longrightarrow> 1 < b \<Longrightarrow> b < p - 1
     \<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
   apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
    apply (rule_tac [2] wset_mem_inv_mem)
       apply (rule inv_inv, simp_all)
   done

    apply (subst wset.simps)
    apply (unfold Let_def, auto)
   done
 
 lemma wset_zcong_prod_1 [rule_format]:
-  "p \<in> zprime -->
+  "zprime p -->
     5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset(a, p). x) = 1] (mod p)"
   apply (induct a p rule: wset_induct)
    prefer 2
    apply (subst wset.simps)
    apply (unfold Let_def, auto)

           apply (rule_tac [5] wset_inv_mem_mem)
                apply (simp_all add: wset_fin)
   apply (rule inv_distinct, auto)
   done
 
-lemma d22set_eq_wset: "p \<in> zprime ==> d22set (p - 2) = wset (p - 2, p)"
+lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2, p)"
   apply safe
    apply (erule wset_mem)
      apply (rule_tac [2] d22set_g_1)
      apply (rule_tac [3] d22set_le)
      apply (rule_tac [4] d22set_mem)

   done
 
 
 subsection {* Wilson *}
 
-lemma prime_g_5: "p \<in> zprime \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
+lemma prime_g_5: "zprime p \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
   apply (unfold zprime_def dvd_def)
   apply (case_tac "p = 4", auto)
    apply (rule notE)
     prefer 2
     apply assumption

    apply (safe, arith)
      apply (rule_tac x = 2 in exI, auto)
   done
 
 theorem Wilson_Russ:
-    "p \<in> zprime ==> [zfact (p - 1) = -1] (mod p)"
+    "zprime p ==> [zfact (p - 1) = -1] (mod p)"
   apply (subgoal_tac "[(p - 1) * zfact (p - 2) = -1 * 1] (mod p)")
    apply (rule_tac [2] zcong_zmult)
     apply (simp only: zprime_def)
     apply (subst zfact.simps)
     apply (rule_tac t = "p - 1 - 1" and s = "p - 2" in subst, auto)