From fd75e4c9f6fe9ec64b3fc47c9fde1abe7cd600a4 Mon Sep 17 00:00:00 2001
From: Jimmy Xin <jxin31415@gmail.com>
Date: Mon, 15 Jul 2024 17:48:09 +0200
Subject: [PATCH 1/4] Update putnam_2013_b5.thy

---
 isabelle/putnam_2013_b5.thy | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/isabelle/putnam_2013_b5.thy b/isabelle/putnam_2013_b5.thy
index e3239254..0c3d6b4d 100644
--- a/isabelle/putnam_2013_b5.thy
+++ b/isabelle/putnam_2013_b5.thy
@@ -4,12 +4,11 @@ begin
 (* uses (nat \<Rightarrow> nat) instead of ({1..n} \<Rightarrow> {1..n}) *)
 theorem putnam_2013_b5:
   fixes n :: nat
-  and k :: nat
-  and fiter :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
+    and k :: nat
+    and fiter :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
   assumes npos: "n \<ge> 1"
-  and kinX: "k \<in> {1..n}"
-  and hfiter: "\<forall>f::nat\<Rightarrow>nat. fiter f = (f ` {1..n} \<subseteq> {1..n} \<and> (\<forall>x::nat\<in>{1..n}. \<exists>j::nat. (f^^j) x \<le> k)) \<and> (\<forall>x::nat > n. f x = 0) \<and> f 0 = 0"
+    and kinX: "k \<in> {1..n}"
+  defines "fiter \<equiv> \<lambda>f. (f ` {1..n} \<subseteq> {1..n} \<and> (\<forall>x::nat\<in>{1..n}. \<exists>j::nat. (f^^j) x \<le> k)) \<and> (\<forall>x::nat > n. f x = 0) \<and> f 0 = 0"
   shows "card {f::nat\<Rightarrow>nat. fiter f} = k * n^(n-1)"
-  sorry
 
-end
\ No newline at end of file
+end

From 90c40f33e7f7c21187f146ee60e3fd8574d4e50b Mon Sep 17 00:00:00 2001
From: Jimmy Xin <jxin31415@gmail.com>
Date: Mon, 15 Jul 2024 17:48:18 +0200
Subject: [PATCH 2/4] Update putnam_2013_b5.thy

---
 isabelle/putnam_2013_b5.thy | 1 +
 1 file changed, 1 insertion(+)

diff --git a/isabelle/putnam_2013_b5.thy b/isabelle/putnam_2013_b5.thy
index 0c3d6b4d..86618693 100644
--- a/isabelle/putnam_2013_b5.thy
+++ b/isabelle/putnam_2013_b5.thy
@@ -10,5 +10,6 @@ theorem putnam_2013_b5:
     and kinX: "k \<in> {1..n}"
   defines "fiter \<equiv> \<lambda>f. (f ` {1..n} \<subseteq> {1..n} \<and> (\<forall>x::nat\<in>{1..n}. \<exists>j::nat. (f^^j) x \<le> k)) \<and> (\<forall>x::nat > n. f x = 0) \<and> f 0 = 0"
   shows "card {f::nat\<Rightarrow>nat. fiter f} = k * n^(n-1)"
+  sorry
 
 end

From be5607df7a1cf7d47777d6d8943fd7136c7b4d0a Mon Sep 17 00:00:00 2001
From: Jimmy Xin <jxin31415@gmail.com>
Date: Wed, 24 Jul 2024 23:03:11 +0200
Subject: [PATCH 3/4] Update putnam_2013_a5.thy

---
 isabelle/putnam_2013_a5.thy | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/isabelle/putnam_2013_a5.thy b/isabelle/putnam_2013_a5.thy
index 9e9997d9..4b61b516 100644
--- a/isabelle/putnam_2013_a5.thy
+++ b/isabelle/putnam_2013_a5.thy
@@ -1,21 +1,24 @@
 theory putnam_2013_a5 imports Complex_Main
 "HOL-Analysis.Finite_Cartesian_Product"
 "HOL-Analysis.Lebesgue_Measure"
+"HOL-Analysis.Cross3"
 begin
 
-(* uses (nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real), (nat \<Rightarrow> (real^2)), and (nat \<Rightarrow> (real^3)) instead of limiting inputs to (Fin m) and ensuring inputs are strictly increasing *)
+(* uses (nat ⇒ nat ⇒ nat ⇒ real), (nat ⇒ (real^2)), and (nat ⇒ (real^3)) instead of limiting inputs to (Fin m) and ensuring inputs are strictly increasing *)
 theorem putnam_2013_a5:
   fixes m :: nat
-  and area2 :: "(real^2) \<Rightarrow> (real^2) \<Rightarrow> (real^2) \<Rightarrow> real"
-  and area3 :: "(real^3) \<Rightarrow> (real^3) \<Rightarrow> (real^3) \<Rightarrow> real"
-  and areadef2 :: "(nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real) \<Rightarrow> bool"
-  and areadef3 :: "(nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real) \<Rightarrow> bool"
-  assumes mge3: "m \<ge> 3"
-  and harea2: "\<forall>a b c::real^2. area2 a b c = emeasure lebesgue (convex hull {a, b, c})"
-  and harea3: "\<forall>a b c::real^3. area3 a b c = emeasure lebesgue (convex hull {a, b, c})"
-  and hareadef2: "\<forall>a::nat\<Rightarrow>nat\<Rightarrow>nat\<Rightarrow>real. areadef2 a = (\<forall>A::nat\<Rightarrow>(real^2). (\<Sum>i::nat\<in>{0..(m-1)}. \<Sum>j::nat\<in>{i<..(m-1)}. \<Sum>k::nat\<in>{j<..(m-1)}. (a i j k * area2 (A i) (A j) (A k))) \<ge> 0)"
-  and hareadef3: "\<forall>a::nat\<Rightarrow>nat\<Rightarrow>nat\<Rightarrow>real. areadef3 a = (\<forall>A::nat\<Rightarrow>(real^3). (\<Sum>i::nat\<in>{0..(m-1)}. \<Sum>j::nat\<in>{i<..(m-1)}. \<Sum>k::nat\<in>{j<..(m-1)}. (a i j k * area3 (A i) (A j) (A k))) \<ge> 0)"
-  shows "\<forall>a::nat\<Rightarrow>nat\<Rightarrow>nat\<Rightarrow>real. (areadef2 a \<longrightarrow> areadef3 a)"
+    and area2 :: "(real^2) ⇒ (real^2) ⇒ (real^2) ⇒ real"
+    and area3 :: "(real^3) ⇒ (real^3) ⇒ (real^3) ⇒ real"
+    and areadef2 :: "(nat ⇒ nat ⇒ nat ⇒ real) ⇒ bool"
+    and areadef3 :: "(nat ⇒ nat ⇒ nat ⇒ real) ⇒ bool"
+    and cross :: "(real^3) ⇒ (real^3) ⇒ (real^3) ⇒ (real^3)"
+  defines "cross ≡ λ a b c. sgn (cross3 (b - a) (c - a))"
+  assumes mge3: "m ≥ 3"
+    and harea2: "∀a b c::real^2. area2 a b c = emeasure lebesgue (convex hull {a, b, c})"
+    and harea3: "∀a b c::real^3. area3 a b c = emeasure lebesgue (convex hull {a, b, c, a + (cross a b c), b + (cross a b c), c + (cross a b c)})"
+    and hareadef2: "∀a::nat⇒nat⇒nat⇒real. areadef2 a = (∀A::nat⇒(real^2). (∑i::nat∈{0..(m-1)}. ∑j::nat∈{i<..(m-1)}. ∑k::nat∈{j<..(m-1)}. (a i j k * area2 (A i) (A j) (A k))) ≥ 0)"
+    and hareadef3: "∀a::nat⇒nat⇒nat⇒real. areadef3 a = (∀A::nat⇒(real^3). (∑i::nat∈{0..(m-1)}. ∑j::nat∈{i<..(m-1)}. ∑k::nat∈{j<..(m-1)}. (a i j k * area3 (A i) (A j) (A k))) ≥ 0)"
+  shows "∀a::nat⇒nat⇒nat⇒real. (areadef2 a ⟶ areadef3 a)"
   sorry
 
 end

From f45661490574349d90e0d32ce4eedc3172ab5b8e Mon Sep 17 00:00:00 2001
From: Jimmy Xin <jxin31415@gmail.com>
Date: Wed, 24 Jul 2024 23:03:43 +0200
Subject: [PATCH 4/4] Update putnam_2013_a5.thy

---
 isabelle/putnam_2013_a5.thy | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/isabelle/putnam_2013_a5.thy b/isabelle/putnam_2013_a5.thy
index 4b61b516..27aa032b 100644
--- a/isabelle/putnam_2013_a5.thy
+++ b/isabelle/putnam_2013_a5.thy
@@ -4,21 +4,21 @@ theory putnam_2013_a5 imports Complex_Main
 "HOL-Analysis.Cross3"
 begin
 
-(* uses (nat ⇒ nat ⇒ nat ⇒ real), (nat ⇒ (real^2)), and (nat ⇒ (real^3)) instead of limiting inputs to (Fin m) and ensuring inputs are strictly increasing *)
+(* uses (nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real), (nat \<Rightarrow> (real^2)), and (nat \<Rightarrow> (real^3)) instead of limiting inputs to (Fin m) and ensuring inputs are strictly increasing *)
 theorem putnam_2013_a5:
   fixes m :: nat
-    and area2 :: "(real^2) ⇒ (real^2) ⇒ (real^2) ⇒ real"
-    and area3 :: "(real^3) ⇒ (real^3) ⇒ (real^3) ⇒ real"
-    and areadef2 :: "(nat ⇒ nat ⇒ nat ⇒ real) ⇒ bool"
-    and areadef3 :: "(nat ⇒ nat ⇒ nat ⇒ real) ⇒ bool"
-    and cross :: "(real^3) ⇒ (real^3) ⇒ (real^3) ⇒ (real^3)"
-  defines "cross ≡ λ a b c. sgn (cross3 (b - a) (c - a))"
-  assumes mge3: "m ≥ 3"
-    and harea2: "∀a b c::real^2. area2 a b c = emeasure lebesgue (convex hull {a, b, c})"
-    and harea3: "∀a b c::real^3. area3 a b c = emeasure lebesgue (convex hull {a, b, c, a + (cross a b c), b + (cross a b c), c + (cross a b c)})"
-    and hareadef2: "∀a::nat⇒nat⇒nat⇒real. areadef2 a = (∀A::nat⇒(real^2). (∑i::nat∈{0..(m-1)}. ∑j::nat∈{i<..(m-1)}. ∑k::nat∈{j<..(m-1)}. (a i j k * area2 (A i) (A j) (A k))) ≥ 0)"
-    and hareadef3: "∀a::nat⇒nat⇒nat⇒real. areadef3 a = (∀A::nat⇒(real^3). (∑i::nat∈{0..(m-1)}. ∑j::nat∈{i<..(m-1)}. ∑k::nat∈{j<..(m-1)}. (a i j k * area3 (A i) (A j) (A k))) ≥ 0)"
-  shows "∀a::nat⇒nat⇒nat⇒real. (areadef2 a ⟶ areadef3 a)"
+    and area2 :: "(real^2) \<Rightarrow> (real^2) \<Rightarrow> (real^2) \<Rightarrow> real"
+    and area3 :: "(real^3) \<Rightarrow> (real^3) \<Rightarrow> (real^3) \<Rightarrow> real"
+    and areadef2 :: "(nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real) \<Rightarrow> bool"
+    and areadef3 :: "(nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real) \<Rightarrow> bool"
+    and cross :: "(real^3) \<Rightarrow> (real^3) \<Rightarrow> (real^3) \<Rightarrow> (real^3)"
+  defines "cross \<equiv> \<lambda> a b c. sgn (cross3 (b - a) (c - a))"
+  assumes mge3: "m \<ge> 3"
+    and harea2: "\<forall>a b c::real^2. area2 a b c = emeasure lebesgue (convex hull {a, b, c})"
+    and harea3: "\<forall>a b c::real^3. area3 a b c = emeasure lebesgue (convex hull {a, b, c, a + (cross a b c), b + (cross a b c), c + (cross a b c)})"
+    and hareadef2: "\<forall>a::nat\<Rightarrow>nat\<Rightarrow>nat\<Rightarrow>real. areadef2 a = (\<forall>A::nat\<Rightarrow>(real^2). (\<Sum>i::nat\<in>{0..(m-1)}. \<Sum>j::nat\<in>{i<..(m-1)}. \<Sum>k::nat\<in>{j<..(m-1)}. (a i j k * area2 (A i) (A j) (A k))) \<ge> 0)"
+    and hareadef3: "\<forall>a::nat\<Rightarrow>nat\<Rightarrow>nat\<Rightarrow>real. areadef3 a = (\<forall>A::nat\<Rightarrow>(real^3). (\<Sum>i::nat\<in>{0..(m-1)}. \<Sum>j::nat\<in>{i<..(m-1)}. \<Sum>k::nat\<in>{j<..(m-1)}. (a i j k * area3 (A i) (A j) (A k))) \<ge> 0)"
+  shows "\<forall>a::nat\<Rightarrow>nat\<Rightarrow>nat\<Rightarrow>real. (areadef2 a \<longrightarrow> areadef3 a)"
   sorry
 
 end