src/ZF/upair.thy
author paulson
Sun Jul 14 19:59:55 2002 +0200 (2002-07-14)
changeset 13357 6f54e992777e
parent 13356 c9cfe1638bf2
child 13544 895994073bdf
permissions -rw-r--r--
Removal of mono.thy
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
wenzelm@11770
    19
declare atomize_ball [symmetric, rulify]
paulson@6153
    20
paulson@13356
    21
(*belongs to theory ZF*)
paulson@13356
    22
declare bspec [dest?]
paulson@13356
    23
paulson@13259
    24
lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *)
paulson@13259
    25
lemmas Pow_top = subset_refl [THEN PowI] (* A : Pow(A) *)
paulson@13259
    26
paulson@13259
    27
paulson@13357
    28
subsection{*Unordered Pairs: constant @{term Upair}*}
paulson@13259
    29
paulson@13259
    30
lemma Upair_iff [simp]: "c : Upair(a,b) <-> (c=a | c=b)"
paulson@13259
    31
by (unfold Upair_def, blast)
paulson@13259
    32
paulson@13259
    33
lemma UpairI1: "a : Upair(a,b)"
paulson@13259
    34
by simp
paulson@13259
    35
paulson@13259
    36
lemma UpairI2: "b : Upair(a,b)"
paulson@13259
    37
by simp
paulson@13259
    38
paulson@13259
    39
lemma UpairE:
paulson@13259
    40
    "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
paulson@13259
    41
apply simp
paulson@13259
    42
apply blast 
paulson@13259
    43
done
paulson@13259
    44
paulson@13357
    45
subsection{*Rules for Binary Union, Defined via @{term Upair}*}
paulson@13259
    46
paulson@13259
    47
lemma Un_iff [simp]: "c : A Un B <-> (c:A | c:B)"
paulson@13259
    48
apply (simp add: Un_def)
paulson@13259
    49
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
paulson@13259
    50
done
paulson@13259
    51
paulson@13259
    52
lemma UnI1: "c : A ==> c : A Un B"
paulson@13259
    53
by simp
paulson@13259
    54
paulson@13259
    55
lemma UnI2: "c : B ==> c : A Un B"
paulson@13259
    56
by simp
paulson@13259
    57
paulson@13356
    58
declare UnI1 [elim?]  UnI2 [elim?]
paulson@13356
    59
paulson@13259
    60
lemma UnE [elim!]: "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
paulson@13259
    61
apply simp 
paulson@13259
    62
apply blast 
paulson@13259
    63
done
paulson@13259
    64
paulson@13259
    65
(*Stronger version of the rule above*)
paulson@13259
    66
lemma UnE': "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
paulson@13259
    67
apply simp 
paulson@13259
    68
apply blast 
paulson@13259
    69
done
paulson@13259
    70
paulson@13259
    71
(*Classical introduction rule: no commitment to A vs B*)
paulson@13259
    72
lemma UnCI [intro!]: "(c ~: B ==> c : A) ==> c : A Un B"
paulson@13259
    73
apply simp
paulson@13259
    74
apply blast
paulson@13259
    75
done
paulson@13259
    76
paulson@13259
    77
paulson@13357
    78
subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}
paulson@13259
    79
paulson@13259
    80
lemma Int_iff [simp]: "c : A Int B <-> (c:A & c:B)"
paulson@13259
    81
apply (unfold Int_def)
paulson@13259
    82
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
paulson@13259
    83
done
paulson@13259
    84
paulson@13259
    85
lemma IntI [intro!]: "[| c : A;  c : B |] ==> c : A Int B"
paulson@13259
    86
by simp
paulson@13259
    87
paulson@13259
    88
lemma IntD1: "c : A Int B ==> c : A"
paulson@13259
    89
by simp
paulson@13259
    90
paulson@13259
    91
lemma IntD2: "c : A Int B ==> c : B"
paulson@13259
    92
by simp
paulson@13259
    93
paulson@13259
    94
lemma IntE [elim!]: "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
paulson@13259
    95
by simp
paulson@13259
    96
paulson@13259
    97
paulson@13357
    98
subsection{*Rules for Set Difference, Defined via @{term Upair}*}
paulson@13259
    99
paulson@13259
   100
lemma Diff_iff [simp]: "c : A-B <-> (c:A & c~:B)"
paulson@13259
   101
by (unfold Diff_def, blast)
paulson@13259
   102
paulson@13259
   103
lemma DiffI [intro!]: "[| c : A;  c ~: B |] ==> c : A - B"
paulson@13259
   104
by simp
paulson@13259
   105
paulson@13259
   106
lemma DiffD1: "c : A - B ==> c : A"
paulson@13259
   107
by simp
paulson@13259
   108
paulson@13259
   109
lemma DiffD2: "c : A - B ==> c ~: B"
paulson@13259
   110
by simp
paulson@13259
   111
paulson@13259
   112
lemma DiffE [elim!]: "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
paulson@13259
   113
by simp
paulson@13259
   114
paulson@13259
   115
paulson@13357
   116
subsection{*Rules for @{term cons}*}
paulson@13259
   117
paulson@13259
   118
lemma cons_iff [simp]: "a : cons(b,A) <-> (a=b | a:A)"
paulson@13259
   119
apply (unfold cons_def)
paulson@13259
   120
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
paulson@13259
   121
done
paulson@13259
   122
paulson@13259
   123
(*risky as a typechecking rule, but solves otherwise unconstrained goals of
paulson@13259
   124
the form x : ?A*)
paulson@13259
   125
lemma consI1 [simp,TC]: "a : cons(a,B)"
paulson@13259
   126
by simp
paulson@13259
   127
paulson@13259
   128
paulson@13259
   129
lemma consI2: "a : B ==> a : cons(b,B)"
paulson@13259
   130
by simp
paulson@13259
   131
paulson@13259
   132
lemma consE [elim!]:
paulson@13259
   133
    "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"
paulson@13259
   134
apply simp 
paulson@13259
   135
apply blast 
paulson@13259
   136
done
paulson@13259
   137
paulson@13259
   138
(*Stronger version of the rule above*)
paulson@13259
   139
lemma consE':
paulson@13259
   140
    "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
paulson@13259
   141
apply simp 
paulson@13259
   142
apply blast 
paulson@13259
   143
done
paulson@13259
   144
paulson@13259
   145
(*Classical introduction rule*)
paulson@13259
   146
lemma consCI [intro!]: "(a~:B ==> a=b) ==> a: cons(b,B)"
paulson@13259
   147
apply simp
paulson@13259
   148
apply blast
paulson@13259
   149
done
paulson@13259
   150
paulson@13259
   151
lemma cons_not_0 [simp]: "cons(a,B) ~= 0"
paulson@13259
   152
by (blast elim: equalityE)
paulson@13259
   153
paulson@13259
   154
lemmas cons_neq_0 = cons_not_0 [THEN notE, standard]
paulson@13259
   155
paulson@13259
   156
declare cons_not_0 [THEN not_sym, simp]
paulson@13259
   157
paulson@13259
   158
paulson@13357
   159
subsection{*Singletons*}
paulson@13259
   160
paulson@13259
   161
lemma singleton_iff: "a : {b} <-> a=b"
paulson@13259
   162
by simp
paulson@13259
   163
paulson@13259
   164
lemma singletonI [intro!]: "a : {a}"
paulson@13259
   165
by (rule consI1)
paulson@13259
   166
paulson@13259
   167
lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!]
paulson@13259
   168
paulson@13259
   169
paulson@13357
   170
subsection{*Rules for Descriptions*}
paulson@13259
   171
paulson@13259
   172
lemma the_equality [intro]:
paulson@13259
   173
    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
paulson@13259
   174
apply (unfold the_def) 
paulson@13259
   175
apply (fast dest: subst)
paulson@13259
   176
done
paulson@13259
   177
paulson@13259
   178
(* Only use this if you already know EX!x. P(x) *)
paulson@13259
   179
lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
paulson@13259
   180
by blast
paulson@13259
   181
paulson@13259
   182
lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
paulson@13259
   183
apply (erule ex1E)
paulson@13259
   184
apply (subst the_equality)
paulson@13259
   185
apply (blast+)
paulson@13259
   186
done
paulson@13259
   187
paulson@13259
   188
(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
paulson@13259
   189
  (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
paulson@13259
   190
paulson@13259
   191
(*If it's "undefined", it's zero!*)
paulson@13259
   192
lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
paulson@13259
   193
apply (unfold the_def)
paulson@13259
   194
apply (blast elim!: ReplaceE)
paulson@13259
   195
done
paulson@13259
   196
paulson@13259
   197
(*Easier to apply than theI: conclusion has only one occurrence of P*)
paulson@13259
   198
lemma theI2:
paulson@13259
   199
    assumes p1: "~ Q(0) ==> EX! x. P(x)"
paulson@13259
   200
        and p2: "!!x. P(x) ==> Q(x)"
paulson@13259
   201
    shows "Q(THE x. P(x))"
paulson@13259
   202
apply (rule classical)
paulson@13259
   203
apply (rule p2)
paulson@13259
   204
apply (rule theI)
paulson@13259
   205
apply (rule classical)
paulson@13259
   206
apply (rule p1)
paulson@13259
   207
apply (erule the_0 [THEN subst], assumption)
paulson@13259
   208
done
paulson@13259
   209
paulson@13357
   210
lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
paulson@13357
   211
by blast
paulson@13357
   212
paulson@13357
   213
subsection{*Conditional Terms: @{text "if-then-else"}*}
paulson@13259
   214
paulson@13259
   215
lemma if_true [simp]: "(if True then a else b) = a"
paulson@13259
   216
by (unfold if_def, blast)
paulson@13259
   217
paulson@13259
   218
lemma if_false [simp]: "(if False then a else b) = b"
paulson@13259
   219
by (unfold if_def, blast)
paulson@13259
   220
paulson@13259
   221
(*Never use with case splitting, or if P is known to be true or false*)
paulson@13259
   222
lemma if_cong:
paulson@13259
   223
    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |]  
paulson@13259
   224
     ==> (if P then a else b) = (if Q then c else d)"
paulson@13259
   225
by (simp add: if_def cong add: conj_cong)
paulson@13259
   226
paulson@13259
   227
(*Prevents simplification of x and y: faster and allows the execution
paulson@13259
   228
  of functional programs. NOW THE DEFAULT.*)
paulson@13259
   229
lemma if_weak_cong: "P<->Q ==> (if P then x else y) = (if Q then x else y)"
paulson@13259
   230
by simp
paulson@13259
   231
paulson@13259
   232
(*Not needed for rewriting, since P would rewrite to True anyway*)
paulson@13259
   233
lemma if_P: "P ==> (if P then a else b) = a"
paulson@13259
   234
by (unfold if_def, blast)
paulson@13259
   235
paulson@13259
   236
(*Not needed for rewriting, since P would rewrite to False anyway*)
paulson@13259
   237
lemma if_not_P: "~P ==> (if P then a else b) = b"
paulson@13259
   238
by (unfold if_def, blast)
paulson@13259
   239
paulson@13259
   240
lemma split_if: "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
paulson@13259
   241
(*no case_tac yet!*)
paulson@13259
   242
apply (rule_tac P=Q in case_split_thm, simp_all)
paulson@13259
   243
done
paulson@13259
   244
paulson@13259
   245
(** Rewrite rules for boolean case-splitting: faster than 
paulson@13259
   246
	addsplits[split_if]
paulson@13259
   247
**)
paulson@13259
   248
paulson@13259
   249
lemmas split_if_eq1 = split_if [of "%x. x = b", standard]
paulson@13259
   250
lemmas split_if_eq2 = split_if [of "%x. a = x", standard]
paulson@13259
   251
paulson@13259
   252
lemmas split_if_mem1 = split_if [of "%x. x : b", standard]
paulson@13259
   253
lemmas split_if_mem2 = split_if [of "%x. a : x", standard]
paulson@13259
   254
paulson@13259
   255
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
paulson@13259
   256
paulson@13259
   257
(*Logically equivalent to split_if_mem2*)
paulson@13259
   258
lemma if_iff: "a: (if P then x else y) <-> P & a:x | ~P & a:y"
paulson@13259
   259
by (simp split add: split_if)
paulson@13259
   260
paulson@13259
   261
lemma if_type [TC]:
paulson@13259
   262
    "[| P ==> a: A;  ~P ==> b: A |] ==> (if P then a else b): A"
paulson@13259
   263
by (simp split add: split_if)
paulson@13259
   264
paulson@13259
   265
paulson@13357
   266
subsection{*Consequences of Foundation*}
paulson@13259
   267
paulson@13259
   268
(*was called mem_anti_sym*)
paulson@13259
   269
lemma mem_asym: "[| a:b;  ~P ==> b:a |] ==> P"
paulson@13259
   270
apply (rule classical)
paulson@13259
   271
apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE])
paulson@13259
   272
apply (blast elim!: equalityE)+
paulson@13259
   273
done
paulson@13259
   274
paulson@13259
   275
(*was called mem_anti_refl*)
paulson@13259
   276
lemma mem_irrefl: "a:a ==> P"
paulson@13259
   277
by (blast intro: mem_asym)
paulson@13259
   278
paulson@13259
   279
(*mem_irrefl should NOT be added to default databases:
paulson@13259
   280
      it would be tried on most goals, making proofs slower!*)
paulson@13259
   281
paulson@13259
   282
lemma mem_not_refl: "a ~: a"
paulson@13259
   283
apply (rule notI)
paulson@13259
   284
apply (erule mem_irrefl)
paulson@13259
   285
done
paulson@13259
   286
paulson@13259
   287
(*Good for proving inequalities by rewriting*)
paulson@13259
   288
lemma mem_imp_not_eq: "a:A ==> a ~= A"
paulson@13259
   289
by (blast elim!: mem_irrefl)
paulson@13259
   290
paulson@13357
   291
lemma eq_imp_not_mem: "a=A ==> a ~: A"
paulson@13357
   292
by (blast intro: elim: mem_irrefl)
paulson@13357
   293
paulson@13357
   294
subsection{*Rules for Successor*}
paulson@13259
   295
paulson@13259
   296
lemma succ_iff: "i : succ(j) <-> i=j | i:j"
paulson@13259
   297
by (unfold succ_def, blast)
paulson@13259
   298
paulson@13259
   299
lemma succI1 [simp]: "i : succ(i)"
paulson@13259
   300
by (simp add: succ_iff)
paulson@13259
   301
paulson@13259
   302
lemma succI2: "i : j ==> i : succ(j)"
paulson@13259
   303
by (simp add: succ_iff)
paulson@13259
   304
paulson@13259
   305
lemma succE [elim!]: 
paulson@13259
   306
    "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
paulson@13259
   307
apply (simp add: succ_iff, blast) 
paulson@13259
   308
done
paulson@13259
   309
paulson@13259
   310
(*Classical introduction rule*)
paulson@13259
   311
lemma succCI [intro!]: "(i~:j ==> i=j) ==> i: succ(j)"
paulson@13259
   312
by (simp add: succ_iff, blast)
paulson@13259
   313
paulson@13259
   314
lemma succ_not_0 [simp]: "succ(n) ~= 0"
paulson@13259
   315
by (blast elim!: equalityE)
paulson@13259
   316
paulson@13259
   317
lemmas succ_neq_0 = succ_not_0 [THEN notE, standard, elim!]
paulson@13259
   318
paulson@13259
   319
declare succ_not_0 [THEN not_sym, simp]
paulson@13259
   320
declare sym [THEN succ_neq_0, elim!]
paulson@13259
   321
paulson@13259
   322
(* succ(c) <= B ==> c : B *)
paulson@13259
   323
lemmas succ_subsetD = succI1 [THEN [2] subsetD]
paulson@13259
   324
paulson@13259
   325
(* succ(b) ~= b *)
paulson@13259
   326
lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym, standard]
paulson@13259
   327
paulson@13259
   328
lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n"
paulson@13259
   329
by (blast elim: mem_asym elim!: equalityE)
paulson@13259
   330
paulson@13259
   331
lemmas succ_inject = succ_inject_iff [THEN iffD1, standard, dest!]
paulson@13259
   332
paulson@13259
   333
ML
paulson@13259
   334
{*
paulson@13259
   335
val Pow_bottom = thm "Pow_bottom";
paulson@13259
   336
val Pow_top = thm "Pow_top";
paulson@13259
   337
val Upair_iff = thm "Upair_iff";
paulson@13259
   338
val UpairI1 = thm "UpairI1";
paulson@13259
   339
val UpairI2 = thm "UpairI2";
paulson@13259
   340
val UpairE = thm "UpairE";
paulson@13259
   341
val Un_iff = thm "Un_iff";
paulson@13259
   342
val UnI1 = thm "UnI1";
paulson@13259
   343
val UnI2 = thm "UnI2";
paulson@13259
   344
val UnE = thm "UnE";
paulson@13259
   345
val UnE' = thm "UnE'";
paulson@13259
   346
val UnCI = thm "UnCI";
paulson@13259
   347
val Int_iff = thm "Int_iff";
paulson@13259
   348
val IntI = thm "IntI";
paulson@13259
   349
val IntD1 = thm "IntD1";
paulson@13259
   350
val IntD2 = thm "IntD2";
paulson@13259
   351
val IntE = thm "IntE";
paulson@13259
   352
val Diff_iff = thm "Diff_iff";
paulson@13259
   353
val DiffI = thm "DiffI";
paulson@13259
   354
val DiffD1 = thm "DiffD1";
paulson@13259
   355
val DiffD2 = thm "DiffD2";
paulson@13259
   356
val DiffE = thm "DiffE";
paulson@13259
   357
val cons_iff = thm "cons_iff";
paulson@13259
   358
val consI1 = thm "consI1";
paulson@13259
   359
val consI2 = thm "consI2";
paulson@13259
   360
val consE = thm "consE";
paulson@13259
   361
val consE' = thm "consE'";
paulson@13259
   362
val consCI = thm "consCI";
paulson@13259
   363
val cons_not_0 = thm "cons_not_0";
paulson@13259
   364
val cons_neq_0 = thm "cons_neq_0";
paulson@13259
   365
val singleton_iff = thm "singleton_iff";
paulson@13259
   366
val singletonI = thm "singletonI";
paulson@13259
   367
val singletonE = thm "singletonE";
paulson@13259
   368
val the_equality = thm "the_equality";
paulson@13259
   369
val the_equality2 = thm "the_equality2";
paulson@13259
   370
val theI = thm "theI";
paulson@13259
   371
val the_0 = thm "the_0";
paulson@13259
   372
val theI2 = thm "theI2";
paulson@13259
   373
val if_true = thm "if_true";
paulson@13259
   374
val if_false = thm "if_false";
paulson@13259
   375
val if_cong = thm "if_cong";
paulson@13259
   376
val if_weak_cong = thm "if_weak_cong";
paulson@13259
   377
val if_P = thm "if_P";
paulson@13259
   378
val if_not_P = thm "if_not_P";
paulson@13259
   379
val split_if = thm "split_if";
paulson@13259
   380
val split_if_eq1 = thm "split_if_eq1";
paulson@13259
   381
val split_if_eq2 = thm "split_if_eq2";
paulson@13259
   382
val split_if_mem1 = thm "split_if_mem1";
paulson@13259
   383
val split_if_mem2 = thm "split_if_mem2";
paulson@13259
   384
val if_iff = thm "if_iff";
paulson@13259
   385
val if_type = thm "if_type";
paulson@13259
   386
val mem_asym = thm "mem_asym";
paulson@13259
   387
val mem_irrefl = thm "mem_irrefl";
paulson@13259
   388
val mem_not_refl = thm "mem_not_refl";
paulson@13259
   389
val mem_imp_not_eq = thm "mem_imp_not_eq";
paulson@13259
   390
val succ_iff = thm "succ_iff";
paulson@13259
   391
val succI1 = thm "succI1";
paulson@13259
   392
val succI2 = thm "succI2";
paulson@13259
   393
val succE = thm "succE";
paulson@13259
   394
val succCI = thm "succCI";
paulson@13259
   395
val succ_not_0 = thm "succ_not_0";
paulson@13259
   396
val succ_neq_0 = thm "succ_neq_0";
paulson@13259
   397
val succ_subsetD = thm "succ_subsetD";
paulson@13259
   398
val succ_neq_self = thm "succ_neq_self";
paulson@13259
   399
val succ_inject_iff = thm "succ_inject_iff";
paulson@13259
   400
val succ_inject = thm "succ_inject";
paulson@13259
   401
paulson@13259
   402
val split_ifs = thms "split_ifs";
paulson@13259
   403
*}
paulson@13259
   404
paulson@6153
   405
end