equal
deleted
inserted
replaced
16 files "Tools/typechk": |
16 files "Tools/typechk": |
17 |
17 |
18 setup TypeCheck.setup |
18 setup TypeCheck.setup |
19 declare atomize_ball [symmetric, rulify] |
19 declare atomize_ball [symmetric, rulify] |
20 |
20 |
|
21 (*belongs to theory ZF*) |
|
22 declare bspec [dest?] |
|
23 |
21 (*** Lemmas about power sets ***) |
24 (*** Lemmas about power sets ***) |
22 |
25 |
23 lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *) |
26 lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *) |
24 lemmas Pow_top = subset_refl [THEN PowI] (* A : Pow(A) *) |
27 lemmas Pow_top = subset_refl [THEN PowI] (* A : Pow(A) *) |
25 |
28 |
51 lemma UnI1: "c : A ==> c : A Un B" |
54 lemma UnI1: "c : A ==> c : A Un B" |
52 by simp |
55 by simp |
53 |
56 |
54 lemma UnI2: "c : B ==> c : A Un B" |
57 lemma UnI2: "c : B ==> c : A Un B" |
55 by simp |
58 by simp |
|
59 |
|
60 (*belongs to theory upair*) |
|
61 declare UnI1 [elim?] UnI2 [elim?] |
56 |
62 |
57 lemma UnE [elim!]: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" |
63 lemma UnE [elim!]: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" |
58 apply simp |
64 apply simp |
59 apply blast |
65 apply blast |
60 done |
66 done |