author | paulson |
Wed, 15 May 2002 10:42:32 +0200 | |
changeset 13149 | 773657d466cb |
parent 13118 | 336b0bcbd27c |
child 13162 | 660a71e712af |
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 |
||
42 |
(*MOST IMPORTANT that this is added to the simpset BEFORE OrdQuant.ML |
|
43 |
is loaded: it's Ord_atomize would convert this rule to |
|
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 |
||
12667 | 61 |
declare Ord_Un [intro,simp,TC] |
62 |
declare Ord_UN [intro,simp,TC] |
|
63 |
declare Ord_Union [intro,simp,TC] |
|
12620 | 64 |
|
13118 | 65 |
(** Now some very basic ZF theorems **) |
66 |
||
67 |
lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))" |
|
68 |
by blast |
|
69 |
||
70 |
lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)" |
|
71 |
by blast |
|
72 |
||
73 |
lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)" |
|
74 |
by (unfold trans_def trans_on_def, blast) |
|
75 |
||
76 |
lemma image_is_UN: "\<lbrakk>function(g); x <= domain(g)\<rbrakk> \<Longrightarrow> g``x = (UN k:x. {g`k})" |
|
77 |
by (blast intro: function_apply_equality [THEN sym] function_apply_Pair) |
|
78 |
||
79 |
lemma functionI: |
|
80 |
"\<lbrakk>!!x y y'. \<lbrakk><x,y>:r; <x,y'>:r\<rbrakk> \<Longrightarrow> y=y'\<rbrakk> \<Longrightarrow> function(r)" |
|
81 |
by (simp add: function_def, blast) |
|
82 |
||
83 |
lemma function_lam: "function (lam x:A. b(x))" |
|
84 |
by (simp add: function_def lam_def) |
|
85 |
||
86 |
lemma relation_lam: "relation (lam x:A. b(x))" |
|
13149
773657d466cb
better simplification of trivial existential equalities
paulson
parents:
13118
diff
changeset
|
87 |
by (simp add: relation_def lam_def) |
13118 | 88 |
|
89 |
lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)" |
|
90 |
by (simp add: restrict_def) |
|
91 |
||
12620 | 92 |
(** These mostly belong to theory Ordinal **) |
93 |
||
94 |
lemma Union_upper_le: |
|
95 |
"\<lbrakk>j: J; i\<le>j; Ord(\<Union>(J))\<rbrakk> \<Longrightarrow> i \<le> \<Union>J" |
|
96 |
apply (subst Union_eq_UN) |
|
12820 | 97 |
apply (rule UN_upper_le, auto) |
12620 | 98 |
done |
99 |
||
12667 | 100 |
lemma zero_not_Limit [iff]: "~ Limit(0)" |
101 |
by (simp add: Limit_def) |
|
102 |
||
103 |
lemma Limit_has_1: "Limit(i) \<Longrightarrow> 1 < i" |
|
104 |
by (blast intro: Limit_has_0 Limit_has_succ) |
|
105 |
||
106 |
lemma Limit_Union [rule_format]: "\<lbrakk>I \<noteq> 0; \<forall>i\<in>I. Limit(i)\<rbrakk> \<Longrightarrow> Limit(\<Union>I)" |
|
107 |
apply (simp add: Limit_def lt_def) |
|
108 |
apply (blast intro!: equalityI) |
|
109 |
done |
|
110 |
||
12620 | 111 |
lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)" |
12820 | 112 |
apply (simp add: Limit_def lt_Ord2, clarify) |
12620 | 113 |
apply (drule_tac i=y in ltD) |
12825 | 114 |
apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2) |
12620 | 115 |
done |
116 |
||
117 |
lemma UN_upper_lt: |
|
12825 | 118 |
"\<lbrakk>a\<in>A; i < b(a); Ord(\<Union>x\<in>A. b(x))\<rbrakk> \<Longrightarrow> i < (\<Union>x\<in>A. b(x))" |
12620 | 119 |
by (unfold lt_def, blast) |
120 |
||
121 |
lemma lt_imp_0_lt: "j<i \<Longrightarrow> 0<i" |
|
122 |
by (blast intro: lt_trans1 Ord_0_le [OF lt_Ord]) |
|
123 |
||
124 |
lemma Ord_set_cases: |
|
125 |
"\<forall>i\<in>I. Ord(i) \<Longrightarrow> I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))" |
|
126 |
apply (clarify elim!: not_emptyE) |
|
127 |
apply (cases "\<Union>(I)" rule: Ord_cases) |
|
128 |
apply (blast intro: Ord_Union) |
|
129 |
apply (blast intro: subst_elem) |
|
130 |
apply auto |
|
131 |
apply (clarify elim!: equalityE succ_subsetE) |
|
132 |
apply (simp add: Union_subset_iff) |
|
133 |
apply (subgoal_tac "B = succ(j)", blast ) |
|
134 |
apply (rule le_anti_sym) |
|
135 |
apply (simp add: le_subset_iff) |
|
136 |
apply (simp add: ltI) |
|
137 |
done |
|
138 |
||
139 |
lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)|] ==> succ(j) \<in> X" |
|
140 |
by (drule Ord_set_cases, auto) |
|
141 |
||
142 |
(*See also Transset_iff_Union_succ*) |
|
143 |
lemma Ord_Union_succ_eq: "Ord(i) \<Longrightarrow> \<Union>(succ(i)) = i" |
|
144 |
by (blast intro: Ord_trans) |
|
2540 | 145 |
|
12620 | 146 |
lemma lt_Union_iff: "\<forall>i\<in>A. Ord(i) \<Longrightarrow> (j < \<Union>(A)) <-> (\<exists>i\<in>A. j<i)" |
147 |
by (auto simp: lt_def Ord_Union) |
|
148 |
||
149 |
lemma Un_upper1_lt: "[|k < i; Ord(j)|] ==> k < i Un j" |
|
150 |
by (simp add: lt_def) |
|
151 |
||
152 |
lemma Un_upper2_lt: "[|k < j; Ord(i)|] ==> k < i Un j" |
|
153 |
by (simp add: lt_def) |
|
154 |
||
155 |
lemma Ord_OUN [intro,simp]: |
|
156 |
"\<lbrakk>!!x. x<A \<Longrightarrow> Ord(B(x))\<rbrakk> \<Longrightarrow> Ord(\<Union>x<A. B(x))" |
|
157 |
by (simp add: OUnion_def ltI Ord_UN) |
|
158 |
||
159 |
lemma OUN_upper_lt: |
|
160 |
"\<lbrakk>a<A; i < b(a); Ord(\<Union>x<A. b(x))\<rbrakk> \<Longrightarrow> i < (\<Union>x<A. b(x))" |
|
161 |
by (unfold OUnion_def lt_def, blast ) |
|
162 |
||
163 |
lemma OUN_upper_le: |
|
164 |
"\<lbrakk>a<A; i\<le>b(a); Ord(\<Union>x<A. b(x))\<rbrakk> \<Longrightarrow> i \<le> (\<Union>x<A. b(x))" |
|
12820 | 165 |
apply (unfold OUnion_def, auto) |
12620 | 166 |
apply (rule UN_upper_le ) |
167 |
apply (auto simp add: lt_def) |
|
168 |
done |
|
2469 | 169 |
|
12620 | 170 |
lemma Limit_OUN_eq: "Limit(i) ==> (UN x<i. x) = i" |
171 |
by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord) |
|
172 |
||
173 |
(* No < version; consider (UN i:nat.i)=nat *) |
|
174 |
lemma OUN_least: |
|
175 |
"(!!x. x<A ==> B(x) \<subseteq> C) ==> (UN x<A. B(x)) \<subseteq> C" |
|
176 |
by (simp add: OUnion_def UN_least ltI) |
|
177 |
||
178 |
(* No < version; consider (UN i:nat.i)=nat *) |
|
179 |
lemma OUN_least_le: |
|
180 |
"[| Ord(i); !!x. x<A ==> b(x) \<le> i |] ==> (UN x<A. b(x)) \<le> i" |
|
181 |
by (simp add: OUnion_def UN_least_le ltI Ord_0_le) |
|
182 |
||
183 |
lemma le_implies_OUN_le_OUN: |
|
184 |
"[| !!x. x<A ==> c(x) \<le> d(x) |] ==> (UN x<A. c(x)) \<le> (UN x<A. d(x))" |
|
185 |
by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN) |
|
186 |
||
187 |
lemma OUN_UN_eq: |
|
188 |
"(!!x. x:A ==> Ord(B(x))) |
|
189 |
==> (UN z < (UN x:A. B(x)). C(z)) = (UN x:A. UN z < B(x). C(z))" |
|
190 |
by (simp add: OUnion_def) |
|
191 |
||
192 |
lemma OUN_Union_eq: |
|
193 |
"(!!x. x:X ==> Ord(x)) |
|
194 |
==> (UN z < Union(X). C(z)) = (UN x:X. UN z < x. C(z))" |
|
195 |
by (simp add: OUnion_def) |
|
196 |
||
12763 | 197 |
(*So that rule_format will get rid of ALL x<A...*) |
198 |
lemma atomize_oall [symmetric, rulify]: |
|
199 |
"(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))" |
|
200 |
by (simp add: oall_def atomize_all atomize_imp) |
|
201 |
||
2469 | 202 |
end |