src/HOL/Fun.ML
author oheimb
Fri May 31 19:12:00 1996 +0200 (1996-05-31)
changeset 1776 d7e77cb8ce5c
parent 1754 852093aeb0ab
child 1822 c192d7dc22e7
permissions -rw-r--r--
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
as there have been unnecessary proofs of anonymous thms, which could not be
removed (by name) from the !simpset where necessary. All these thms except
singleton_iff were already proved in Set.ML.
therefore in Set.ML: New version of singletonE, proof of new thm singleton_iff
     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 (*** Range of a function ***)
    23 
    24 (*Frequently b does not have the syntactic form of f(x).*)
    25 val [prem] = goalw Fun.thy [range_def] "b=f(x) ==> b : range(f)";
    26 by (EVERY1 [rtac CollectI, rtac exI, rtac prem]);
    27 qed "range_eqI";
    28 
    29 val rangeI = refl RS range_eqI;
    30 
    31 val [major,minor] = goalw Fun.thy [range_def]
    32     "[| b : range(%x.f(x));  !!x. b=f(x) ==> P |] ==> P"; 
    33 by (rtac (major RS CollectD RS exE) 1);
    34 by (etac minor 1);
    35 qed "rangeE";
    36 
    37 (*** Image of a set under a function ***)
    38 
    39 val prems = goalw Fun.thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
    40 by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
    41 qed "image_eqI";
    42 
    43 val imageI = refl RS image_eqI;
    44 
    45 (*The eta-expansion gives variable-name preservation.*)
    46 val major::prems = goalw Fun.thy [image_def]
    47     "[| b : (%x.f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
    48 by (rtac (major RS CollectD RS bexE) 1);
    49 by (REPEAT (ares_tac prems 1));
    50 qed "imageE";
    51 
    52 goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
    53 by (rtac set_ext 1);
    54 by (fast_tac (!claset addIs [imageI] addSEs [imageE]) 1);
    55 qed "image_compose";
    56 
    57 goal Fun.thy "f``(A Un B) = f``A Un f``B";
    58 by (rtac set_ext 1);
    59 by (fast_tac (!claset addIs [imageI,UnCI] addSEs [imageE,UnE]) 1);
    60 qed "image_Un";
    61 
    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 addSIs [ballI]) 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,rangeI]
   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,subsetD]) 1);
   168 qed "inj_onto_Inv";
   169 
   170 
   171 (*** Set reasoning tools ***)
   172 
   173 AddSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
   174             ComplI, IntI, DiffI, UnCI, insertCI]; 
   175 AddIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]; 
   176 AddSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
   177 	    make_elim singleton_inject,
   178             CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]; 
   179 AddEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
   180             subsetD, subsetCE];
   181 
   182 val set_cs = HOL_cs 
   183     addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
   184             ComplI, IntI, DiffI, UnCI, insertCI] 
   185     addIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI] 
   186     addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
   187             make_elim singleton_inject,
   188             CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] 
   189     addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
   190             subsetD, subsetCE];
   191 
   192 fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;