Update putnam_1969_b2.thy

trishullab · Oct 19, 2024 · 3c1d446 · 3c1d446
1 parent d272865
commit 3c1d446
Showing 1 changed file with 4 additions and 5 deletions.
diff --git a/isabelle/putnam_1969_b2.thy b/isabelle/putnam_1969_b2.thy
@@ -6,11 +6,10 @@ begin
 definition putnam_1969_b2_solution :: bool where "putnam_1969_b2_solution \<equiv> undefined"
 (* False *)
 theorem putnam_1969_b2:
-  fixes G (structure)
-  and h :: "nat \<Rightarrow> bool"
-  assumes hG: "group G \<and> finite (carrier G)"
-  defines "h \<equiv> (\<lambda>n::nat. (\<exists>H::nat\<Rightarrow>('a set). (\<forall>i::nat\<in>{0..(n-1)}. subgroup (H i) G \<and> H i \<noteq> carrier G) \<and> (carrier G = (\<Union>i::nat\<in>{0..(n-1)}. H i))))"
-  shows "\<not>(h 2) \<and> ((\<not>(h 3)) \<longleftrightarrow> putnam_1969_b2_solution)"
+  fixes P :: "nat \<Rightarrow> bool"
+  defines "P \<equiv> \<lambda> n. \<forall> G. group G \<and> finite (carrier G) \<longrightarrow>
+    (\<forall> H. (\<forall> i\<in>{0..<n}. subgroup (H i) G \<and> (H i) \<noteq> carrier G) \<longrightarrow> (carrier G \<noteq> (\<Union>i::nat\<in>{0..<n}. H i)))"
+  shows "P 2 \<and> (P 3 \<longleftrightarrow> putnam_1969_b2_solution)"
   sorry
 
 end