isabelle: src/ZF/AC/WO_AC.ML@1a386a1e002c (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	1	(* Title: ZF/AC/WO_AC.ML
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	3	Author: Krzysztof Grabczewski
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	4
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	5	Lemmas used in the proofs like WO? ==> AC?
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	6	*)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	7
11317 7f9e4c389318 X-symbols for set theory paulson parents: 5137 diff changeset	8	Goal "[\| well_ord(Union(A),r); 0\\<notin>A; B \\<in> A \|] \
7f9e4c389318 X-symbols for set theory paulson parents: 5137 diff changeset	9	\ ==> (THE b. first(b,B,r)) \\<in> B";
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3731 diff changeset	10	by (fast_tac (claset() addSEs [well_ord_imp_ex1_first RS theI RS
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	11	(first_def RS def_imp_iff RS iffD1 RS conjunct1)]) 1);
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	12	qed "first_in_B";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	13
11317 7f9e4c389318 X-symbols for set theory paulson parents: 5137 diff changeset	14	Goal "[\| well_ord(Union(A), R); 0\\<notin>A \|] ==> \\<exists>f. f:(\\<Pi>X \\<in> A. X)";
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3731 diff changeset	15	by (fast_tac (claset() addSEs [first_in_B] addSIs [lam_type]) 1);
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	16	qed "ex_choice_fun";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	17
11317 7f9e4c389318 X-symbols for set theory paulson parents: 5137 diff changeset	18	Goal "well_ord(A, R) ==> \\<exists>f. f:(\\<Pi>X \\<in> Pow(A)-{0}. X)";
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3731 diff changeset	19	by (fast_tac (claset() addSEs [well_ord_subset RS ex_choice_fun]) 1);
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	20	qed "ex_choice_fun_Pow";

author	wenzelm
	Mon, 22 Oct 2001 17:58:11 +0200
changeset 11879	1a386a1e002c
parent 11317	7f9e4c389318
permissions	-rw-r--r--