Fix the proof of zagier_fix in experimental kernel.

HOL-Theorem-Prover · Aug 17, 2023 · c505f57 · c505f57
1 parent fada2db
commit c505f57
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/examples/fermat/twosq/windmillScript.sml b/examples/fermat/twosq/windmillScript.sml
@@ -1354,9 +1354,11 @@ Theorem zagier_fixes:
   !n. n MOD 4 <> 0 ==> fixes zagier (mills n) = {(x,x,z) | n = windmill (x,x,z)}
 Proof
   rw[fixes_def, mills_def, EXTENSION, EQ_IMP_THM] >| [
-    `x' <> 0` by metis_tac[windmill_with_no_mind] >>
+    rename1 `windmill (x,y,z)` >>
+    `x <> 0` by metis_tac[windmill_with_no_mind] >>
     fs[zagier_fix, windmill_def],
-    `x' <> 0` by metis_tac[windmill_with_no_mind] >>
+    rename1 `windmill (x,x,z)` >>
+    `x <> 0` by metis_tac[windmill_with_no_mind] >>
     simp[zagier_fix]
   ]
 QED