src/HOL/Fun.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6301 08245f5a436d
child 6829 50459a995aa3
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
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
wenzelm@5069
    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
nipkow@5608
    36
qed_goalw "id_apply" thy [id_def] "id x = x" (K [rtac refl 1]);
nipkow@5608
    37
Addsimps [id_apply];
oheimb@5441
    38
oheimb@5441
    39
oheimb@5306
    40
section "o";
oheimb@5306
    41
oheimb@5306
    42
qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
oheimb@5306
    43
 (K [rtac refl 1]);
oheimb@5306
    44
Addsimps [o_apply];
oheimb@5306
    45
oheimb@5306
    46
qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
oheimb@5306
    47
  (K [rtac ext 1, rtac refl 1]);
oheimb@5306
    48
nipkow@5608
    49
qed_goalw "id_o" thy [id_def] "id o g = g"
oheimb@5306
    50
 (K [rtac ext 1, Simp_tac 1]);
nipkow@5608
    51
Addsimps [id_o];
oheimb@5306
    52
nipkow@5608
    53
qed_goalw "o_id" thy [id_def] "f o id = f"
oheimb@5306
    54
 (K [rtac ext 1, Simp_tac 1]);
nipkow@5608
    55
Addsimps [o_id];
oheimb@5306
    56
oheimb@5306
    57
Goalw [o_def] "(f o g)``r = f``(g``r)";
oheimb@5306
    58
by (Blast_tac 1);
oheimb@5306
    59
qed "image_compose";
oheimb@5306
    60
paulson@5852
    61
Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
paulson@5852
    62
by (Blast_tac 1);
paulson@5852
    63
qed "UNION_o";
paulson@5852
    64
oheimb@5306
    65
oheimb@5306
    66
section "inj";
paulson@6171
    67
(**NB: inj now just translates to inj_on**)
oheimb@5306
    68
clasohm@923
    69
(*** inj(f): f is a one-to-one function ***)
clasohm@923
    70
paulson@6171
    71
(*for Tools/datatype_rep_proofs*)
paulson@6171
    72
val [prem] = Goalw [inj_on_def]
paulson@6171
    73
    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)";
paulson@6171
    74
by (blast_tac (claset() addIs [prem RS spec RS mp]) 1);
paulson@6171
    75
qed "datatype_injI";
clasohm@923
    76
paulson@6171
    77
Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
paulson@5316
    78
by (Blast_tac 1);
clasohm@923
    79
qed "injD";
clasohm@923
    80
clasohm@923
    81
(*Useful with the simplifier*)
paulson@5316
    82
Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
clasohm@923
    83
by (rtac iffI 1);
paulson@5316
    84
by (etac arg_cong 2);
paulson@5316
    85
by (etac injD 1);
paulson@5318
    86
by (assume_tac 1);
clasohm@923
    87
qed "inj_eq";
clasohm@923
    88
paulson@5316
    89
Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
paulson@5316
    90
by (etac injD 1);
clasohm@923
    91
by (rtac selectI 1);
clasohm@923
    92
by (rtac refl 1);
clasohm@923
    93
qed "inj_select";
clasohm@923
    94
clasohm@923
    95
(*A one-to-one function has an inverse (given using select).*)
paulson@5316
    96
Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
paulson@5316
    97
by (etac inj_select 1);
nipkow@2912
    98
qed "inv_f_f";
clasohm@923
    99
paulson@6235
   100
Addsimps [inv_f_f];
paulson@6235
   101
clasohm@923
   102
(* Useful??? *)
paulson@5316
   103
val [oneone,minor] = Goal
nipkow@2912
   104
    "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
nipkow@2912
   105
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
clasohm@923
   106
by (rtac (rangeI RS minor) 1);
clasohm@923
   107
qed "inj_transfer";
clasohm@923
   108
clasohm@923
   109
nipkow@4830
   110
(*** inj_on f A: f is one-to-one over A ***)
clasohm@923
   111
paulson@5316
   112
val prems = Goalw [inj_on_def]
nipkow@4830
   113
    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
wenzelm@4089
   114
by (blast_tac (claset() addIs prems) 1);
nipkow@4830
   115
qed "inj_onI";
paulson@6171
   116
val injI = inj_onI;                  (*for compatibility*)
clasohm@923
   117
paulson@5316
   118
val [major] = Goal 
nipkow@4830
   119
    "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
nipkow@4830
   120
by (rtac inj_onI 1);
clasohm@923
   121
by (etac (apply_inverse RS trans) 1);
clasohm@923
   122
by (REPEAT (eresolve_tac [asm_rl,major] 1));
nipkow@4830
   123
qed "inj_on_inverseI";
paulson@6171
   124
val inj_inverseI = inj_on_inverseI;   (*for compatibility*)
clasohm@923
   125
paulson@5316
   126
Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
paulson@5316
   127
by (Blast_tac 1);
nipkow@4830
   128
qed "inj_onD";
clasohm@923
   129
paulson@5143
   130
Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
nipkow@4830
   131
by (blast_tac (claset() addSDs [inj_onD]) 1);
nipkow@4830
   132
qed "inj_on_iff";
clasohm@923
   133
paulson@5316
   134
Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
paulson@5316
   135
by (Blast_tac 1);
nipkow@4830
   136
qed "inj_on_contraD";
clasohm@923
   137
paulson@5316
   138
Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
paulson@3341
   139
by (Blast_tac 1);
nipkow@4830
   140
qed "subset_inj_on";
paulson@3341
   141
clasohm@923
   142
paulson@6235
   143
(** surj **)
paulson@6235
   144
paulson@6267
   145
val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
paulson@6267
   146
by (blast_tac (claset() addIs [prem RS sym]) 1);
paulson@6235
   147
qed "surjI";
paulson@6235
   148
paulson@6235
   149
Goalw [surj_def] "surj f ==> range f = UNIV";
paulson@6235
   150
by Auto_tac;
paulson@6235
   151
qed "surj_range";
paulson@6235
   152
paulson@6267
   153
Goalw [surj_def] "surj f ==> EX x. y = f x";
paulson@6267
   154
by (Blast_tac 1);
paulson@6267
   155
qed "surjD";
paulson@6267
   156
paulson@6235
   157
paulson@6171
   158
(*** Lemmas about injective functions and inv ***)
clasohm@923
   159
paulson@6171
   160
Goalw [o_def] "[| inj_on f A;  inj_on g (range f) |] ==> inj_on (g o f) A";
paulson@6171
   161
by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
paulson@6171
   162
qed "comp_inj_on";
clasohm@923
   163
paulson@5316
   164
Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
paulson@5316
   165
by (fast_tac (claset() addIs [selectI]) 1);
nipkow@2912
   166
qed "f_inv_f";
clasohm@923
   167
paulson@6235
   168
Goal "surj f ==> f(inv f y) = y";
paulson@6235
   169
by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
paulson@6235
   170
qed "surj_f_inv_f";
paulson@6235
   171
paulson@6171
   172
Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
nipkow@2912
   173
by (rtac (arg_cong RS box_equals) 1);
paulson@5316
   174
by (REPEAT (ares_tac [f_inv_f] 1));
nipkow@2912
   175
qed "inv_injective";
nipkow@2912
   176
paulson@6235
   177
Goal "A <= range(f) ==> inj_on (inv f) A";
nipkow@4830
   178
by (fast_tac (claset() addIs [inj_onI] 
paulson@6235
   179
                       addEs [inv_injective, injD]) 1);
nipkow@4830
   180
qed "inj_on_inv";
clasohm@923
   181
paulson@6235
   182
Goal "surj f ==> inj (inv f)";
paulson@6235
   183
by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
paulson@6235
   184
qed "surj_imp_inj_inv";
paulson@6235
   185
paulson@6290
   186
Goal "f``(A Int B) <= f``A Int f``B";
paulson@6290
   187
by (Blast_tac 1);
paulson@6290
   188
qed "image_Int_subset";
paulson@6290
   189
paulson@6290
   190
Goal "f``A - f``B <= f``(A - B)";
paulson@6290
   191
by (Blast_tac 1);
paulson@6290
   192
qed "image_diff_subset";
paulson@6290
   193
wenzelm@5069
   194
Goalw [inj_on_def]
paulson@5148
   195
   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
paulson@4059
   196
by (Blast_tac 1);
nipkow@4830
   197
qed "inj_on_image_Int";
paulson@4059
   198
wenzelm@5069
   199
Goalw [inj_on_def]
paulson@5148
   200
   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
paulson@4059
   201
by (Blast_tac 1);
nipkow@4830
   202
qed "inj_on_image_set_diff";
paulson@4059
   203
paulson@6171
   204
Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B";
paulson@4059
   205
by (Blast_tac 1);
paulson@4059
   206
qed "image_Int";
paulson@4059
   207
paulson@6171
   208
Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B";
paulson@4059
   209
by (Blast_tac 1);
paulson@4059
   210
qed "image_set_diff";
paulson@4059
   211
paulson@6235
   212
Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";
paulson@6235
   213
by Auto_tac;
paulson@6235
   214
qed "inv_image_comp";
paulson@5847
   215
paulson@6301
   216
Goal "inj f ==> (f a : f``A) = (a : A)";
paulson@6301
   217
by (blast_tac (claset() addDs [injD]) 1);
paulson@6301
   218
qed "inj_image_mem_iff";
paulson@6301
   219
paulson@6301
   220
Goal "inj f ==> (f``A = f``B) = (A = B)";
paulson@6301
   221
by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
paulson@6301
   222
qed "inj_image_eq_iff";
paulson@6301
   223
wenzelm@4089
   224
val set_cs = claset() delrules [equalityI];
oheimb@5305
   225
oheimb@5305
   226
oheimb@5305
   227
section "fun_upd";
oheimb@5305
   228
oheimb@5305
   229
Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
oheimb@5305
   230
by Safe_tac;
oheimb@5305
   231
by (etac subst 1);
oheimb@5305
   232
by (rtac ext 2);
oheimb@5305
   233
by Auto_tac;
oheimb@5305
   234
qed "fun_upd_idem_iff";
oheimb@5305
   235
oheimb@5305
   236
(* f x = y ==> f(x:=y) = f *)
oheimb@5305
   237
bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
oheimb@5305
   238
oheimb@5305
   239
(* f(x := f x) = f *)
oheimb@5305
   240
AddIffs [refl RS fun_upd_idem];
oheimb@5305
   241
oheimb@5305
   242
Goal "(f(x:=y))z = (if z=x then y else f z)";
oheimb@5305
   243
by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
oheimb@5305
   244
qed "fun_upd_apply";
oheimb@5305
   245
Addsimps [fun_upd_apply];
oheimb@5305
   246
oheimb@5305
   247
qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 
oheimb@5305
   248
	(K [Simp_tac 1]);
oheimb@5306
   249
qed_goal "fun_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
oheimb@5305
   250
	(K [Asm_simp_tac 1]);
oheimb@5305
   251
(*Addsimps [fun_upd_same, fun_upd_other];*)
oheimb@5305
   252
oheimb@5305
   253
Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
oheimb@5305
   254
by (rtac ext 1);
oheimb@5305
   255
by (Auto_tac);
oheimb@5305
   256
qed "fun_upd_twist";
paulson@5852
   257
paulson@5852
   258
paulson@5852
   259
(*** -> and Pi, by Florian Kammueller and LCP ***)
paulson@5852
   260
paulson@5852
   261
val prems = Goalw [Pi_def]
paulson@5852
   262
"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
paulson@5852
   263
\    ==> f: Pi A B";
paulson@5852
   264
by (auto_tac (claset(), simpset() addsimps prems));
paulson@5852
   265
qed "Pi_I";
paulson@5852
   266
paulson@5852
   267
val prems = Goal 
paulson@5852
   268
"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
paulson@5852
   269
by (blast_tac (claset() addIs Pi_I::prems) 1);
paulson@5852
   270
qed "funcsetI";
paulson@5852
   271
paulson@5852
   272
Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
paulson@5852
   273
by Auto_tac;
paulson@5852
   274
qed "Pi_mem";
paulson@5852
   275
paulson@5852
   276
Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
paulson@5852
   277
by Auto_tac;
paulson@5852
   278
qed "funcset_mem";
paulson@5852
   279
paulson@5852
   280
Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
paulson@5852
   281
by Auto_tac;
paulson@5852
   282
qed "apply_arb";
paulson@5852
   283
paulson@5852
   284
Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
paulson@5852
   285
by (rtac ext 1);
paulson@5852
   286
by Auto_tac;
paulson@5852
   287
val Pi_extensionality = ballI RSN (3, result());
paulson@5852
   288
paulson@5852
   289
(*** compose ***)
paulson@5852
   290
paulson@5852
   291
Goalw [Pi_def, compose_def, restrict_def]
paulson@5852
   292
     "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
paulson@5852
   293
by Auto_tac;
paulson@5852
   294
qed "funcset_compose";
paulson@5852
   295
paulson@5852
   296
Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
paulson@5852
   297
\     ==> compose A h (compose A g f) = compose A (compose B h g) f";
paulson@5852
   298
by (res_inst_tac [("A","A")] Pi_extensionality 1);
paulson@5852
   299
by (blast_tac (claset() addIs [funcset_compose]) 1);
paulson@5852
   300
by (blast_tac (claset() addIs [funcset_compose]) 1);
paulson@5852
   301
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
paulson@5852
   302
by Auto_tac;
paulson@5852
   303
qed "compose_assoc";
paulson@5852
   304
paulson@5852
   305
Goal "[| f: A funcset B; g: B funcset C; x: A |]==> compose A g f x = g(f(x))";
paulson@5852
   306
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
paulson@5852
   307
qed "compose_eq";
paulson@5852
   308
paulson@5852
   309
Goal "[| f : A funcset B; f `` A = B; g: B funcset C; g `` B = C |]\
paulson@5852
   310
\     ==> compose A g f `` A = C";
paulson@5852
   311
by (auto_tac (claset(),
paulson@5852
   312
	      simpset() addsimps [image_def, compose_eq]));
paulson@5852
   313
qed "surj_compose";
paulson@5852
   314
paulson@5852
   315
paulson@5852
   316
Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
paulson@5852
   317
\     ==> inj_on (compose A g f) A";
paulson@5852
   318
by (auto_tac (claset(),
paulson@5852
   319
	      simpset() addsimps [inj_on_def, compose_eq]));
paulson@5852
   320
qed "inj_on_compose";
paulson@5852
   321
paulson@5852
   322
paulson@5852
   323
(*** restrict / lam ***)
paulson@5852
   324
Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A funcset B";
paulson@5852
   325
by (auto_tac (claset(),
paulson@5852
   326
	      simpset() addsimps [restrict_def, Pi_def]));
paulson@5852
   327
qed "restrict_in_funcset";
paulson@5852
   328
paulson@5852
   329
val prems = Goalw [restrict_def, Pi_def]
paulson@5852
   330
     "(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
paulson@5852
   331
by (asm_simp_tac (simpset() addsimps prems) 1);
paulson@5852
   332
qed "restrictI";
paulson@5852
   333
paulson@5852
   334
paulson@5852
   335
Goal "x: A ==> (lam y: A. f y) x = f x";
paulson@5852
   336
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
paulson@5852
   337
qed "restrict_apply1";
paulson@5852
   338
paulson@5852
   339
Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
paulson@5852
   340
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
paulson@5852
   341
qed "restrict_apply1_mem";
paulson@5852
   342
paulson@5852
   343
Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
paulson@5852
   344
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
paulson@5852
   345
qed "restrict_apply2";
paulson@5852
   346
paulson@5852
   347
paulson@5852
   348
val prems = Goal
paulson@5852
   349
    "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
paulson@5852
   350
by (rtac ext 1);
paulson@5852
   351
by (auto_tac (claset(),
paulson@5852
   352
	      simpset() addsimps prems@[restrict_def, Pi_def]));
paulson@5852
   353
qed "restrict_ext";
paulson@5852
   354
paulson@5852
   355
paulson@5852
   356
(*** Inverse ***)
paulson@5852
   357
paulson@5852
   358
Goal "[|f `` A = B;  x: B |] ==> ? y: A. f y = x";
paulson@5852
   359
by (Blast_tac 1);
paulson@5852
   360
qed "surj_image";
paulson@5852
   361
paulson@5852
   362
Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
paulson@5852
   363
\                ==> (lam x: B. (Inv A f) x) : B funcset A";
paulson@5852
   364
by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
paulson@5852
   365
qed "Inv_funcset";
paulson@5852
   366
paulson@5852
   367
paulson@5852
   368
Goal "[| f: A funcset B;  inj_on f A;  f `` A = B;  x: A |] \
paulson@5852
   369
\     ==> (lam y: B. (Inv A f) y) (f x) = x";
paulson@5852
   370
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
paulson@5852
   371
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
paulson@5852
   372
by (rtac selectI2 1);
paulson@5852
   373
by Auto_tac;
paulson@5852
   374
qed "Inv_f_f";
paulson@5852
   375
paulson@5852
   376
Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
paulson@5852
   377
\     ==> f ((lam y: B. (Inv A f y)) x) = x";
paulson@5852
   378
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
paulson@5852
   379
by (fast_tac (claset() addIs [selectI2]) 1);
paulson@5852
   380
qed "f_Inv_f";
paulson@5852
   381
paulson@5852
   382
Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
paulson@5852
   383
\     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
paulson@5852
   384
by (rtac Pi_extensionality 1);
paulson@5852
   385
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
paulson@5852
   386
by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
paulson@5852
   387
by (asm_simp_tac
paulson@5852
   388
    (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
paulson@5852
   389
qed "compose_Inv_id";
paulson@5852
   390
paulson@5852
   391
paulson@5852
   392
(*** Pi and Applyall ***)
paulson@5852
   393
paulson@5852
   394
Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
paulson@5852
   395
by Auto_tac;
paulson@5852
   396
qed "Pi_eq_empty";
paulson@5852
   397
paulson@5852
   398
Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
paulson@5852
   399
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
paulson@5852
   400
qed "Pi_total1";
paulson@5852
   401
paulson@5852
   402
Goal "[| a : A; Pi A B ~= {} |] ==> Applyall (Pi A B) a = B a";
paulson@5852
   403
by (auto_tac (claset(), simpset() addsimps [Applyall_def, Pi_def]));
paulson@5852
   404
by (rename_tac "g z" 1);
paulson@5852
   405
by (res_inst_tac [("x","%y. if  (y = a) then z else g y")] exI 1);
paulson@5852
   406
by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
paulson@5852
   407
qed "Applyall_beta";
paulson@5852
   408
paulson@5865
   409
Goal "Pi {} B = { (%x. @ y. True) }";
paulson@5865
   410
by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
paulson@5865
   411
qed "Pi_empty";
paulson@5852
   412
paulson@5865
   413
val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
paulson@5865
   414
by (auto_tac (claset(),
paulson@5865
   415
	      simpset() addsimps [impOfSubs major]));
paulson@5865
   416
qed "Pi_mono";