author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 48891  c0eafbd55de3 
child 58828  6d076fdd933d 
permissions  rwrr 
2469  1 
(* Title: ZF/upair.thy 
2 
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory 

3 
Copyright 1993 University of Cambridge 

13259  4 

5 
Observe the order of dependence: 

6 
Upair is defined in terms of Replace 

46820  7 
\<union> is defined in terms of Upair and \<Union>(similarly for Int) 
13259  8 
cons is defined in terms of Upair and Un 
9 
Ordered pairs and descriptions are defined using cons ("set notation") 

2469  10 
*) 
11 

13357  12 
header{*Unordered Pairs*} 
13 

46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46821
diff
changeset

14 
theory upair 
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46821
diff
changeset

15 
imports ZF 
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46821
diff
changeset

16 
keywords "print_tcset" :: diag 
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46821
diff
changeset

17 
begin 
6153  18 

48891  19 
ML_file "Tools/typechk.ML" 
9907  20 
setup TypeCheck.setup 
6153  21 

13780  22 
lemma atomize_ball [symmetric, rulify]: 
46953  23 
"(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))" 
13780  24 
by (simp add: Ball_def atomize_all atomize_imp) 
13259  25 

26 

13357  27 
subsection{*Unordered Pairs: constant @{term Upair}*} 
13259  28 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

29 
lemma Upair_iff [simp]: "c \<in> Upair(a,b) \<longleftrightarrow> (c=a  c=b)" 
13259  30 
by (unfold Upair_def, blast) 
31 

46820  32 
lemma UpairI1: "a \<in> Upair(a,b)" 
13259  33 
by simp 
34 

46820  35 
lemma UpairI2: "b \<in> Upair(a,b)" 
13259  36 
by simp 
37 

46820  38 
lemma UpairE: "[ a \<in> Upair(b,c); a=b ==> P; a=c ==> P ] ==> P" 
13780  39 
by (simp, blast) 
13259  40 

13357  41 
subsection{*Rules for Binary Union, Defined via @{term Upair}*} 
13259  42 

46953  43 
lemma Un_iff [simp]: "c \<in> A \<union> B \<longleftrightarrow> (c \<in> A  c \<in> B)" 
13259  44 
apply (simp add: Un_def) 
45 
apply (blast intro: UpairI1 UpairI2 elim: UpairE) 

46 
done 

47 

46820  48 
lemma UnI1: "c \<in> A ==> c \<in> A \<union> B" 
13259  49 
by simp 
50 

46820  51 
lemma UnI2: "c \<in> B ==> c \<in> A \<union> B" 
13259  52 
by simp 
53 

13356  54 
declare UnI1 [elim?] UnI2 [elim?] 
55 

46953  56 
lemma UnE [elim!]: "[ c \<in> A \<union> B; c \<in> A ==> P; c \<in> B ==> P ] ==> P" 
13780  57 
by (simp, blast) 
13259  58 

59 
(*Stronger version of the rule above*) 

46953  60 
lemma UnE': "[ c \<in> A \<union> B; c \<in> A ==> P; [ c \<in> B; c\<notin>A ] ==> P ] ==> P" 
13780  61 
by (simp, blast) 
13259  62 

63 
(*Classical introduction rule: no commitment to A vs B*) 

46820  64 
lemma UnCI [intro!]: "(c \<notin> B ==> c \<in> A) ==> c \<in> A \<union> B" 
13780  65 
by (simp, blast) 
13259  66 

13357  67 
subsection{*Rules for Binary Intersection, Defined via @{term Upair}*} 
13259  68 

46953  69 
lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> (c \<in> A & c \<in> B)" 
13259  70 
apply (unfold Int_def) 
71 
apply (blast intro: UpairI1 UpairI2 elim: UpairE) 

72 
done 

73 

46820  74 
lemma IntI [intro!]: "[ c \<in> A; c \<in> B ] ==> c \<in> A \<inter> B" 
13259  75 
by simp 
76 

46820  77 
lemma IntD1: "c \<in> A \<inter> B ==> c \<in> A" 
13259  78 
by simp 
79 

46820  80 
lemma IntD2: "c \<in> A \<inter> B ==> c \<in> B" 
13259  81 
by simp 
82 

46953  83 
lemma IntE [elim!]: "[ c \<in> A \<inter> B; [ c \<in> A; c \<in> B ] ==> P ] ==> P" 
13259  84 
by simp 
85 

86 

13357  87 
subsection{*Rules for Set Difference, Defined via @{term Upair}*} 
13259  88 

46953  89 
lemma Diff_iff [simp]: "c \<in> AB \<longleftrightarrow> (c \<in> A & c\<notin>B)" 
13259  90 
by (unfold Diff_def, blast) 
91 

46820  92 
lemma DiffI [intro!]: "[ c \<in> A; c \<notin> B ] ==> c \<in> A  B" 
13259  93 
by simp 
94 

46820  95 
lemma DiffD1: "c \<in> A  B ==> c \<in> A" 
13259  96 
by simp 
97 

46820  98 
lemma DiffD2: "c \<in> A  B ==> c \<notin> B" 
13259  99 
by simp 
100 

46953  101 
lemma DiffE [elim!]: "[ c \<in> A  B; [ c \<in> A; c\<notin>B ] ==> P ] ==> P" 
13259  102 
by simp 
103 

104 

13357  105 
subsection{*Rules for @{term cons}*} 
13259  106 

46953  107 
lemma cons_iff [simp]: "a \<in> cons(b,A) \<longleftrightarrow> (a=b  a \<in> A)" 
13259  108 
apply (unfold cons_def) 
109 
apply (blast intro: UpairI1 UpairI2 elim: UpairE) 

110 
done 

111 

112 
(*risky as a typechecking rule, but solves otherwise unconstrained goals of 

46820  113 
the form x \<in> ?A*) 
114 
lemma consI1 [simp,TC]: "a \<in> cons(a,B)" 

13259  115 
by simp 
116 

117 

46820  118 
lemma consI2: "a \<in> B ==> a \<in> cons(b,B)" 
13259  119 
by simp 
120 

46953  121 
lemma consE [elim!]: "[ a \<in> cons(b,A); a=b ==> P; a \<in> A ==> P ] ==> P" 
13780  122 
by (simp, blast) 
13259  123 

124 
(*Stronger version of the rule above*) 

125 
lemma consE': 

46953  126 
"[ a \<in> cons(b,A); a=b ==> P; [ a \<in> A; a\<noteq>b ] ==> P ] ==> P" 
13780  127 
by (simp, blast) 
13259  128 

129 
(*Classical introduction rule*) 

46953  130 
lemma consCI [intro!]: "(a\<notin>B ==> a=b) ==> a \<in> cons(b,B)" 
13780  131 
by (simp, blast) 
13259  132 

46820  133 
lemma cons_not_0 [simp]: "cons(a,B) \<noteq> 0" 
13259  134 
by (blast elim: equalityE) 
135 

45602  136 
lemmas cons_neq_0 = cons_not_0 [THEN notE] 
13259  137 

138 
declare cons_not_0 [THEN not_sym, simp] 

139 

140 

13357  141 
subsection{*Singletons*} 
13259  142 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

143 
lemma singleton_iff: "a \<in> {b} \<longleftrightarrow> a=b" 
13259  144 
by simp 
145 

46820  146 
lemma singletonI [intro!]: "a \<in> {a}" 
13259  147 
by (rule consI1) 
148 

45602  149 
lemmas singletonE = singleton_iff [THEN iffD1, elim_format, elim!] 
13259  150 

151 

14883  152 
subsection{*Descriptions*} 
13259  153 

154 
lemma the_equality [intro]: 

155 
"[ P(a); !!x. P(x) ==> x=a ] ==> (THE x. P(x)) = a" 

46820  156 
apply (unfold the_def) 
13259  157 
apply (fast dest: subst) 
158 
done 

159 

160 
(* Only use this if you already know EX!x. P(x) *) 

161 
lemma the_equality2: "[ EX! x. P(x); P(a) ] ==> (THE x. P(x)) = a" 

162 
by blast 

163 

164 
lemma theI: "EX! x. P(x) ==> P(THE x. P(x))" 

165 
apply (erule ex1E) 

166 
apply (subst the_equality) 

167 
apply (blast+) 

168 
done 

169 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

170 
(*No congruence rule is necessary: if @{term"\<forall>y.P(y)\<longleftrightarrow>Q(y)"} then 
46820  171 
@{term "THE x.P(x)"} rewrites to @{term "THE x.Q(x)"} *) 
13259  172 

173 
(*If it's "undefined", it's zero!*) 

174 
lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0" 

175 
apply (unfold the_def) 

176 
apply (blast elim!: ReplaceE) 

177 
done 

178 

179 
(*Easier to apply than theI: conclusion has only one occurrence of P*) 

180 
lemma theI2: 

181 
assumes p1: "~ Q(0) ==> EX! x. P(x)" 

182 
and p2: "!!x. P(x) ==> Q(x)" 

183 
shows "Q(THE x. P(x))" 

184 
apply (rule classical) 

185 
apply (rule p2) 

186 
apply (rule theI) 

187 
apply (rule classical) 

188 
apply (rule p1) 

189 
apply (erule the_0 [THEN subst], assumption) 

190 
done 

191 

13357  192 
lemma the_eq_trivial [simp]: "(THE x. x = a) = a" 
193 
by blast 

194 

13544  195 
lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a" 
196 
by blast 

197 

13780  198 

13357  199 
subsection{*Conditional Terms: @{text "ifthenelse"}*} 
13259  200 

201 
lemma if_true [simp]: "(if True then a else b) = a" 

202 
by (unfold if_def, blast) 

203 

204 
lemma if_false [simp]: "(if False then a else b) = b" 

205 
by (unfold if_def, blast) 

206 

207 
(*Never use with case splitting, or if P is known to be true or false*) 

208 
lemma if_cong: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

209 
"[ P\<longleftrightarrow>Q; Q ==> a=c; ~Q ==> b=d ] 
13259  210 
==> (if P then a else b) = (if Q then c else d)" 
211 
by (simp add: if_def cong add: conj_cong) 

212 

46953  213 
(*Prevents simplification of x and y \<in> faster and allows the execution 
13259  214 
of functional programs. NOW THE DEFAULT.*) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

215 
lemma if_weak_cong: "P\<longleftrightarrow>Q ==> (if P then x else y) = (if Q then x else y)" 
13259  216 
by simp 
217 

218 
(*Not needed for rewriting, since P would rewrite to True anyway*) 

219 
lemma if_P: "P ==> (if P then a else b) = a" 

220 
by (unfold if_def, blast) 

221 

222 
(*Not needed for rewriting, since P would rewrite to False anyway*) 

223 
lemma if_not_P: "~P ==> (if P then a else b) = b" 

224 
by (unfold if_def, blast) 

225 

13780  226 
lemma split_if [split]: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

227 
"P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))" 
14153  228 
by (case_tac Q, simp_all) 
13259  229 

45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45602
diff
changeset

230 
(** Rewrite rules for boolean casesplitting: faster than split_if [split] 
13259  231 
**) 
232 

45602  233 
lemmas split_if_eq1 = split_if [of "%x. x = b"] for b 
234 
lemmas split_if_eq2 = split_if [of "%x. a = x"] for x 

13259  235 

46820  236 
lemmas split_if_mem1 = split_if [of "%x. x \<in> b"] for b 
237 
lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for x 

13259  238 

239 
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 

240 

241 
(*Logically equivalent to split_if_mem2*) 

46953  242 
lemma if_iff: "a: (if P then x else y) \<longleftrightarrow> P & a \<in> x  ~P & a \<in> y" 
13780  243 
by simp 
13259  244 

245 
lemma if_type [TC]: 

46953  246 
"[ P ==> a \<in> A; ~P ==> b \<in> A ] ==> (if P then a else b): A" 
13780  247 
by simp 
248 

249 
(** Splitting IFs in the assumptions **) 

250 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

251 
lemma split_if_asm: "P(if Q then x else y) \<longleftrightarrow> (~((Q & ~P(x))  (~Q & ~P(y))))" 
13780  252 
by simp 
253 

254 
lemmas if_splits = split_if split_if_asm 

13259  255 

256 

13357  257 
subsection{*Consequences of Foundation*} 
13259  258 

259 
(*was called mem_anti_sym*) 

46953  260 
lemma mem_asym: "[ a \<in> b; ~P ==> b \<in> a ] ==> P" 
13259  261 
apply (rule classical) 
262 
apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE]) 

263 
apply (blast elim!: equalityE)+ 

264 
done 

265 

266 
(*was called mem_anti_refl*) 

46953  267 
lemma mem_irrefl: "a \<in> a ==> P" 
13259  268 
by (blast intro: mem_asym) 
269 

270 
(*mem_irrefl should NOT be added to default databases: 

271 
it would be tried on most goals, making proofs slower!*) 

272 

46820  273 
lemma mem_not_refl: "a \<notin> a" 
13259  274 
apply (rule notI) 
275 
apply (erule mem_irrefl) 

276 
done 

277 

278 
(*Good for proving inequalities by rewriting*) 

46953  279 
lemma mem_imp_not_eq: "a \<in> A ==> a \<noteq> A" 
13259  280 
by (blast elim!: mem_irrefl) 
281 

46820  282 
lemma eq_imp_not_mem: "a=A ==> a \<notin> A" 
13357  283 
by (blast intro: elim: mem_irrefl) 
284 

285 
subsection{*Rules for Successor*} 

13259  286 

46953  287 
lemma succ_iff: "i \<in> succ(j) \<longleftrightarrow> i=j  i \<in> j" 
13259  288 
by (unfold succ_def, blast) 
289 

46820  290 
lemma succI1 [simp]: "i \<in> succ(i)" 
13259  291 
by (simp add: succ_iff) 
292 

46820  293 
lemma succI2: "i \<in> j ==> i \<in> succ(j)" 
13259  294 
by (simp add: succ_iff) 
295 

46820  296 
lemma succE [elim!]: 
46953  297 
"[ i \<in> succ(j); i=j ==> P; i \<in> j ==> P ] ==> P" 
46820  298 
apply (simp add: succ_iff, blast) 
13259  299 
done 
300 

301 
(*Classical introduction rule*) 

46953  302 
lemma succCI [intro!]: "(i\<notin>j ==> i=j) ==> i \<in> succ(j)" 
13259  303 
by (simp add: succ_iff, blast) 
304 

46820  305 
lemma succ_not_0 [simp]: "succ(n) \<noteq> 0" 
13259  306 
by (blast elim!: equalityE) 
307 

45602  308 
lemmas succ_neq_0 = succ_not_0 [THEN notE, elim!] 
13259  309 

310 
declare succ_not_0 [THEN not_sym, simp] 

311 
declare sym [THEN succ_neq_0, elim!] 

312 

46820  313 
(* @{term"succ(c) \<subseteq> B ==> c \<in> B"} *) 
13259  314 
lemmas succ_subsetD = succI1 [THEN [2] subsetD] 
315 

46820  316 
(* @{term"succ(b) \<noteq> b"} *) 
45602  317 
lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym] 
13259  318 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

319 
lemma succ_inject_iff [simp]: "succ(m) = succ(n) \<longleftrightarrow> m=n" 
13259  320 
by (blast elim: mem_asym elim!: equalityE) 
321 

45602  322 
lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!] 
13259  323 

13780  324 

325 
subsection{*Miniscoping of the Bounded Universal Quantifier*} 

326 

327 
lemma ball_simps1: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

328 
"(\<forall>x\<in>A. P(x) & Q) \<longleftrightarrow> (\<forall>x\<in>A. P(x)) & (A=0  Q)" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

329 
"(\<forall>x\<in>A. P(x)  Q) \<longleftrightarrow> ((\<forall>x\<in>A. P(x))  Q)" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

330 
"(\<forall>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) \<longrightarrow> Q)" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

331 
"(~(\<forall>x\<in>A. P(x))) \<longleftrightarrow> (\<exists>x\<in>A. ~P(x))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

332 
"(\<forall>x\<in>0.P(x)) \<longleftrightarrow> True" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

333 
"(\<forall>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) & (\<forall>x\<in>i. P(x))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

334 
"(\<forall>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) & (\<forall>x\<in>B. P(x))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

335 
"(\<forall>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<forall>y\<in>A. P(f(y)))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

336 
"(\<forall>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P(x))" 
13780  337 
by blast+ 
338 

339 
lemma ball_simps2: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

340 
"(\<forall>x\<in>A. P & Q(x)) \<longleftrightarrow> (A=0  P) & (\<forall>x\<in>A. Q(x))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

341 
"(\<forall>x\<in>A. P  Q(x)) \<longleftrightarrow> (P  (\<forall>x\<in>A. Q(x)))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

342 
"(\<forall>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q(x)))" 
13780  343 
by blast+ 
344 

345 
lemma ball_simps3: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

346 
"(\<forall>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))" 
13780  347 
by blast+ 
348 

349 
lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3 

350 

351 
lemma ball_conj_distrib: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

352 
"(\<forall>x\<in>A. P(x) & Q(x)) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) & (\<forall>x\<in>A. Q(x)))" 
13780  353 
by blast 
354 

355 

356 
subsection{*Miniscoping of the Bounded Existential Quantifier*} 

357 

358 
lemma bex_simps1: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

359 
"(\<exists>x\<in>A. P(x) & Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) & Q)" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

360 
"(\<exists>x\<in>A. P(x)  Q) \<longleftrightarrow> (\<exists>x\<in>A. P(x))  (A\<noteq>0 & Q)" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

361 
"(\<exists>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) \<longrightarrow> (A\<noteq>0 & Q))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

362 
"(\<exists>x\<in>0.P(x)) \<longleftrightarrow> False" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

363 
"(\<exists>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i)  (\<exists>x\<in>i. P(x))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

364 
"(\<exists>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a)  (\<exists>x\<in>B. P(x))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

365 
"(\<exists>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<exists>y\<in>A. P(f(y)))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

366 
"(\<exists>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P(x))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

367 
"(~(\<exists>x\<in>A. P(x))) \<longleftrightarrow> (\<forall>x\<in>A. ~P(x))" 
13780  368 
by blast+ 
369 

370 
lemma bex_simps2: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

371 
"(\<exists>x\<in>A. P & Q(x)) \<longleftrightarrow> (P & (\<exists>x\<in>A. Q(x)))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

372 
"(\<exists>x\<in>A. P  Q(x)) \<longleftrightarrow> (A\<noteq>0 & P)  (\<exists>x\<in>A. Q(x))" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

373 
"(\<exists>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> ((A=0  P) \<longrightarrow> (\<exists>x\<in>A. Q(x)))" 
13780  374 
by blast+ 
375 

376 
lemma bex_simps3: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

377 
"(\<exists>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<exists>x\<in>A. Q(x) & P(x))" 
13780  378 
by blast 
379 

380 
lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3 

381 

382 
lemma bex_disj_distrib: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

383 
"(\<exists>x\<in>A. P(x)  Q(x)) \<longleftrightarrow> ((\<exists>x\<in>A. P(x))  (\<exists>x\<in>A. Q(x)))" 
13780  384 
by blast 
385 

386 

387 
(** Onepoint rule for bounded quantifiers: see HOL/Set.ML **) 

388 

46953  389 
lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) \<longleftrightarrow> (a \<in> A)" 
13780  390 
by blast 
391 

46953  392 
lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) \<longleftrightarrow> (a \<in> A)" 
13780  393 
by blast 
394 

46953  395 
lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) \<longleftrightarrow> (a \<in> A & P(a))" 
13780  396 
by blast 
397 

46953  398 
lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) \<longleftrightarrow> (a \<in> A & P(a))" 
13780  399 
by blast 
400 

46953  401 
lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) \<longleftrightarrow> (a \<in> A \<longrightarrow> P(a))" 
13780  402 
by blast 
403 

46953  404 
lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) \<longleftrightarrow> (a \<in> A \<longrightarrow> P(a))" 
13780  405 
by blast 
406 

407 

408 
subsection{*Miniscoping of the Replacement Operator*} 

409 

410 
text{*These cover both @{term Replace} and @{term Collect}*} 

411 
lemma Rep_simps [simp]: 

46953  412 
"{x. y \<in> 0, R(x,y)} = 0" 
413 
"{x \<in> 0. P(x)} = 0" 

414 
"{x \<in> A. Q} = (if Q then A else 0)" 

13780  415 
"RepFun(0,f) = 0" 
416 
"RepFun(succ(i),f) = cons(f(i), RepFun(i,f))" 

417 
"RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))" 

418 
by (simp_all, blast+) 

419 

420 

421 
subsection{*Miniscoping of Unions*} 

422 

423 
lemma UN_simps1: 

46820  424 
"(\<Union>x\<in>C. cons(a, B(x))) = (if C=0 then 0 else cons(a, \<Union>x\<in>C. B(x)))" 
425 
"(\<Union>x\<in>C. A(x) \<union> B') = (if C=0 then 0 else (\<Union>x\<in>C. A(x)) \<union> B')" 

426 
"(\<Union>x\<in>C. A' \<union> B(x)) = (if C=0 then 0 else A' \<union> (\<Union>x\<in>C. B(x)))" 

427 
"(\<Union>x\<in>C. A(x) \<inter> B') = ((\<Union>x\<in>C. A(x)) \<inter> B')" 

428 
"(\<Union>x\<in>C. A' \<inter> B(x)) = (A' \<inter> (\<Union>x\<in>C. B(x)))" 

429 
"(\<Union>x\<in>C. A(x)  B') = ((\<Union>x\<in>C. A(x))  B')" 

430 
"(\<Union>x\<in>C. A'  B(x)) = (if C=0 then 0 else A'  (\<Inter>x\<in>C. B(x)))" 

431 
apply (simp_all add: Inter_def) 

13780  432 
apply (blast intro!: equalityI )+ 
433 
done 

434 

435 
lemma UN_simps2: 

46820  436 
"(\<Union>x\<in>\<Union>(A). B(x)) = (\<Union>y\<in>A. \<Union>x\<in>y. B(x))" 
437 
"(\<Union>z\<in>(\<Union>x\<in>A. B(x)). C(z)) = (\<Union>x\<in>A. \<Union>z\<in>B(x). C(z))" 

438 
"(\<Union>x\<in>RepFun(A,f). B(x)) = (\<Union>a\<in>A. B(f(a)))" 

13780  439 
by blast+ 
440 

441 
lemmas UN_simps [simp] = UN_simps1 UN_simps2 

442 

443 
text{*Opposite of miniscoping: pull the operator out*} 

444 

445 
lemma UN_extend_simps1: 

46820  446 
"(\<Union>x\<in>C. A(x)) \<union> B = (if C=0 then B else (\<Union>x\<in>C. A(x) \<union> B))" 
447 
"((\<Union>x\<in>C. A(x)) \<inter> B) = (\<Union>x\<in>C. A(x) \<inter> B)" 

448 
"((\<Union>x\<in>C. A(x))  B) = (\<Union>x\<in>C. A(x)  B)" 

449 
apply simp_all 

13780  450 
apply blast+ 
451 
done 

452 

453 
lemma UN_extend_simps2: 

46820  454 
"cons(a, \<Union>x\<in>C. B(x)) = (if C=0 then {a} else (\<Union>x\<in>C. cons(a, B(x))))" 
455 
"A \<union> (\<Union>x\<in>C. B(x)) = (if C=0 then A else (\<Union>x\<in>C. A \<union> B(x)))" 

456 
"(A \<inter> (\<Union>x\<in>C. B(x))) = (\<Union>x\<in>C. A \<inter> B(x))" 

457 
"A  (\<Inter>x\<in>C. B(x)) = (if C=0 then A else (\<Union>x\<in>C. A  B(x)))" 

458 
"(\<Union>y\<in>A. \<Union>x\<in>y. B(x)) = (\<Union>x\<in>\<Union>(A). B(x))" 

459 
"(\<Union>a\<in>A. B(f(a))) = (\<Union>x\<in>RepFun(A,f). B(x))" 

460 
apply (simp_all add: Inter_def) 

13780  461 
apply (blast intro!: equalityI)+ 
462 
done 

463 

464 
lemma UN_UN_extend: 

46820  465 
"(\<Union>x\<in>A. \<Union>z\<in>B(x). C(z)) = (\<Union>z\<in>(\<Union>x\<in>A. B(x)). C(z))" 
13780  466 
by blast 
467 

468 
lemmas UN_extend_simps = UN_extend_simps1 UN_extend_simps2 UN_UN_extend 

469 

470 

471 
subsection{*Miniscoping of Intersections*} 

472 

473 
lemma INT_simps1: 

46820  474 
"(\<Inter>x\<in>C. A(x) \<inter> B) = (\<Inter>x\<in>C. A(x)) \<inter> B" 
475 
"(\<Inter>x\<in>C. A(x)  B) = (\<Inter>x\<in>C. A(x))  B" 

476 
"(\<Inter>x\<in>C. A(x) \<union> B) = (if C=0 then 0 else (\<Inter>x\<in>C. A(x)) \<union> B)" 

13780  477 
by (simp_all add: Inter_def, blast+) 
478 

479 
lemma INT_simps2: 

46820  480 
"(\<Inter>x\<in>C. A \<inter> B(x)) = A \<inter> (\<Inter>x\<in>C. B(x))" 
481 
"(\<Inter>x\<in>C. A  B(x)) = (if C=0 then 0 else A  (\<Union>x\<in>C. B(x)))" 

482 
"(\<Inter>x\<in>C. cons(a, B(x))) = (if C=0 then 0 else cons(a, \<Inter>x\<in>C. B(x)))" 

483 
"(\<Inter>x\<in>C. A \<union> B(x)) = (if C=0 then 0 else A \<union> (\<Inter>x\<in>C. B(x)))" 

484 
apply (simp_all add: Inter_def) 

13780  485 
apply (blast intro!: equalityI)+ 
486 
done 

487 

488 
lemmas INT_simps [simp] = INT_simps1 INT_simps2 

489 

490 
text{*Opposite of miniscoping: pull the operator out*} 

491 

492 

493 
lemma INT_extend_simps1: 

46820  494 
"(\<Inter>x\<in>C. A(x)) \<inter> B = (\<Inter>x\<in>C. A(x) \<inter> B)" 
495 
"(\<Inter>x\<in>C. A(x))  B = (\<Inter>x\<in>C. A(x)  B)" 

496 
"(\<Inter>x\<in>C. A(x)) \<union> B = (if C=0 then B else (\<Inter>x\<in>C. A(x) \<union> B))" 

13780  497 
apply (simp_all add: Inter_def, blast+) 
498 
done 

499 

500 
lemma INT_extend_simps2: 

46820  501 
"A \<inter> (\<Inter>x\<in>C. B(x)) = (\<Inter>x\<in>C. A \<inter> B(x))" 
502 
"A  (\<Union>x\<in>C. B(x)) = (if C=0 then A else (\<Inter>x\<in>C. A  B(x)))" 

503 
"cons(a, \<Inter>x\<in>C. B(x)) = (if C=0 then {a} else (\<Inter>x\<in>C. cons(a, B(x))))" 

504 
"A \<union> (\<Inter>x\<in>C. B(x)) = (if C=0 then A else (\<Inter>x\<in>C. A \<union> B(x)))" 

505 
apply (simp_all add: Inter_def) 

13780  506 
apply (blast intro!: equalityI)+ 
507 
done 

508 

509 
lemmas INT_extend_simps = INT_extend_simps1 INT_extend_simps2 

510 

511 

512 
subsection{*Other simprules*} 

513 

514 

515 
(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***) 

516 

517 
lemma misc_simps [simp]: 

46820  518 
"0 \<union> A = A" 
519 
"A \<union> 0 = A" 

520 
"0 \<inter> A = 0" 

521 
"A \<inter> 0 = 0" 

13780  522 
"0  A = 0" 
523 
"A  0 = A" 

46820  524 
"\<Union>(0) = 0" 
525 
"\<Union>(cons(b,A)) = b \<union> \<Union>(A)" 

526 
"\<Inter>({b}) = b" 

13780  527 
by blast+ 
528 

6153  529 
end 