isabelle: src/ZF/AC/WO1_WO8.ML@2f831a45d571 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	1	(* Title: ZF/AC/WO1_WO8.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	The proof of WO8 <-> WO1 (Rubin & Rubin p. 6)
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	(* ********************************************************************** *)
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	9	(* Trivial implication "WO1 ==> WO8" *)
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	10	(* ********************************************************************** *)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	11
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	12	goalw thy WO_defs "!!Z. WO1 ==> WO8";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1932 diff changeset	13	by (Fast_tac 1);
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: 1123 diff changeset	14	qed "WO1_WO8";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	15
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	16	(* ********************************************************************** *)
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	17	(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *)
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	18	(* ********************************************************************** *)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	19
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	20	goalw thy WO_defs "!!Z. WO8 ==> WO1";
1208 bc3093616ba4 Ran expandshort and corrected spelling of Grabczewski paulson parents: 1196 diff changeset	21	by (rtac allI 1);
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	22	by (eres_inst_tac [("x","{{x}. x:A}")] allE 1);
1208 bc3093616ba4 Ran expandshort and corrected spelling of Grabczewski paulson parents: 1196 diff changeset	23	by (etac impE 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 2493 diff changeset	24	by (fast_tac (claset() addSEs [lam_sing_bij RS bij_is_inj RS
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	25	well_ord_rvimage]) 2);
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	26	by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 2493 diff changeset	27	by (fast_tac (claset() addSIs [lam_type]
771b1f6422a8 isatool fixclasimp; wenzelm parents: 2493 diff changeset	28	addss (simpset() addsimps [singleton_eq_iff, the_equality])) 1);
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: 1123 diff changeset	29	qed "WO8_WO1";

author	wenzelm
	Fri, 05 Dec 1997 17:31:01 +0100
changeset 4373	2f831a45d571
parent 4091	771b1f6422a8
child 5068	fb28eaa07e01
permissions	-rw-r--r--