src/ZF/upair.thy
author wenzelm
Thu Jul 23 14:25:05 2015 +0200 (2015-07-23)
changeset 60770 240563fbf41d
parent 58871 c399ae4b836f
child 61798 27f3c10b0b50
permissions -rw-r--r--
isabelle update_cartouches;
paulson@2469
     1
(*  Title:      ZF/upair.thy
paulson@2469
     2
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
paulson@2469
     3
    Copyright   1993  University of Cambridge
paulson@13259
     4
paulson@13259
     5
Observe the order of dependence:
paulson@13259
     6
    Upair is defined in terms of Replace
paulson@46820
     7
    \<union> is defined in terms of Upair and \<Union>(similarly for Int)
paulson@13259
     8
    cons is defined in terms of Upair and Un
paulson@13259
     9
    Ordered pairs and descriptions are defined using cons ("set notation")
paulson@2469
    10
*)
paulson@2469
    11
wenzelm@60770
    12
section\<open>Unordered Pairs\<close>
paulson@13357
    13
wenzelm@46950
    14
theory upair
wenzelm@46950
    15
imports ZF
wenzelm@46950
    16
keywords "print_tcset" :: diag
wenzelm@46950
    17
begin
paulson@6153
    18
wenzelm@48891
    19
ML_file "Tools/typechk.ML"
paulson@6153
    20
paulson@13780
    21
lemma atomize_ball [symmetric, rulify]:
paulson@46953
    22
     "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"
paulson@13780
    23
by (simp add: Ball_def atomize_all atomize_imp)
paulson@13259
    24
paulson@13259
    25
wenzelm@60770
    26
subsection\<open>Unordered Pairs: constant @{term Upair}\<close>
paulson@13259
    27
paulson@46821
    28
lemma Upair_iff [simp]: "c \<in> Upair(a,b) \<longleftrightarrow> (c=a | c=b)"
paulson@13259
    29
by (unfold Upair_def, blast)
paulson@13259
    30
paulson@46820
    31
lemma UpairI1: "a \<in> Upair(a,b)"
paulson@13259
    32
by simp
paulson@13259
    33
paulson@46820
    34
lemma UpairI2: "b \<in> Upair(a,b)"
paulson@13259
    35
by simp
paulson@13259
    36
paulson@46820
    37
lemma UpairE: "[| a \<in> Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
paulson@13780
    38
by (simp, blast)
paulson@13259
    39
wenzelm@60770
    40
subsection\<open>Rules for Binary Union, Defined via @{term Upair}\<close>
paulson@13259
    41
paulson@46953
    42
lemma Un_iff [simp]: "c \<in> A \<union> B \<longleftrightarrow> (c \<in> A | c \<in> B)"
paulson@13259
    43
apply (simp add: Un_def)
paulson@13259
    44
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
paulson@13259
    45
done
paulson@13259
    46
paulson@46820
    47
lemma UnI1: "c \<in> A ==> c \<in> A \<union> B"
paulson@13259
    48
by simp
paulson@13259
    49
paulson@46820
    50
lemma UnI2: "c \<in> B ==> c \<in> A \<union> B"
paulson@13259
    51
by simp
paulson@13259
    52
paulson@13356
    53
declare UnI1 [elim?]  UnI2 [elim?]
paulson@13356
    54
paulson@46953
    55
lemma UnE [elim!]: "[| c \<in> A \<union> B;  c \<in> A ==> P;  c \<in> B ==> P |] ==> P"
paulson@13780
    56
by (simp, blast)
paulson@13259
    57
paulson@13259
    58
(*Stronger version of the rule above*)
paulson@46953
    59
lemma UnE': "[| c \<in> A \<union> B;  c \<in> A ==> P;  [| c \<in> B;  c\<notin>A |] ==> P |] ==> P"
paulson@13780
    60
by (simp, blast)
paulson@13259
    61
paulson@13259
    62
(*Classical introduction rule: no commitment to A vs B*)
paulson@46820
    63
lemma UnCI [intro!]: "(c \<notin> B ==> c \<in> A) ==> c \<in> A \<union> B"
paulson@13780
    64
by (simp, blast)
paulson@13259
    65
wenzelm@60770
    66
subsection\<open>Rules for Binary Intersection, Defined via @{term Upair}\<close>
paulson@13259
    67
paulson@46953
    68
lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> (c \<in> A & c \<in> B)"
paulson@13259
    69
apply (unfold Int_def)
paulson@13259
    70
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
paulson@13259
    71
done
paulson@13259
    72
paulson@46820
    73
lemma IntI [intro!]: "[| c \<in> A;  c \<in> B |] ==> c \<in> A \<inter> B"
paulson@13259
    74
by simp
paulson@13259
    75
paulson@46820
    76
lemma IntD1: "c \<in> A \<inter> B ==> c \<in> A"
paulson@13259
    77
by simp
paulson@13259
    78
paulson@46820
    79
lemma IntD2: "c \<in> A \<inter> B ==> c \<in> B"
paulson@13259
    80
by simp
paulson@13259
    81
paulson@46953
    82
lemma IntE [elim!]: "[| c \<in> A \<inter> B;  [| c \<in> A; c \<in> B |] ==> P |] ==> P"
paulson@13259
    83
by simp
paulson@13259
    84
paulson@13259
    85
wenzelm@60770
    86
subsection\<open>Rules for Set Difference, Defined via @{term Upair}\<close>
paulson@13259
    87
paulson@46953
    88
lemma Diff_iff [simp]: "c \<in> A-B \<longleftrightarrow> (c \<in> A & c\<notin>B)"
paulson@13259
    89
by (unfold Diff_def, blast)
paulson@13259
    90
paulson@46820
    91
lemma DiffI [intro!]: "[| c \<in> A;  c \<notin> B |] ==> c \<in> A - B"
paulson@13259
    92
by simp
paulson@13259
    93
paulson@46820
    94
lemma DiffD1: "c \<in> A - B ==> c \<in> A"
paulson@13259
    95
by simp
paulson@13259
    96
paulson@46820
    97
lemma DiffD2: "c \<in> A - B ==> c \<notin> B"
paulson@13259
    98
by simp
paulson@13259
    99
paulson@46953
   100
lemma DiffE [elim!]: "[| c \<in> A - B;  [| c \<in> A; c\<notin>B |] ==> P |] ==> P"
paulson@13259
   101
by simp
paulson@13259
   102
paulson@13259
   103
wenzelm@60770
   104
subsection\<open>Rules for @{term cons}\<close>
paulson@13259
   105
paulson@46953
   106
lemma cons_iff [simp]: "a \<in> cons(b,A) \<longleftrightarrow> (a=b | a \<in> A)"
paulson@13259
   107
apply (unfold cons_def)
paulson@13259
   108
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
paulson@13259
   109
done
paulson@13259
   110
paulson@13259
   111
(*risky as a typechecking rule, but solves otherwise unconstrained goals of
paulson@46820
   112
the form x \<in> ?A*)
paulson@46820
   113
lemma consI1 [simp,TC]: "a \<in> cons(a,B)"
paulson@13259
   114
by simp
paulson@13259
   115
paulson@13259
   116
paulson@46820
   117
lemma consI2: "a \<in> B ==> a \<in> cons(b,B)"
paulson@13259
   118
by simp
paulson@13259
   119
paulson@46953
   120
lemma consE [elim!]: "[| a \<in> cons(b,A);  a=b ==> P;  a \<in> A ==> P |] ==> P"
paulson@13780
   121
by (simp, blast)
paulson@13259
   122
paulson@13259
   123
(*Stronger version of the rule above*)
paulson@13259
   124
lemma consE':
paulson@46953
   125
    "[| a \<in> cons(b,A);  a=b ==> P;  [| a \<in> A;  a\<noteq>b |] ==> P |] ==> P"
paulson@13780
   126
by (simp, blast)
paulson@13259
   127
paulson@13259
   128
(*Classical introduction rule*)
paulson@46953
   129
lemma consCI [intro!]: "(a\<notin>B ==> a=b) ==> a \<in> cons(b,B)"
paulson@13780
   130
by (simp, blast)
paulson@13259
   131
paulson@46820
   132
lemma cons_not_0 [simp]: "cons(a,B) \<noteq> 0"
paulson@13259
   133
by (blast elim: equalityE)
paulson@13259
   134
wenzelm@45602
   135
lemmas cons_neq_0 = cons_not_0 [THEN notE]
paulson@13259
   136
paulson@13259
   137
declare cons_not_0 [THEN not_sym, simp]
paulson@13259
   138
paulson@13259
   139
wenzelm@60770
   140
subsection\<open>Singletons\<close>
paulson@13259
   141
paulson@46821
   142
lemma singleton_iff: "a \<in> {b} \<longleftrightarrow> a=b"
paulson@13259
   143
by simp
paulson@13259
   144
paulson@46820
   145
lemma singletonI [intro!]: "a \<in> {a}"
paulson@13259
   146
by (rule consI1)
paulson@13259
   147
wenzelm@45602
   148
lemmas singletonE = singleton_iff [THEN iffD1, elim_format, elim!]
paulson@13259
   149
paulson@13259
   150
wenzelm@60770
   151
subsection\<open>Descriptions\<close>
paulson@13259
   152
paulson@13259
   153
lemma the_equality [intro]:
paulson@13259
   154
    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
paulson@46820
   155
apply (unfold the_def)
paulson@13259
   156
apply (fast dest: subst)
paulson@13259
   157
done
paulson@13259
   158
paulson@13259
   159
(* Only use this if you already know EX!x. P(x) *)
paulson@13259
   160
lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
paulson@13259
   161
by blast
paulson@13259
   162
paulson@13259
   163
lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
paulson@13259
   164
apply (erule ex1E)
paulson@13259
   165
apply (subst the_equality)
paulson@13259
   166
apply (blast+)
paulson@13259
   167
done
paulson@13259
   168
paulson@46821
   169
(*No congruence rule is necessary: if @{term"\<forall>y.P(y)\<longleftrightarrow>Q(y)"} then
paulson@46820
   170
  @{term "THE x.P(x)"}  rewrites to @{term "THE x.Q(x)"} *)
paulson@13259
   171
paulson@13259
   172
(*If it's "undefined", it's zero!*)
paulson@13259
   173
lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
paulson@13259
   174
apply (unfold the_def)
paulson@13259
   175
apply (blast elim!: ReplaceE)
paulson@13259
   176
done
paulson@13259
   177
paulson@13259
   178
(*Easier to apply than theI: conclusion has only one occurrence of P*)
paulson@13259
   179
lemma theI2:
paulson@13259
   180
    assumes p1: "~ Q(0) ==> EX! x. P(x)"
paulson@13259
   181
        and p2: "!!x. P(x) ==> Q(x)"
paulson@13259
   182
    shows "Q(THE x. P(x))"
paulson@13259
   183
apply (rule classical)
paulson@13259
   184
apply (rule p2)
paulson@13259
   185
apply (rule theI)
paulson@13259
   186
apply (rule classical)
paulson@13259
   187
apply (rule p1)
paulson@13259
   188
apply (erule the_0 [THEN subst], assumption)
paulson@13259
   189
done
paulson@13259
   190
paulson@13357
   191
lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
paulson@13357
   192
by blast
paulson@13357
   193
paulson@13544
   194
lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a"
paulson@13544
   195
by blast
paulson@13544
   196
paulson@13780
   197
wenzelm@60770
   198
subsection\<open>Conditional Terms: @{text "if-then-else"}\<close>
paulson@13259
   199
paulson@13259
   200
lemma if_true [simp]: "(if True then a else b) = a"
paulson@13259
   201
by (unfold if_def, blast)
paulson@13259
   202
paulson@13259
   203
lemma if_false [simp]: "(if False then a else b) = b"
paulson@13259
   204
by (unfold if_def, blast)
paulson@13259
   205
paulson@13259
   206
(*Never use with case splitting, or if P is known to be true or false*)
paulson@13259
   207
lemma if_cong:
paulson@46821
   208
    "[| P\<longleftrightarrow>Q;  Q ==> a=c;  ~Q ==> b=d |]
paulson@13259
   209
     ==> (if P then a else b) = (if Q then c else d)"
paulson@13259
   210
by (simp add: if_def cong add: conj_cong)
paulson@13259
   211
paulson@46953
   212
(*Prevents simplification of x and y \<in> faster and allows the execution
paulson@13259
   213
  of functional programs. NOW THE DEFAULT.*)
paulson@46821
   214
lemma if_weak_cong: "P\<longleftrightarrow>Q ==> (if P then x else y) = (if Q then x else y)"
paulson@13259
   215
by simp
paulson@13259
   216
paulson@13259
   217
(*Not needed for rewriting, since P would rewrite to True anyway*)
paulson@13259
   218
lemma if_P: "P ==> (if P then a else b) = a"
paulson@13259
   219
by (unfold if_def, blast)
paulson@13259
   220
paulson@13259
   221
(*Not needed for rewriting, since P would rewrite to False anyway*)
paulson@13259
   222
lemma if_not_P: "~P ==> (if P then a else b) = b"
paulson@13259
   223
by (unfold if_def, blast)
paulson@13259
   224
paulson@13780
   225
lemma split_if [split]:
paulson@46821
   226
     "P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))"
paulson@14153
   227
by (case_tac Q, simp_all)
paulson@13259
   228
wenzelm@45620
   229
(** Rewrite rules for boolean case-splitting: faster than split_if [split]
paulson@13259
   230
**)
paulson@13259
   231
wenzelm@45602
   232
lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
wenzelm@45602
   233
lemmas split_if_eq2 = split_if [of "%x. a = x"] for x
paulson@13259
   234
paulson@46820
   235
lemmas split_if_mem1 = split_if [of "%x. x \<in> b"] for b
paulson@46820
   236
lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for x
paulson@13259
   237
paulson@13259
   238
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
paulson@13259
   239
paulson@13259
   240
(*Logically equivalent to split_if_mem2*)
paulson@46953
   241
lemma if_iff: "a: (if P then x else y) \<longleftrightarrow> P & a \<in> x | ~P & a \<in> y"
paulson@13780
   242
by simp
paulson@13259
   243
paulson@13259
   244
lemma if_type [TC]:
paulson@46953
   245
    "[| P ==> a \<in> A;  ~P ==> b \<in> A |] ==> (if P then a else b): A"
paulson@13780
   246
by simp
paulson@13780
   247
paulson@13780
   248
(** Splitting IFs in the assumptions **)
paulson@13780
   249
paulson@46821
   250
lemma split_if_asm: "P(if Q then x else y) \<longleftrightarrow> (~((Q & ~P(x)) | (~Q & ~P(y))))"
paulson@13780
   251
by simp
paulson@13780
   252
paulson@13780
   253
lemmas if_splits = split_if split_if_asm
paulson@13259
   254
paulson@13259
   255
wenzelm@60770
   256
subsection\<open>Consequences of Foundation\<close>
paulson@13259
   257
paulson@13259
   258
(*was called mem_anti_sym*)
paulson@46953
   259
lemma mem_asym: "[| a \<in> b;  ~P ==> b \<in> a |] ==> P"
paulson@13259
   260
apply (rule classical)
paulson@13259
   261
apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE])
paulson@13259
   262
apply (blast elim!: equalityE)+
paulson@13259
   263
done
paulson@13259
   264
paulson@13259
   265
(*was called mem_anti_refl*)
paulson@46953
   266
lemma mem_irrefl: "a \<in> a ==> P"
paulson@13259
   267
by (blast intro: mem_asym)
paulson@13259
   268
paulson@13259
   269
(*mem_irrefl should NOT be added to default databases:
paulson@13259
   270
      it would be tried on most goals, making proofs slower!*)
paulson@13259
   271
paulson@46820
   272
lemma mem_not_refl: "a \<notin> a"
paulson@13259
   273
apply (rule notI)
paulson@13259
   274
apply (erule mem_irrefl)
paulson@13259
   275
done
paulson@13259
   276
paulson@13259
   277
(*Good for proving inequalities by rewriting*)
paulson@46953
   278
lemma mem_imp_not_eq: "a \<in> A ==> a \<noteq> A"
paulson@13259
   279
by (blast elim!: mem_irrefl)
paulson@13259
   280
paulson@46820
   281
lemma eq_imp_not_mem: "a=A ==> a \<notin> A"
paulson@13357
   282
by (blast intro: elim: mem_irrefl)
paulson@13357
   283
wenzelm@60770
   284
subsection\<open>Rules for Successor\<close>
paulson@13259
   285
paulson@46953
   286
lemma succ_iff: "i \<in> succ(j) \<longleftrightarrow> i=j | i \<in> j"
paulson@13259
   287
by (unfold succ_def, blast)
paulson@13259
   288
paulson@46820
   289
lemma succI1 [simp]: "i \<in> succ(i)"
paulson@13259
   290
by (simp add: succ_iff)
paulson@13259
   291
paulson@46820
   292
lemma succI2: "i \<in> j ==> i \<in> succ(j)"
paulson@13259
   293
by (simp add: succ_iff)
paulson@13259
   294
paulson@46820
   295
lemma succE [elim!]:
paulson@46953
   296
    "[| i \<in> succ(j);  i=j ==> P;  i \<in> j ==> P |] ==> P"
paulson@46820
   297
apply (simp add: succ_iff, blast)
paulson@13259
   298
done
paulson@13259
   299
paulson@13259
   300
(*Classical introduction rule*)
paulson@46953
   301
lemma succCI [intro!]: "(i\<notin>j ==> i=j) ==> i \<in> succ(j)"
paulson@13259
   302
by (simp add: succ_iff, blast)
paulson@13259
   303
paulson@46820
   304
lemma succ_not_0 [simp]: "succ(n) \<noteq> 0"
paulson@13259
   305
by (blast elim!: equalityE)
paulson@13259
   306
wenzelm@45602
   307
lemmas succ_neq_0 = succ_not_0 [THEN notE, elim!]
paulson@13259
   308
paulson@13259
   309
declare succ_not_0 [THEN not_sym, simp]
paulson@13259
   310
declare sym [THEN succ_neq_0, elim!]
paulson@13259
   311
paulson@46820
   312
(* @{term"succ(c) \<subseteq> B ==> c \<in> B"} *)
paulson@13259
   313
lemmas succ_subsetD = succI1 [THEN [2] subsetD]
paulson@13259
   314
paulson@46820
   315
(* @{term"succ(b) \<noteq> b"} *)
wenzelm@45602
   316
lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym]
paulson@13259
   317
paulson@46821
   318
lemma succ_inject_iff [simp]: "succ(m) = succ(n) \<longleftrightarrow> m=n"
paulson@13259
   319
by (blast elim: mem_asym elim!: equalityE)
paulson@13259
   320
wenzelm@45602
   321
lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!]
paulson@13259
   322
paulson@13780
   323
wenzelm@60770
   324
subsection\<open>Miniscoping of the Bounded Universal Quantifier\<close>
paulson@13780
   325
paulson@13780
   326
lemma ball_simps1:
paulson@46821
   327
     "(\<forall>x\<in>A. P(x) & Q)   \<longleftrightarrow> (\<forall>x\<in>A. P(x)) & (A=0 | Q)"
paulson@46821
   328
     "(\<forall>x\<in>A. P(x) | Q)   \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) | Q)"
paulson@46821
   329
     "(\<forall>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) \<longrightarrow> Q)"
paulson@46821
   330
     "(~(\<forall>x\<in>A. P(x))) \<longleftrightarrow> (\<exists>x\<in>A. ~P(x))"
paulson@46821
   331
     "(\<forall>x\<in>0.P(x)) \<longleftrightarrow> True"
paulson@46821
   332
     "(\<forall>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) & (\<forall>x\<in>i. P(x))"
paulson@46821
   333
     "(\<forall>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) & (\<forall>x\<in>B. P(x))"
paulson@46821
   334
     "(\<forall>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<forall>y\<in>A. P(f(y)))"
paulson@46821
   335
     "(\<forall>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P(x))"
paulson@13780
   336
by blast+
paulson@13780
   337
paulson@13780
   338
lemma ball_simps2:
paulson@46821
   339
     "(\<forall>x\<in>A. P & Q(x))   \<longleftrightarrow> (A=0 | P) & (\<forall>x\<in>A. Q(x))"
paulson@46821
   340
     "(\<forall>x\<in>A. P | Q(x))   \<longleftrightarrow> (P | (\<forall>x\<in>A. Q(x)))"
paulson@46821
   341
     "(\<forall>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q(x)))"
paulson@13780
   342
by blast+
paulson@13780
   343
paulson@13780
   344
lemma ball_simps3:
paulson@46821
   345
     "(\<forall>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))"
paulson@13780
   346
by blast+
paulson@13780
   347
paulson@13780
   348
lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3
paulson@13780
   349
paulson@13780
   350
lemma ball_conj_distrib:
paulson@46821
   351
    "(\<forall>x\<in>A. P(x) & Q(x)) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) & (\<forall>x\<in>A. Q(x)))"
paulson@13780
   352
by blast
paulson@13780
   353
paulson@13780
   354
wenzelm@60770
   355
subsection\<open>Miniscoping of the Bounded Existential Quantifier\<close>
paulson@13780
   356
paulson@13780
   357
lemma bex_simps1:
paulson@46821
   358
     "(\<exists>x\<in>A. P(x) & Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) & Q)"
paulson@46821
   359
     "(\<exists>x\<in>A. P(x) | Q) \<longleftrightarrow> (\<exists>x\<in>A. P(x)) | (A\<noteq>0 & Q)"
paulson@46821
   360
     "(\<exists>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) \<longrightarrow> (A\<noteq>0 & Q))"
paulson@46821
   361
     "(\<exists>x\<in>0.P(x)) \<longleftrightarrow> False"
paulson@46821
   362
     "(\<exists>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) | (\<exists>x\<in>i. P(x))"
paulson@46821
   363
     "(\<exists>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) | (\<exists>x\<in>B. P(x))"
paulson@46821
   364
     "(\<exists>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<exists>y\<in>A. P(f(y)))"
paulson@46821
   365
     "(\<exists>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y.  P(x))"
paulson@46821
   366
     "(~(\<exists>x\<in>A. P(x))) \<longleftrightarrow> (\<forall>x\<in>A. ~P(x))"
paulson@13780
   367
by blast+
paulson@13780
   368
paulson@13780
   369
lemma bex_simps2:
paulson@46821
   370
     "(\<exists>x\<in>A. P & Q(x)) \<longleftrightarrow> (P & (\<exists>x\<in>A. Q(x)))"
paulson@46821
   371
     "(\<exists>x\<in>A. P | Q(x)) \<longleftrightarrow> (A\<noteq>0 & P) | (\<exists>x\<in>A. Q(x))"
paulson@46821
   372
     "(\<exists>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> ((A=0 | P) \<longrightarrow> (\<exists>x\<in>A. Q(x)))"
paulson@13780
   373
by blast+
paulson@13780
   374
paulson@13780
   375
lemma bex_simps3:
paulson@46821
   376
     "(\<exists>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<exists>x\<in>A. Q(x) & P(x))"
paulson@13780
   377
by blast
paulson@13780
   378
paulson@13780
   379
lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3
paulson@13780
   380
paulson@13780
   381
lemma bex_disj_distrib:
paulson@46821
   382
    "(\<exists>x\<in>A. P(x) | Q(x)) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) | (\<exists>x\<in>A. Q(x)))"
paulson@13780
   383
by blast
paulson@13780
   384
paulson@13780
   385
paulson@13780
   386
(** One-point rule for bounded quantifiers: see HOL/Set.ML **)
paulson@13780
   387
paulson@46953
   388
lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) \<longleftrightarrow> (a \<in> A)"
paulson@13780
   389
by blast
paulson@13780
   390
paulson@46953
   391
lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) \<longleftrightarrow> (a \<in> A)"
paulson@13780
   392
by blast
paulson@13780
   393
paulson@46953
   394
lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) \<longleftrightarrow> (a \<in> A & P(a))"
paulson@13780
   395
by blast
paulson@13780
   396
paulson@46953
   397
lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) \<longleftrightarrow> (a \<in> A & P(a))"
paulson@13780
   398
by blast
paulson@13780
   399
paulson@46953
   400
lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) \<longleftrightarrow> (a \<in> A \<longrightarrow> P(a))"
paulson@13780
   401
by blast
paulson@13780
   402
paulson@46953
   403
lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) \<longleftrightarrow> (a \<in> A \<longrightarrow> P(a))"
paulson@13780
   404
by blast
paulson@13780
   405
paulson@13780
   406
wenzelm@60770
   407
subsection\<open>Miniscoping of the Replacement Operator\<close>
paulson@13780
   408
wenzelm@60770
   409
text\<open>These cover both @{term Replace} and @{term Collect}\<close>
paulson@13780
   410
lemma Rep_simps [simp]:
paulson@46953
   411
     "{x. y \<in> 0, R(x,y)} = 0"
paulson@46953
   412
     "{x \<in> 0. P(x)} = 0"
paulson@46953
   413
     "{x \<in> A. Q} = (if Q then A else 0)"
paulson@13780
   414
     "RepFun(0,f) = 0"
paulson@13780
   415
     "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))"
paulson@13780
   416
     "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"
paulson@13780
   417
by (simp_all, blast+)
paulson@13780
   418
paulson@13780
   419
wenzelm@60770
   420
subsection\<open>Miniscoping of Unions\<close>
paulson@13780
   421
paulson@13780
   422
lemma UN_simps1:
paulson@46820
   423
     "(\<Union>x\<in>C. cons(a, B(x))) = (if C=0 then 0 else cons(a, \<Union>x\<in>C. B(x)))"
paulson@46820
   424
     "(\<Union>x\<in>C. A(x) \<union> B')   = (if C=0 then 0 else (\<Union>x\<in>C. A(x)) \<union> B')"
paulson@46820
   425
     "(\<Union>x\<in>C. A' \<union> B(x))   = (if C=0 then 0 else A' \<union> (\<Union>x\<in>C. B(x)))"
paulson@46820
   426
     "(\<Union>x\<in>C. A(x) \<inter> B')  = ((\<Union>x\<in>C. A(x)) \<inter> B')"
paulson@46820
   427
     "(\<Union>x\<in>C. A' \<inter> B(x))  = (A' \<inter> (\<Union>x\<in>C. B(x)))"
paulson@46820
   428
     "(\<Union>x\<in>C. A(x) - B')    = ((\<Union>x\<in>C. A(x)) - B')"
paulson@46820
   429
     "(\<Union>x\<in>C. A' - B(x))    = (if C=0 then 0 else A' - (\<Inter>x\<in>C. B(x)))"
paulson@46820
   430
apply (simp_all add: Inter_def)
paulson@13780
   431
apply (blast intro!: equalityI )+
paulson@13780
   432
done
paulson@13780
   433
paulson@13780
   434
lemma UN_simps2:
paulson@46820
   435
      "(\<Union>x\<in>\<Union>(A). B(x)) = (\<Union>y\<in>A. \<Union>x\<in>y. B(x))"
paulson@46820
   436
      "(\<Union>z\<in>(\<Union>x\<in>A. B(x)). C(z)) = (\<Union>x\<in>A. \<Union>z\<in>B(x). C(z))"
paulson@46820
   437
      "(\<Union>x\<in>RepFun(A,f). B(x))     = (\<Union>a\<in>A. B(f(a)))"
paulson@13780
   438
by blast+
paulson@13780
   439
paulson@13780
   440
lemmas UN_simps [simp] = UN_simps1 UN_simps2
paulson@13780
   441
wenzelm@60770
   442
text\<open>Opposite of miniscoping: pull the operator out\<close>
paulson@13780
   443
paulson@13780
   444
lemma UN_extend_simps1:
paulson@46820
   445
     "(\<Union>x\<in>C. A(x)) \<union> B   = (if C=0 then B else (\<Union>x\<in>C. A(x) \<union> B))"
paulson@46820
   446
     "((\<Union>x\<in>C. A(x)) \<inter> B) = (\<Union>x\<in>C. A(x) \<inter> B)"
paulson@46820
   447
     "((\<Union>x\<in>C. A(x)) - B) = (\<Union>x\<in>C. A(x) - B)"
paulson@46820
   448
apply simp_all
paulson@13780
   449
apply blast+
paulson@13780
   450
done
paulson@13780
   451
paulson@13780
   452
lemma UN_extend_simps2:
paulson@46820
   453
     "cons(a, \<Union>x\<in>C. B(x)) = (if C=0 then {a} else (\<Union>x\<in>C. cons(a, B(x))))"
paulson@46820
   454
     "A \<union> (\<Union>x\<in>C. B(x))   = (if C=0 then A else (\<Union>x\<in>C. A \<union> B(x)))"
paulson@46820
   455
     "(A \<inter> (\<Union>x\<in>C. B(x))) = (\<Union>x\<in>C. A \<inter> B(x))"
paulson@46820
   456
     "A - (\<Inter>x\<in>C. B(x))    = (if C=0 then A else (\<Union>x\<in>C. A - B(x)))"
paulson@46820
   457
     "(\<Union>y\<in>A. \<Union>x\<in>y. B(x)) = (\<Union>x\<in>\<Union>(A). B(x))"
paulson@46820
   458
     "(\<Union>a\<in>A. B(f(a))) = (\<Union>x\<in>RepFun(A,f). B(x))"
paulson@46820
   459
apply (simp_all add: Inter_def)
paulson@13780
   460
apply (blast intro!: equalityI)+
paulson@13780
   461
done
paulson@13780
   462
paulson@13780
   463
lemma UN_UN_extend:
paulson@46820
   464
     "(\<Union>x\<in>A. \<Union>z\<in>B(x). C(z)) = (\<Union>z\<in>(\<Union>x\<in>A. B(x)). C(z))"
paulson@13780
   465
by blast
paulson@13780
   466
paulson@13780
   467
lemmas UN_extend_simps = UN_extend_simps1 UN_extend_simps2 UN_UN_extend
paulson@13780
   468
paulson@13780
   469
wenzelm@60770
   470
subsection\<open>Miniscoping of Intersections\<close>
paulson@13780
   471
paulson@13780
   472
lemma INT_simps1:
paulson@46820
   473
     "(\<Inter>x\<in>C. A(x) \<inter> B) = (\<Inter>x\<in>C. A(x)) \<inter> B"
paulson@46820
   474
     "(\<Inter>x\<in>C. A(x) - B)   = (\<Inter>x\<in>C. A(x)) - B"
paulson@46820
   475
     "(\<Inter>x\<in>C. A(x) \<union> B)  = (if C=0 then 0 else (\<Inter>x\<in>C. A(x)) \<union> B)"
paulson@13780
   476
by (simp_all add: Inter_def, blast+)
paulson@13780
   477
paulson@13780
   478
lemma INT_simps2:
paulson@46820
   479
     "(\<Inter>x\<in>C. A \<inter> B(x)) = A \<inter> (\<Inter>x\<in>C. B(x))"
paulson@46820
   480
     "(\<Inter>x\<in>C. A - B(x))   = (if C=0 then 0 else A - (\<Union>x\<in>C. B(x)))"
paulson@46820
   481
     "(\<Inter>x\<in>C. cons(a, B(x))) = (if C=0 then 0 else cons(a, \<Inter>x\<in>C. B(x)))"
paulson@46820
   482
     "(\<Inter>x\<in>C. A \<union> B(x))  = (if C=0 then 0 else A \<union> (\<Inter>x\<in>C. B(x)))"
paulson@46820
   483
apply (simp_all add: Inter_def)
paulson@13780
   484
apply (blast intro!: equalityI)+
paulson@13780
   485
done
paulson@13780
   486
paulson@13780
   487
lemmas INT_simps [simp] = INT_simps1 INT_simps2
paulson@13780
   488
wenzelm@60770
   489
text\<open>Opposite of miniscoping: pull the operator out\<close>
paulson@13780
   490
paulson@13780
   491
paulson@13780
   492
lemma INT_extend_simps1:
paulson@46820
   493
     "(\<Inter>x\<in>C. A(x)) \<inter> B = (\<Inter>x\<in>C. A(x) \<inter> B)"
paulson@46820
   494
     "(\<Inter>x\<in>C. A(x)) - B = (\<Inter>x\<in>C. A(x) - B)"
paulson@46820
   495
     "(\<Inter>x\<in>C. A(x)) \<union> B  = (if C=0 then B else (\<Inter>x\<in>C. A(x) \<union> B))"
paulson@13780
   496
apply (simp_all add: Inter_def, blast+)
paulson@13780
   497
done
paulson@13780
   498
paulson@13780
   499
lemma INT_extend_simps2:
paulson@46820
   500
     "A \<inter> (\<Inter>x\<in>C. B(x)) = (\<Inter>x\<in>C. A \<inter> B(x))"
paulson@46820
   501
     "A - (\<Union>x\<in>C. B(x))   = (if C=0 then A else (\<Inter>x\<in>C. A - B(x)))"
paulson@46820
   502
     "cons(a, \<Inter>x\<in>C. B(x)) = (if C=0 then {a} else (\<Inter>x\<in>C. cons(a, B(x))))"
paulson@46820
   503
     "A \<union> (\<Inter>x\<in>C. B(x))  = (if C=0 then A else (\<Inter>x\<in>C. A \<union> B(x)))"
paulson@46820
   504
apply (simp_all add: Inter_def)
paulson@13780
   505
apply (blast intro!: equalityI)+
paulson@13780
   506
done
paulson@13780
   507
paulson@13780
   508
lemmas INT_extend_simps = INT_extend_simps1 INT_extend_simps2
paulson@13780
   509
paulson@13780
   510
wenzelm@60770
   511
subsection\<open>Other simprules\<close>
paulson@13780
   512
paulson@13780
   513
paulson@13780
   514
(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***)
paulson@13780
   515
paulson@13780
   516
lemma misc_simps [simp]:
paulson@46820
   517
     "0 \<union> A = A"
paulson@46820
   518
     "A \<union> 0 = A"
paulson@46820
   519
     "0 \<inter> A = 0"
paulson@46820
   520
     "A \<inter> 0 = 0"
paulson@13780
   521
     "0 - A = 0"
paulson@13780
   522
     "A - 0 = A"
paulson@46820
   523
     "\<Union>(0) = 0"
paulson@46820
   524
     "\<Union>(cons(b,A)) = b \<union> \<Union>(A)"
paulson@46820
   525
     "\<Inter>({b}) = b"
paulson@13780
   526
by blast+
paulson@13780
   527
paulson@6153
   528
end