|
1 (* Title: ZF/Coind/Language.ML |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 (* ############################################################ *) |
|
8 (* General lemmas *) |
|
9 (* ############################################################ *) |
|
10 |
|
11 goal ZF.thy "!!a.~a=b ==> ~a:{b}"; |
|
12 by (fast_tac ZF_cs 1); |
|
13 qed "notsingletonI"; |
|
14 |
|
15 goal ZF.thy "!!a.~a:{b} ==> ~a=b"; |
|
16 by (fast_tac ZF_cs 1); |
|
17 qed "notsingletonD"; |
|
18 |
|
19 val prems = goal ZF.thy "[| a~:{b}; a~=b ==> P |] ==> P"; |
|
20 by (cut_facts_tac prems 1); |
|
21 by (resolve_tac prems 1); |
|
22 by (fast_tac ZF_cs 1); |
|
23 qed "notsingletonE"; |
|
24 |
|
25 goal ZF.thy "!!x. x : A Un B ==> x: B Un A"; |
|
26 by (fast_tac ZF_cs 1); |
|
27 qed "lem_fix"; |
|
28 |
|
29 goal ZF.thy "!!A.[| x~:A; x=y |] ==> y~:A"; |
|
30 by (fast_tac ZF_cs 1); |
|
31 qed "map_lem1"; |
|
32 |
|
33 |
|
34 open Language; |
|
35 |
|
36 (* ############################################################ *) |
|
37 (* Inclusion in Quine Universes *) |
|
38 (* ############################################################ *) |
|
39 |
|
40 goal Language.thy "!!c.c:Const ==> c:quniv(A)"; |
|
41 by (fast_tac (ZF_cs addIs [univ_subset_quniv RS subsetD,constU]) 1); |
|
42 qed "constQU"; |
|
43 |
|
44 goal Language.thy "!!x.x:ExVar ==> x:quniv(A)"; |
|
45 by (fast_tac (ZF_cs addIs [univ_subset_quniv RS subsetD,exvarU]) 1); |
|
46 qed "exvarQU"; |
|
47 |
|
48 goal Language.thy "!!e.e:Exp ==> e:quniv(0)"; |
|
49 by (rtac subsetD 1); |
|
50 by (rtac subset_trans 1); |
|
51 by (rtac Exp.dom_subset 1); |
|
52 by (rtac univ_subset_quniv 1); |
|
53 by (assume_tac 1); |
|
54 qed "expQU"; |
|
55 |