author  paulson 
Wed, 15 May 2002 10:42:32 +0200  
changeset 13149  773657d466cb 
parent 13118  336b0bcbd27c 
child 13162  660a71e712af 
permissions  rwrr 
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 