isabelle: src/ZF/AC/WO_AC.ML@032babd0120b (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
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	8	open WO_AC;
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	9
5137 60205b0de9b9 Huge tidy-up: removal of leading \!\! paulson parents: 5068 diff changeset	10	Goal "[\| well_ord(Union(A),r); 0~:A; B:A \|] \
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	11	\ ==> (THE b. first(b,B,r)) : B";
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3731 diff changeset	12	by (fast_tac (claset() addSEs [well_ord_imp_ex1_first RS theI RS
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	13	(first_def RS def_imp_iff RS iffD1 RS conjunct1)]) 1);
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	14	qed "first_in_B";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	15
5137 60205b0de9b9 Huge tidy-up: removal of leading \!\! paulson parents: 5068 diff changeset	16	Goal "[\| well_ord(Union(A), R); 0~:A \|] ==> EX f. f:(PROD X:A. X)";
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3731 diff changeset	17	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	18	qed "ex_choice_fun";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	19
5137 60205b0de9b9 Huge tidy-up: removal of leading \!\! paulson parents: 5068 diff changeset	20	Goal "well_ord(A, R) ==> EX f. f:(PROD X: Pow(A)-{0}. X)";
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3731 diff changeset	21	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	22	qed "ex_choice_fun_Pow";

author	paulson
	Thu, 07 Jan 1999 18:30:55 +0100
changeset 6070	032babd0120b
parent 5137	60205b0de9b9
child 11317	7f9e4c389318
permissions	-rw-r--r--