isabelle: src/ZF/AC/AC0_AC1.ML@62b6288e6005 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1204 diff changeset	1	(* Title: ZF/AC/AC0_AC1.ML
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1204 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	AC0 is equivalent to AC1
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	6	AC0 comes from Suppes, AC1 from Rubin & Rubin
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
5067 62b6288e6005 isatool fixgoal; wenzelm parents: 4091 diff changeset	9	Goal "!!A. 0~:A ==> A <= Pow(Union(A))-{0}";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1924 diff changeset	10	by (Fast_tac 1);
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	11	qed "subset_Pow_Union";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	12
5067 62b6288e6005 isatool fixgoal; wenzelm parents: 4091 diff changeset	13	Goal "!!f. [\| f:(PROD X:A. X); D<=A \|] ==> EX g. g:(PROD X:D. X)";
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3731 diff changeset	14	by (fast_tac (claset() addSIs [restrict_type, apply_type]) 1);
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	15	val lemma1 = result();
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	16
5067 62b6288e6005 isatool fixgoal; wenzelm parents: 4091 diff changeset	17	Goalw AC_defs "!!Z. AC0 ==> AC1";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	18	by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1);
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: 1123 diff changeset	19	qed "AC0_AC1";
1123 5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs lcp parents: diff changeset	20
5067 62b6288e6005 isatool fixgoal; wenzelm parents: 4091 diff changeset	21	Goalw AC_defs "!!Z. AC1 ==> AC0";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1924 diff changeset	22	by (Deepen_tac 0 1);
1924 0f1a583457da Corrected for new classical reasoner: redundant rules paulson parents: 1461 diff changeset	23	(*Large search space. Faster proof by
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3731 diff changeset	24	by (fast_tac (claset() addSIs [notI, singletonI] addSEs [notE, DiffE]) 1);
1924 0f1a583457da Corrected for new classical reasoner: redundant rules paulson parents: 1461 diff changeset	25	*)
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: 1123 diff changeset	26	qed "AC1_AC0";

author	wenzelm
	Mon, 22 Jun 1998 17:12:27 +0200
changeset 5067	62b6288e6005
parent 4091	771b1f6422a8
child 5137	60205b0de9b9
permissions	-rw-r--r--