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