src/HOL/Fun.ML
author paulson
Wed Jul 15 10:15:13 1998 +0200 (1998-07-15)
changeset 5143 b94cd208f073
parent 5069 3ea049f7979d
child 5148 74919e8f221c
permissions -rw-r--r--
Removal of leading "\!\!..." from most Goal commands
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@4656
    16
val prems = goal thy
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@4656
    25
goal HOL.thy "!!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@4656
    29
goal Set.thy "!!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
clasohm@923
    34
(*** inj(f): f is a one-to-one function ***)
clasohm@923
    35
paulson@4656
    36
val prems = goalw thy [inj_def]
clasohm@923
    37
    "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
wenzelm@4089
    38
by (blast_tac (claset() addIs prems) 1);
clasohm@923
    39
qed "injI";
clasohm@923
    40
paulson@4656
    41
val [major] = goal thy "(!!x. g(f(x)) = x) ==> inj(f)";
clasohm@923
    42
by (rtac injI 1);
clasohm@923
    43
by (etac (arg_cong RS box_equals) 1);
clasohm@923
    44
by (rtac major 1);
clasohm@923
    45
by (rtac major 1);
clasohm@923
    46
qed "inj_inverseI";
clasohm@923
    47
paulson@4656
    48
val [major,minor] = goalw thy [inj_def]
clasohm@923
    49
    "[| inj(f); f(x) = f(y) |] ==> x=y";
clasohm@923
    50
by (rtac (major RS spec RS spec RS mp) 1);
clasohm@923
    51
by (rtac minor 1);
clasohm@923
    52
qed "injD";
clasohm@923
    53
clasohm@923
    54
(*Useful with the simplifier*)
paulson@4656
    55
val [major] = goal thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
clasohm@923
    56
by (rtac iffI 1);
clasohm@923
    57
by (etac (major RS injD) 1);
clasohm@923
    58
by (etac arg_cong 1);
clasohm@923
    59
qed "inj_eq";
clasohm@923
    60
paulson@4656
    61
val [major] = goal thy "inj(f) ==> (@x. f(x)=f(y)) = y";
clasohm@923
    62
by (rtac (major RS injD) 1);
clasohm@923
    63
by (rtac selectI 1);
clasohm@923
    64
by (rtac refl 1);
clasohm@923
    65
qed "inj_select";
clasohm@923
    66
clasohm@923
    67
(*A one-to-one function has an inverse (given using select).*)
paulson@4656
    68
val [major] = goalw thy [inv_def] "inj(f) ==> inv f (f x) = x";
clasohm@923
    69
by (EVERY1 [rtac (major RS inj_select)]);
nipkow@2912
    70
qed "inv_f_f";
clasohm@923
    71
clasohm@923
    72
(* Useful??? *)
paulson@4656
    73
val [oneone,minor] = goal thy
nipkow@2912
    74
    "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
nipkow@2912
    75
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
clasohm@923
    76
by (rtac (rangeI RS minor) 1);
clasohm@923
    77
qed "inj_transfer";
clasohm@923
    78
clasohm@923
    79
nipkow@4830
    80
(*** inj_on f A: f is one-to-one over A ***)
clasohm@923
    81
nipkow@4830
    82
val prems = goalw thy [inj_on_def]
nipkow@4830
    83
    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
wenzelm@4089
    84
by (blast_tac (claset() addIs prems) 1);
nipkow@4830
    85
qed "inj_onI";
clasohm@923
    86
paulson@4656
    87
val [major] = goal thy 
nipkow@4830
    88
    "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
nipkow@4830
    89
by (rtac inj_onI 1);
clasohm@923
    90
by (etac (apply_inverse RS trans) 1);
clasohm@923
    91
by (REPEAT (eresolve_tac [asm_rl,major] 1));
nipkow@4830
    92
qed "inj_on_inverseI";
clasohm@923
    93
nipkow@4830
    94
val major::prems = goalw thy [inj_on_def]
nipkow@4830
    95
    "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
clasohm@923
    96
by (rtac (major RS bspec RS bspec RS mp) 1);
clasohm@923
    97
by (REPEAT (resolve_tac prems 1));
nipkow@4830
    98
qed "inj_onD";
clasohm@923
    99
paulson@5143
   100
Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
nipkow@4830
   101
by (blast_tac (claset() addSDs [inj_onD]) 1);
nipkow@4830
   102
qed "inj_on_iff";
clasohm@923
   103
paulson@4656
   104
val major::prems = goal thy
nipkow@4830
   105
    "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
clasohm@923
   106
by (rtac contrapos 1);
nipkow@4830
   107
by (etac (major RS inj_onD) 2);
clasohm@923
   108
by (REPEAT (resolve_tac prems 1));
nipkow@4830
   109
qed "inj_on_contraD";
clasohm@923
   110
wenzelm@5069
   111
Goalw [inj_on_def]
nipkow@4830
   112
    "!!A B. [| A<=B; inj_on f B |] ==> inj_on f A";
paulson@3341
   113
by (Blast_tac 1);
nipkow@4830
   114
qed "subset_inj_on";
paulson@3341
   115
clasohm@923
   116
clasohm@923
   117
(*** Lemmas about inj ***)
clasohm@923
   118
wenzelm@5069
   119
Goalw [o_def]
nipkow@4830
   120
    "!!f g. [| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
nipkow@4830
   121
by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
clasohm@923
   122
qed "comp_inj";
clasohm@923
   123
nipkow@4830
   124
val [prem] = goal thy "inj(f) ==> inj_on f A";
nipkow@4830
   125
by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1);
clasohm@923
   126
qed "inj_imp";
clasohm@923
   127
paulson@4656
   128
val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y";
clasohm@923
   129
by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
nipkow@2912
   130
qed "f_inv_f";
clasohm@923
   131
paulson@4656
   132
val prems = goal thy
nipkow@2912
   133
    "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
nipkow@2912
   134
by (rtac (arg_cong RS box_equals) 1);
nipkow@2912
   135
by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
nipkow@2912
   136
qed "inv_injective";
nipkow@2912
   137
paulson@5143
   138
Goal "[| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
nipkow@4830
   139
by (fast_tac (claset() addIs [inj_onI] 
nipkow@2912
   140
                      addEs [inv_injective,injD]) 1);
nipkow@4830
   141
qed "inj_on_inv";
clasohm@923
   142
wenzelm@5069
   143
Goalw [inj_on_def]
nipkow@4830
   144
   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
paulson@4059
   145
by (Blast_tac 1);
nipkow@4830
   146
qed "inj_on_image_Int";
paulson@4059
   147
wenzelm@5069
   148
Goalw [inj_on_def]
nipkow@4830
   149
   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
paulson@4059
   150
by (Blast_tac 1);
nipkow@4830
   151
qed "inj_on_image_set_diff";
paulson@4059
   152
paulson@5143
   153
Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B";
paulson@4059
   154
by (Blast_tac 1);
paulson@4059
   155
qed "image_Int";
paulson@4059
   156
paulson@5143
   157
Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B";
paulson@4059
   158
by (Blast_tac 1);
paulson@4059
   159
qed "image_set_diff";
paulson@4059
   160
clasohm@923
   161
wenzelm@4089
   162
val set_cs = claset() delrules [equalityI];