author | paulson |
Tue, 18 Jun 2002 10:52:08 +0200 | |
changeset 13218 | 3732064ccbd1 |
parent 13175 | 81082cfa5618 |
child 13244 | 7b37e218f298 |
permissions | -rw-r--r-- |
2469 | 1 |
(* Title: ZF/AC/OrdQuant.thy |
2 |
ID: $Id$ |
|
3 |
Authors: Krzysztof Grabczewski and L C Paulson |
|
4 |
||
5 |
Quantifiers and union operator for ordinals. |
|
6 |
*) |
|
7 |
||
12620 | 8 |
theory OrdQuant = Ordinal: |
2469 | 9 |
|
12620 | 10 |
constdefs |
2469 | 11 |
|
12 |
(* Ordinal Quantifiers *) |
|
12620 | 13 |
oall :: "[i, i => o] => o" |
14 |
"oall(A, P) == ALL x. x<A --> P(x)" |
|
15 |
||
16 |
oex :: "[i, i => o] => o" |
|
17 |
"oex(A, P) == EX x. x<A & P(x)" |
|
2469 | 18 |
|
19 |
(* Ordinal Union *) |
|
12620 | 20 |
OUnion :: "[i, i => i] => i" |
21 |
"OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}" |
|
2469 | 22 |
|
23 |
syntax |
|
12620 | 24 |
"@oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10) |
25 |
"@oex" :: "[idt, i, o] => o" ("(3EX _<_./ _)" 10) |
|
26 |
"@OUNION" :: "[idt, i, i] => i" ("(3UN _<_./ _)" 10) |
|
2469 | 27 |
|
28 |
translations |
|
29 |
"ALL x<a. P" == "oall(a, %x. P)" |
|
30 |
"EX x<a. P" == "oex(a, %x. P)" |
|
31 |
"UN x<a. B" == "OUnion(a, %x. B)" |
|
32 |
||
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
6093
diff
changeset
|
33 |
syntax (xsymbols) |
12620 | 34 |
"@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10) |
35 |
"@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10) |
|
36 |
"@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10) |
|
37 |
||
38 |
||
12825 | 39 |
(** simplification of the new quantifiers **) |
40 |
||
41 |
||
13169 | 42 |
(*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize |
43 |
is proved. Ord_atomize would convert this rule to |
|
12825 | 44 |
x < 0 ==> P(x) == True, which causes dire effects!*) |
45 |
lemma [simp]: "(ALL x<0. P(x))" |
|
46 |
by (simp add: oall_def) |
|
47 |
||
48 |
lemma [simp]: "~(EX x<0. P(x))" |
|
49 |
by (simp add: oex_def) |
|
50 |
||
51 |
lemma [simp]: "(ALL x<succ(i). P(x)) <-> (Ord(i) --> P(i) & (ALL x<i. P(x)))" |
|
52 |
apply (simp add: oall_def le_iff) |
|
53 |
apply (blast intro: lt_Ord2) |
|
54 |
done |
|
55 |
||
56 |
lemma [simp]: "(EX x<succ(i). P(x)) <-> (Ord(i) & (P(i) | (EX x<i. P(x))))" |
|
57 |
apply (simp add: oex_def le_iff) |
|
58 |
apply (blast intro: lt_Ord2) |
|
59 |
done |
|
60 |
||
13118 | 61 |
(** Now some very basic ZF theorems **) |
62 |
||
13172 | 63 |
(*FIXME: move to Rel.thy*) |
13118 | 64 |
lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)" |
65 |
by (unfold trans_def trans_on_def, blast) |
|
66 |
||
12620 | 67 |
lemma Ord_OUN [intro,simp]: |
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13149
diff
changeset
|
68 |
"[| !!x. x<A ==> Ord(B(x)) |] ==> Ord(\<Union>x<A. B(x))" |
12620 | 69 |
by (simp add: OUnion_def ltI Ord_UN) |
70 |
||
71 |
lemma OUN_upper_lt: |
|
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13149
diff
changeset
|
72 |
"[| a<A; i < b(a); Ord(\<Union>x<A. b(x)) |] ==> i < (\<Union>x<A. b(x))" |
12620 | 73 |
by (unfold OUnion_def lt_def, blast ) |
74 |
||
75 |
lemma OUN_upper_le: |
|
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13149
diff
changeset
|
76 |
"[| a<A; i\<le>b(a); Ord(\<Union>x<A. b(x)) |] ==> i \<le> (\<Union>x<A. b(x))" |
12820 | 77 |
apply (unfold OUnion_def, auto) |
12620 | 78 |
apply (rule UN_upper_le ) |
79 |
apply (auto simp add: lt_def) |
|
80 |
done |
|
2469 | 81 |
|
12620 | 82 |
lemma Limit_OUN_eq: "Limit(i) ==> (UN x<i. x) = i" |
83 |
by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord) |
|
84 |
||
85 |
(* No < version; consider (UN i:nat.i)=nat *) |
|
86 |
lemma OUN_least: |
|
87 |
"(!!x. x<A ==> B(x) \<subseteq> C) ==> (UN x<A. B(x)) \<subseteq> C" |
|
88 |
by (simp add: OUnion_def UN_least ltI) |
|
89 |
||
90 |
(* No < version; consider (UN i:nat.i)=nat *) |
|
91 |
lemma OUN_least_le: |
|
92 |
"[| Ord(i); !!x. x<A ==> b(x) \<le> i |] ==> (UN x<A. b(x)) \<le> i" |
|
93 |
by (simp add: OUnion_def UN_least_le ltI Ord_0_le) |
|
94 |
||
95 |
lemma le_implies_OUN_le_OUN: |
|
96 |
"[| !!x. x<A ==> c(x) \<le> d(x) |] ==> (UN x<A. c(x)) \<le> (UN x<A. d(x))" |
|
97 |
by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN) |
|
98 |
||
99 |
lemma OUN_UN_eq: |
|
100 |
"(!!x. x:A ==> Ord(B(x))) |
|
101 |
==> (UN z < (UN x:A. B(x)). C(z)) = (UN x:A. UN z < B(x). C(z))" |
|
102 |
by (simp add: OUnion_def) |
|
103 |
||
104 |
lemma OUN_Union_eq: |
|
105 |
"(!!x. x:X ==> Ord(x)) |
|
106 |
==> (UN z < Union(X). C(z)) = (UN x:X. UN z < x. C(z))" |
|
107 |
by (simp add: OUnion_def) |
|
108 |
||
12763 | 109 |
(*So that rule_format will get rid of ALL x<A...*) |
110 |
lemma atomize_oall [symmetric, rulify]: |
|
111 |
"(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))" |
|
112 |
by (simp add: oall_def atomize_all atomize_imp) |
|
113 |
||
13169 | 114 |
(*** universal quantifier for ordinals ***) |
115 |
||
116 |
lemma oallI [intro!]: |
|
117 |
"[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)" |
|
13170 | 118 |
by (simp add: oall_def) |
13169 | 119 |
|
120 |
lemma ospec: "[| ALL x<A. P(x); x<A |] ==> P(x)" |
|
13170 | 121 |
by (simp add: oall_def) |
13169 | 122 |
|
123 |
lemma oallE: |
|
124 |
"[| ALL x<A. P(x); P(x) ==> Q; ~x<A ==> Q |] ==> Q" |
|
13170 | 125 |
apply (simp add: oall_def, blast) |
13169 | 126 |
done |
127 |
||
128 |
lemma rev_oallE [elim]: |
|
129 |
"[| ALL x<A. P(x); ~x<A ==> Q; P(x) ==> Q |] ==> Q" |
|
13170 | 130 |
apply (simp add: oall_def, blast) |
13169 | 131 |
done |
132 |
||
133 |
||
134 |
(*Trival rewrite rule; (ALL x<a.P)<->P holds only if a is not 0!*) |
|
135 |
lemma oall_simp [simp]: "(ALL x<a. True) <-> True" |
|
13170 | 136 |
by blast |
13169 | 137 |
|
138 |
(*Congruence rule for rewriting*) |
|
139 |
lemma oall_cong [cong]: |
|
140 |
"[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')" |
|
141 |
by (simp add: oall_def) |
|
142 |
||
143 |
||
144 |
(*** existential quantifier for ordinals ***) |
|
145 |
||
146 |
lemma oexI [intro]: |
|
147 |
"[| P(x); x<A |] ==> EX x<A. P(x)" |
|
13170 | 148 |
apply (simp add: oex_def, blast) |
13169 | 149 |
done |
150 |
||
151 |
(*Not of the general form for such rules; ~EX has become ALL~ *) |
|
152 |
lemma oexCI: |
|
153 |
"[| ALL x<A. ~P(x) ==> P(a); a<A |] ==> EX x<A. P(x)" |
|
13170 | 154 |
apply (simp add: oex_def, blast) |
13169 | 155 |
done |
156 |
||
157 |
lemma oexE [elim!]: |
|
158 |
"[| EX x<A. P(x); !!x. [| x<A; P(x) |] ==> Q |] ==> Q" |
|
13170 | 159 |
apply (simp add: oex_def, blast) |
13169 | 160 |
done |
161 |
||
162 |
lemma oex_cong [cong]: |
|
163 |
"[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) |] ==> oex(a,P) <-> oex(a',P')" |
|
164 |
apply (simp add: oex_def cong add: conj_cong) |
|
165 |
done |
|
166 |
||
167 |
||
168 |
(*** Rules for Ordinal-Indexed Unions ***) |
|
169 |
||
170 |
lemma OUN_I [intro]: "[| a<i; b: B(a) |] ==> b: (UN z<i. B(z))" |
|
13170 | 171 |
by (unfold OUnion_def lt_def, blast) |
13169 | 172 |
|
173 |
lemma OUN_E [elim!]: |
|
174 |
"[| b : (UN z<i. B(z)); !!a.[| b: B(a); a<i |] ==> R |] ==> R" |
|
13170 | 175 |
apply (unfold OUnion_def lt_def, blast) |
13169 | 176 |
done |
177 |
||
178 |
lemma OUN_iff: "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))" |
|
13170 | 179 |
by (unfold OUnion_def oex_def lt_def, blast) |
13169 | 180 |
|
181 |
lemma OUN_cong [cong]: |
|
182 |
"[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))" |
|
183 |
by (simp add: OUnion_def lt_def OUN_iff) |
|
184 |
||
185 |
lemma lt_induct: |
|
186 |
"[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) |] ==> P(i)" |
|
187 |
apply (simp add: lt_def oall_def) |
|
188 |
apply (erule conjE) |
|
13170 | 189 |
apply (erule Ord_induct, assumption, blast) |
13169 | 190 |
done |
191 |
||
192 |
ML |
|
193 |
{* |
|
194 |
val oall_def = thm "oall_def" |
|
195 |
val oex_def = thm "oex_def" |
|
196 |
val OUnion_def = thm "OUnion_def" |
|
197 |
||
198 |
val oallI = thm "oallI"; |
|
199 |
val ospec = thm "ospec"; |
|
200 |
val oallE = thm "oallE"; |
|
201 |
val rev_oallE = thm "rev_oallE"; |
|
202 |
val oall_simp = thm "oall_simp"; |
|
203 |
val oall_cong = thm "oall_cong"; |
|
204 |
val oexI = thm "oexI"; |
|
205 |
val oexCI = thm "oexCI"; |
|
206 |
val oexE = thm "oexE"; |
|
207 |
val oex_cong = thm "oex_cong"; |
|
208 |
val OUN_I = thm "OUN_I"; |
|
209 |
val OUN_E = thm "OUN_E"; |
|
210 |
val OUN_iff = thm "OUN_iff"; |
|
211 |
val OUN_cong = thm "OUN_cong"; |
|
212 |
val lt_induct = thm "lt_induct"; |
|
213 |
||
214 |
val Ord_atomize = |
|
215 |
atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs); |
|
216 |
simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all); |
|
217 |
*} |
|
218 |
||
2469 | 219 |
end |