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