src/HOL/Fun.ML
author oheimb
Wed Aug 12 16:23:25 1998 +0200 (1998-08-12)
changeset 5305 513925de8962
parent 5148 74919e8f221c
child 5306 3d1368a3a2a2
permissions -rw-r--r--
cleanup for Fun.thy:
merged Update.{thy|ML} into Fun.{thy|ML}
moved o_def from HOL.thy to Fun.thy
added Id_def to Fun.thy
moved image_compose from Set.ML to Fun.ML
moved o_apply and o_assoc from simpdata.ML to Fun.ML
moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML
added fun_upd_twist to Fun.ML
     1 (*  Title:      HOL/Fun
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Lemmas about functions.
     7 *)
     8 
     9 
    10 qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
    11  (K [rtac refl 1]);
    12 Addsimps [o_apply];
    13 
    14 qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
    15   (K [rtac ext 1, rtac refl 1]);
    16 
    17 Goalw [o_def] "(f o g)``r = f``(g``r)";
    18 by (Blast_tac 1);
    19 qed "image_compose";
    20 
    21 Goal "(f = g) = (!x. f(x)=g(x))";
    22 by (rtac iffI 1);
    23 by (Asm_simp_tac 1);
    24 by (rtac ext 1 THEN Asm_simp_tac 1);
    25 qed "expand_fun_eq";
    26 
    27 val prems = goal thy
    28     "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
    29 by (rtac (arg_cong RS box_equals) 1);
    30 by (REPEAT (resolve_tac (prems@[refl]) 1));
    31 qed "apply_inverse";
    32 
    33 
    34 (** "Axiom" of Choice, proved using the description operator **)
    35 
    36 goal HOL.thy "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
    37 by (fast_tac (claset() addEs [selectI]) 1);
    38 qed "choice";
    39 
    40 goal Set.thy "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
    41 by (fast_tac (claset() addEs [selectI]) 1);
    42 qed "bchoice";
    43 
    44 
    45 (*** inj(f): f is a one-to-one function ***)
    46 
    47 val prems = goalw thy [inj_def]
    48     "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
    49 by (blast_tac (claset() addIs prems) 1);
    50 qed "injI";
    51 
    52 val [major] = goal thy "(!!x. g(f(x)) = x) ==> inj(f)";
    53 by (rtac injI 1);
    54 by (etac (arg_cong RS box_equals) 1);
    55 by (rtac major 1);
    56 by (rtac major 1);
    57 qed "inj_inverseI";
    58 
    59 val [major,minor] = goalw thy [inj_def]
    60     "[| inj(f); f(x) = f(y) |] ==> x=y";
    61 by (rtac (major RS spec RS spec RS mp) 1);
    62 by (rtac minor 1);
    63 qed "injD";
    64 
    65 (*Useful with the simplifier*)
    66 val [major] = goal thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
    67 by (rtac iffI 1);
    68 by (etac (major RS injD) 1);
    69 by (etac arg_cong 1);
    70 qed "inj_eq";
    71 
    72 val [major] = goal thy "inj(f) ==> (@x. f(x)=f(y)) = y";
    73 by (rtac (major RS injD) 1);
    74 by (rtac selectI 1);
    75 by (rtac refl 1);
    76 qed "inj_select";
    77 
    78 (*A one-to-one function has an inverse (given using select).*)
    79 val [major] = goalw thy [inv_def] "inj(f) ==> inv f (f x) = x";
    80 by (EVERY1 [rtac (major RS inj_select)]);
    81 qed "inv_f_f";
    82 
    83 (* Useful??? *)
    84 val [oneone,minor] = goal thy
    85     "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
    86 by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
    87 by (rtac (rangeI RS minor) 1);
    88 qed "inj_transfer";
    89 
    90 
    91 (*** inj_on f A: f is one-to-one over A ***)
    92 
    93 val prems = goalw thy [inj_on_def]
    94     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
    95 by (blast_tac (claset() addIs prems) 1);
    96 qed "inj_onI";
    97 
    98 val [major] = goal thy 
    99     "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
   100 by (rtac inj_onI 1);
   101 by (etac (apply_inverse RS trans) 1);
   102 by (REPEAT (eresolve_tac [asm_rl,major] 1));
   103 qed "inj_on_inverseI";
   104 
   105 val major::prems = goalw thy [inj_on_def]
   106     "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   107 by (rtac (major RS bspec RS bspec RS mp) 1);
   108 by (REPEAT (resolve_tac prems 1));
   109 qed "inj_onD";
   110 
   111 Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   112 by (blast_tac (claset() addSDs [inj_onD]) 1);
   113 qed "inj_on_iff";
   114 
   115 val major::prems = goal thy
   116     "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   117 by (rtac contrapos 1);
   118 by (etac (major RS inj_onD) 2);
   119 by (REPEAT (resolve_tac prems 1));
   120 qed "inj_on_contraD";
   121 
   122 Goalw [inj_on_def]
   123     "[| A<=B; inj_on f B |] ==> inj_on f A";
   124 by (Blast_tac 1);
   125 qed "subset_inj_on";
   126 
   127 
   128 (*** Lemmas about inj ***)
   129 
   130 Goalw [o_def]
   131     "[| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
   132 by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
   133 qed "comp_inj";
   134 
   135 val [prem] = goal thy "inj(f) ==> inj_on f A";
   136 by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1);
   137 qed "inj_imp";
   138 
   139 val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y";
   140 by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
   141 qed "f_inv_f";
   142 
   143 val prems = goal thy
   144     "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
   145 by (rtac (arg_cong RS box_equals) 1);
   146 by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
   147 qed "inv_injective";
   148 
   149 Goal "[| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
   150 by (fast_tac (claset() addIs [inj_onI] 
   151                       addEs [inv_injective,injD]) 1);
   152 qed "inj_on_inv";
   153 
   154 Goalw [inj_on_def]
   155    "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
   156 by (Blast_tac 1);
   157 qed "inj_on_image_Int";
   158 
   159 Goalw [inj_on_def]
   160    "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
   161 by (Blast_tac 1);
   162 qed "inj_on_image_set_diff";
   163 
   164 Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B";
   165 by (Blast_tac 1);
   166 qed "image_Int";
   167 
   168 Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B";
   169 by (Blast_tac 1);
   170 qed "image_set_diff";
   171 
   172 
   173 val set_cs = claset() delrules [equalityI];
   174 
   175 
   176 section "fun_upd";
   177 
   178 Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
   179 by Safe_tac;
   180 by (etac subst 1);
   181 by (rtac ext 2);
   182 by Auto_tac;
   183 qed "fun_upd_idem_iff";
   184 
   185 (* f x = y ==> f(x:=y) = f *)
   186 bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
   187 
   188 (* f(x := f x) = f *)
   189 AddIffs [refl RS fun_upd_idem];
   190 
   191 Goal "(f(x:=y))z = (if z=x then y else f z)";
   192 by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
   193 qed "fun_upd_apply";
   194 Addsimps [fun_upd_apply];
   195 
   196 qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 
   197 	(K [Simp_tac 1]);
   198 qed_goal "fund_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
   199 	(K [Asm_simp_tac 1]);
   200 (*Addsimps [fun_upd_same, fun_upd_other];*)
   201 
   202 Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
   203 by (rtac ext 1);
   204 by (Auto_tac);
   205 qed "fun_upd_twist";