src/HOL/Fun.ML
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2499 0bc87b063447
child 2890 f27002fc531d
permissions -rw-r--r--
added AxClasses test;
     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 (*** Image of a set under a function ***)
    23 
    24 (*Frequently b does not have the syntactic form of f(x).*)
    25 val prems = goalw Fun.thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
    26 by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
    27 qed "image_eqI";
    28 
    29 bind_thm ("imageI", refl RS image_eqI);
    30 
    31 (*The eta-expansion gives variable-name preservation.*)
    32 val major::prems = goalw Fun.thy [image_def]
    33     "[| b : (%x.f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
    34 by (rtac (major RS CollectD RS bexE) 1);
    35 by (REPEAT (ares_tac prems 1));
    36 qed "imageE";
    37 
    38 AddIs  [imageI]; 
    39 AddSEs [imageE]; 
    40 
    41 goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
    42 by (Fast_tac 1);
    43 qed "image_compose";
    44 
    45 goal Fun.thy "f``(A Un B) = f``A Un f``B";
    46 by (Fast_tac 1);
    47 qed "image_Un";
    48 
    49 (*** Range of a function -- just a translation for image! ***)
    50 
    51 goal Fun.thy "!!b. b=f(x) ==> b : range(f)";
    52 by (EVERY1 [etac image_eqI, rtac UNIV_I]);
    53 bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
    54 
    55 bind_thm ("rangeI", UNIV_I RS imageI);
    56 
    57 val [major,minor] = goal Fun.thy 
    58     "[| b : range(%x.f(x));  !!x. b=f(x) ==> P |] ==> P"; 
    59 by (rtac (major RS imageE) 1);
    60 by (etac minor 1);
    61 qed "rangeE";
    62 (*** inj(f): f is a one-to-one function ***)
    63 
    64 val prems = goalw Fun.thy [inj_def]
    65     "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
    66 by (fast_tac (!claset addIs prems) 1);
    67 qed "injI";
    68 
    69 val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
    70 by (rtac injI 1);
    71 by (etac (arg_cong RS box_equals) 1);
    72 by (rtac major 1);
    73 by (rtac major 1);
    74 qed "inj_inverseI";
    75 
    76 val [major,minor] = goalw Fun.thy [inj_def]
    77     "[| inj(f); f(x) = f(y) |] ==> x=y";
    78 by (rtac (major RS spec RS spec RS mp) 1);
    79 by (rtac minor 1);
    80 qed "injD";
    81 
    82 (*Useful with the simplifier*)
    83 val [major] = goal Fun.thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
    84 by (rtac iffI 1);
    85 by (etac (major RS injD) 1);
    86 by (etac arg_cong 1);
    87 qed "inj_eq";
    88 
    89 val [major] = goal Fun.thy "inj(f) ==> (@x.f(x)=f(y)) = y";
    90 by (rtac (major RS injD) 1);
    91 by (rtac selectI 1);
    92 by (rtac refl 1);
    93 qed "inj_select";
    94 
    95 (*A one-to-one function has an inverse (given using select).*)
    96 val [major] = goalw Fun.thy [Inv_def] "inj(f) ==> Inv f (f x) = x";
    97 by (EVERY1 [rtac (major RS inj_select)]);
    98 qed "Inv_f_f";
    99 
   100 (* Useful??? *)
   101 val [oneone,minor] = goal Fun.thy
   102     "[| inj(f); !!y. y: range(f) ==> P(Inv f y) |] ==> P(x)";
   103 by (res_inst_tac [("t", "x")] (oneone RS (Inv_f_f RS subst)) 1);
   104 by (rtac (rangeI RS minor) 1);
   105 qed "inj_transfer";
   106 
   107 
   108 (*** inj_onto f A: f is one-to-one over A ***)
   109 
   110 val prems = goalw Fun.thy [inj_onto_def]
   111     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
   112 by (fast_tac (!claset addIs prems) 1);
   113 qed "inj_ontoI";
   114 
   115 val [major] = goal Fun.thy 
   116     "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A";
   117 by (rtac inj_ontoI 1);
   118 by (etac (apply_inverse RS trans) 1);
   119 by (REPEAT (eresolve_tac [asm_rl,major] 1));
   120 qed "inj_onto_inverseI";
   121 
   122 val major::prems = goalw Fun.thy [inj_onto_def]
   123     "[| inj_onto f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   124 by (rtac (major RS bspec RS bspec RS mp) 1);
   125 by (REPEAT (resolve_tac prems 1));
   126 qed "inj_ontoD";
   127 
   128 goal Fun.thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   129 by (fast_tac (!claset addSEs [inj_ontoD]) 1);
   130 qed "inj_onto_iff";
   131 
   132 val major::prems = goal Fun.thy
   133     "[| inj_onto f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   134 by (rtac contrapos 1);
   135 by (etac (major RS inj_ontoD) 2);
   136 by (REPEAT (resolve_tac prems 1));
   137 qed "inj_onto_contraD";
   138 
   139 
   140 (*** Lemmas about inj ***)
   141 
   142 val prems = goalw Fun.thy [o_def]
   143     "[| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
   144 by (cut_facts_tac prems 1);
   145 by (fast_tac (!claset addIs [injI]
   146                      addEs [injD,inj_ontoD]) 1);
   147 qed "comp_inj";
   148 
   149 val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
   150 by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
   151 qed "inj_imp";
   152 
   153 val [prem] = goalw Fun.thy [Inv_def] "y : range(f) ==> f(Inv f y) = y";
   154 by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
   155 qed "f_Inv_f";
   156 
   157 val prems = goal Fun.thy
   158     "[| Inv f x=Inv f y; x: range(f);  y: range(f) |] ==> x=y";
   159 by (rtac (arg_cong RS box_equals) 1);
   160 by (REPEAT (resolve_tac (prems @ [f_Inv_f]) 1));
   161 qed "Inv_injective";
   162 
   163 val prems = goal Fun.thy
   164     "[| inj(f);  A<=range(f) |] ==> inj_onto (Inv f) A";
   165 by (cut_facts_tac prems 1);
   166 by (fast_tac (!claset addIs [inj_ontoI] 
   167                       addEs [Inv_injective,injD]) 1);
   168 qed "inj_onto_Inv";
   169 
   170 
   171 AddIs  [rangeI]; 
   172 AddSEs [rangeE]; 
   173 
   174 val set_cs = !claset delrules [equalityI];
   175 
   176