# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1669047709 0
# Node ID 4d6d8dfd2cd2ffbded3742f5aba9cc5ddc24b529
# Parent  137cec33346f0193c92fb6e619500024eecf08e7
Added an example for Isabelle/CTT

diff -r 137cec33346f -r 4d6d8dfd2cd2 src/CTT/ex/Elimination.thy
--- a/src/CTT/ex/Elimination.thy	Sun Nov 20 23:53:39 2022 +0100
+++ b/src/CTT/ex/Elimination.thy	Mon Nov 21 16:21:49 2022 +0000
@@ -146,6 +146,28 @@
        apply (typechk SumE_fst assms)
   done
 
+text \<open>A structured proof of AC\<close>
+lemma Axiom_of_Choice:
+  assumes "A type"
+    and "\<And>x. x:A \<Longrightarrow> B(x) type"
+    and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
+  shows "(\<^bold>\<lambda>f. <\<^bold>\<lambda>x. fst(f`x), \<^bold>\<lambda>x. snd(f`x)>) 
+        : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
+proof (intr assms)
+  fix f a
+  assume f: "f : \<Prod>x:A. Sum(B(x), C(x))" and "a : A" 
+  then have fa: "f`a : Sum(B(a), C(a))"
+    by (rule ProdE)
+  then show "fst(f ` a) : B(a)" 
+    by (rule SumE_fst)
+  have "snd(f ` a) : C(a, fst(f ` a))"
+    by (rule SumE_snd [OF fa]) (typechk SumE_fst assms \<open>a : A\<close>)
+  moreover have "(\<^bold>\<lambda>x. fst(f ` x)) ` a = fst(f ` a) : B(a)"
+    by (rule ProdC [OF \<open>a : A\<close>]) (typechk SumE_fst f)
+  ultimately show "snd(f`a) : C(a, (\<^bold>\<lambda>x. fst(f ` x)) ` a)"
+    by (intro replace_type [OF subst_eqtyparg]) (typechk SumE_fst assms \<open>a : A\<close>)
+qed
+
 text "Axiom of choice.  Proof without fst, snd.  Harder still!"
 schematic_goal [folded basic_defs]:
   assumes "A type"