From 494bd8721123d002ef1e7f68abfa019b0bcc5a64 Mon Sep 17 00:00:00 2001
From: liwenda1990 <liwenda1990@hotmail.com>
Date: Tue, 27 Sep 2022 16:11:30 +0100
Subject: [PATCH 1/2] fixed some Isabelle errors reported by Yutaka and Daniel

---
 isabelle/test/amc12a_2020_p4.thy         | 12 ++++++------
 isabelle/test/amc12b_2021_p18.thy        |  4 ++--
 isabelle/test/amc12b_2021_p4.thy         |  4 ++--
 isabelle/test/imo_1974_p3.thy            |  6 ++++++
 isabelle/test/mathd_numbertheory_135.thy |  9 ++++++++-
 isabelle/test/mathd_numbertheory_321.thy |  2 +-
 isabelle/test/mathd_numbertheory_447.thy |  2 +-
 7 files changed, 26 insertions(+), 13 deletions(-)

diff --git a/isabelle/test/amc12a_2020_p4.thy b/isabelle/test/amc12a_2020_p4.thy
index bf7a1d8..238a5b1 100644
--- a/isabelle/test/amc12a_2020_p4.thy
+++ b/isabelle/test/amc12a_2020_p4.thy
@@ -6,13 +6,13 @@ theory amc12a_2020_p4
   imports Complex_Main 
 begin
 
+function digits :: "nat \<Rightarrow> nat list" where 
+  "digits n = (if n div 10 = 0 then [n] else (n mod 10) # (digits (n div 10)))"
+  by auto
+termination by (relation "measure id") auto
+
 theorem amc12a_2020_p4:
-  fixes a b c d :: nat
-  assumes h0: "1 \<le> a \<and> a \<le> 9 \<and> even a"
-    and h1: "0 \<le> b \<and> b \<le> 9 \<and> even b"
-    and h2: "0 \<le> c \<and> c \<le> 9 \<and> even c"
-    and h3: "0 \<le> d \<and> d \<le> 9 \<and> even d"
-  shows "card {n :: nat. n = 10 * (10*(10*a + b) + c) + d \<and> 5 dvd n} = 100"
+  shows "card {n :: nat. 1000\<le>n \<and> n\<le>9999 \<and> (\<forall>d\<in>set (digits n). even d) \<and> 5 dvd n} = 100"
   sorry
 
 end
diff --git a/isabelle/test/amc12b_2021_p18.thy b/isabelle/test/amc12b_2021_p18.thy
index d942358..c2e6d07 100644
--- a/isabelle/test/amc12b_2021_p18.thy
+++ b/isabelle/test/amc12b_2021_p18.thy
@@ -8,8 +8,8 @@ begin
 
 theorem amc12b_2021_p18:
   fixes z :: complex
-  assumes h0: "12 * norm z = 2 * 
-      norm (z + 2) + norm (z^2 + 1) + 31"
+  assumes h0: "12 * (norm z)^2 = 2 * 
+      (norm (z + 2))^2 + (norm (z^2 + 1))^2 + 31"
   shows "z + 6 / z = -2"
   sorry
 
diff --git a/isabelle/test/amc12b_2021_p4.thy b/isabelle/test/amc12b_2021_p4.thy
index 6ffb79a..8a6d017 100644
--- a/isabelle/test/amc12b_2021_p4.thy
+++ b/isabelle/test/amc12b_2021_p4.thy
@@ -8,8 +8,8 @@ begin
 
 theorem amc12b_2021_p4:
   fixes m a :: nat
-  assumes h0: "m / a = 3 / (4::real)" 
-  shows "84 * m + 70 * a / (m + a) = (76::real)" 
+  assumes h0: "of_nat m / of_nat a = 3 / (4::real)" 
+  shows "(84 * m + 70 * a) / (m + a) = (76::real)" 
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/test/imo_1974_p3.thy b/isabelle/test/imo_1974_p3.thy
index 6b6da59..fbf5de8 100644
--- a/isabelle/test/imo_1974_p3.thy
+++ b/isabelle/test/imo_1974_p3.thy
@@ -7,6 +7,12 @@ theory imo_1974_p3
   "HOL-Number_Theory.Number_Theory"
 begin
 
+lemma 
+  assumes "n=0"
+  shows "(\<Sum> k < n. ( (2 * n + 1) choose
+          (2 * k + 1)) * (2^(3 * k))) = 0"
+  using assms by auto
+
 theorem imo_1974_p3:
   fixes n ::nat 
   shows "\<not> 5 dvd (\<Sum> k < n. ( (2 * n + 1) choose
diff --git a/isabelle/test/mathd_numbertheory_135.thy b/isabelle/test/mathd_numbertheory_135.thy
index 06056b9..43bbab4 100644
--- a/isabelle/test/mathd_numbertheory_135.thy
+++ b/isabelle/test/mathd_numbertheory_135.thy
@@ -6,13 +6,20 @@ theory mathd_numbertheory_135
   imports Complex_Main "HOL-Computational_Algebra.Computational_Algebra"
 begin
 
+function digits :: "nat \<Rightarrow> nat list" where 
+  "digits n = (if n div 10 = 0 then [n] else (n mod 10) # (digits (n div 10)))"
+  by auto
+termination by (relation "measure id") auto
+
 theorem mathd_numbertheory_135:
   fixes n a b c::nat
   assumes "n = 3^17 + 3^10"
     and "11 dvd (n + 1)"
+    and "a\<noteq>b" "b\<noteq>c" "a\<noteq>c"
+    and "a\<in>{0..9}" "b\<in>{0..9}" "c\<in>{0..9}" 
     and "odd a \<and> odd c"
     and "\<not> 3 dvd b"
-    and "n = 10*(10*(10*(10*(10*(10*(10*(10*a +b) +c) +a) +c) +c) +b) +a) +b" 
+    and "digits n = [b,a,b,c,d,a,c,b,a]" 
   shows "10*(10 * a + b) + c = 129"
   sorry
 
diff --git a/isabelle/test/mathd_numbertheory_321.thy b/isabelle/test/mathd_numbertheory_321.thy
index 3470865..78cfd87 100644
--- a/isabelle/test/mathd_numbertheory_321.thy
+++ b/isabelle/test/mathd_numbertheory_321.thy
@@ -9,7 +9,7 @@ begin
 
 theorem mathd_numbertheory_321:
   fixes n::int
-  assumes "\<forall>n::int. 1\<le>n \<and> n\<le> 1399 \<and> [n*160 = 1] (mod 1399)"
+  assumes "1\<le>n \<and> n\<le> 1399 \<and> [n*160 = 1] (mod 1399)"
   shows "n = 1058"
   sorry
 
diff --git a/isabelle/test/mathd_numbertheory_447.thy b/isabelle/test/mathd_numbertheory_447.thy
index 9e2c216..c1d3253 100644
--- a/isabelle/test/mathd_numbertheory_447.thy
+++ b/isabelle/test/mathd_numbertheory_447.thy
@@ -8,7 +8,7 @@ theory mathd_numbertheory_447 imports
 begin
 
 theorem mathd_numbertheory_447:
-  "(\<Sum> k \<in>{n. 3 dvd n \<and> 0<n \<and> n<50}. k mod 3) = (78::nat)"
+  "(\<Sum> k \<in>{n. 3 dvd n \<and> 0<n \<and> n<50}. k mod 10) = (78::nat)"
   sorry
 
 end
\ No newline at end of file

From b175389ab7d64fc1d083203ea70aa6a9b88836f5 Mon Sep 17 00:00:00 2001
From: liwenda1990 <liwenda1990@hotmail.com>
Date: Tue, 27 Sep 2022 16:33:20 +0100
Subject: [PATCH 2/2] reverted changes in imo_1974_p3

---
 isabelle/test/imo_1974_p3.thy | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/isabelle/test/imo_1974_p3.thy b/isabelle/test/imo_1974_p3.thy
index fbf5de8..6b6da59 100644
--- a/isabelle/test/imo_1974_p3.thy
+++ b/isabelle/test/imo_1974_p3.thy
@@ -7,12 +7,6 @@ theory imo_1974_p3
   "HOL-Number_Theory.Number_Theory"
 begin
 
-lemma 
-  assumes "n=0"
-  shows "(\<Sum> k < n. ( (2 * n + 1) choose
-          (2 * k + 1)) * (2^(3 * k))) = 0"
-  using assms by auto
-
 theorem imo_1974_p3:
   fixes n ::nat 
   shows "\<not> 5 dvd (\<Sum> k < n. ( (2 * n + 1) choose