src/HOL/Fun.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7536 5c094aec523d
child 7876 1b3b683c092e
permissions -rw-r--r--
tidied; added lemma restrict_to_left
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@4656
     9
paulson@7089
    10
Goal "(f = g) = (! x. f(x)=g(x))";
clasohm@923
    11
by (rtac iffI 1);
clasohm@1264
    12
by (Asm_simp_tac 1);
clasohm@1264
    13
by (rtac ext 1 THEN Asm_simp_tac 1);
clasohm@923
    14
qed "expand_fun_eq";
clasohm@923
    15
paulson@5316
    16
val prems = Goal
clasohm@923
    17
    "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
clasohm@923
    18
by (rtac (arg_cong RS box_equals) 1);
clasohm@923
    19
by (REPEAT (resolve_tac (prems@[refl]) 1));
clasohm@923
    20
qed "apply_inverse";
clasohm@923
    21
clasohm@923
    22
paulson@4656
    23
(** "Axiom" of Choice, proved using the description operator **)
paulson@4656
    24
paulson@5316
    25
Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
paulson@4656
    26
by (fast_tac (claset() addEs [selectI]) 1);
paulson@4656
    27
qed "choice";
paulson@4656
    28
paulson@5316
    29
Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
paulson@4656
    30
by (fast_tac (claset() addEs [selectI]) 1);
paulson@4656
    31
qed "bchoice";
paulson@4656
    32
paulson@4656
    33
nipkow@5608
    34
section "id";
oheimb@5441
    35
paulson@7089
    36
Goalw [id_def] "id x = x";
paulson@7089
    37
by (rtac refl 1);
paulson@7089
    38
qed "id_apply";
nipkow@5608
    39
Addsimps [id_apply];
oheimb@5441
    40
oheimb@5441
    41
oheimb@5306
    42
section "o";
oheimb@5306
    43
paulson@7089
    44
Goalw [o_def] "(f o g) x = f (g x)";
paulson@7089
    45
by (rtac refl 1);
paulson@7089
    46
qed "o_apply";
oheimb@5306
    47
Addsimps [o_apply];
oheimb@5306
    48
paulson@7089
    49
Goalw [o_def] "f o (g o h) = f o g o h";
paulson@7089
    50
by (rtac ext 1);
paulson@7089
    51
by (rtac refl 1);
paulson@7089
    52
qed "o_assoc";
oheimb@5306
    53
paulson@7089
    54
Goalw [id_def] "id o g = g";
paulson@7089
    55
by (rtac ext 1);
paulson@7089
    56
by (Simp_tac 1);
paulson@7089
    57
qed "id_o";
nipkow@5608
    58
Addsimps [id_o];
oheimb@5306
    59
paulson@7089
    60
Goalw [id_def] "f o id = f";
paulson@7089
    61
by (rtac ext 1);
paulson@7089
    62
by (Simp_tac 1);
paulson@7089
    63
qed "o_id";
nipkow@5608
    64
Addsimps [o_id];
oheimb@5306
    65
oheimb@5306
    66
Goalw [o_def] "(f o g)``r = f``(g``r)";
oheimb@5306
    67
by (Blast_tac 1);
oheimb@5306
    68
qed "image_compose";
oheimb@5306
    69
paulson@7536
    70
Goal "f``g``A = (UN x:A. {f (g x)})";
paulson@7536
    71
by (Blast_tac 1);
paulson@7536
    72
qed "image_image_eq_UN";
paulson@7536
    73
paulson@5852
    74
Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
paulson@5852
    75
by (Blast_tac 1);
paulson@6829
    76
qed "UN_o";
paulson@5852
    77
berghofe@7014
    78
(** lemma for proving injectivity of representation functions for **)
berghofe@7014
    79
(** datatypes involving function types                            **)
berghofe@7014
    80
berghofe@7014
    81
Goalw [o_def]
paulson@7089
    82
  "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
paulson@7089
    83
by (rtac ext 1);
paulson@7089
    84
by (etac allE 1);
paulson@7089
    85
by (etac allE 1);
paulson@7089
    86
by (etac mp 1);
paulson@7089
    87
by (etac fun_cong 1);
berghofe@7014
    88
qed "inj_fun_lemma";
berghofe@7014
    89
oheimb@5306
    90
oheimb@5306
    91
section "inj";
paulson@6171
    92
(**NB: inj now just translates to inj_on**)
oheimb@5306
    93
clasohm@923
    94
(*** inj(f): f is a one-to-one function ***)
clasohm@923
    95
paulson@6171
    96
(*for Tools/datatype_rep_proofs*)
paulson@6171
    97
val [prem] = Goalw [inj_on_def]
paulson@6171
    98
    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)";
paulson@6171
    99
by (blast_tac (claset() addIs [prem RS spec RS mp]) 1);
paulson@6171
   100
qed "datatype_injI";
clasohm@923
   101
paulson@6171
   102
Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
paulson@5316
   103
by (Blast_tac 1);
clasohm@923
   104
qed "injD";
clasohm@923
   105
clasohm@923
   106
(*Useful with the simplifier*)
paulson@5316
   107
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
clasohm@923
   108
by (rtac iffI 1);
paulson@5316
   109
by (etac arg_cong 2);
paulson@5316
   110
by (etac injD 1);
paulson@5318
   111
by (assume_tac 1);
clasohm@923
   112
qed "inj_eq";
clasohm@923
   113
paulson@5316
   114
Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
paulson@5316
   115
by (etac injD 1);
clasohm@923
   116
by (rtac selectI 1);
clasohm@923
   117
by (rtac refl 1);
clasohm@923
   118
qed "inj_select";
clasohm@923
   119
clasohm@923
   120
(*A one-to-one function has an inverse (given using select).*)
paulson@5316
   121
Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
paulson@5316
   122
by (etac inj_select 1);
nipkow@2912
   123
qed "inv_f_f";
paulson@7338
   124
Addsimps [inv_f_f];
clasohm@923
   125
paulson@7338
   126
Goal "[| inj(f);  f x = y |] ==> inv f y = x";
paulson@7338
   127
by (etac subst 1);
paulson@7338
   128
by (etac inv_f_f 1);
paulson@7338
   129
qed "inv_f_eq";
paulson@6235
   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";
paulson@6171
   150
val 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";
paulson@6171
   158
val inj_inverseI = inj_on_inverseI;   (*for compatibility*)
clasohm@923
   159
paulson@5316
   160
Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
paulson@5316
   161
by (Blast_tac 1);
nipkow@4830
   162
qed "inj_onD";
clasohm@923
   163
paulson@5143
   164
Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
nipkow@4830
   165
by (blast_tac (claset() addSDs [inj_onD]) 1);
nipkow@4830
   166
qed "inj_on_iff";
clasohm@923
   167
paulson@5316
   168
Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
paulson@5316
   169
by (Blast_tac 1);
nipkow@4830
   170
qed "inj_on_contraD";
clasohm@923
   171
paulson@5316
   172
Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
paulson@3341
   173
by (Blast_tac 1);
nipkow@4830
   174
qed "subset_inj_on";
paulson@3341
   175
clasohm@923
   176
paulson@6235
   177
(** surj **)
paulson@6235
   178
paulson@6267
   179
val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
paulson@6267
   180
by (blast_tac (claset() addIs [prem RS sym]) 1);
paulson@6235
   181
qed "surjI";
paulson@6235
   182
paulson@6235
   183
Goalw [surj_def] "surj f ==> range f = UNIV";
paulson@6235
   184
by Auto_tac;
paulson@6235
   185
qed "surj_range";
paulson@6235
   186
paulson@6267
   187
Goalw [surj_def] "surj f ==> EX x. y = f x";
paulson@6267
   188
by (Blast_tac 1);
paulson@6267
   189
qed "surjD";
paulson@6267
   190
paulson@6235
   191
paulson@7374
   192
(** Bijections **)
paulson@7374
   193
paulson@7374
   194
Goalw [bij_def] "[| inj f; surj f |] ==> bij f";
paulson@7374
   195
by (Blast_tac 1);
paulson@7374
   196
qed "bijI";
paulson@7374
   197
paulson@7374
   198
Goalw [bij_def] "bij f ==> inj f";
paulson@7374
   199
by (Blast_tac 1);
paulson@7374
   200
qed "bij_is_inj";
paulson@7374
   201
paulson@7374
   202
Goalw [bij_def] "bij f ==> surj f";
paulson@7374
   203
by (Blast_tac 1);
paulson@7374
   204
qed "bij_is_surj";
paulson@7374
   205
paulson@7374
   206
paulson@6171
   207
(*** Lemmas about injective functions and inv ***)
clasohm@923
   208
nipkow@7051
   209
Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
paulson@6171
   210
by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
paulson@6171
   211
qed "comp_inj_on";
clasohm@923
   212
paulson@5316
   213
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
paulson@5316
   214
by (fast_tac (claset() addIs [selectI]) 1);
nipkow@2912
   215
qed "f_inv_f";
clasohm@923
   216
paulson@6235
   217
Goal "surj f ==> f(inv f y) = y";
paulson@6235
   218
by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
paulson@6235
   219
qed "surj_f_inv_f";
paulson@6235
   220
paulson@6171
   221
Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
nipkow@2912
   222
by (rtac (arg_cong RS box_equals) 1);
paulson@5316
   223
by (REPEAT (ares_tac [f_inv_f] 1));
nipkow@2912
   224
qed "inv_injective";
nipkow@2912
   225
paulson@6235
   226
Goal "A <= range(f) ==> inj_on (inv f) A";
nipkow@4830
   227
by (fast_tac (claset() addIs [inj_onI] 
paulson@6235
   228
                       addEs [inv_injective, injD]) 1);
nipkow@4830
   229
qed "inj_on_inv";
clasohm@923
   230
paulson@6235
   231
Goal "surj f ==> inj (inv f)";
paulson@6235
   232
by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
paulson@6235
   233
qed "surj_imp_inj_inv";
paulson@6235
   234
paulson@7514
   235
(** We seem to need both the id-forms and the (%x. x) forms; the latter can
paulson@7514
   236
    arise by rewriting, while id may be used explicitly. **)
paulson@7514
   237
paulson@7514
   238
Goal "(%x. x) `` Y = Y";
paulson@7514
   239
by (Blast_tac 1);
paulson@7514
   240
qed "image_ident";
paulson@7514
   241
paulson@7514
   242
Goalw [id_def] "id `` Y = Y";
paulson@7514
   243
by (Blast_tac 1);
paulson@7514
   244
qed "image_id";
paulson@7514
   245
Addsimps [image_ident, image_id];
paulson@7514
   246
paulson@7514
   247
Goal "(%x. x) -`` Y = Y";
paulson@7514
   248
by (Blast_tac 1);
paulson@7514
   249
qed "vimage_ident";
paulson@7514
   250
paulson@7514
   251
Goalw [id_def] "id -`` A = A";
paulson@7514
   252
by Auto_tac;
paulson@7514
   253
qed "vimage_id";
paulson@7514
   254
Addsimps [vimage_ident, vimage_id];
paulson@7514
   255
paulson@6290
   256
Goal "f``(A Int B) <= f``A Int f``B";
paulson@6290
   257
by (Blast_tac 1);
paulson@6290
   258
qed "image_Int_subset";
paulson@6290
   259
paulson@6290
   260
Goal "f``A - f``B <= f``(A - B)";
paulson@6290
   261
by (Blast_tac 1);
paulson@6290
   262
qed "image_diff_subset";
paulson@6290
   263
wenzelm@5069
   264
Goalw [inj_on_def]
paulson@5148
   265
   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
paulson@4059
   266
by (Blast_tac 1);
nipkow@4830
   267
qed "inj_on_image_Int";
paulson@4059
   268
wenzelm@5069
   269
Goalw [inj_on_def]
paulson@5148
   270
   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
paulson@4059
   271
by (Blast_tac 1);
nipkow@4830
   272
qed "inj_on_image_set_diff";
paulson@4059
   273
paulson@6171
   274
Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B";
paulson@4059
   275
by (Blast_tac 1);
paulson@4059
   276
qed "image_Int";
paulson@4059
   277
paulson@6171
   278
Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B";
paulson@4059
   279
by (Blast_tac 1);
paulson@4059
   280
qed "image_set_diff";
paulson@4059
   281
paulson@6235
   282
Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";
paulson@6235
   283
by Auto_tac;
paulson@6235
   284
qed "inv_image_comp";
paulson@5847
   285
paulson@6301
   286
Goal "inj f ==> (f a : f``A) = (a : A)";
paulson@6301
   287
by (blast_tac (claset() addDs [injD]) 1);
paulson@6301
   288
qed "inj_image_mem_iff";
paulson@6301
   289
paulson@6301
   290
Goal "inj f ==> (f``A = f``B) = (A = B)";
paulson@6301
   291
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
paulson@6301
   292
qed "inj_image_eq_iff";
paulson@6301
   293
paulson@6829
   294
Goal  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
paulson@6829
   295
by (Blast_tac 1);
paulson@6829
   296
qed "image_UN";
paulson@6829
   297
paulson@6829
   298
(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
paulson@6829
   299
Goalw [inj_on_def]
paulson@6829
   300
   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |] \
paulson@6829
   301
\   ==> f `` (INTER A B) = (INT x:A. f `` B x)";
paulson@6829
   302
by (Blast_tac 1);
paulson@6829
   303
qed "image_INT";
paulson@6829
   304
wenzelm@4089
   305
val set_cs = claset() delrules [equalityI];
oheimb@5305
   306
oheimb@5305
   307
oheimb@5305
   308
section "fun_upd";
oheimb@5305
   309
oheimb@5305
   310
Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
oheimb@5305
   311
by Safe_tac;
oheimb@5305
   312
by (etac subst 1);
oheimb@5305
   313
by (rtac ext 2);
oheimb@5305
   314
by Auto_tac;
oheimb@5305
   315
qed "fun_upd_idem_iff";
oheimb@5305
   316
oheimb@5305
   317
(* f x = y ==> f(x:=y) = f *)
oheimb@5305
   318
bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
oheimb@5305
   319
oheimb@5305
   320
(* f(x := f x) = f *)
oheimb@5305
   321
AddIffs [refl RS fun_upd_idem];
oheimb@5305
   322
oheimb@5305
   323
Goal "(f(x:=y))z = (if z=x then y else f z)";
oheimb@5305
   324
by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
oheimb@5305
   325
qed "fun_upd_apply";
oheimb@5305
   326
Addsimps [fun_upd_apply];
oheimb@5305
   327
paulson@7445
   328
(*fun_upd_apply supersedes these two*)
paulson@7089
   329
Goal "(f(x:=y)) x = y";
paulson@7089
   330
by (Simp_tac 1);
paulson@7089
   331
qed "fun_upd_same";
paulson@7089
   332
paulson@7089
   333
Goal "z~=x ==> (f(x:=y)) z = f z";
paulson@7089
   334
by (Asm_simp_tac 1);
paulson@7089
   335
qed "fun_upd_other";
paulson@7089
   336
paulson@7445
   337
Goal "f(x:=y,x:=z) = f(x:=z)";
paulson@7445
   338
by (rtac ext 1);
paulson@7445
   339
by (Simp_tac 1);
paulson@7445
   340
qed "fun_upd_upd";
paulson@7445
   341
Addsimps [fun_upd_upd];
oheimb@5305
   342
oheimb@5305
   343
Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
oheimb@5305
   344
by (rtac ext 1);
paulson@7089
   345
by Auto_tac;
oheimb@5305
   346
qed "fun_upd_twist";
paulson@5852
   347
paulson@5852
   348
paulson@5852
   349
(*** -> and Pi, by Florian Kammueller and LCP ***)
paulson@5852
   350
paulson@5852
   351
val prems = Goalw [Pi_def]
paulson@5852
   352
"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
paulson@5852
   353
\    ==> f: Pi A B";
paulson@5852
   354
by (auto_tac (claset(), simpset() addsimps prems));
paulson@5852
   355
qed "Pi_I";
paulson@5852
   356
paulson@5852
   357
val prems = Goal 
paulson@5852
   358
"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
paulson@5852
   359
by (blast_tac (claset() addIs Pi_I::prems) 1);
paulson@5852
   360
qed "funcsetI";
paulson@5852
   361
paulson@5852
   362
Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
paulson@5852
   363
by Auto_tac;
paulson@5852
   364
qed "Pi_mem";
paulson@5852
   365
paulson@5852
   366
Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
paulson@5852
   367
by Auto_tac;
paulson@5852
   368
qed "funcset_mem";
paulson@5852
   369
paulson@5852
   370
Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
paulson@5852
   371
by Auto_tac;
paulson@5852
   372
qed "apply_arb";
paulson@5852
   373
paulson@5852
   374
Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
paulson@5852
   375
by (rtac ext 1);
paulson@5852
   376
by Auto_tac;
paulson@5852
   377
val Pi_extensionality = ballI RSN (3, result());
paulson@5852
   378
paulson@5852
   379
(*** compose ***)
paulson@5852
   380
paulson@5852
   381
Goalw [Pi_def, compose_def, restrict_def]
paulson@5852
   382
     "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
paulson@5852
   383
by Auto_tac;
paulson@5852
   384
qed "funcset_compose";
paulson@5852
   385
paulson@5852
   386
Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
paulson@5852
   387
\     ==> compose A h (compose A g f) = compose A (compose B h g) f";
paulson@5852
   388
by (res_inst_tac [("A","A")] Pi_extensionality 1);
paulson@5852
   389
by (blast_tac (claset() addIs [funcset_compose]) 1);
paulson@5852
   390
by (blast_tac (claset() addIs [funcset_compose]) 1);
paulson@5852
   391
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
paulson@5852
   392
by Auto_tac;
paulson@5852
   393
qed "compose_assoc";
paulson@5852
   394
paulson@5852
   395
Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))";
paulson@5852
   396
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
paulson@5852
   397
qed "compose_eq";
paulson@5852
   398
paulson@5852
   399
Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
paulson@5852
   400
\     ==> compose A g f `` A = C";
paulson@5852
   401
by (auto_tac (claset(),
paulson@5852
   402
	      simpset() addsimps [image_def, compose_eq]));
paulson@5852
   403
qed "surj_compose";
paulson@5852
   404
paulson@5852
   405
paulson@5852
   406
Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
paulson@5852
   407
\     ==> inj_on (compose A g f) A";
paulson@5852
   408
by (auto_tac (claset(),
paulson@5852
   409
	      simpset() addsimps [inj_on_def, compose_eq]));
paulson@5852
   410
qed "inj_on_compose";
paulson@5852
   411
paulson@5852
   412
paulson@5852
   413
(*** restrict / lam ***)
paulson@5852
   414
Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A funcset B";
paulson@5852
   415
by (auto_tac (claset(),
paulson@5852
   416
	      simpset() addsimps [restrict_def, Pi_def]));
paulson@5852
   417
qed "restrict_in_funcset";
paulson@5852
   418
paulson@5852
   419
val prems = Goalw [restrict_def, Pi_def]
paulson@5852
   420
     "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
paulson@5852
   421
by (asm_simp_tac (simpset() addsimps prems) 1);
paulson@5852
   422
qed "restrictI";
paulson@5852
   423
paulson@5852
   424
paulson@5852
   425
Goal "x: A ==> (lam y: A. f y) x = f x";
paulson@5852
   426
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
paulson@5852
   427
qed "restrict_apply1";
paulson@5852
   428
paulson@5852
   429
Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
paulson@5852
   430
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
paulson@5852
   431
qed "restrict_apply1_mem";
paulson@5852
   432
paulson@5852
   433
Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
paulson@5852
   434
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
paulson@5852
   435
qed "restrict_apply2";
paulson@5852
   436
paulson@5852
   437
paulson@5852
   438
val prems = Goal
paulson@5852
   439
    "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
paulson@5852
   440
by (rtac ext 1);
paulson@5852
   441
by (auto_tac (claset(),
paulson@5852
   442
	      simpset() addsimps prems@[restrict_def, Pi_def]));
paulson@5852
   443
qed "restrict_ext";
paulson@5852
   444
paulson@5852
   445
paulson@5852
   446
(*** Inverse ***)
paulson@5852
   447
paulson@5852
   448
Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
paulson@5852
   449
by (Blast_tac 1);
paulson@5852
   450
qed "surj_image";
paulson@5852
   451
paulson@5852
   452
Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
paulson@5852
   453
\                ==> (lam x: B. (Inv A f) x) : B funcset A";
paulson@5852
   454
by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
paulson@5852
   455
qed "Inv_funcset";
paulson@5852
   456
paulson@5852
   457
paulson@5852
   458
Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
paulson@5852
   459
\     ==> (lam y: B. (Inv A f) y) (f x) = x";
paulson@5852
   460
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
paulson@5852
   461
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
paulson@5852
   462
by (rtac selectI2 1);
paulson@5852
   463
by Auto_tac;
paulson@5852
   464
qed "Inv_f_f";
paulson@5852
   465
paulson@5852
   466
Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
paulson@5852
   467
\     ==> f ((lam y: B. (Inv A f y)) x) = x";
paulson@5852
   468
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
paulson@5852
   469
by (fast_tac (claset() addIs [selectI2]) 1);
paulson@5852
   470
qed "f_Inv_f";
paulson@5852
   471
paulson@5852
   472
Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
paulson@5852
   473
\     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
paulson@5852
   474
by (rtac Pi_extensionality 1);
paulson@5852
   475
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
paulson@5852
   476
by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
paulson@5852
   477
by (asm_simp_tac
paulson@5852
   478
    (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
paulson@5852
   479
qed "compose_Inv_id";
paulson@5852
   480
paulson@5852
   481
paulson@5852
   482
(*** Pi and Applyall ***)
paulson@5852
   483
paulson@5852
   484
Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
paulson@5852
   485
by Auto_tac;
paulson@5852
   486
qed "Pi_eq_empty";
paulson@5852
   487
paulson@5852
   488
Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
paulson@5852
   489
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
paulson@5852
   490
qed "Pi_total1";
paulson@5852
   491
paulson@5852
   492
Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
paulson@5852
   493
by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
paulson@5852
   494
by (rename_tac "g z" 1);
paulson@5852
   495
by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
paulson@5852
   496
by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
paulson@5852
   497
qed "Applyall_beta";
paulson@5852
   498
paulson@5865
   499
Goal "Pi {} B = { (%x. @ y. True) }";
paulson@5865
   500
by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
paulson@5865
   501
qed "Pi_empty";
paulson@5852
   502
paulson@5865
   503
val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
paulson@5865
   504
by (auto_tac (claset(),
paulson@5865
   505
	      simpset() addsimps [impOfSubs major]));
paulson@5865
   506
qed "Pi_mono";