author | paulson |
Mon, 23 Jul 2001 17:47:49 +0200 | |
changeset 11448 | aa519e0cc050 |
parent 6121 | 5fe77b9b5185 |
permissions | -rw-r--r-- |
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
1 |
(**** ZF examples ****) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
2 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
3 |
Pretty.setmargin 72; (*existing macros just allow this margin*) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
4 |
print_depth 0; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
5 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
6 |
(*** Powerset example ***) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
7 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
8 |
val [prem] = goal ZF.thy "A<=B ==> Pow(A) <= Pow(B)"; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
9 |
by (resolve_tac [subsetI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
10 |
by (resolve_tac [PowI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
11 |
by (dresolve_tac [PowD] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
12 |
by (eresolve_tac [subset_trans] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
13 |
by (resolve_tac [prem] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
14 |
val Pow_mono = result(); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
15 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
16 |
goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)"; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
17 |
by (resolve_tac [equalityI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
18 |
by (resolve_tac [Int_greatest] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
19 |
by (resolve_tac [Int_lower1 RS Pow_mono] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
20 |
by (resolve_tac [Int_lower2 RS Pow_mono] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
21 |
by (resolve_tac [subsetI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
22 |
by (eresolve_tac [IntE] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
23 |
by (resolve_tac [PowI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
24 |
by (REPEAT (dresolve_tac [PowD] 1)); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
25 |
by (resolve_tac [Int_greatest] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
26 |
by (REPEAT (assume_tac 1)); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
27 |
choplev 0; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
28 |
by (fast_tac (ZF_cs addIs [equalityI]) 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
29 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
30 |
Goal "C<=D ==> Union(C) <= Union(D)"; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
31 |
by (resolve_tac [subsetI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
32 |
by (eresolve_tac [UnionE] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
33 |
by (resolve_tac [UnionI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
34 |
by (eresolve_tac [subsetD] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
35 |
by (assume_tac 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
36 |
by (assume_tac 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
37 |
choplev 0; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
38 |
by (resolve_tac [Union_least] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
39 |
by (resolve_tac [Union_upper] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
40 |
by (eresolve_tac [subsetD] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
41 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
42 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
43 |
val prems = goal ZF.thy |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
44 |
"[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
45 |
\ (f Un g)`a = f`a"; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
46 |
by (resolve_tac [apply_equality] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
47 |
by (resolve_tac [UnI1] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
48 |
by (resolve_tac [apply_Pair] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
49 |
by (resolve_tac prems 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
50 |
by (resolve_tac prems 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
51 |
by (resolve_tac [fun_disjoint_Un] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
52 |
by (resolve_tac prems 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
53 |
by (resolve_tac prems 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
54 |
by (resolve_tac prems 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
55 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
56 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
57 |
Goal "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
58 |
\ (f Un g)`a = f`a"; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
59 |
by (resolve_tac [apply_equality] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
60 |
by (resolve_tac [UnI1] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
61 |
by (resolve_tac [apply_Pair] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
62 |
by (assume_tac 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
63 |
by (assume_tac 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
64 |
by (resolve_tac [fun_disjoint_Un] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
65 |
by (assume_tac 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
66 |
by (assume_tac 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
67 |
by (assume_tac 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
68 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
69 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
70 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
71 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
72 |
goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))"; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
73 |
by (resolve_tac [equalityI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
74 |
by (resolve_tac [subsetI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
75 |
fe imageE; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
76 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
77 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
78 |
goal ZF.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x)) Int B"; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
79 |
by (resolve_tac [equalityI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
80 |
by (resolve_tac [Int_greatest] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
81 |
fr UN_mono; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
82 |
by (resolve_tac [Int_lower1] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
83 |
fr UN_least; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
84 |
???? |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
85 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
86 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
87 |
> goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)"; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
88 |
Level 0 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
89 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
90 |
1. Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
91 |
> by (resolve_tac [equalityI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
92 |
Level 1 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
93 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
94 |
1. Pow(A Int B) <= Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
95 |
2. Pow(A) Int Pow(B) <= Pow(A Int B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
96 |
> by (resolve_tac [Int_greatest] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
97 |
Level 2 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
98 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
99 |
1. Pow(A Int B) <= Pow(A) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
100 |
2. Pow(A Int B) <= Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
101 |
3. Pow(A) Int Pow(B) <= Pow(A Int B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
102 |
> by (resolve_tac [Int_lower1 RS Pow_mono] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
103 |
Level 3 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
104 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
105 |
1. Pow(A Int B) <= Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
106 |
2. Pow(A) Int Pow(B) <= Pow(A Int B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
107 |
> by (resolve_tac [Int_lower2 RS Pow_mono] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
108 |
Level 4 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
109 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
110 |
1. Pow(A) Int Pow(B) <= Pow(A Int B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
111 |
> by (resolve_tac [subsetI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
112 |
Level 5 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
113 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
114 |
1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
115 |
> by (eresolve_tac [IntE] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
116 |
Level 6 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
117 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
118 |
1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
119 |
> by (resolve_tac [PowI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
120 |
Level 7 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
121 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
122 |
1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
123 |
> by (REPEAT (dresolve_tac [PowD] 1)); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
124 |
Level 8 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
125 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
126 |
1. !!x. [| x <= A; x <= B |] ==> x <= A Int B |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
127 |
> by (resolve_tac [Int_greatest] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
128 |
Level 9 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
129 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
130 |
1. !!x. [| x <= A; x <= B |] ==> x <= A |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
131 |
2. !!x. [| x <= A; x <= B |] ==> x <= B |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
132 |
> by (REPEAT (assume_tac 1)); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
133 |
Level 10 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
134 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
135 |
No subgoals! |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
136 |
> choplev 0; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
137 |
Level 0 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
138 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
139 |
1. Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
140 |
> by (fast_tac (ZF_cs addIs [equalityI]) 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
141 |
Level 1 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
142 |
Pow(A Int B) = Pow(A) Int Pow(B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
143 |
No subgoals! |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
144 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
145 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
146 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
147 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
148 |
> val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)"; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
149 |
Level 0 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
150 |
Union(C) <= Union(D) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
151 |
1. Union(C) <= Union(D) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
152 |
> by (resolve_tac [subsetI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
153 |
Level 1 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
154 |
Union(C) <= Union(D) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
155 |
1. !!x. x : Union(C) ==> x : Union(D) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
156 |
> by (eresolve_tac [UnionE] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
157 |
Level 2 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
158 |
Union(C) <= Union(D) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
159 |
1. !!x B. [| x : B; B : C |] ==> x : Union(D) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
160 |
> by (resolve_tac [UnionI] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
161 |
Level 3 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
162 |
Union(C) <= Union(D) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
163 |
1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
164 |
2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
165 |
> by (resolve_tac [prem RS subsetD] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
166 |
Level 4 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
167 |
Union(C) <= Union(D) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
168 |
1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
169 |
2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
170 |
> by (assume_tac 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
171 |
Level 5 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
172 |
Union(C) <= Union(D) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
173 |
1. !!x B. [| x : B; B : C |] ==> x : B |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
174 |
> by (assume_tac 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
175 |
Level 6 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
176 |
Union(C) <= Union(D) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
177 |
No subgoals! |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
178 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
179 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
180 |
|
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
181 |
> val prems = goal ZF.thy |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
182 |
# "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \ |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
183 |
# \ (f Un g)`a = f`a"; |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
184 |
Level 0 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
185 |
(f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
186 |
1. (f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
187 |
> by (resolve_tac [apply_equality] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
188 |
Level 1 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
189 |
(f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
190 |
1. <a,f ` a> : f Un g |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
191 |
2. f Un g : (PROD x:?A. ?B(x)) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
192 |
> by (resolve_tac [UnI1] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
193 |
Level 2 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
194 |
(f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
195 |
1. <a,f ` a> : f |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
196 |
2. f Un g : (PROD x:?A. ?B(x)) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
197 |
> by (resolve_tac [apply_Pair] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
198 |
Level 3 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
199 |
(f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
200 |
1. f : (PROD x:?A2. ?B2(x)) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
201 |
2. a : ?A2 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
202 |
3. f Un g : (PROD x:?A. ?B(x)) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
203 |
> by (resolve_tac prems 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
204 |
Level 4 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
205 |
(f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
206 |
1. a : A |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
207 |
2. f Un g : (PROD x:?A. ?B(x)) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
208 |
> by (resolve_tac prems 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
209 |
Level 5 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
210 |
(f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
211 |
1. f Un g : (PROD x:?A. ?B(x)) |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
212 |
> by (resolve_tac [fun_disjoint_Un] 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
213 |
Level 6 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
214 |
(f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
215 |
1. f : ?A3 -> ?B3 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
216 |
2. g : ?C3 -> ?D3 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
217 |
3. ?A3 Int ?C3 = 0 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
218 |
> by (resolve_tac prems 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
219 |
Level 7 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
220 |
(f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
221 |
1. g : ?C3 -> ?D3 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
222 |
2. A Int ?C3 = 0 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
223 |
> by (resolve_tac prems 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
224 |
Level 8 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
225 |
(f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
226 |
1. A Int C = 0 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
227 |
> by (resolve_tac prems 1); |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
228 |
Level 9 |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
229 |
(f Un g) ` a = f ` a |
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset
|
230 |
No subgoals! |