src/HOL/Fun.ML
author paulson
Fri Jul 26 12:17:04 1996 +0200 (1996-07-26)
changeset 1883 00b4b6992945
parent 1837 ce5dc74dec97
child 2031 03a843f0f447
permissions -rw-r--r--
Redefining "range" as a macro
     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 goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
    39 by (rtac set_ext 1);
    40 by (fast_tac (!claset addIs [imageI] addSEs [imageE]) 1);
    41 qed "image_compose";
    42 
    43 goal Fun.thy "f``(A Un B) = f``A Un f``B";
    44 by (rtac set_ext 1);
    45 by (fast_tac (!claset addIs [imageI,UnCI] addSEs [imageE,UnE]) 1);
    46 qed "image_Un";
    47 
    48 (*** Range of a function -- just a translation for image! ***)
    49 
    50 goal Fun.thy "!!b. b=f(x) ==> b : range(f)";
    51 by (EVERY1 [etac image_eqI, rtac UNIV_I]);
    52 bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
    53 
    54 bind_thm ("rangeI", UNIV_I RS imageI);
    55 
    56 val [major,minor] = goal Fun.thy 
    57     "[| b : range(%x.f(x));  !!x. b=f(x) ==> P |] ==> P"; 
    58 by (rtac (major RS imageE) 1);
    59 by (etac minor 1);
    60 qed "rangeE";
    61 (*** inj(f): f is a one-to-one function ***)
    62 
    63 val prems = goalw Fun.thy [inj_def]
    64     "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
    65 by (fast_tac (!claset addIs prems) 1);
    66 qed "injI";
    67 
    68 val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
    69 by (rtac injI 1);
    70 by (etac (arg_cong RS box_equals) 1);
    71 by (rtac major 1);
    72 by (rtac major 1);
    73 qed "inj_inverseI";
    74 
    75 val [major,minor] = goalw Fun.thy [inj_def]
    76     "[| inj(f); f(x) = f(y) |] ==> x=y";
    77 by (rtac (major RS spec RS spec RS mp) 1);
    78 by (rtac minor 1);
    79 qed "injD";
    80 
    81 (*Useful with the simplifier*)
    82 val [major] = goal Fun.thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
    83 by (rtac iffI 1);
    84 by (etac (major RS injD) 1);
    85 by (etac arg_cong 1);
    86 qed "inj_eq";
    87 
    88 val [major] = goal Fun.thy "inj(f) ==> (@x.f(x)=f(y)) = y";
    89 by (rtac (major RS injD) 1);
    90 by (rtac selectI 1);
    91 by (rtac refl 1);
    92 qed "inj_select";
    93 
    94 (*A one-to-one function has an inverse (given using select).*)
    95 val [major] = goalw Fun.thy [Inv_def] "inj(f) ==> Inv f (f x) = x";
    96 by (EVERY1 [rtac (major RS inj_select)]);
    97 qed "Inv_f_f";
    98 
    99 (* Useful??? *)
   100 val [oneone,minor] = goal Fun.thy
   101     "[| inj(f); !!y. y: range(f) ==> P(Inv f y) |] ==> P(x)";
   102 by (res_inst_tac [("t", "x")] (oneone RS (Inv_f_f RS subst)) 1);
   103 by (rtac (rangeI RS minor) 1);
   104 qed "inj_transfer";
   105 
   106 
   107 (*** inj_onto f A: f is one-to-one over A ***)
   108 
   109 val prems = goalw Fun.thy [inj_onto_def]
   110     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
   111 by (fast_tac (!claset addIs prems addSIs [ballI]) 1);
   112 qed "inj_ontoI";
   113 
   114 val [major] = goal Fun.thy 
   115     "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A";
   116 by (rtac inj_ontoI 1);
   117 by (etac (apply_inverse RS trans) 1);
   118 by (REPEAT (eresolve_tac [asm_rl,major] 1));
   119 qed "inj_onto_inverseI";
   120 
   121 val major::prems = goalw Fun.thy [inj_onto_def]
   122     "[| inj_onto f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   123 by (rtac (major RS bspec RS bspec RS mp) 1);
   124 by (REPEAT (resolve_tac prems 1));
   125 qed "inj_ontoD";
   126 
   127 goal Fun.thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   128 by (fast_tac (!claset addSEs [inj_ontoD]) 1);
   129 qed "inj_onto_iff";
   130 
   131 val major::prems = goal Fun.thy
   132     "[| inj_onto f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   133 by (rtac contrapos 1);
   134 by (etac (major RS inj_ontoD) 2);
   135 by (REPEAT (resolve_tac prems 1));
   136 qed "inj_onto_contraD";
   137 
   138 
   139 (*** Lemmas about inj ***)
   140 
   141 val prems = goalw Fun.thy [o_def]
   142     "[| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
   143 by (cut_facts_tac prems 1);
   144 by (fast_tac (!claset addIs [injI,rangeI]
   145                      addEs [injD,inj_ontoD]) 1);
   146 qed "comp_inj";
   147 
   148 val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
   149 by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
   150 qed "inj_imp";
   151 
   152 val [prem] = goalw Fun.thy [Inv_def] "y : range(f) ==> f(Inv f y) = y";
   153 by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
   154 qed "f_Inv_f";
   155 
   156 val prems = goal Fun.thy
   157     "[| Inv f x=Inv f y; x: range(f);  y: range(f) |] ==> x=y";
   158 by (rtac (arg_cong RS box_equals) 1);
   159 by (REPEAT (resolve_tac (prems @ [f_Inv_f]) 1));
   160 qed "Inv_injective";
   161 
   162 val prems = goal Fun.thy
   163     "[| inj(f);  A<=range(f) |] ==> inj_onto (Inv f) A";
   164 by (cut_facts_tac prems 1);
   165 by (fast_tac (!claset addIs [inj_ontoI] 
   166                      addEs [Inv_injective,injD,subsetD]) 1);
   167 qed "inj_onto_Inv";
   168 
   169 
   170 (*** Set reasoning tools ***)
   171 
   172 AddSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
   173             ComplI, IntI, DiffI, UnCI, insertCI]; 
   174 AddIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]; 
   175 AddSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
   176 	    make_elim singleton_inject,
   177             CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]; 
   178 AddEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
   179             subsetD, subsetCE];
   180 
   181 val set_cs = !claset delrules [equalityI];
   182 
   183