src/HOL/Fun.ML
author wenzelm
Thu Jun 22 23:04:34 2000 +0200 (2000-06-22)
changeset 9108 9fff97d29837
parent 8767 eae30939b592
child 9339 0d8b0eb2932d
permissions -rw-r--r--
bind_thm(s);
clasohm@1465
     1
(*  Title:      HOL/Fun
clasohm@923
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1993  University of Cambridge
clasohm@923
     5
clasohm@923
     6
Lemmas about functions.
clasohm@923
     7
*)
clasohm@923
     8
paulson@7089
     9
Goal "(f = g) = (! x. f(x)=g(x))";
clasohm@923
    10
by (rtac iffI 1);
clasohm@1264
    11
by (Asm_simp_tac 1);
clasohm@1264
    12
by (rtac ext 1 THEN Asm_simp_tac 1);
clasohm@923
    13
qed "expand_fun_eq";
clasohm@923
    14
paulson@5316
    15
val prems = Goal
clasohm@923
    16
    "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
clasohm@923
    17
by (rtac (arg_cong RS box_equals) 1);
clasohm@923
    18
by (REPEAT (resolve_tac (prems@[refl]) 1));
clasohm@923
    19
qed "apply_inverse";
clasohm@923
    20
clasohm@923
    21
paulson@4656
    22
(** "Axiom" of Choice, proved using the description operator **)
paulson@4656
    23
paulson@5316
    24
Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
paulson@4656
    25
by (fast_tac (claset() addEs [selectI]) 1);
paulson@4656
    26
qed "choice";
paulson@4656
    27
paulson@5316
    28
Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
paulson@4656
    29
by (fast_tac (claset() addEs [selectI]) 1);
paulson@4656
    30
qed "bchoice";
paulson@4656
    31
paulson@4656
    32
nipkow@5608
    33
section "id";
oheimb@5441
    34
paulson@7089
    35
Goalw [id_def] "id x = x";
paulson@7089
    36
by (rtac refl 1);
paulson@7089
    37
qed "id_apply";
nipkow@5608
    38
Addsimps [id_apply];
oheimb@5441
    39
paulson@8226
    40
Goal "inv id = id";
paulson@8226
    41
by (simp_tac (simpset() addsimps [inv_def,id_def]) 1);
paulson@8226
    42
qed "inv_id";
paulson@8226
    43
Addsimps [inv_id];
paulson@8226
    44
oheimb@5441
    45
oheimb@5306
    46
section "o";
oheimb@5306
    47
paulson@7089
    48
Goalw [o_def] "(f o g) x = f (g x)";
paulson@7089
    49
by (rtac refl 1);
paulson@7089
    50
qed "o_apply";
oheimb@5306
    51
Addsimps [o_apply];
oheimb@5306
    52
paulson@7089
    53
Goalw [o_def] "f o (g o h) = f o g o h";
paulson@7089
    54
by (rtac ext 1);
paulson@7089
    55
by (rtac refl 1);
paulson@7089
    56
qed "o_assoc";
oheimb@5306
    57
paulson@7089
    58
Goalw [id_def] "id o g = g";
paulson@7089
    59
by (rtac ext 1);
paulson@7089
    60
by (Simp_tac 1);
paulson@7089
    61
qed "id_o";
nipkow@5608
    62
Addsimps [id_o];
oheimb@5306
    63
paulson@7089
    64
Goalw [id_def] "f o id = f";
paulson@7089
    65
by (rtac ext 1);
paulson@7089
    66
by (Simp_tac 1);
paulson@7089
    67
qed "o_id";
nipkow@5608
    68
Addsimps [o_id];
oheimb@5306
    69
oheimb@5306
    70
Goalw [o_def] "(f o g)``r = f``(g``r)";
oheimb@5306
    71
by (Blast_tac 1);
oheimb@5306
    72
qed "image_compose";
oheimb@5306
    73
paulson@7916
    74
Goal "f``A = (UN x:A. {f x})";
paulson@7536
    75
by (Blast_tac 1);
paulson@7916
    76
qed "image_eq_UN";
paulson@7536
    77
paulson@5852
    78
Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
paulson@5852
    79
by (Blast_tac 1);
paulson@6829
    80
qed "UN_o";
paulson@5852
    81
berghofe@7014
    82
(** lemma for proving injectivity of representation functions for **)
berghofe@7014
    83
(** datatypes involving function types                            **)
berghofe@7014
    84
berghofe@7014
    85
Goalw [o_def]
paulson@7089
    86
  "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
paulson@7089
    87
by (rtac ext 1);
paulson@7089
    88
by (etac allE 1);
paulson@7089
    89
by (etac allE 1);
paulson@7089
    90
by (etac mp 1);
paulson@7089
    91
by (etac fun_cong 1);
berghofe@7014
    92
qed "inj_fun_lemma";
berghofe@7014
    93
oheimb@5306
    94
oheimb@5306
    95
section "inj";
paulson@6171
    96
(**NB: inj now just translates to inj_on**)
oheimb@5306
    97
clasohm@923
    98
(*** inj(f): f is a one-to-one function ***)
clasohm@923
    99
paulson@6171
   100
(*for Tools/datatype_rep_proofs*)
paulson@6171
   101
val [prem] = Goalw [inj_on_def]
paulson@6171
   102
    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)";
paulson@6171
   103
by (blast_tac (claset() addIs [prem RS spec RS mp]) 1);
paulson@6171
   104
qed "datatype_injI";
clasohm@923
   105
paulson@6171
   106
Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
paulson@5316
   107
by (Blast_tac 1);
clasohm@923
   108
qed "injD";
clasohm@923
   109
clasohm@923
   110
(*Useful with the simplifier*)
paulson@5316
   111
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
clasohm@923
   112
by (rtac iffI 1);
paulson@5316
   113
by (etac arg_cong 2);
paulson@5316
   114
by (etac injD 1);
paulson@5318
   115
by (assume_tac 1);
clasohm@923
   116
qed "inj_eq";
clasohm@923
   117
paulson@5316
   118
Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
paulson@5316
   119
by (etac injD 1);
clasohm@923
   120
by (rtac selectI 1);
clasohm@923
   121
by (rtac refl 1);
clasohm@923
   122
qed "inj_select";
clasohm@923
   123
clasohm@923
   124
(*A one-to-one function has an inverse (given using select).*)
paulson@5316
   125
Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
paulson@5316
   126
by (etac inj_select 1);
nipkow@2912
   127
qed "inv_f_f";
paulson@7338
   128
Addsimps [inv_f_f];
clasohm@923
   129
paulson@7338
   130
Goal "[| inj(f);  f x = y |] ==> inv f y = x";
paulson@7338
   131
by (etac subst 1);
paulson@7338
   132
by (etac inv_f_f 1);
paulson@7338
   133
qed "inv_f_eq";
paulson@6235
   134
clasohm@923
   135
(* Useful??? *)
paulson@5316
   136
val [oneone,minor] = Goal
nipkow@2912
   137
    "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
nipkow@2912
   138
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
clasohm@923
   139
by (rtac (rangeI RS minor) 1);
clasohm@923
   140
qed "inj_transfer";
clasohm@923
   141
berghofe@7014
   142
Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
berghofe@7014
   143
by (rtac ext 1);
berghofe@7014
   144
by (etac injD 1);
berghofe@7014
   145
by (etac fun_cong 1);
berghofe@7014
   146
qed "inj_o";
clasohm@923
   147
nipkow@4830
   148
(*** inj_on f A: f is one-to-one over A ***)
clasohm@923
   149
paulson@5316
   150
val prems = Goalw [inj_on_def]
nipkow@4830
   151
    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
wenzelm@4089
   152
by (blast_tac (claset() addIs prems) 1);
nipkow@4830
   153
qed "inj_onI";
wenzelm@9108
   154
bind_thm ("injI", inj_onI);                  (*for compatibility*)
clasohm@923
   155
paulson@5316
   156
val [major] = Goal 
nipkow@4830
   157
    "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
nipkow@4830
   158
by (rtac inj_onI 1);
clasohm@923
   159
by (etac (apply_inverse RS trans) 1);
clasohm@923
   160
by (REPEAT (eresolve_tac [asm_rl,major] 1));
nipkow@4830
   161
qed "inj_on_inverseI";
wenzelm@9108
   162
bind_thm ("inj_inverseI", inj_on_inverseI);   (*for compatibility*)
clasohm@923
   163
paulson@8285
   164
Goal "(inj f) = (inv f o f = id)";
paulson@8285
   165
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
paulson@8285
   166
by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1);
paulson@8285
   167
qed "inj_iff";
paulson@8285
   168
paulson@5316
   169
Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
paulson@5316
   170
by (Blast_tac 1);
nipkow@4830
   171
qed "inj_onD";
clasohm@923
   172
paulson@5143
   173
Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
nipkow@4830
   174
by (blast_tac (claset() addSDs [inj_onD]) 1);
nipkow@4830
   175
qed "inj_on_iff";
clasohm@923
   176
paulson@5316
   177
Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
paulson@5316
   178
by (Blast_tac 1);
nipkow@4830
   179
qed "inj_on_contraD";
clasohm@923
   180
oheimb@8156
   181
Goal "inj (%s. {s})";
paulson@8253
   182
by (rtac injI 1);
paulson@8253
   183
by (etac singleton_inject 1);
oheimb@8156
   184
qed "inj_singleton";
oheimb@8156
   185
paulson@5316
   186
Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
paulson@3341
   187
by (Blast_tac 1);
nipkow@4830
   188
qed "subset_inj_on";
paulson@3341
   189
clasohm@923
   190
paulson@6235
   191
(** surj **)
paulson@6235
   192
paulson@6267
   193
val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
paulson@6267
   194
by (blast_tac (claset() addIs [prem RS sym]) 1);
paulson@6235
   195
qed "surjI";
paulson@6235
   196
paulson@6235
   197
Goalw [surj_def] "surj f ==> range f = UNIV";
paulson@6235
   198
by Auto_tac;
paulson@6235
   199
qed "surj_range";
paulson@6235
   200
paulson@6267
   201
Goalw [surj_def] "surj f ==> EX x. y = f x";
paulson@6267
   202
by (Blast_tac 1);
paulson@6267
   203
qed "surjD";
paulson@6267
   204
paulson@8253
   205
Goal "inj f ==> surj (inv f)";
paulson@8253
   206
by (blast_tac (claset() addIs [surjI, inv_f_f]) 1);
paulson@8253
   207
qed "inj_imp_surj_inv";
paulson@7374
   208
paulson@7374
   209
paulson@6171
   210
(*** Lemmas about injective functions and inv ***)
clasohm@923
   211
nipkow@7051
   212
Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
paulson@6171
   213
by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
paulson@6171
   214
qed "comp_inj_on";
clasohm@923
   215
paulson@5316
   216
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
paulson@5316
   217
by (fast_tac (claset() addIs [selectI]) 1);
nipkow@2912
   218
qed "f_inv_f";
clasohm@923
   219
paulson@6235
   220
Goal "surj f ==> f(inv f y) = y";
paulson@6235
   221
by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
paulson@6235
   222
qed "surj_f_inv_f";
paulson@6235
   223
paulson@6171
   224
Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
nipkow@2912
   225
by (rtac (arg_cong RS box_equals) 1);
paulson@5316
   226
by (REPEAT (ares_tac [f_inv_f] 1));
nipkow@2912
   227
qed "inv_injective";
nipkow@2912
   228
paulson@6235
   229
Goal "A <= range(f) ==> inj_on (inv f) A";
nipkow@4830
   230
by (fast_tac (claset() addIs [inj_onI] 
paulson@6235
   231
                       addEs [inv_injective, injD]) 1);
nipkow@4830
   232
qed "inj_on_inv";
clasohm@923
   233
paulson@6235
   234
Goal "surj f ==> inj (inv f)";
paulson@6235
   235
by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
paulson@6235
   236
qed "surj_imp_inj_inv";
paulson@6235
   237
paulson@8285
   238
Goal "(surj f) = (f o inv f = id)";
paulson@8285
   239
by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
paulson@8285
   240
by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
paulson@8285
   241
qed "surj_iff";
paulson@8285
   242
paulson@8253
   243
paulson@8253
   244
(** Bijections **)
paulson@8253
   245
paulson@8253
   246
Goalw [bij_def] "[| inj f; surj f |] ==> bij f";
paulson@8253
   247
by (Blast_tac 1);
paulson@8253
   248
qed "bijI";
paulson@8253
   249
paulson@8253
   250
Goalw [bij_def] "bij f ==> inj f";
paulson@8253
   251
by (Blast_tac 1);
paulson@8253
   252
qed "bij_is_inj";
paulson@8253
   253
paulson@8253
   254
Goalw [bij_def] "bij f ==> surj f";
paulson@8253
   255
by (Blast_tac 1);
paulson@8253
   256
qed "bij_is_surj";
paulson@8253
   257
paulson@8253
   258
Goalw [bij_def] "bij f ==> bij (inv f)";
paulson@8253
   259
by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1);
paulson@8253
   260
qed "bij_imp_bij_inv";
paulson@8253
   261
paulson@8253
   262
val prems = 
paulson@8253
   263
Goalw [inv_def] "[| !! x. g (f x) = x;  !! y. f (g y) = y |] ==> inv f = g";
paulson@8253
   264
by (rtac ext 1);
paulson@8253
   265
by (auto_tac (claset(), simpset() addsimps prems));
paulson@8253
   266
qed "inv_equality";
paulson@8253
   267
paulson@8253
   268
Goalw [bij_def] "bij f ==> inv (inv f) = f";
paulson@8253
   269
by (rtac inv_equality 1);
paulson@8253
   270
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
paulson@8253
   271
qed "inv_inv_eq";
paulson@8253
   272
paulson@8253
   273
Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f";
paulson@8253
   274
by (rtac (inv_equality) 1);
paulson@8253
   275
by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
paulson@8253
   276
qed "o_inv_distrib";
paulson@8253
   277
paulson@8253
   278
paulson@7514
   279
(** We seem to need both the id-forms and the (%x. x) forms; the latter can
paulson@7514
   280
    arise by rewriting, while id may be used explicitly. **)
paulson@7514
   281
paulson@7514
   282
Goal "(%x. x) `` Y = Y";
paulson@7514
   283
by (Blast_tac 1);
paulson@7514
   284
qed "image_ident";
paulson@7514
   285
paulson@7514
   286
Goalw [id_def] "id `` Y = Y";
paulson@7514
   287
by (Blast_tac 1);
paulson@7514
   288
qed "image_id";
paulson@7514
   289
Addsimps [image_ident, image_id];
paulson@7514
   290
paulson@7514
   291
Goal "(%x. x) -`` Y = Y";
paulson@7514
   292
by (Blast_tac 1);
paulson@7514
   293
qed "vimage_ident";
paulson@7514
   294
paulson@7514
   295
Goalw [id_def] "id -`` A = A";
paulson@7514
   296
by Auto_tac;
paulson@7514
   297
qed "vimage_id";
paulson@7514
   298
Addsimps [vimage_ident, vimage_id];
paulson@7514
   299
paulson@7876
   300
Goal "f -`` (f `` A) = {y. EX x:A. f x = f y}";
paulson@7876
   301
by (blast_tac (claset() addIs [sym]) 1);
paulson@7876
   302
qed "vimage_image_eq";
paulson@7876
   303
paulson@8173
   304
Goal "f `` (f -`` A) <= A";
paulson@8173
   305
by (Blast_tac 1);
paulson@8173
   306
qed "image_vimage_subset";
paulson@8173
   307
paulson@8173
   308
Goal "f `` (f -`` A) = A Int range f";
paulson@8173
   309
by (Blast_tac 1);
paulson@8173
   310
qed "image_vimage_eq";
paulson@8173
   311
Addsimps [image_vimage_eq];
paulson@8173
   312
paulson@8173
   313
Goal "surj f ==> f `` (f -`` A) = A";
paulson@8173
   314
by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
paulson@8173
   315
qed "surj_image_vimage_eq";
paulson@8173
   316
paulson@8253
   317
Goal "surj f ==> f `` (inv f `` A) = A";
paulson@8253
   318
by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
paulson@8253
   319
qed "image_surj_f_inv_f";
paulson@8253
   320
paulson@8173
   321
Goalw [inj_on_def] "inj f ==> f -`` (f `` A) = A";
paulson@8173
   322
by (Blast_tac 1);
paulson@8173
   323
qed "inj_vimage_image_eq";
paulson@8173
   324
paulson@8253
   325
Goal "inj f ==> (inv f) `` (f `` A) = A";
paulson@8253
   326
by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
paulson@8253
   327
qed "image_inv_f_f";
paulson@8253
   328
paulson@8173
   329
Goalw [surj_def] "surj f ==> f -`` B <= A ==> B <= f `` A";
paulson@8173
   330
by (blast_tac (claset() addIs [sym]) 1);
paulson@8173
   331
qed "vimage_subsetD";
paulson@8173
   332
paulson@8173
   333
Goalw [inj_on_def] "inj f ==> B <= f `` A ==> f -`` B <= A";
paulson@8173
   334
by (Blast_tac 1);
paulson@8173
   335
qed "vimage_subsetI";
paulson@8173
   336
paulson@8173
   337
Goalw [bij_def] "bij f ==> (f -`` B <= A) = (B <= f `` A)";
paulson@8173
   338
by (blast_tac (claset() delrules [subsetI]
paulson@8173
   339
			addIs [vimage_subsetI, vimage_subsetD]) 1);
paulson@8173
   340
qed "vimage_subset_eq";
paulson@8173
   341
paulson@6290
   342
Goal "f``(A Int B) <= f``A Int f``B";
paulson@6290
   343
by (Blast_tac 1);
paulson@6290
   344
qed "image_Int_subset";
paulson@6290
   345
paulson@6290
   346
Goal "f``A - f``B <= f``(A - B)";
paulson@6290
   347
by (Blast_tac 1);
paulson@6290
   348
qed "image_diff_subset";
paulson@6290
   349
wenzelm@5069
   350
Goalw [inj_on_def]
paulson@5148
   351
   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
paulson@4059
   352
by (Blast_tac 1);
nipkow@4830
   353
qed "inj_on_image_Int";
paulson@4059
   354
wenzelm@5069
   355
Goalw [inj_on_def]
paulson@5148
   356
   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
paulson@4059
   357
by (Blast_tac 1);
nipkow@4830
   358
qed "inj_on_image_set_diff";
paulson@4059
   359
paulson@6171
   360
Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B";
paulson@4059
   361
by (Blast_tac 1);
paulson@4059
   362
qed "image_Int";
paulson@4059
   363
paulson@6171
   364
Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B";
paulson@4059
   365
by (Blast_tac 1);
paulson@4059
   366
qed "image_set_diff";
paulson@4059
   367
paulson@6235
   368
Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";
paulson@6235
   369
by Auto_tac;
paulson@6235
   370
qed "inv_image_comp";
paulson@5847
   371
paulson@6301
   372
Goal "inj f ==> (f a : f``A) = (a : A)";
paulson@6301
   373
by (blast_tac (claset() addDs [injD]) 1);
paulson@6301
   374
qed "inj_image_mem_iff";
paulson@6301
   375
paulson@8253
   376
Goalw [inj_on_def] "inj f ==> (f``A <= f``B) = (A<=B)";
paulson@8253
   377
by (Blast_tac 1);
paulson@8253
   378
qed "inj_image_subset_iff";
paulson@8253
   379
paulson@6301
   380
Goal "inj f ==> (f``A = f``B) = (A = B)";
paulson@6301
   381
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
paulson@6301
   382
qed "inj_image_eq_iff";
paulson@6301
   383
paulson@6829
   384
Goal  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
paulson@6829
   385
by (Blast_tac 1);
paulson@6829
   386
qed "image_UN";
paulson@6829
   387
paulson@6829
   388
(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
paulson@6829
   389
Goalw [inj_on_def]
paulson@6829
   390
   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |] \
paulson@6829
   391
\   ==> f `` (INTER A B) = (INT x:A. f `` B x)";
paulson@6829
   392
by (Blast_tac 1);
paulson@6829
   393
qed "image_INT";
paulson@6829
   394
paulson@8309
   395
(*Compare with image_INT: no use of inj_on, and if f is surjective then
paulson@8309
   396
  it doesn't matter whether A is empty*)
paulson@8309
   397
Goalw [bij_def] "bij f ==> f `` (INTER A B) = (INT x:A. f `` B x)";
paulson@8309
   398
by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI], 
paulson@8309
   399
	       simpset()) 1);
paulson@8309
   400
qed "bij_image_INT";
paulson@8309
   401
paulson@8309
   402
Goal "bij f ==> f `` Collect P = {y. P (inv f y)}";
paulson@8309
   403
by Auto_tac;
paulson@8309
   404
by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
paulson@8309
   405
by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
paulson@8309
   406
qed "bij_image_Collect_eq";
paulson@8309
   407
paulson@8309
   408
Goal "bij f ==> f -`` A = inv f `` A";
paulson@8767
   409
by Safe_tac;
paulson@8309
   410
by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
paulson@8309
   411
by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
paulson@8309
   412
qed "bij_vimage_eq_inv_image";
paulson@8309
   413
wenzelm@4089
   414
val set_cs = claset() delrules [equalityI];
oheimb@5305
   415
oheimb@5305
   416
oheimb@5305
   417
section "fun_upd";
oheimb@5305
   418
oheimb@5305
   419
Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
oheimb@5305
   420
by Safe_tac;
oheimb@5305
   421
by (etac subst 1);
oheimb@5305
   422
by (rtac ext 2);
oheimb@5305
   423
by Auto_tac;
oheimb@5305
   424
qed "fun_upd_idem_iff";
oheimb@5305
   425
oheimb@5305
   426
(* f x = y ==> f(x:=y) = f *)
oheimb@5305
   427
bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
oheimb@5305
   428
oheimb@5305
   429
(* f(x := f x) = f *)
oheimb@5305
   430
AddIffs [refl RS fun_upd_idem];
oheimb@5305
   431
oheimb@5305
   432
Goal "(f(x:=y))z = (if z=x then y else f z)";
oheimb@5305
   433
by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
oheimb@5305
   434
qed "fun_upd_apply";
oheimb@5305
   435
Addsimps [fun_upd_apply];
oheimb@5305
   436
paulson@7445
   437
(*fun_upd_apply supersedes these two*)
paulson@7089
   438
Goal "(f(x:=y)) x = y";
paulson@7089
   439
by (Simp_tac 1);
paulson@7089
   440
qed "fun_upd_same";
paulson@7089
   441
paulson@7089
   442
Goal "z~=x ==> (f(x:=y)) z = f z";
paulson@7089
   443
by (Asm_simp_tac 1);
paulson@7089
   444
qed "fun_upd_other";
paulson@7089
   445
paulson@7445
   446
Goal "f(x:=y,x:=z) = f(x:=z)";
paulson@7445
   447
by (rtac ext 1);
paulson@7445
   448
by (Simp_tac 1);
paulson@7445
   449
qed "fun_upd_upd";
paulson@7445
   450
Addsimps [fun_upd_upd];
oheimb@5305
   451
oheimb@8258
   452
Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)";
oheimb@5305
   453
by (rtac ext 1);
paulson@7089
   454
by Auto_tac;
oheimb@5305
   455
qed "fun_upd_twist";
paulson@5852
   456
paulson@5852
   457
paulson@5852
   458
(*** -> and Pi, by Florian Kammueller and LCP ***)
paulson@5852
   459
paulson@5852
   460
val prems = Goalw [Pi_def]
paulson@5852
   461
"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
paulson@5852
   462
\    ==> f: Pi A B";
paulson@5852
   463
by (auto_tac (claset(), simpset() addsimps prems));
paulson@5852
   464
qed "Pi_I";
paulson@5852
   465
paulson@5852
   466
val prems = Goal 
paulson@5852
   467
"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
paulson@5852
   468
by (blast_tac (claset() addIs Pi_I::prems) 1);
paulson@5852
   469
qed "funcsetI";
paulson@5852
   470
paulson@5852
   471
Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
paulson@5852
   472
by Auto_tac;
paulson@5852
   473
qed "Pi_mem";
paulson@5852
   474
paulson@5852
   475
Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
paulson@5852
   476
by Auto_tac;
paulson@5852
   477
qed "funcset_mem";
paulson@5852
   478
paulson@5852
   479
Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
paulson@5852
   480
by Auto_tac;
paulson@5852
   481
qed "apply_arb";
paulson@5852
   482
paulson@5852
   483
Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
paulson@5852
   484
by (rtac ext 1);
paulson@5852
   485
by Auto_tac;
wenzelm@9108
   486
bind_thm ("Pi_extensionality", ballI RSN (3, result()));
paulson@5852
   487
paulson@8138
   488
paulson@5852
   489
(*** compose ***)
paulson@5852
   490
paulson@5852
   491
Goalw [Pi_def, compose_def, restrict_def]
paulson@5852
   492
     "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
paulson@5852
   493
by Auto_tac;
paulson@5852
   494
qed "funcset_compose";
paulson@5852
   495
paulson@5852
   496
Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
paulson@5852
   497
\     ==> compose A h (compose A g f) = compose A (compose B h g) f";
paulson@5852
   498
by (res_inst_tac [("A","A")] Pi_extensionality 1);
paulson@5852
   499
by (blast_tac (claset() addIs [funcset_compose]) 1);
paulson@5852
   500
by (blast_tac (claset() addIs [funcset_compose]) 1);
paulson@5852
   501
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
paulson@5852
   502
by Auto_tac;
paulson@5852
   503
qed "compose_assoc";
paulson@5852
   504
paulson@5852
   505
Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))";
paulson@5852
   506
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
paulson@5852
   507
qed "compose_eq";
paulson@5852
   508
paulson@5852
   509
Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
paulson@5852
   510
\     ==> compose A g f `` A = C";
paulson@5852
   511
by (auto_tac (claset(),
paulson@5852
   512
	      simpset() addsimps [image_def, compose_eq]));
paulson@5852
   513
qed "surj_compose";
paulson@5852
   514
paulson@5852
   515
Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
paulson@5852
   516
\     ==> inj_on (compose A g f) A";
paulson@5852
   517
by (auto_tac (claset(),
oheimb@8081
   518
	      simpset() addsimps [inj_on_def, compose_eq]));
paulson@5852
   519
qed "inj_on_compose";
paulson@5852
   520
paulson@5852
   521
paulson@5852
   522
(*** restrict / lam ***)
paulson@8138
   523
paulson@8138
   524
Goal "f``A <= B ==> (lam x: A. f x) : A funcset B";
paulson@5852
   525
by (auto_tac (claset(),
paulson@5852
   526
	      simpset() addsimps [restrict_def, Pi_def]));
paulson@5852
   527
qed "restrict_in_funcset";
paulson@5852
   528
paulson@5852
   529
val prems = Goalw [restrict_def, Pi_def]
paulson@5852
   530
     "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
paulson@5852
   531
by (asm_simp_tac (simpset() addsimps prems) 1);
paulson@5852
   532
qed "restrictI";
paulson@5852
   533
paulson@5852
   534
Goal "x: A ==> (lam y: A. f y) x = f x";
paulson@5852
   535
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
paulson@5852
   536
qed "restrict_apply1";
paulson@5852
   537
paulson@5852
   538
Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
paulson@5852
   539
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
paulson@5852
   540
qed "restrict_apply1_mem";
paulson@5852
   541
paulson@5852
   542
Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
paulson@5852
   543
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
paulson@5852
   544
qed "restrict_apply2";
paulson@5852
   545
paulson@5852
   546
val prems = Goal
paulson@5852
   547
    "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
paulson@5852
   548
by (rtac ext 1);
paulson@5852
   549
by (auto_tac (claset(),
paulson@5852
   550
	      simpset() addsimps prems@[restrict_def, Pi_def]));
paulson@5852
   551
qed "restrict_ext";
paulson@5852
   552
paulson@8138
   553
Goalw [inj_on_def, restrict_def] "inj_on (restrict f A) A = inj_on f A";
paulson@8138
   554
by Auto_tac;
paulson@8138
   555
qed "inj_on_restrict_eq";
paulson@8138
   556
paulson@5852
   557
paulson@5852
   558
(*** Inverse ***)
paulson@5852
   559
paulson@5852
   560
Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
paulson@5852
   561
by (Blast_tac 1);
paulson@5852
   562
qed "surj_image";
paulson@5852
   563
paulson@5852
   564
Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
paulson@5852
   565
\                ==> (lam x: B. (Inv A f) x) : B funcset A";
paulson@5852
   566
by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
paulson@5852
   567
qed "Inv_funcset";
paulson@5852
   568
paulson@5852
   569
paulson@5852
   570
Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
paulson@5852
   571
\     ==> (lam y: B. (Inv A f) y) (f x) = x";
paulson@5852
   572
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
oheimb@8081
   573
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
paulson@5852
   574
by (rtac selectI2 1);
paulson@5852
   575
by Auto_tac;
paulson@5852
   576
qed "Inv_f_f";
paulson@5852
   577
paulson@5852
   578
Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
paulson@5852
   579
\     ==> f ((lam y: B. (Inv A f y)) x) = x";
paulson@5852
   580
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
paulson@5852
   581
by (fast_tac (claset() addIs [selectI2]) 1);
paulson@5852
   582
qed "f_Inv_f";
paulson@5852
   583
paulson@5852
   584
Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
paulson@5852
   585
\     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
paulson@5852
   586
by (rtac Pi_extensionality 1);
paulson@5852
   587
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
paulson@5852
   588
by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
paulson@5852
   589
by (asm_simp_tac
paulson@5852
   590
    (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
paulson@5852
   591
qed "compose_Inv_id";
paulson@5852
   592
paulson@5852
   593
paulson@5852
   594
(*** Pi and Applyall ***)
paulson@5852
   595
paulson@5852
   596
Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
paulson@5852
   597
by Auto_tac;
paulson@5852
   598
qed "Pi_eq_empty";
paulson@5852
   599
paulson@5852
   600
Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
paulson@5852
   601
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
paulson@5852
   602
qed "Pi_total1";
paulson@5852
   603
paulson@5852
   604
Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
paulson@5852
   605
by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
paulson@5852
   606
by (rename_tac "g z" 1);
paulson@5852
   607
by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
paulson@5852
   608
by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
paulson@5852
   609
qed "Applyall_beta";
paulson@5852
   610
paulson@5865
   611
Goal "Pi {} B = { (%x. @ y. True) }";
paulson@5865
   612
by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
paulson@5865
   613
qed "Pi_empty";
paulson@5852
   614
paulson@5865
   615
val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
paulson@5865
   616
by (auto_tac (claset(),
paulson@5865
   617
	      simpset() addsimps [impOfSubs major]));
paulson@5865
   618
qed "Pi_mono";