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 1/2] 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 2/2] 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