fix(proofs): finish Isabelle base corpus repair (polymorphic nat/list lemmas) (#279)

## What

Completes the **Isabelle base corpus** repair so the
`verification-proofs-cron`
Isabelle job goes green. Follow-up to #278 (theory renames + first
annotations).

Run #5 on Isabelle2025-2 gave the complete remaining failure list; this
annotates
exactly those lemmas:

- **EchidnaNat**: `add_assoc`, `add_zero_right_inductive` (induction
couldn't pick a
rule on a polymorphic `n`), `mult_zero_left/right`,
`mult_one_left/right`,
`mult_comm` — all under-constrained over `{zero,plus,times}`; annotated
`:: nat`.
- **EchidnaList**: `map_rev` — HOL's simpset orients `rev_map` the other
way, so
  `by simp` couldn't close it → `by (simp add: rev_map)`.

With these, the four base theories (Basic, EchidnaList, EchidnaNat,
Propositional)
verify on Isabelle2025-2.

## Honest status on the rest

- **GroupTheory.thy** — still excluded. Genuine math bugs (lemmas omit
`assumes "group G"` then use `assms`; `center_closed` uses
`group.m_comm`, valid
  only for `comm_group`). Needs real, tested HOL-Algebra work.
- **Mizar** — install fully works; but the `.miz` files have genuine,
heterogeneous
  verification errors (`propositional.miz`: 24 errors, all the
`thus A c= B; thus B c= A` set-equality skeleton; `basic.miz`: a
`makeenv`
  error). These are broken corpus files, not config.

I'll follow up on those (see my message). Verified on GitHub runners
since
`isabelle.in.tum.de` is `403`-blocked from the dev sandbox.

🤖 Generated with [Claude Code](https://claude.com/claude-code)


---
_Generated by [Claude
Code](https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

proofs/isabelle/EchidnaList.thy

@@ -248,7 +248,7 @@ text \<open>
 
 lemma map_rev:
   "map f (rev xs) = rev (map f xs)"
-  by simp
+  by (simp add: rev_map)
 
 section \<open>Filter Function\<close>
 

proofs/isabelle/EchidnaNat.thy

@@ -47,15 +47,15 @@ text \<open>
 \<close>
 
 lemma add_assoc:
-  "(m + n) + p = m + (n + p)"
+  "((m::nat) + n) + p = m + (n + p)"
   by simp
 
 text \<open>
   Explicit inductive proof of right zero for addition.
 \<close>
 
 lemma add_zero_right_inductive:
-  shows "n + 0 = n"
+  shows "(n::nat) + 0 = n"
 proof (induction n)
   case 0
   show ?case by simp
@@ -71,31 +71,31 @@ text \<open>
 \<close>
 
 lemma mult_zero_left:
-  "0 * n = 0"
+  "(0::nat) * n = 0"
   by simp
 
 lemma mult_zero_right:
-  "n * 0 = 0"
+  "(n::nat) * 0 = 0"
   by simp
 
 text \<open>
   Multiplication with one (identity).
 \<close>
 
 lemma mult_one_left:
-  "1 * n = n"
+  "(1::nat) * n = n"
   by simp
 
 lemma mult_one_right:
-  "n * 1 = n"
+  "(n::nat) * 1 = n"
   by simp
 
 text \<open>
   Multiplication is commutative.
 \<close>
 
 lemma mult_comm:
-  "m * n = n * m"
+  "(m::nat) * n = n * m"
   by simp
 
 text \<open>