src/HOL/Fun.ML
author nipkow
Fri Apr 04 16:33:28 1997 +0200 (1997-04-04)
changeset 2912 3fac3e8d5d3e
parent 2890 f27002fc531d
child 2922 580647a879cf
permissions -rw-r--r--
moved inj and surj from Set to Fun and Inv -> inv.
     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 goal Fun.thy "(f = g) = (!x. f(x)=g(x))";
    10 by (rtac iffI 1);
    11 by (Asm_simp_tac 1);
    12 by (rtac ext 1 THEN Asm_simp_tac 1);
    13 qed "expand_fun_eq";
    14 
    15 val prems = goal Fun.thy
    16     "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
    17 by (rtac (arg_cong RS box_equals) 1);
    18 by (REPEAT (resolve_tac (prems@[refl]) 1));
    19 qed "apply_inverse";
    20 
    21 
    22 (*** inj(f): f is a one-to-one function ***)
    23 
    24 val prems = goalw Fun.thy [inj_def]
    25     "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
    26 by (fast_tac (!claset addIs prems) 1);
    27 qed "injI";
    28 
    29 val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
    30 by (rtac injI 1);
    31 by (etac (arg_cong RS box_equals) 1);
    32 by (rtac major 1);
    33 by (rtac major 1);
    34 qed "inj_inverseI";
    35 
    36 val [major,minor] = goalw Fun.thy [inj_def]
    37     "[| inj(f); f(x) = f(y) |] ==> x=y";
    38 by (rtac (major RS spec RS spec RS mp) 1);
    39 by (rtac minor 1);
    40 qed "injD";
    41 
    42 (*Useful with the simplifier*)
    43 val [major] = goal Fun.thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
    44 by (rtac iffI 1);
    45 by (etac (major RS injD) 1);
    46 by (etac arg_cong 1);
    47 qed "inj_eq";
    48 
    49 val [major] = goal Fun.thy "inj(f) ==> (@x.f(x)=f(y)) = y";
    50 by (rtac (major RS injD) 1);
    51 by (rtac selectI 1);
    52 by (rtac refl 1);
    53 qed "inj_select";
    54 
    55 (*A one-to-one function has an inverse (given using select).*)
    56 val [major] = goalw Fun.thy [inv_def] "inj(f) ==> inv f (f x) = x";
    57 by (EVERY1 [rtac (major RS inj_select)]);
    58 qed "inv_f_f";
    59 
    60 (* Useful??? *)
    61 val [oneone,minor] = goal Fun.thy
    62     "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
    63 by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
    64 by (rtac (rangeI RS minor) 1);
    65 qed "inj_transfer";
    66 
    67 
    68 (*** inj_onto f A: f is one-to-one over A ***)
    69 
    70 val prems = goalw Fun.thy [inj_onto_def]
    71     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
    72 by (fast_tac (!claset addIs prems) 1);
    73 qed "inj_ontoI";
    74 
    75 val [major] = goal Fun.thy 
    76     "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A";
    77 by (rtac inj_ontoI 1);
    78 by (etac (apply_inverse RS trans) 1);
    79 by (REPEAT (eresolve_tac [asm_rl,major] 1));
    80 qed "inj_onto_inverseI";
    81 
    82 val major::prems = goalw Fun.thy [inj_onto_def]
    83     "[| inj_onto f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
    84 by (rtac (major RS bspec RS bspec RS mp) 1);
    85 by (REPEAT (resolve_tac prems 1));
    86 qed "inj_ontoD";
    87 
    88 goal Fun.thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
    89 by (fast_tac (!claset addSEs [inj_ontoD]) 1);
    90 qed "inj_onto_iff";
    91 
    92 val major::prems = goal Fun.thy
    93     "[| inj_onto f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
    94 by (rtac contrapos 1);
    95 by (etac (major RS inj_ontoD) 2);
    96 by (REPEAT (resolve_tac prems 1));
    97 qed "inj_onto_contraD";
    98 
    99 
   100 (*** Lemmas about inj ***)
   101 
   102 val prems = goalw Fun.thy [o_def]
   103     "[| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
   104 by (cut_facts_tac prems 1);
   105 by (fast_tac (!claset addIs [injI]
   106                      addEs [injD,inj_ontoD]) 1);
   107 qed "comp_inj";
   108 
   109 val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
   110 by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
   111 qed "inj_imp";
   112 
   113 val [prem] = goalw Fun.thy [inv_def] "y : range(f) ==> f(inv f y) = y";
   114 by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
   115 qed "f_inv_f";
   116 
   117 val prems = goal Fun.thy
   118     "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
   119 by (rtac (arg_cong RS box_equals) 1);
   120 by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
   121 qed "inv_injective";
   122 
   123 val prems = goal Fun.thy
   124     "[| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
   125 by (cut_facts_tac prems 1);
   126 by (fast_tac (!claset addIs [inj_ontoI] 
   127                       addEs [inv_injective,injD]) 1);
   128 qed "inj_onto_inv";
   129 
   130 
   131 val set_cs = !claset delrules [equalityI];