equal
deleted
inserted
replaced
12 |
12 |
13 goal thy "!!f. [| f:(PROD X:A. X); D<=A |] ==> EX g. g:(PROD X:D. X)"; |
13 goal thy "!!f. [| f:(PROD X:A. X); D<=A |] ==> EX g. g:(PROD X:D. X)"; |
14 by (fast_tac (AC_cs addSIs [restrict_type, apply_type]) 1); |
14 by (fast_tac (AC_cs addSIs [restrict_type, apply_type]) 1); |
15 val lemma1 = result(); |
15 val lemma1 = result(); |
16 |
16 |
17 val prems = goalw thy AC_defs "!!Z. AC0 ==> AC1"; |
17 goalw thy AC_defs "!!Z. AC0 ==> AC1"; |
18 by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1); |
18 by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1); |
19 result(); |
19 qed "AC0_AC1"; |
20 |
20 |
21 val prems = goalw thy AC_defs "!!Z. AC1 ==> AC0"; |
21 goalw thy AC_defs "!!Z. AC1 ==> AC0"; |
22 by (fast_tac (FOL_cs addSIs [notI, singletonI] addSEs [notE, DiffE]) 1); |
22 by (fast_tac (FOL_cs addSIs [notI, singletonI] addSEs [notE, DiffE]) 1); |
23 result(); |
23 qed "AC1_AC0"; |