equal
deleted
inserted
replaced
133 text "AXIOM OF CHOICE! Delicate use of elimination rules" |
133 text "AXIOM OF CHOICE! Delicate use of elimination rules" |
134 schematic_goal |
134 schematic_goal |
135 assumes "A type" |
135 assumes "A type" |
136 and "\<And>x. x:A \<Longrightarrow> B(x) type" |
136 and "\<And>x. x:A \<Longrightarrow> B(x) type" |
137 and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type" |
137 and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type" |
138 shows "?a : \<Prod>h: (\<Prod>x:A. \<Sum>y:B(x). C(x,y)). |
138 shows "?a : (\<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))" |
139 (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))" |
|
140 apply (intr assms) |
139 apply (intr assms) |
141 prefer 2 apply add_mp |
140 prefer 2 apply add_mp |
142 prefer 2 apply add_mp |
141 prefer 2 apply add_mp |
143 apply (erule SumE_fst) |
142 apply (erule SumE_fst) |
144 apply (rule replace_type) |
143 apply (rule replace_type) |
151 text "Axiom of choice. Proof without fst, snd. Harder still!" |
150 text "Axiom of choice. Proof without fst, snd. Harder still!" |
152 schematic_goal [folded basic_defs]: |
151 schematic_goal [folded basic_defs]: |
153 assumes "A type" |
152 assumes "A type" |
154 and "\<And>x. x:A \<Longrightarrow> B(x) type" |
153 and "\<And>x. x:A \<Longrightarrow> B(x) type" |
155 and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type" |
154 and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type" |
156 shows "?a : \<Prod>h: (\<Prod>x:A. \<Sum>y:B(x). C(x,y)). |
155 shows "?a : (\<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))" |
157 (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))" |
|
158 apply (intr assms) |
156 apply (intr assms) |
159 (*Must not use add_mp as subst_prodE hides the construction.*) |
157 (*Must not use add_mp as subst_prodE hides the construction.*) |
160 apply (rule ProdE [THEN SumE]) |
158 apply (rule ProdE [THEN SumE]) |
161 apply assumption |
159 apply assumption |
162 apply assumption |
160 apply assumption |