fix(proofs): repair Isabelle/Mizar self-proof corpora for the weekly cron

Justfile

@@ -325,22 +325,30 @@ proofs-isabelle:
 # Verify the Mizar self-proof corpus (proofs/mizar) with the Mizar verifier.
 proofs-mizar:
     #!/usr/bin/env bash
-    set -euo pipefail
+    # Not -e: makeenv/verifier signal errors via a per-file .err (line col code),
+    # not a reliable exit code, so inspect that rather than abort on first non-zero.
+    set -uo pipefail
     : "${MIZFILES:?MIZFILES must point at the Mizar share dir}"
     cd proofs/mizar
     rc=0
     for f in *.miz; do
-        echo "=== makeenv + verifier $f ==="
-        makeenv "$f"
-        verifier "$f" || rc=1
-        errfile="${f%.miz}.err"
-        if [ -s "$errfile" ]; then
-            echo "Mizar errors in $f:" >&2
-            cat "$errfile" >&2
+        base="${f%.miz}"
+        echo "=== $f ==="
+        makeenv "$f" || echo "(makeenv exit $?)"
+        verifier "$f" || echo "(verifier exit $?)"
+        if [ -s "$base.err" ]; then
+            echo "--- $base.err (line col code) ---"
+            cat "$base.err"
+            while read -r line col code; do
+                src="$(sed -n "${line}p" "$f" 2>/dev/null)"
+                [ -n "$src" ] && echo "    L${line}:${col} (code ${code}): ${src}"
+            done < "$base.err"
             rc=1
+        else
+            echo "($f verifies clean)"
         fi
     done
-    if [ "$rc" -ne 0 ]; then echo "Mizar corpus: VERIFICATION ERRORS" >&2; exit 1; fi
+    [ "$rc" -eq 0 ] || { echo "Mizar corpus: VERIFICATION ERRORS (see .err above)" >&2; exit 1; }
     echo "Mizar corpus: all files verify"
 
 # Format code

proofs/isabelle/List.thy → proofs/isabelle/EchidnaList.thy

@@ -1,5 +1,5 @@
 (*
-  List.thy - List Proofs in Isabelle/HOL
+  EchidnaList.thy - List Proofs in Isabelle/HOL
 
   This theory demonstrates reasoning about lists:
   - Append properties
@@ -10,9 +10,12 @@
 
   Part of the ECHIDNA theorem proving platform
   Tier 1 Prover: Isabelle/HOL
+
+  NB: named EchidnaList (not List) so its fact names (append_assoc, length_append,
+  map_append, ...) do not collide with HOL's own theory List.
 *)
 
-theory List
+theory EchidnaList
   imports Main
 begin
 

proofs/isabelle/Nat.thy → proofs/isabelle/EchidnaNat.thy

@@ -1,5 +1,5 @@
 (*
-  Nat.thy - Natural Number Proofs in Isabelle/HOL
+  EchidnaNat.thy - Natural Number Proofs in Isabelle/HOL
 
   This theory demonstrates reasoning about natural numbers:
   - Arithmetic properties (addition, multiplication)
@@ -9,9 +9,14 @@
 
   Part of the ECHIDNA theorem proving platform
   Tier 1 Prover: Isabelle/HOL
+
+  NB: named EchidnaNat (not Nat) so fact names do not collide with HOL's own
+  theory Nat (e.g. Nat.le_refl). The three basic addition lemmas are annotated
+  :: nat so their goals are about natural numbers rather than an
+  under-constrained polymorphic {zero, plus} type that simp cannot discharge.
 *)
 
-theory Nat
+theory EchidnaNat
   imports Main
 begin
 
@@ -22,19 +27,19 @@ text \<open>
 \<close>
 
 lemma add_zero_left:
-  "0 + n = n"
+  "(0::nat) + n = n"
   by simp
 
 lemma add_zero_right:
-  "n + 0 = n"
+  "(n::nat) + 0 = n"
   by simp
 
 text \<open>
   Addition is commutative.
 \<close>
 
 lemma add_comm:
-  "m + n = n + m"
+  "(m::nat) + n = n + m"
   by simp
 
 text \<open>

proofs/isabelle/ROOT

@@ -4,7 +4,11 @@
 
   Gated by `just proofs-isabelle` and the weekly verification-proofs-cron
   workflow. Covers the base-HOL theories that type-check on the current
-  Isabelle release (confirmed green on Isabelle2025-2).
+  Isabelle release (Isabelle2025-2).
+
+  Nat and List were renamed to EchidnaNat / EchidnaList: a theory named Nat or
+  List collides with HOL's own theories of those names (duplicate fact
+  declarations such as Nat.le_refl / List.append_assoc).
 
   NOTE: algebra/GroupTheory.thy is intentionally NOT in a gated session. It is
   "ML training corpus" material (per its own header) that does not verify on
@@ -18,6 +22,6 @@ session "Echidna_Isabelle" = "HOL" +
   description \<open>ECHIDNA Isabelle/HOL self-proof corpus (base HOL).\<close>
   theories
     Basic
-    List
-    Nat
+    EchidnaList
+    EchidnaNat
     Propositional