isabelle: src/ZF/AC/AC1_WO2.ML@c32c7ef228c6 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1206 diff changeset	1	(* Title: ZF/AC/AC1_WO2.ML
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1206 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	The proof of AC1 ==> WO2
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
2167 5819e85ad261 Adjusting to new version of uresult paulson parents: 1461 diff changeset	8	(Establishing the existence of a bijection -- hence the need for uresult)
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	9	val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==> \
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1206 diff changeset	10	\ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	11	by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);
1206 30df104ceb91 Ran expandshort and changed spelling of Grabczewski lcp parents: 1196 diff changeset	12	by (rtac f_subsets_imp_UN_HH_eq_x 1);
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	13	by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));
5470 855654b691db eliminated equals0E paulson parents: 5241 diff changeset	14	by (fast_tac (claset() addSDs [prem RS apply_type]) 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 2469 diff changeset	15	by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1);
2167 5819e85ad261 Adjusting to new version of uresult paulson parents: 1461 diff changeset	16	val lemma1 = uresult() \|> standard;
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	17
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5068 diff changeset	18	Goalw [AC1_def, WO2_def, eqpoll_def] "AC1 ==> WO2";
1206 30df104ceb91 Ran expandshort and changed spelling of Grabczewski lcp parents: 1196 diff changeset	19	by (rtac allI 1);
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	20	by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 2469 diff changeset	21	by (fast_tac (claset() addSDs [lemma1] addSIs [Ord_Least]) 1);
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: 1123 diff changeset	22	qed "AC1_WO2";

author	wenzelm
	Tue, 29 Aug 2000 20:14:16 +0200
changeset 9732	c32c7ef228c6
parent 9305	3dfae8f90dcf
child 11317	7f9e4c389318
permissions	-rw-r--r--