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;
```