src/HOL/NumberTheory/EulerFermat.thy

   RRset2norRR :: "int set => int => int => int"
 
 inductive "RsetR m"
   intros
     empty [simp]: "{} \<in> RsetR m"
-    insert: "A \<in> RsetR m ==> zgcd (a, m) = #1 ==>
+    insert: "A \<in> RsetR m ==> zgcd (a, m) = Numeral1 ==>
       \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
 
 recdef BnorRset
   "measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
   "BnorRset (a, m) =
-   (if #0 < a then
-    let na = BnorRset (a - #1, m)
-    in (if zgcd (a, m) = #1 then insert a na else na)
+   (if Numeral0 < a then
+    let na = BnorRset (a - Numeral1, m)
+    in (if zgcd (a, m) = Numeral1 then insert a na else na)
     else {})"
 
 defs
-  norRRset_def: "norRRset m == BnorRset (m - #1, m)"
+  norRRset_def: "norRRset m == BnorRset (m - Numeral1, m)"
   noXRRset_def: "noXRRset m x == (\<lambda>a. a * x) ` norRRset m"
   phi_def: "phi m == card (norRRset m)"
   is_RRset_def: "is_RRset A m == A \<in> RsetR m \<and> card A = phi m"
   RRset2norRR_def:
     "RRset2norRR A m a ==
-     (if #1 < m \<and> is_RRset A m \<and> a \<in> A then
+     (if Numeral1 < m \<and> is_RRset A m \<and> a \<in> A then
         SOME b. zcong a b m \<and> b \<in> norRRset m
-      else #0)"
+      else Numeral0)"
 
 constdefs
   zcongm :: "int => int => int => bool"
   "zcongm m == \<lambda>a b. zcong a b m"
 
-lemma abs_eq_1_iff [iff]: "(abs z = (#1::int)) = (z = #1 \<or> z = #-1)"
+lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = # -1)"
   -- {* LCP: not sure why this lemma is needed now *}
   apply (auto simp add: zabs_def)
   done
 
 

 
 declare BnorRset.simps [simp del]
 
 lemma BnorRset_induct:
   "(!!a m. P {} a m) ==>
-    (!!a m. #0 < (a::int) ==> P (BnorRset (a - #1, m::int)) (a - #1) m
+    (!!a m. Numeral0 < (a::int) ==> P (BnorRset (a - Numeral1, m::int)) (a - Numeral1) m
       ==> P (BnorRset(a,m)) a m)
     ==> P (BnorRset(u,v)) u v"
 proof -
   case rule_context
   show ?thesis
     apply (rule BnorRset.induct)
     apply safe
-     apply (case_tac [2] "#0 < a")
+     apply (case_tac [2] "Numeral0 < a")
       apply (rule_tac [2] rule_context)
        apply simp_all
      apply (simp_all add: BnorRset.simps rule_context)
   done
 qed

 
 lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
   apply (auto dest: Bnor_mem_zle)
   done
 
-lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> #0 < b"
+lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> Numeral0 < b"
   apply (induct a m rule: BnorRset_induct)
    prefer 2
    apply (subst BnorRset.simps)
    apply (unfold Let_def)
    apply auto
   done
 
 lemma Bnor_mem_if [rule_format]:
-    "zgcd (b, m) = #1 --> #0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
+    "zgcd (b, m) = Numeral1 --> Numeral0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
   apply (induct a m rule: BnorRset.induct)
   apply auto
    apply (case_tac "a = b")
     prefer 2
     apply (simp add: order_less_le)

   apply auto
   apply (rule RsetR.insert)
     apply (rule_tac [3] allI)
     apply (rule_tac [3] impI)
     apply (rule_tac [3] zcong_not)
-       apply (subgoal_tac [6] "a' \<le> a - #1")
+       apply (subgoal_tac [6] "a' \<le> a - Numeral1")
         apply (rule_tac [7] Bnor_mem_zle)
         apply (rule_tac [5] Bnor_mem_zg)
         apply auto
   done
 

    apply (subst BnorRset.simps)
    apply (unfold Let_def)
    apply auto
   done
 
-lemma aux: "a \<le> b - #1 ==> a < (b::int)"
+lemma aux: "a \<le> b - Numeral1 ==> a < (b::int)"
   apply auto
   done
 
 lemma norR_mem_unique:
-  "#1 < m ==>
-    zgcd (a, m) = #1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
+  "Numeral1 < m ==>
+    zgcd (a, m) = Numeral1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
   apply (unfold norRRset_def)
   apply (cut_tac a = a and m = m in zcong_zless_unique)
    apply auto
    apply (rule_tac [2] m = m in zcong_zless_imp_eq)
        apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
 	 order_less_imp_le aux simp add: zcong_sym)
   apply (rule_tac "x" = "b" in exI)
   apply safe
   apply (rule Bnor_mem_if)
-    apply (case_tac [2] "b = #0")
+    apply (case_tac [2] "b = Numeral0")
      apply (auto intro: order_less_le [THEN iffD2])
    prefer 2
    apply (simp only: zcong_def)
    apply (subgoal_tac "zgcd (a, m) = m")
     prefer 2

 
 
 text {* \medskip @{term noXRRset} *}
 
 lemma RRset_gcd [rule_format]:
-    "is_RRset A m ==> a \<in> A --> zgcd (a, m) = #1"
+    "is_RRset A m ==> a \<in> A --> zgcd (a, m) = Numeral1"
   apply (unfold is_RRset_def)
   apply (rule RsetR.induct)
     apply auto
   done
 
 lemma RsetR_zmult_mono:
   "A \<in> RsetR m ==>
-    #0 < m ==> zgcd (x, m) = #1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
+    Numeral0 < m ==> zgcd (x, m) = Numeral1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
   apply (erule RsetR.induct)
    apply simp_all
   apply (rule RsetR.insert)
     apply auto
    apply (blast intro: zgcd_zgcd_zmult)
   apply (simp add: zcong_cancel)
   done
 
 lemma card_nor_eq_noX:
-  "#0 < m ==>
-    zgcd (x, m) = #1 ==> card (noXRRset m x) = card (norRRset m)"
+  "Numeral0 < m ==>
+    zgcd (x, m) = Numeral1 ==> card (noXRRset m x) = card (norRRset m)"
   apply (unfold norRRset_def noXRRset_def)
   apply (rule card_image)
    apply (auto simp add: inj_on_def Bnor_fin)
   apply (simp add: BnorRset.simps)
   done
 
 lemma noX_is_RRset:
-    "#0 < m ==> zgcd (x, m) = #1 ==> is_RRset (noXRRset m x) m"
+    "Numeral0 < m ==> zgcd (x, m) = Numeral1 ==> is_RRset (noXRRset m x) m"
   apply (unfold is_RRset_def phi_def)
   apply (auto simp add: card_nor_eq_noX)
   apply (unfold noXRRset_def norRRset_def)
   apply (rule RsetR_zmult_mono)
     apply (rule Bnor_in_RsetR)
     apply simp_all
   done
 
 lemma aux_some:
-  "#1 < m ==> is_RRset A m ==> a \<in> A
+  "Numeral1 < m ==> is_RRset A m ==> a \<in> A
     ==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and>
       (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m"
   apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex])
    apply (rule_tac [2] RRset_gcd)
     apply simp_all
   done
 
 lemma RRset2norRR_correct:
-  "#1 < m ==> is_RRset A m ==> a \<in> A ==>
+  "Numeral1 < m ==> is_RRset A m ==> a \<in> A ==>
     [a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m"
   apply (unfold RRset2norRR_def)
   apply simp
   apply (rule aux_some)
     apply simp_all

   apply (erule RsetR.induct)
    apply auto
   done
 
 lemma RRset_zcong_eq [rule_format]:
-  "#1 < m ==>
+  "Numeral1 < m ==>
     is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
   apply (unfold is_RRset_def)
   apply (rule RsetR.induct)
     apply (auto simp add: zcong_sym)
   done

     (SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a"
   apply auto
   done
 
 lemma RRset2norRR_inj:
-    "#1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A"
+    "Numeral1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A"
   apply (unfold RRset2norRR_def inj_on_def)
   apply auto
   apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and>
       ([y = b] (mod m) \<and> b \<in> norRRset m)")
    apply (rule_tac [2] aux)

   apply (rule_tac b = b in zcong_trans)
    apply (simp_all add: zcong_sym)
   done
 
 lemma RRset2norRR_eq_norR:
-    "#1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m"
+    "Numeral1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m"
   apply (rule card_seteq)
     prefer 3
     apply (subst card_image)
       apply (rule_tac [2] RRset2norRR_inj)
        apply auto

   apply (unfold inj_on_def)
   apply auto
   done
 
 lemma Bnor_prod_power [rule_format]:
-  "x \<noteq> #0 ==> a < m --> setprod ((\<lambda>a. a * x) ` BnorRset (a, m)) =
+  "x \<noteq> Numeral0 ==> a < m --> setprod ((\<lambda>a. a * x) ` BnorRset (a, m)) =
       setprod (BnorRset(a, m)) * x^card (BnorRset (a, m))"
   apply (induct a m rule: BnorRset_induct)
    prefer 2
    apply (subst BnorRset.simps)
    apply (unfold Let_def)

    apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
     apply (auto intro: fin_bijRl fin_bijRr zcong_zmult)
   done
 
 lemma Bnor_prod_zgcd [rule_format]:
-    "a < m --> zgcd (setprod (BnorRset (a, m)), m) = #1"
+    "a < m --> zgcd (setprod (BnorRset (a, m)), m) = Numeral1"
   apply (induct a m rule: BnorRset_induct)
    prefer 2
    apply (subst BnorRset.simps)
    apply (unfold Let_def)
    apply auto
   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   apply (blast intro: zgcd_zgcd_zmult)
   done
 
 theorem Euler_Fermat:
-    "#0 < m ==> zgcd (x, m) = #1 ==> [x^(phi m) = #1] (mod m)"
+    "Numeral0 < m ==> zgcd (x, m) = Numeral1 ==> [x^(phi m) = Numeral1] (mod m)"
   apply (unfold norRRset_def phi_def)
-  apply (case_tac "x = #0")
-   apply (case_tac [2] "m = #1")
+  apply (case_tac "x = Numeral0")
+   apply (case_tac [2] "m = Numeral1")
     apply (rule_tac [3] iffD1)
-     apply (rule_tac [3] k = "setprod (BnorRset (m - #1, m))"
+     apply (rule_tac [3] k = "setprod (BnorRset (m - Numeral1, m))"
        in zcong_cancel2)
       prefer 5
       apply (subst Bnor_prod_power [symmetric])
         apply (rule_tac [7] Bnor_prod_zgcd)
         apply simp_all

   apply (rule Bnor_fin)
   done
 
 lemma Bnor_prime [rule_format (no_asm)]:
   "p \<in> zprime ==>
-    a < p --> (\<forall>b. #0 < b \<and> b \<le> a --> zgcd (b, p) = #1)
+    a < p --> (\<forall>b. Numeral0 < b \<and> b \<le> a --> zgcd (b, p) = Numeral1)
     --> card (BnorRset (a, p)) = nat a"
   apply (unfold zprime_def)
   apply (induct a p rule: BnorRset.induct)
   apply (subst BnorRset.simps)
   apply (unfold Let_def)
   apply auto
   done
 
-lemma phi_prime: "p \<in> zprime ==> phi p = nat (p - #1)"
+lemma phi_prime: "p \<in> zprime ==> phi p = nat (p - Numeral1)"
   apply (unfold phi_def norRRset_def)
   apply (rule Bnor_prime)
     apply auto
   apply (erule zless_zprime_imp_zrelprime)
    apply simp_all
   done
 
 theorem Little_Fermat:
-    "p \<in> zprime ==> \<not> p dvd x ==> [x^(nat (p - #1)) = #1] (mod p)"
+    "p \<in> zprime ==> \<not> p dvd x ==> [x^(nat (p - Numeral1)) = Numeral1] (mod p)"
   apply (subst phi_prime [symmetric])
    apply (rule_tac [2] Euler_Fermat)
     apply (erule_tac [3] zprime_imp_zrelprime)
     apply (unfold zprime_def)
     apply auto