Merge pull request #232 from trishullab/george

Fix misformalizations per #204.

isabelle/putnam_1962_a2.thy

@@ -4,11 +4,11 @@ theory putnam_1962_a2 imports Complex_Main
 begin
 
 definition putnam_1962_a2_solution :: "(real \<Rightarrow> real) set" where "putnam_1962_a2_solution \<equiv> undefined"
-(* {f :: real \<Rightarrow> real. \<exists> a c :: real. a > 0 \<and> f = (\<lambda> x. a / (1 - c * x)^2)} *)
+(* {f :: real \<Rightarrow> real. \<exists> a c :: real. a \<ge> 0 \<and> f = (\<lambda> x. a / (1 - c * x)^2)} *)
 theorem putnam_1962_a2:
   fixes hf :: "real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
     and hfinf :: "(real \<Rightarrow> real) \<Rightarrow> bool"
-  defines "hf \<equiv> \<lambda> (e :: real) (f :: real \<Rightarrow> real). \<forall> x \<in> {0<..<e}. (interval_lebesgue_integral lebesgue 0 x f) / x = sqrt ((f 0) * (f x))"
+  defines "hf \<equiv> \<lambda> (e :: real) (f :: real \<Rightarrow> real). (\<forall> x :: real. f x \<ge> 0) \<and> (\<forall> x \<in> {0<..<e}. (interval_lebesgue_integral lebesgue 0 x f) / x = sqrt ((f 0) * (f x)))"
     and "hfinf \<equiv> \<lambda> (f :: real \<Rightarrow> real). \<forall> x > 0. (interval_lebesgue_integral lebesgue 0 x f) / x = sqrt((f 0) * (f x))"
   shows "(\<forall> f :: real \<Rightarrow> real. (hfinf f \<longrightarrow> (\<exists> g \<in> putnam_1962_a2_solution. \<forall> x \<ge> 0. g x = f x)) \<and> 
   (\<forall> e > 0. hf e f \<longrightarrow> (\<exists> g \<in> putnam_1962_a2_solution. \<forall> x \<in> {0..<e}. g x = f x))) \<and> 

isabelle/putnam_1963_a3.thy

@@ -7,19 +7,17 @@ definition putnam_1963_a3_solution :: "(real \<Rightarrow> real) \<Rightarrow> n
 "putnam_1963_a3_solution \<equiv> undefined"
 (*  \<lambda> (f :: real \<Rightarrow> real) (n :: nat) (x :: real) (t :: real). (x-t)^(n-1) * (f t) / (fact (n-1)) * t^n *)
 theorem putnam_1963_a3:
-  fixes n :: "nat"
-    and f :: "real \<Rightarrow> real"
-    and P :: "nat \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real)"
-    and delta :: "(real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real)"
-    and D :: "nat \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real)"
-    and y :: "real \<Rightarrow> real"
-  defines "delta \<equiv> \<lambda> g. ((\<lambda> x :: real. x * deriv g x))"
-    and "D \<equiv> \<lambda> m :: nat. \<lambda> g :: real \<Rightarrow> real. (\<lambda> x :: real. (delta g) x - (real m) * (g x))"
-    and "y \<equiv> \<lambda> x :: real. interval_lebesgue_integral lebesgue 1 (ereal x) (putnam_1963_a3_solution f n x)"
-  assumes hn : "n \<ge> 1"
-    and hf : "continuous_on UNIV f"
-    and hP : "P 0 y = y \<and> (\<forall> m \<in> {0::nat..<n}. P (m + 1) y = D (n - 1 - m) (P m y))"
-  shows "(\<forall> k :: nat < n. ((deriv^^k) f) C1_differentiable_on UNIV) \<and> (\<forall> x :: real \<ge> 1. P n y x = f x) \<and> (\<forall> i \<in> {0::nat..<n}. ((deriv^^i) y) 1 = 0)"
+  fixes P :: "nat \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real)"
+    and n :: "nat"
+    and f y :: "real \<Rightarrow> real"
+  assumes hP : "(\<forall> x. P 0 x = x) \<and> (\<forall> (i :: nat) (y :: real \<Rightarrow> real). P (i + 1) y = P i (\<lambda> x. x * deriv y x - (real_of_nat i) * y x))"
+    and hn : "0 < n"
+    and hf : "continuous_on {1..} f"
+  shows "((\<forall> k :: nat < n. 
+           ((deriv^^k) y) C1_differentiable_on {1..} ∧
+           ((deriv^^k) y) 1 = 0) \<and>
+        (\<forall> x :: real. x \<ge> 0 \<longrightarrow> (P n y) x = f x)) \<longleftrightarrow>
+        (\<forall> x :: real \<ge> 1. y x = interval_lebesgue_integral lebesgue 1 (ereal x) (putnam_1963_a3_solution f n x))"
   sorry
 
 end

isabelle/putnam_1965_a6.thy

@@ -3,12 +3,16 @@ Complex_Main
 begin
 
 theorem putnam_1965_a6:
-  fixes u v m :: real
-  and pinter :: "(real \<times> real) \<Rightarrow> bool"
-  assumes hm: "m > 1"
-  and huv: "u \<ge> 0 \<and> v \<ge> 0"
-  defines "pinter \<equiv> (\<lambda>p::real\<times>real. u * (fst p) + v * (snd p) = 1 \<and> (fst p) powr m + (snd p) powr m = 1)"
-  shows "((\<exists>! p :: real \<times> real. pinter p) \<and> (\<exists> p :: real \<times> real. fst p \<ge> 0 \<and> snd p \<ge> 0 \<and> pinter p)) \<longleftrightarrow> (\<exists> n :: real. u powr n + v powr n = 1 \<and> m powi -1 + n powi -1 = 1)"
+  fixes u v m :: "real"
+  assumes hu : "0 < u"
+    and hv : "0 < v"
+    and hm : "1 < m"
+  shows "(\<exists> x :: real > 0. \<exists> y :: real > 0.
+          u * x + v * y = 1 \<and>
+          x powr m + y powr m = 1 \<and>
+          u = x powr (m - 1) \<and>
+          v = y powr (m - 1)) \<longleftrightarrow>
+         (\<exists> n :: real. u powr n + v powr n = 1 \<and> 1/m + 1/n = 1)"
   sorry
 
 end

isabelle/putnam_1965_b4.thy

@@ -5,9 +5,16 @@ begin
 definition putnam_1965_b4_solution :: "(((real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> real) \<times> ((real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> real)) \<times> ((real set) \<times> (real \<Rightarrow> real))" where "putnam_1965_b4_solution \<equiv> undefined"
 (* ((\<lambda> h :: real \<Rightarrow> real. \<lambda> x :: real. h x + x, \<lambda> h :: real \<Rightarrow> real. \<lambda> x :: real. h x + 1), ({x :: real. x \<ge> 0}, sqrt)) *)
 theorem putnam_1965_b4:
-  fixes f :: "nat \<Rightarrow> real \<Rightarrow> real"
-  assumes hf: "\<forall> n > 0. f n = (\<lambda> x :: real. (\<Sum> i = 0 .. n div 2. (n choose (2 * i)) * x ^ i) / (\<Sum> i = 0 .. (n - 1) div 2. (n choose (2 * i + 1)) * x ^ i))"
-  shows "let ((p, q), (s, g)) = putnam_1965_b4_solution in (\<forall> n > 0. f (n + 1) = (\<lambda> x. p (f n) x / q (f n) x) \<and> s = {x :: real. convergent (\<lambda> n. f n x)} \<and> (\<forall> x \<in> s. (\<lambda> n. f n x) \<longlonglongrightarrow> g x))"
+  fixes f u v :: "nat \<Rightarrow> real \<Rightarrow> real"
+    and n :: "nat"
+  assumes hu : "\<forall> n :: nat > 0. \<forall> x. u n x = (\<Sum> i = 0 .. n div 2. (n choose (2 * i)) * x ^ i)"
+    and hv : "\<forall> n :: nat > 0. \<forall> x. v n x = (\<Sum> i = 0 .. (n - 1) div 2. (n choose (2 * i + 1)) * x ^ i)"
+    and hf : "\<forall> n :: nat > 0. \<forall> x. f n x = u n x / v n x"
+    and hn : "0 < n"
+  shows "let ((p, q), (s, g)) = putnam_1965_b4_solution in 
+           (\<forall> n > 0. v n x \<noteq> 0 \<longrightarrow> v (n+1) x \<noteq> 0 \<longrightarrow> q (f n) x \<noteq> 0 \<longrightarrow>  f (n + 1) = (\<lambda> x. p (f n) x / q (f n) x) \<and>
+           s = {x :: real. convergent (\<lambda> n. f n x)} \<and> 
+           (\<forall> x \<in> s. (\<lambda> n. f n x) \<longlonglongrightarrow> g x))"
   sorry
 
-end
+end

isabelle/putnam_1969_a5.thy

@@ -3,8 +3,19 @@ theory putnam_1969_a5 imports Complex_Main
 begin
 
 theorem putnam_1969_a5:
-  shows "\<forall> x y :: real \<Rightarrow> real. (x differentiable_on UNIV \<and> y differentiable_on UNIV) \<longrightarrow> (\<forall> t > 0. (x 0 = y 0 \<longleftrightarrow> (\<exists> u :: real \<Rightarrow> real. continuous_on UNIV u \<and> x t = 0 \<and> y t = 0 \<and>
-    deriv x = (\<lambda> p :: real \<Rightarrow> -2 * y p + u p) \<and> deriv y = (\<lambda> p :: real \<Rightarrow> -2 * x p + u p))))"
+  fixes x0 y0 t :: "real"
+  assumes ht : "0 < t"
+  shows "x0 = y0 \<longleftrightarrow> (\<exists> x y u :: real \<Rightarrow> real.
+          x differentiable_on UNIV \<and>
+          y differentiable_on UNIV \<and>
+          continuous_on UNIV u \<and>
+          (\<forall> p :: real. deriv x p = -2 * y p + u p) \<and>
+          (\<forall> p :: real. deriv y p = -2 * x p + u p) \<and>
+          x 0 = x0 \<and>
+          y 0 = y0 \<and>
+          x t = 0 \<and>
+          y t = 0)"
   sorry
 
+
 end

isabelle/putnam_1974_a4.thy

@@ -2,11 +2,11 @@ theory putnam_1974_a4 imports Complex_Main
 begin
 
 definition putnam_1974_a4_solution :: "nat \<Rightarrow> real" where "putnam_1974_a4_solution \<equiv> undefined"
-(* (\<lambda>n::nat. (n / 2^(n-1)) * ((n-1) choose (nat \<lfloor>(n-1)/2\<rfloor>))) *)
+(* (\<lambda>n::nat. (n / 2^(n-1)) * ((n-1) choose (nat \<lfloor>n/2\<rfloor>))) *)
 theorem putnam_1974_a4:
   fixes n :: nat
   assumes hn: "n > 0"
-  shows "1/(2^(n-1)) * (\<Sum>k::nat=0..((nat \<lceil>n/2\<rceil>)-1). (n - 2*k) * (n choose k)) = putnam_1974_a4_solution n"
+  shows "1/(2^(n-1)) * (\<Sum>k::nat=0..(nat (\<lfloor> n/2 \<rfloor>)). (n - 2*k) * (n choose k)) = putnam_1974_a4_solution n"
   sorry
 
 end

isabelle/putnam_1974_b1.thy

@@ -5,7 +5,7 @@ Complex_Main
 begin
 
 definition putnam_1974_b1_solution :: "(real^2) list \<Rightarrow> bool" where "putnam_1974_b1_solution \<equiv> undefined"
-(* \<lambda> points. \<exists> (B :: real) (ordering :: nat \<Rightarrow> nat). ordering permutes {0..<5} \<and> (\<forall> i < 5. dist (points!(ordering i)) (points!(ordering ((i + 1) mod 5))) = B) *)
+(* \<lambda> points. \<exists> (B :: real) (ordering :: nat \<Rightarrow> nat). B > 0 \<and> ordering permutes {0..<5} \<and> (\<forall> i < 5. dist (points!(ordering i)) (points!(ordering ((i + 1) mod 5))) = B) *)
 theorem putnam_1974_b1:
   fixes on_unit_circle :: "(real^2) list \<Rightarrow> bool"
   and distance_fun :: "(real^2) list \<Rightarrow> real"

isabelle/putnam_1977_a3.thy

@@ -4,8 +4,10 @@ begin
 definition putnam_1977_a3_solution::"(real\<Rightarrow>real) \<Rightarrow> (real\<Rightarrow>real) \<Rightarrow> (real\<Rightarrow>real)" where "putnam_1977_a3_solution \<equiv> undefined"
 (* \<lambda>f. \<lambda>g. \<lambda>x. g x - f (x-3) + f (x-1) + f (x+1) - f (x+3) *)
 theorem putnam_1977_a3:
-  fixes f g::"real\<Rightarrow>real"
-  shows "let h = (putnam_1977_a3_solution f g) in (\<forall>x::real. f x = (h (x+1) + h (x-1)) / 2 \<and> g x = (h (x+4) + h (x-4)) / 2)"
+  fixes f g h :: "real\<Rightarrow>real"
+  assumes hf : "\<forall> x. f x = (h (x+1) + h (x-1)) / 2"
+    and hg : "\<forall> x. g x = (h (x+4) + h (x-4)) / 2"
+  shows "h = putnam_1977_a3_solution f g"
   sorry
 
 end

isabelle/putnam_1982_b4.thy

@@ -5,7 +5,7 @@ definition putnam_1982_b4_solution::"bool \<times> bool" where "putnam_1982_b4_s
 (* True, True *)
 theorem putnam_1982_b4:
   fixes hn::"(int set) \<Rightarrow> bool"
-  defines "hn \<equiv> \<lambda>n. (\<forall>k::int. (\<Prod>i \<in> n. i) dvd (\<Prod>i \<in> n. (i + k)))"
+  defines "hn \<equiv> \<lambda>n. (\<exists> c :: int. c \<in> n) \<and> (\<forall>k::int. (\<Prod>i \<in> n. i) dvd (\<Prod>i \<in> n. (i + k)))"
   shows "((\<forall>n::(int set). hn n \<longrightarrow> (\<exists>i \<in> n. abs(i) = 1)) \<longleftrightarrow> fst putnam_1982_b4_solution) \<and>
     ((\<forall>n::(int set). (hn n \<and> (\<forall>i \<in> n. i > 0)) \<longrightarrow> n = {1..card n})) \<longleftrightarrow> snd putnam_1982_b4_solution"
   sorry

isabelle/putnam_1984_a6.thy

@@ -10,7 +10,7 @@ theorem putnam_1984_a6:
     and gpeq :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> bool"
   defines "kadistinct \<equiv> \<lambda> (k :: nat) (a :: nat \<Rightarrow> nat). k \<ge> 1 \<and> (\<forall> i j :: nat. (i < k \<and> j < k \<and> i \<noteq> j) \<longrightarrow> a i \<noteq> a j)"
     and "gpeq \<equiv> \<lambda> (g :: nat \<Rightarrow> nat) (p :: nat). p > 0 \<and> (\<forall> (s :: nat) \<ge> 1. g s = g (s + p))"
-  assumes hf : "\<forall> n > 0. f n = (if [n \<noteq> 0] (mod 10) then (n mod 10) else f (n div 10))" 
+  assumes hf : "\<forall> n > 0. f n = (if [fact n \<noteq> 0] (mod 10) then ((fact n) mod 10) else f ((fact n) div 10))" 
   shows "let (b, n) = putnam_1984_a6_solution in \<exists> g :: nat \<Rightarrow> nat. 
 (\<forall> (k :: nat) (a :: nat \<Rightarrow> nat). kadistinct k a \<longrightarrow> g (\<Sum> i=0..(k-1). a i) = f (\<Sum> i=0..(k-1). 5^(a i)))
 \<and> (if b then gpeq g n \<and> (\<forall> p :: nat. gpeq g p \<longrightarrow> p \<ge> n) else \<not>(\<exists> p :: nat. gpeq g p))"

isabelle/putnam_1991_a4.thy

@@ -8,12 +8,10 @@ definition putnam_1991_a4_solution :: bool where "putnam_1991_a4_solution \<equi
 (* True *)
 theorem putnam_1991_a4:
   fixes climit :: "(nat \<Rightarrow> real^2) \<Rightarrow> bool"
-  and rareas :: "(nat \<Rightarrow> real) \<Rightarrow> bool"
-  and crline :: "(nat \<Rightarrow> real^2) \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> bool"
-  defines "climit \<equiv> \<lambda> c. \<not>(\<exists> p :: real^2. \<forall> \<epsilon> :: real. \<epsilon> > 0 \<longrightarrow> (\<exists> i :: nat. c i \<in> ball p \<epsilon>))"
-  and "rareas \<equiv> \<lambda> r. convergent (\<lambda> N. \<Sum> i = 0 .. N. pi * (r i) ^ 2)"
-  and "crline \<equiv> \<lambda> c r. \<forall> v w :: real^2. w \<noteq> 0 \<longrightarrow> (\<exists> i :: nat. {p :: real^2. \<exists> t :: real. p = v + t *s w} \<inter> cball (c i) (r i) \<noteq> {})"
+    and rareas :: "(nat \<Rightarrow> real) \<Rightarrow> bool"
+    and crline :: "(nat \<Rightarrow> real^2) \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> bool"
+  defines "climit \<equiv> \<lambda> c. \<not>(\<exists> p :: real^2. \<forall> \<epsilon> :: real. \<epsilon> > 0 \<longrightarrow> (\<exists> f :: nat \<Rightarrow> nat. strict_mono f \<and> (\<forall> i :: nat. c (f i) \<in> ball p \<epsilon>)))"
+    and "rareas \<equiv> \<lambda> r. convergent (\<lambda> N. \<Sum> i = 0 .. N. pi * (r i) ^ 2)"
+    and "crline \<equiv> \<lambda> c r. \<forall> v w :: real^2. w \<noteq> 0 \<longrightarrow> (\<exists> i :: nat. {p :: real^2. \<exists> t :: real. p = v + t *s w} \<inter> cball (c i) (r i) \<noteq> {})"
   shows "(\<exists> c :: nat \<Rightarrow> real^2. \<exists> r :: nat \<Rightarrow> real. (\<forall> i :: nat. r i \<ge> 0) \<and> climit c \<and> rareas r \<and> crline c r) \<longleftrightarrow> putnam_1991_a4_solution"
   sorry
-
-end

isabelle/putnam_1995_b4.thy

@@ -5,7 +5,8 @@ definition putnam_1995_b4_solution :: "int \<times> int \<times> int \<times> in
 (* (3,1,5,2) *)
 theorem putnam_1995_b4:
   fixes contfrac :: real
-  assumes hcontfrac: "contfrac = 2207 - 1/contfrac"
+  assumes hcontfrac : "contfrac = 2207 - 1/contfrac"
+    and hcontfrac': "1 < contfrac"
   shows "let (a,b,c,d) = putnam_1995_b4_solution in (contfrac powr (1/8) = (a + b * sqrt c) / d)"
   sorry
 

isabelle/putnam_1998_a4.thy

@@ -3,16 +3,14 @@ begin
 
 definition putnam_1998_a4_solution::"nat set" where "putnam_1998_a4_solution \<equiv> undefined"
 (* {n::nat. [n = 1] (mod 6)} *)
-fun digits::"nat \<Rightarrow> nat list" where
-  "digits n = (if n < 10 then [n] else ([n mod 10::nat] @ digits (n div 10::nat)))"
 fun from_digits::"nat list \<Rightarrow> nat" where
   "from_digits L = foldr (\<lambda>a. \<lambda>b. a + 10 * b) L 0"
 theorem putnam_1998_a4:
-  fixes A::"nat\<Rightarrow>nat"
-  assumes hA1 : "A 1 = 0"
-    and hA2 : "A 2 = 1"
-    and hA : "\<forall>n::nat > 2. A n = from_digits (digits (A (n-2)) @ digits (A (n-1)))"
-  shows "putnam_1998_a4_solution = {n::nat. n \<ge> 1 \<and> 11 dvd (A n)}"
+  fixes A::"nat\<Rightarrow>nat list"
+  assumes hA1 : "A 1 = [0]"
+    and hA2 : "A 2 = [1]"
+    and hA : "\<forall>n::nat > 0. A (n+2) = A (n+1) @ A n"
+  shows "putnam_1998_a4_solution = {n::nat. n \<ge> 1 \<and> 11 dvd (from_digits (A n))}"
   sorry
 
 end

isabelle/putnam_2001_b2.thy

@@ -8,7 +8,9 @@ theorem putnam_2001_b2:
   fixes x y :: real
   and eq1 eq2 :: bool
   defines "eq1 \<equiv> 1 / x + 1 / (2 * y) = (x ^ 2 + 3 * y ^ 2) * (3 * x ^ 2 + y ^ 2)"
-  and "eq2 \<equiv> 1 / x - 1 / (2 * y) = 2 * (y ^ 4 - x ^ 4)"
+    and "eq2 \<equiv> 1 / x - 1 / (2 * y) = 2 * (y ^ 4 - x ^ 4)"
+  assumes hx : "x \<noteq> 0"
+    and hy : "y \<noteq> 0"
   shows "(eq1 \<and> eq2) \<longleftrightarrow> (x, y) \<in> putnam_2001_b2_solution"
   sorry
 

isabelle/putnam_2005_a3.thy

@@ -7,11 +7,13 @@ theorem putnam_2005_a3:
   fixes p :: "complex poly"
     and n :: nat
     and g :: "complex \<Rightarrow> complex"
+    and z :: "complex"
   assumes pdeg : "degree p = n"
     and pzeros : "\<forall>z::complex. (poly p z = 0 \<longrightarrow> norm z = 1)"
     and hg : "\<forall>z::complex. g z = (poly p z) / csqrt (z^n)"
     and hn : "n > 0"
-  shows "\<forall>z::complex. (deriv g z = 0 \<longrightarrow> norm z = 1)"
+    and hz : "z \<noteq> 0 \<and> deriv g z = 0"
+  shows "norm z = 1"
   sorry
 
 end

isabelle/putnam_2005_b3.thy

@@ -7,7 +7,9 @@ definition putnam_2005_b3_solution :: "(real \<Rightarrow> real) set" where "put
 (* {f::real\<Rightarrow>real. (\<exists>c d::real. c > 0 \<and> d > 0 \<and> (d = 1 \<longrightarrow> c = 1) \<and> (\<forall>x::real\<in>{0<..}. f x = c * x powr d))} *)
 theorem putnam_2005_b3:
   fixes f :: "real \<Rightarrow> real"
-  shows "(f differentiable_on {0<..} \<and> (\<exists>a::real>0. \<forall>x::real>0. deriv f (a/x) = x / f x)) \<longleftrightarrow> f \<in> putnam_2005_b3_solution"
+  assumes hf : "\<forall> x :: real. 0 < f x"
+    and hf' : "f differentiable_on {0<..}"
+  shows "(\<exists>a::real>0. \<forall>x::real>0. deriv f (a/x) = x / f x) \<longleftrightarrow> f \<in> putnam_2005_b3_solution"
   sorry
 
 end

isabelle/putnam_2007_a1.thy

@@ -5,9 +5,11 @@ begin
 (* Note: Modified definition of tangent to handle this, but this is a bit of cheating - You would have to know that this works *)
 definition putnam_2007_a1_solution :: "real set" where "putnam_2007_a1_solution \<equiv> undefined"
 (* {2/3, 3/2, (13 + sqrt 601)/12, (13 - sqrt 601)/12} *)
-definition reflect_tangent :: "(real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool" where "reflect_tangent \<equiv> (\<lambda>f g::real\<Rightarrow>real. f C1_differentiable_on UNIV \<and> g C1_differentiable_on UNIV \<and> (\<exists>x y::real. f x = y \<and> g y = x \<and> deriv f x = 1 / deriv g y))"
 theorem putnam_2007_a1:
-  shows "\<forall>a::real. (reflect_tangent (\<lambda>x::real. a*x^2 + a*x + 1/24) (\<lambda>y::real. a*y^2 + a*y + 1/24) \<longleftrightarrow> a \<in> putnam_2007_a1_solution)"
+  fixes P :: "(real \<Rightarrow> real) \<Rightarrow> bool"
+    and a :: "real"
+  assumes P_def : "\<forall> f :: real \<Rightarrow> real. (P f \<longleftrightarrow> (\<exists> x y. f x = y \<and> f y = x \<and> deriv f x * deriv f y = 1))"
+  shows "P (\<lambda> t :: real. a * t ^ 2 + a * t + 1 / 24) \<longleftrightarrow> a \<in> putnam_2007_a1_solution"
   sorry
 
 end

isabelle/putnam_2008_b3.thy

@@ -8,7 +8,7 @@ theorem putnam_2008_b3:
   fixes hypercube :: "(real^4) set"
     and contains :: "real \<Rightarrow> real^4 \<Rightarrow> real^4 \<Rightarrow> real^4 \<Rightarrow> bool"
   defines "hypercube \<equiv> {P :: real^4. \<forall> i. \<bar>P$i\<bar> \<le> 1/(real 2)}"
-    and "contains \<equiv> \<lambda> r :: real. \<lambda> center :: real^4. \<lambda> P :: real^4. \<lambda> Q :: real^4. \<forall> s t :: real. (s *s P + t *s Q \<noteq> 0 \<and> dist 0 (s *s P + t *s Q) = r) \<longrightarrow> center + s *s P + t *s Q \<in> hypercube"
+    and "contains \<equiv> \<lambda> r :: real. \<lambda> center :: real^4. \<lambda> P :: real^4. \<lambda> Q :: real^4. (\<not> (\<exists> c1 c2 :: real. c1 \<noteq> 0 \<and> c2 \<noteq> 0 \<and> c1 *s P + c2 *s Q = 0)) \<and> (\<forall> s t :: real. (s *s P + t *s Q \<noteq> 0 \<and> dist 0 (s *s P + t *s Q) = r) \<longrightarrow> center + s *s P + t *s Q \<in> hypercube)"
   shows "(\<exists> center P Q :: real^4. contains putnam_2008_b3_solution center P Q) \<and> (\<forall> r > putnam_2008_b3_solution. \<not>(\<exists> center P Q :: real^4. contains r center P Q))"
   sorry
 

isabelle/putnam_2016_a2.thy

@@ -6,7 +6,7 @@ definition putnam_2016_a2_solution :: real where "putnam_2016_a2_solution \<equi
 (* (3 + sqrt 5) / 2 *)
 theorem putnam_2016_a2:
   fixes M :: "nat \<Rightarrow> nat"
-  defines "M \<equiv> \<lambda> n. GREATEST m. m choose (n - 1) > (m - 1) choose n"
+  assumes hM :  "\<forall> n :: nat > 0. M n = (GREATEST m. m choose (n - 1) > (m - 1) choose n)"
   shows "(\<lambda> n. M n / (real n)) \<longlonglongrightarrow> putnam_2016_a2_solution"
   sorry
 

isabelle/putnam_2017_a1.thy

@@ -9,10 +9,10 @@ theorem putnam_2017_a1:
   assumes IsQualifying_def : "\<forall> S. IsQualifying S \<longleftrightarrow>
     (\<forall> n \<in> S. 0 < n) \<and>
     2 \<in> S \<and>
-    (\<forall> n. n^2 \<in> S \<longrightarrow> n \<in> S) \<and>
+    (\<forall> n > 0. n^2 \<in> S \<longrightarrow> n \<in> S) \<and>
     (\<forall> n \<in> S. (n + 5)^2 \<in> S)"
     and hS : "S = (LEAST A. IsQualifying S)"
   shows "putnam_2017_a1_solution = {x :: int. x > 0} - s"
-  sorry  
+  sorry
 
 end