fixed some Isabelle errors reported by Yutaka and Daniel

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

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
 

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

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
 

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
 

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