src/HOL/Fun.ML
 author berghofe Tue May 21 13:39:31 1996 +0200 (1996-05-21) changeset 1754 852093aeb0ab parent 1672 2c109cd2fdd0 child 1776 d7e77cb8ce5c permissions -rw-r--r--
Replaced fast_tac by Fast_tac (which uses default claset)
New rules are now also added to default claset.
```     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;
```
```   193
```
```   194
```
```   195 fun prover s = prove_goal Fun.thy s (fn _=>[fast_tac set_cs 1]);
```
```   196
```
```   197 val mem_simps = map prover
```
```   198  [ "(a : A Un B)   =  (a:A | a:B)",	(* Un_iff *)
```
```   199    "(a : A Int B)  =  (a:A & a:B)",	(* Int_iff *)
```
```   200    "(a : Compl(B)) =  (~a:B)",		(* Compl_iff *)
```
```   201    "(a : A-B)      =  (a:A & ~a:B)",	(* Diff_iff *)
```
```   202    "(a : {b})      =  (a=b)",
```
```   203    "(a : {x.P(x)}) =  P(a)" ];
```
```   204
```
```   205 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
```
```   206
```
```   207 simpset := !simpset addsimps mem_simps
```
```   208                     addcongs [ball_cong,bex_cong]
```
```   209                     setmksimps (mksimps mksimps_pairs);
```