Merge pull request #200 from trishullab/john

Coq and Isabelle 1987-1990 fixes

coq/src/putnam_1987_a3.v

@@ -2,8 +2,10 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1987_a3_solution := (False, True).
 Theorem putnam_1987_a3
-    (f g: R -> R) 
-    (x: R)
-    : (((Derive_n f 2) x - 2 * (Derive_n f 1) x + f x = 2 * exp x /\ forall (x: R), f x > 0 -> forall (x: R), Derive_n f 1 x > 0) <-> fst putnam_1987_a3_solution) /\ 
-    ((((Derive_n g 2) x - 2 * (Derive_n g 1) x + g x = 2 * exp x /\ forall (x: R), Derive_n g 1 x > 0) -> forall (x: R), g x > 0) <-> snd putnam_1987_a3_solution).
+    : ((forall (f: R -> R), (forall (x: R), ex_derive_n f 1 x /\ ex_derive_n f 2 x /\ (Derive_n f 2) x - 2 * (Derive_n f 1) x + f x = 2 * exp x /\ f x > 0) 
+            -> forall (x: R), Derive_n f 1 x > 0) 
+        <-> fst putnam_1987_a3_solution) /\ 
+    ((forall (g: R -> R), (forall (x: R), ex_derive_n g 1 x /\ ex_derive_n g 2 x /\ (Derive_n g 2) x - 2 * (Derive_n g 1) x + g x = 2 * exp x /\ Derive_n g 1 x > 0) 
+            -> forall (x: R), g x > 0) 
+        <-> snd putnam_1987_a3_solution).
 Proof. Admitted.

coq/src/putnam_1987_b4.v

@@ -1,16 +1,17 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1987_b4_solution := (-1, PI).
+Definition putnam_1987_b4_solution := (True, -1, True, 0).
 Theorem putnam_1987_b4
-    (A := fix a (i j: nat) : (R * R):=
-        match (i, j) with
-        | (O, O) => (0.8, 0.6)
-        | (S i', S j') => 
-            let xn := fst (a i' j') in 
-            let yn := snd (a i' j') in 
-            (xn * cos yn - yn * sin yn,xn * sin yn + yn * cos yn)
-        | (_, _) => (0, 0)
+    (A := fix a (n: nat) : (R * R) :=
+        match n with
+        | O => (0.8, 0.6)
+        | (S n') => 
+            let (xn, yn) := a n' in
+            (xn * cos yn - yn * sin yn, xn * sin yn + yn * cos yn)
     end)
-    : Lim_seq (fun n => fst (A n 0%nat)) = fst putnam_1987_b4_solution /\
-    Lim_seq (fun n => snd (A 0%nat n)) = snd putnam_1987_b4_solution.
+    : let '(existsx, limx, existsy, limy) := putnam_1987_b4_solution in
+    (ex_lim_seq (fun n => fst (A n)) <-> existsx) /\
+    (existsx -> Lim_seq (fun n => fst (A n)) = limx) /\
+    (ex_lim_seq (fun n => snd (A n)) <-> existsy) /\
+    (existsy -> Lim_seq (fun n => snd (A n)) = limy).
 Proof. Admitted.

coq/src/putnam_1988_a2.v

@@ -4,7 +4,8 @@ Open Scope R.
 Definition putnam_1988_a2_solution := True.
 Theorem putnam_1988_a2
     (f : R -> R := fun x => exp (pow x 2))
-    : exists (a b: R) (g: R -> R), 
-    forall (x: R), a < x < b -> Derive (compose f g) = compose (Derive f) (Derive g)
+    : (exists (a b: R) (g: R -> R), a < b /\ 
+    (exists x: R, a < x < b /\ g x <> 0) /\
+    forall (x: R), a < x < b -> ex_derive g x /\ Derive (fun y => f y * g y) x = (Derive f x) * (Derive g x))
     <-> putnam_1988_a2_solution.
 Proof. Admitted.

coq/src/putnam_1988_a3.v

@@ -2,5 +2,5 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1988_a3_solution (a: R) := a > 1/2.
 Theorem putnam_1988_a3
-   : forall (a: R), ex_finite_lim_seq (fun m => sum_n (fun n => Rpower (1/INR n * (1 / sin (1/INR n) - 1)) a) m) <-> putnam_1988_a3_solution a.
+   : forall (a: R), ex_finite_lim_seq (fun m => sum_n_m (fun n => Rpower (1/INR n * (1 / sin (1/INR n)) - 1) a) 1 m) <-> putnam_1988_a3_solution a.
 Proof. Admitted.

coq/src/putnam_1988_a4.v

@@ -1,6 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot. From mathcomp Require Import fintype.
 Definition putnam_1988_a4_solution : Prop * Prop := (True, False).
 Theorem putnam_1988_a4
-    (p : nat -> Prop := fun n : nat =>  (forall color : (R * R) -> 'I_n, exists p q : R * R, color p = color q /\ norm (fst p - fst q, snd p - snd q) = 1))
+    (p : nat -> Prop := fun n : nat => (forall color : (R * R) -> 'I_n, exists p q : R * R, color p = color q /\ norm (fst p - fst q, snd p - snd q) = 1))
     : let (a, b) := putnam_1988_a4_solution in ((p 3%nat) <-> a) /\ ((p 9%nat) <-> b).
-Proof. Admitted.
+Proof. Admitted.

coq/src/putnam_1988_a5.v

@@ -2,6 +2,7 @@ Require Import Basics Reals.
 Open Scope R.
 Theorem putnam_1988_a5
     : exists! (f: R -> R), 
-    forall (x: R), (x > 0 -> f x > 0) ->
-    (compose f f) x = 6 * x - f x.
+    (forall (x: R), x <= 0 -> f x = 0) /\
+    forall (x: R), x > 0 -> 
+    (f x > 0 /\ (compose f f) x = 6 * x - f x).
 Proof. Admitted.

coq/src/putnam_1988_b2.v

@@ -2,6 +2,6 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1988_b2_solution := True.
 Theorem putnam_1988_b2
-    : forall (a: R), a >= 0 -> forall (x: R), pow (x + 1) 2 >= a * (a + 1) ->
-    pow x 2 >= a * (a - 1) <-> putnam_1988_b2_solution.
+    : (forall (a: R), a >= 0 -> forall (x: R), pow (x + 1) 2 >= a * (a + 1) ->
+    pow x 2 >= a * (a - 1)) <-> putnam_1988_b2_solution.
 Proof. Admitted.

coq/src/putnam_1988_b3.v

@@ -2,6 +2,6 @@ Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_1988_b3_solution := (1 + sqrt 3) / 2.
 Theorem putnam_1988_b3
     (r : Z -> R)
-    (hr : forall (n: Z), Z.ge n 1 -> (exists c d : Z, (Z.ge c 0 /\ Z.ge d 0) /\ Z.eq (Z.add c d) n /\ r n = Rabs (IZR c - IZR d * sqrt 3)) /\ (forall c d : Z, (Z.ge c 0 /\ Z.ge d 0 /\ (Z.add c d) = n) -> Rabs (IZR c - IZR d * sqrt 3) >= r n))
-    : putnam_1988_b3_solution > 0 /\ (forall n : Z, Z.ge n 1 -> r n <= putnam_1988_b3_solution) /\ (forall (g: R), g > 0 -> (forall (n: Z), Z.ge n 1 /\ r n <= g) -> g >= putnam_1988_b3_solution).
+    (hr : forall (n: Z), Z.ge n 1 -> (exists c d : Z, Z.ge c 0 /\ Z.ge d 0 /\ (Z.add c d) = n /\ r n = Rabs (IZR c - IZR d * sqrt 3)) /\ (forall c d : Z, (Z.ge c 0 /\ Z.ge d 0 /\ (Z.add c d) = n) -> Rabs (IZR c - IZR d * sqrt 3) >= r n))
+    : putnam_1988_b3_solution > 0 /\ (forall n : Z, Z.ge n 1 -> r n <= putnam_1988_b3_solution) /\ (forall (g: R), g > 0 -> (forall (n: Z), Z.ge n 1 -> r n <= g) -> g >= putnam_1988_b3_solution).
 Proof. Admitted.

coq/src/putnam_1988_b4.v

@@ -1,7 +1,9 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1988_b4
-    (b : nat -> (nat -> R) -> R := fun n a => Rpower (a n) (INR n/(INR n + 1)))
-    : forall (a: nat -> R), (forall (n: nat), a n > 0) ->
-    ex_finite_lim_seq (fun n => sum_n a n) -> ex_finite_lim_seq (fun n => sum_n (fun m => (b m a)) n).
+    (a : nat -> R)
+    (appos : (nat -> R) -> Prop := fun a' : nat -> R => forall n : nat, ge n 1 -> a' n > 0)
+    (apconv : (nat -> R) -> Prop := fun a' : nat -> R => ex_finite_lim_seq (fun N => sum_n_m a' 1 N))
+    (apposconv : (nat -> R) -> Prop := fun a' => appos a' /\ apconv a')
+    : apposconv a -> apposconv (fun n => Rpower (a n) (INR n/(INR n + 1))).
 Proof. Admitted.

coq/src/putnam_1988_b6.v

@@ -1,6 +1,7 @@
-Require Import Ensembles Finite_sets.
+Require Import Ensembles Finite_sets ZArith.
+Open Scope Z.
 Theorem putnam_1988_b6
-    (triangular : nat -> Prop := fun n => exists (m: nat), n = Nat.div (m * (m + 1)) 2)
-    (E: Ensemble (nat*nat) := fun '(a, b) => exists (m: nat), triangular m <-> triangular (Nat.mul a m + b))
-    : ~ exists (n: nat), cardinal (nat*nat) E n.
+    (triangular : Z -> Prop := fun n => exists (m: Z), m >= 0 /\ n = (m * (m + 1)) / 2)
+    (E: Ensemble (Z*Z) := fun '(a, b) => forall (m: Z), m > 0 -> (triangular m <-> triangular (Z.mul a m + b)))
+    : ~ exists (n: nat), cardinal (Z*Z) E n.
 Proof. Admitted.

coq/src/putnam_1989_a1.v

@@ -1,7 +1,7 @@
-Require Import Nat Reals ZArith Znumtheory Coquelicot.Coquelicot.
+Require Import Nat Reals ZArith Znumtheory Coquelicot.Coquelicot Finite_sets.
 Open Scope R.
-Definition putnam_1989_a1_solution (x: R) := x = INR 101.
+Definition putnam_1989_a1_solution := 1%nat.
 Theorem putnam_1989_a1
-    (a : nat -> R := fun n => sum_n (fun n => if odd n then INR (10^(n-1)) else R0) (2*n+2))
-    : forall (n: nat), prime (floor (a n)) -> putnam_1989_a1_solution (a n).
+    (a : nat -> R := fun n => sum_n (fun i => if odd i then INR (10^(i-1)) else R0) (2*n+2))
+    : cardinal nat (fun n => prime (floor (a n))) putnam_1989_a1_solution.
 Proof. Admitted.

coq/src/putnam_1989_a2.v

@@ -3,6 +3,7 @@ Open Scope R.
 Definition putnam_1989_a2_solution (a b: R) := (exp (pow (a*b) 2) - 1)/(a * b).
 Theorem putnam_1989_a2
     (a b: R)
+    (abpos : a > 0 /\ b > 0)
     (f : R -> R -> R := fun x y => Rmax (pow (b*x) 2) (pow (a*y) 2))
     : RInt (fun x => (RInt (fun y => exp (f x y)) 0 b)) 0 a = putnam_1989_a2_solution a b.
 Proof. Admitted.

coq/src/putnam_1989_a3.v

@@ -2,5 +2,5 @@ Require Import Reals Coquelicot.Coquelicot. From Coqtail Require Import Cpow.
 Open Scope C.
 Theorem putnam_1989_a3
     (f : C -> C := fun z => 11 * Cpow z 10 + 10 * Ci * Cpow z 9 + 10 * Ci * z - 11)
-    : forall (x: C), f x = 0 <-> Cmod x = R1.
+    : forall (x: C), f x = 0 -> Cmod x = R1.
 Proof. Admitted.

coq/src/putnam_1990_a1.v

@@ -8,6 +8,5 @@ Theorem putnam_1990_a1
         | S (S O) => 6
         | S (S (S n''' as n'') as n') => (n + 4) * a n' - 4 * n * a n'' + (4 * n - 8) * a n'''
     end)
-    : exists (b c: nat -> nat), forall (n: nat), A n = b n + c n <->
-    (b,c) = putnam_1990_a1_solution. 
+    : let (b,c) := putnam_1990_a1_solution in forall (n: nat), A n = b n + c n.
 Proof. Admitted.

coq/src/putnam_1990_a2.v

@@ -2,6 +2,6 @@ Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Definition putnam_1990_a2_solution := True.
 Theorem putnam_1990_a2
-    (numform : R -> Prop := fun x => exists (n m: nat), x = pow (INR n) (1/3) - pow (INR m) (1/3))
-    : exists (s: nat -> R), forall (i: nat), numform (s i) /\ Lim_seq s = sqrt 2 <-> putnam_1990_a2_solution.
-Proof. Admitted.
+    (numform : R -> Prop := fun x => exists (n m: nat), x = Rpower (INR n) (1/3) - Rpower (INR m) (1/3))
+    : (exists (s: nat -> R), (forall (i: nat), numform (s i)) /\ is_lim_seq s (sqrt 2)) <-> putnam_1990_a2_solution.
+Proof. Admitted.

coq/src/putnam_1990_a5.v

@@ -1,9 +1,6 @@
 From mathcomp Require Import matrix ssralg.
 Open Scope ring_scope.
+Definition putnam_1990_a5_solution := False.
 Theorem putnam_1990_a5 
-    (R : ringType) 
-    (n : nat) 
-    (A B : 'M[R]_n) 
-    : mulmx (mulmx (mulmx A B) A) B = 0 ->
-    mulmx (mulmx (mulmx B A) B) A = 0.
+    : (forall (R : ringType) (n: nat) (A B : 'M[R]_n), n >= 1 -> mulmx (mulmx (mulmx A B) A) B = 0 -> mulmx (mulmx (mulmx B A) B) A = 0) <-> putnam_1990_a5_solution.
 Proof. Admitted.

coq/src/putnam_1990_b1.v

@@ -1,9 +1,9 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
-Definition putnam_1990_b1_solution (f: R -> R) := f = (fun x => sqrt 1990 * exp x) /\ f = (fun x => -sqrt 1990 * exp x).
+Definition putnam_1990_b1_solution (f: R -> R) := f = (fun x => sqrt 1990 * exp x) \/ f = (fun x => -sqrt 1990 * exp x).
 Theorem putnam_1990_b1
     (f : R -> R)
-    : continuity f /\ forall x, ex_derive_n f 1 x -> 
-    forall x, pow (f x) 2 = RInt (fun t => pow (f t) 2 + pow ((Derive f) t) 2) 0 x + 1990 ->
+    (fderiv : (forall x : R, ex_derive f x) /\ continuity (Derive f))
+    : (forall x, pow (f x) 2 = RInt (fun t => pow (f t) 2 + pow ((Derive f) t) 2) 0 x + 1990) <->
     putnam_1990_b1_solution f.
 Proof. Admitted.

coq/src/putnam_1990_b2.v

@@ -1,8 +1,13 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1990_b2 
+    (prod_n : (nat -> R) -> nat -> R := fix P (a: nat -> R) (n : nat) : R := 
+        match n with 
+        | O => 1
+        | S n' => a n' * P a n'
+    end)
     (x z : R)
     (hxz : Rabs x < 1 /\ Rabs z > 1)
-    (P : nat -> R := fun j => (sum_n (fun i => 1 - z * x ^ i) j) / (sum_n (fun i => z - x ^ i) j+1))
-    : 1 + Series (fun j => 1 + x ^ (j+1) * P j) = 0.
+    (P : nat -> R := fun j => (prod_n (fun i => 1 - z * x ^ i) j) / (prod_n (fun i => z - x ^ (i + 1)) j))
+    : 1 + Series (fun j => (1 + x ^ (j+1)) * P (j+1)%nat) = 0.
 Proof. Admitted.

coq/src/putnam_1990_b3.v

@@ -1,14 +1,9 @@
 Require Import Ensembles Finite_sets Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_1990_b3
-    (Mmult_n :=
-    fix Mmult_n {T : Ring} (A : matrix 2 2) (p : nat) :=
-        match p with
-        | O => A
-        | S p' => @Mmult T 2 2 2 A (Mmult_n A p')
-    end)
-    (E : Ensemble (matrix 2 2) := fun (A: matrix 2 2) => 
+    (E : Ensemble (matrix 2 2))
+    (hE : forall (A: matrix 2 2), E A -> 
         forall (i j: nat), and (le 0 i) (lt i 2) /\ and (le 0 j) (lt j 2) -> 
         (coeff_mat 0 A i j) <= 200 /\ exists (m: nat), coeff_mat 0 A i j = INR m ^ 2)
-    : exists (sz : nat), gt sz 50387 /\ cardinal (matrix 2 2) E sz -> exists (A B: matrix 2 2), E A /\ E B /\ Mmult A B = Mmult B A.
+    : (exists (sz : nat), gt sz 50387 /\ cardinal (matrix 2 2) E sz) -> exists (A B: matrix 2 2), E A /\ E B /\ A <> B /\ Mmult A B = Mmult B A.
 Proof. Admitted.

coq/src/putnam_1990_b5.v

@@ -2,8 +2,7 @@ Require Import Reals Ensembles Finite_sets Coquelicot.Coquelicot.
 Definition putnam_1990_b5_solution := True.
 Open Scope R.
 Theorem putnam_1990_b5 
-    (a : nat -> R) 
-    (pn : nat -> R -> R := fun n x => sum_n (fun i => a i * pow x i) n)
-    : forall (n: nat), gt n 0 -> exists (roots: Ensemble R), cardinal R roots n /\ forall (r: R), roots r <-> pn n r = 0 <->
+    (pn : (nat -> R) -> nat -> R -> R := fun a n x => sum_n (fun i => a i * pow x i) n)
+    : (exists (a : nat -> R), forall (n: nat), gt n 0 -> exists (roots: Ensemble R), cardinal R roots n /\ forall (r: R), roots r <-> pn a n r = 0) <->
     putnam_1990_b5_solution.
 Proof. Admitted.

isabelle/putnam_1987_a1.thy

@@ -4,8 +4,8 @@ begin
 
 theorem putnam_1987_a1:
   fixes A B C D :: "(real \<times> real) set"
-  defines "A \<equiv> {(x, y). x ^ 2 - y ^ 2 = x / (x ^ 2 + y ^ 2)}"
-  defines "B \<equiv> {(x, y). 2 * x * y + y / (x ^ 2 + y ^ 2) = 3}"
+  defines "A \<equiv> {(x, y). x ^ 2 + y ^ 2 \<noteq> 0 \<and> x ^ 2 - y ^ 2 = x / (x ^ 2 + y ^ 2)}"
+  defines "B \<equiv> {(x, y). x ^ 2 + y ^ 2 \<noteq> 0 \<and> 2 * x * y + y / (x ^ 2 + y ^ 2) = 3}"
   defines "C \<equiv> {(x, y). x ^ 3 - 3 * x * y ^ 2 + 3 * y = 1}"
   defines "D \<equiv> {(x, y). 3 * x ^ 2 * y - 3 * x - y ^ 3 = 0}"
   shows "A \<inter> B = C \<inter> D"

isabelle/putnam_1987_a5.thy

@@ -16,7 +16,7 @@ theorem putnam_1987_a5:
     and "contdiff \<equiv> \<lambda> (Fi :: real^3 \<Rightarrow> real) (j :: 3) (v :: real^3). (\<lambda> vj :: real. Fi (vrepl v j vj)) differentiable at (v$j) \<and> continuous (at (v$j)) (deriv (\<lambda> vj :: real. Fi (vrepl v j vj)))"
     and "partderiv \<equiv> \<lambda> (Fi :: real^3 \<Rightarrow> real) (j :: 3). \<lambda> v :: real^3. deriv (\<lambda> vj :: real. Fi (vrepl v j vj)) (v$j)"
     and "Fprop1 \<equiv> \<lambda> F :: (real^3 \<Rightarrow> real)^3. \<forall> i :: 3. \<forall> j :: 3. \<forall> v \<noteq> 0. contdiffv (F$i) j v"
-    and "Fprop2 \<equiv> \<lambda> F :: (real^3 \<Rightarrow> real)^3. \<forall> v \<noteq> 0. vector [(partderiv (F$3) 2 - partderiv (F$2) 3) v, (partderiv (F$1) 3 - partderiv (F$3) 1) v, (partderiv (F$2) 1 - partderiv (F$1) 2) v] = 0"
+    and "Fprop2 \<equiv> \<lambda> F :: (real^3 \<Rightarrow> real)^3. \<forall> v \<noteq> 0. (vector [(partderiv (F$3) 2 - partderiv (F$2) 3) v, (partderiv (F$1) 3 - partderiv (F$3) 1) v, (partderiv (F$2) 1 - partderiv (F$1) 2) v] :: real^3) = 0"
     and "Fprop3 \<equiv> \<lambda> F :: (real^3 \<Rightarrow> real)^3. \<forall> x y :: real. (\<chi> i :: 3. (F$i) (vector [x, y, 0])) = G (vector [x, y])"
   shows "(\<exists> F :: (real^3 \<Rightarrow> real)^3. Fprop1 F \<and> Fprop2 F \<and> Fprop3 F) \<longleftrightarrow> putnam_1987_a5_solution"
   sorry

isabelle/putnam_1987_b5.thy

@@ -5,7 +5,7 @@ theorem putnam_1987_b5:
   fixes n::nat and M::"complex^'a^'b"
   assumes matsize : "CARD('a) = n \<and> CARD('b) = 2 * n"
     and npos : "n > 0"
-    and hM : "\<forall>z::(complex^'b^1). (let prod = z ** M in (\<forall>i. prod$i = 0))
+    and hM : "\<forall>z::(complex^'b^1). (\<forall> i. (z ** M)$1$i = 0)
        \<longrightarrow> (\<not>(\<forall>i. z$1$i = 0)) \<longrightarrow> (\<exists>i. Im (z$1$i) \<noteq> 0)"
   shows "\<forall>r::(real^1^'b). \<exists>w::(complex^1^'a). \<forall>i. Re ((M**w)$i$1) = r$i$1"
   sorry

isabelle/putnam_1987_b6.thy

@@ -6,10 +6,11 @@ theorem putnam_1987_b6:
   assumes podd : "odd p \<and> prime p"
     and Ffield : "field F"
     and Fcard : "finite (carrier F) \<and> card (carrier F) = p^2"
+    and Ssub : "S \<subseteq> carrier F"
     and Snz : "\<forall>x \<in> S. x \<noteq> \<zero>\<^bsub>F\<^esub>"
     and Scard : "real_of_nat (card S) = (p^2 - 1::real) / 2"
     and hS : "\<forall>a::'a. a \<in> carrier F \<longrightarrow> a \<noteq> \<zero>\<^bsub>F\<^esub> \<longrightarrow> \<not>((a \<in> S) \<longleftrightarrow> ((\<ominus>\<^bsub>F\<^esub> a) \<in> S))"
-  shows "even (card (S \<inter> {x. (\<exists>a \<in> S. x = a \<oplus>\<^bsub>F\<^esub> a)}))"
+  shows "even (card (S \<inter> {x \<in> carrier F. (\<exists>a \<in> S. x = a \<oplus>\<^bsub>F\<^esub> a)}))"
   sorry
 
 end

isabelle/putnam_1988_a6.thy

@@ -16,7 +16,7 @@ theorem putnam_1988_a6:
           scale a (x \<oplus>\<^bsub>V\<^esub> y) = scale a x \<oplus>\<^bsub>V\<^esub> scale a y \<and> scale (a \<oplus>\<^bsub>F\<^esub> b) x = scale a x \<oplus>\<^bsub>V\<^esub> scale b x \<and> 
           scale a (scale b x) = scale (a \<otimes>\<^bsub>F\<^esub> b) x \<and> scale \<one>\<^bsub>F\<^esub> x = x \<and> 
           A (scale a x \<oplus>\<^bsub>V\<^esub> scale b y) = scale a (A x) \<oplus>\<^bsub>V\<^esub> scale b (A y)) \<and>
-          n = (GREATEST k :: nat. \<exists> s :: 'b list. set s \<subseteq> carrier V \<and> length s = k \<and> card (set s) = k \<longrightarrow>
+          n = (GREATEST k :: nat. \<exists> s :: 'b list. set s \<subseteq> carrier V \<and> length s = k \<and> card (set s) = k \<and>
           (\<forall> coeffs :: 'a list. set coeffs \<subseteq> carrier F \<and> length coeffs = n \<and> 
           (\<Oplus>\<^bsub>V\<^esub> i \<in> {0..<n}. scale (coeffs!i) (s!i)) = \<zero>\<^bsub>V\<^esub> \<longrightarrow> (\<forall> i \<in> {0..<n}. coeffs!i = \<zero>\<^bsub>F\<^esub>))) \<and>
           (\<exists> evecs \<subseteq> ((carrier V) - {\<zero>\<^bsub>V\<^esub>}). card evecs = n + 1 \<and> (\<forall> evec \<in> evecs. \<exists> a \<in> carrier F. A evec = scale a evec) \<and>

isabelle/putnam_1989_a1.thy

@@ -6,7 +6,7 @@ definition putnam_1989_a1_solution::nat where "putnam_1989_a1_solution \<equiv>
 theorem putnam_1989_a1:
   fixes pdigalt::"(nat list) \<Rightarrow> bool"
   defines "pdigalt \<equiv> \<lambda>pdig. odd (length pdig) \<and> (\<forall>i \<in> {0..<(length pdig)}. pdig!i = (if (even i) then 1 else 0))"
-  shows "putnam_1989_a1_solution = card {p::nat. p > 0 \<and> prime p \<and> (\<forall>dig. (foldr (\<lambda>a b. a + 10 * b) dig 0) = p \<longrightarrow> pdigalt dig)}"
+  shows "putnam_1989_a1_solution = card {p::nat. p > 0 \<and> prime p \<and> (\<exists> dig. (foldr (\<lambda>a b. a + 10 * b) dig 0) = p \<and> pdigalt dig)}"
   sorry
 
 end

isabelle/putnam_1989_b1.thy

@@ -14,7 +14,7 @@ theorem putnam_1989_b1:
     and "edges \<equiv> {p \<in> square. p$1 = 0 \<or> p$1 = 1 \<or> p$2 = 0 \<or> p$2 = 1}"
     and "center \<equiv> \<chi> i :: 2. (1 :: real) / 2"
     and "Scloser \<equiv> {p \<in> square. \<forall> q \<in> edges. dist p center < dist p q}"
-  shows "let (a, b, c, d) = putnam_1989_b1_solution in b > 0 \<and> d > 0 \<and> (\<not>(\<exists> n :: int. n^2 = b)) \<and>
+  shows "let (a, b, c, d) = putnam_1989_b1_solution in b > 0 \<and> d > 0 \<and> (\<not>(\<exists> n :: int. (n^2) dvd b)) \<and> (Gcd {a, c, d} = 1) \<and>
   measure lebesgue Scloser / measure lebesgue square = (a * sqrt (real_of_int b) + c) / d"
   sorry
 

isabelle/putnam_1990_a4.thy

@@ -5,7 +5,7 @@ begin
 definition putnam_1990_a4_solution :: "nat" where "putnam_1990_a4_solution \<equiv> undefined"
 (* 3 *)
 theorem putnam_1990_a4:
-  shows "(LEAST n :: nat. n > 0 \<and> (\<exists> S :: (real^2) set. card S = n \<and> (\<forall> Q :: real^2. \<exists> P \<in> S. \<not>(\<exists> q :: rat. (real_of_rat) q = dist P Q)))) = putnam_1990_a4_solution"
+  shows "(LEAST n :: nat. (\<exists> S :: (real^2) set. card S = n \<and> (\<forall> Q :: real^2. \<exists> P \<in> S. \<not>(\<exists> q :: rat. real_of_rat q = dist P Q)))) = putnam_1990_a4_solution"
   sorry
 
 end