fix(proofs): comprehensively nat-annotate EchidnaNat to green the Isabelle base

proofs/isabelle/EchidnaNat.thy

@@ -194,27 +194,27 @@ text \<open>
 \<close>
 
 lemma power_zero:
-  "n ^ 0 = 1"
+  "(n::nat) ^ 0 = 1"
   by simp
 
 lemma power_one:
-  "n ^ 1 = n"
+  "(n::nat) ^ 1 = n"
   by simp
 
 lemma power_add:
-  "n ^ (m + p) = n ^ m * n ^ p"
+  "(n::nat) ^ (m + p) = n ^ m * n ^ p"
   by (simp add: power_add)
 
 lemma power_mult:
-  "n ^ (m * p) = (n ^ m) ^ p"
+  "(n::nat) ^ (m * p) = (n ^ m) ^ p"
   by (simp add: power_mult)
 
 text \<open>
   Explicit inductive proof for power addition law.
 \<close>
 
 lemma power_add_inductive:
-  shows "n ^ (m + p) = n ^ m * n ^ p"
+  shows "(n::nat) ^ (m + p) = n ^ m * n ^ p"
 proof (induction m)
   case 0
   show ?case by simp
@@ -240,31 +240,31 @@ text \<open>
 \<close>
 
 lemma le_refl:
-  "n \<le> n"
+  "(n::nat) \<le> n"
   by simp
 
 lemma le_trans:
-  "m \<le> n \<Longrightarrow> n \<le> p \<Longrightarrow> m \<le> p"
+  "(m::nat) \<le> n \<Longrightarrow> n \<le> p \<Longrightarrow> m \<le> p"
   by simp
 
 lemma le_antisym:
-  "m \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n"
+  "(m::nat) \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n"
   by simp
 
 text \<open>
   Strict ordering properties.
 \<close>
 
 lemma less_irrefl:
-  "\<not>(n < n)"
+  "\<not>((n::nat) < n)"
   by simp
 
 lemma less_trans:
-  "m < n \<Longrightarrow> n < p \<Longrightarrow> m < p"
+  "(m::nat) < n \<Longrightarrow> n < p \<Longrightarrow> m < p"
   by simp
 
 lemma less_imp_le:
-  "m < n \<Longrightarrow> m \<le> n"
+  "(m::nat) < n \<Longrightarrow> m \<le> n"
   by simp
 
 text \<open>
@@ -290,23 +290,23 @@ text \<open>
 \<close>
 
 lemma add_le_mono:
-  "m \<le> n \<Longrightarrow> m + p \<le> n + p"
+  "(m::nat) \<le> n \<Longrightarrow> m + p \<le> n + p"
   by simp
 
 lemma add_less_mono:
-  "m < n \<Longrightarrow> m + p < n + p"
+  "(m::nat) < n \<Longrightarrow> m + p < n + p"
   by simp
 
 text \<open>
   Cancellation laws for addition.
 \<close>
 
 lemma add_left_cancel:
-  "p + m = p + n \<longleftrightarrow> m = n"
+  "(p::nat) + m = p + n \<longleftrightarrow> m = n"
   by simp
 
 lemma add_right_cancel:
-  "m + p = n + p \<longleftrightarrow> m = n"
+  "(m::nat) + p = n + p \<longleftrightarrow> m = n"
   by simp
 
 section \<open>Division and Modulo\<close>
@@ -316,27 +316,27 @@ text \<open>
 \<close>
 
 lemma div_mult_self:
-  "n > 0 \<Longrightarrow> (m * n) div n = m"
+  "(n::nat) > 0 \<Longrightarrow> (m * n) div n = m"
   by simp
 
 lemma mod_mult_self:
-  "n > 0 \<Longrightarrow> (m * n) mod n = 0"
+  "(n::nat) > 0 \<Longrightarrow> (m * n) mod n = 0"
   by simp
 
 lemma div_less:
-  "m < n \<Longrightarrow> n > 0 \<Longrightarrow> m div n = 0"
+  "(m::nat) < n \<Longrightarrow> n > 0 \<Longrightarrow> m div n = 0"
   by simp
 
 lemma mod_less:
-  "m < n \<Longrightarrow> n > 0 \<Longrightarrow> m mod n = m"
+  "(m::nat) < n \<Longrightarrow> n > 0 \<Longrightarrow> m mod n = m"
   by simp
 
 text \<open>
   Division-modulo identity.
 \<close>
 
 lemma div_mod_equality:
-  "n > 0 \<Longrightarrow> (m div n) * n + m mod n = m"
+  "(n::nat) > 0 \<Longrightarrow> (m div n) * n + m mod n = m"
   by simp
 
 section \<open>Even and Odd\<close>
@@ -346,31 +346,31 @@ text \<open>
 \<close>
 
 lemma even_zero:
-  "even 0"
+  "even (0::nat)"
   by simp
 
 lemma even_double:
-  "even (2 * n)"
+  "even (2 * (n::nat))"
   by simp
 
 lemma even_succ_succ:
-  "even n \<longleftrightarrow> even (Suc (Suc n))"
+  "even (n::nat) \<longleftrightarrow> even (Suc (Suc n))"
   by simp
 
 text \<open>
   Sum of two even numbers is even.
 \<close>
 
 lemma even_add:
-  "even m \<Longrightarrow> even n \<Longrightarrow> even (m + n)"
+  "even (m::nat) \<Longrightarrow> even n \<Longrightarrow> even (m + n)"
   by simp
 
 text \<open>
   Product involving an even number is even.
 \<close>
 
 lemma even_mult:
-  "even m \<or> even n \<Longrightarrow> even (m * n)"
+  "even (m::nat) \<or> even n \<Longrightarrow> even (m * n)"
   by auto
 
 section \<open>Strong Induction\<close>
@@ -382,8 +382,8 @@ text \<open>
 \<close>
 
 lemma strong_induction_example:
-  assumes "\<And>n. (\<forall>m. m < n \<longrightarrow> P m) \<Longrightarrow> P n"
-  shows "P n"
+  assumes "\<And>k::nat. (\<forall>m. m < k \<longrightarrow> P m) \<Longrightarrow> P k"
+  shows "P (n::nat)"
 proof -
   have "\<forall>m. m \<le> n \<longrightarrow> P m"
   proof (induction n)