src/HOL/Fun.ML
 author paulson Mon May 26 12:37:24 1997 +0200 (1997-05-26) changeset 3341 89fe22bf9f54 parent 2935 998cb95fdd43 child 3842 b55686a7b22c permissions -rw-r--r--
New theorem subset_inj_onto
```     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 (*** inj(f): f is a one-to-one function ***)
```
```    23
```
```    24 val prems = goalw Fun.thy [inj_def]
```
```    25     "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
```
```    26 by (blast_tac (!claset addIs prems) 1);
```
```    27 qed "injI";
```
```    28
```
```    29 val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
```
```    30 by (rtac injI 1);
```
```    31 by (etac (arg_cong RS box_equals) 1);
```
```    32 by (rtac major 1);
```
```    33 by (rtac major 1);
```
```    34 qed "inj_inverseI";
```
```    35
```
```    36 val [major,minor] = goalw Fun.thy [inj_def]
```
```    37     "[| inj(f); f(x) = f(y) |] ==> x=y";
```
```    38 by (rtac (major RS spec RS spec RS mp) 1);
```
```    39 by (rtac minor 1);
```
```    40 qed "injD";
```
```    41
```
```    42 (*Useful with the simplifier*)
```
```    43 val [major] = goal Fun.thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
```
```    44 by (rtac iffI 1);
```
```    45 by (etac (major RS injD) 1);
```
```    46 by (etac arg_cong 1);
```
```    47 qed "inj_eq";
```
```    48
```
```    49 val [major] = goal Fun.thy "inj(f) ==> (@x.f(x)=f(y)) = y";
```
```    50 by (rtac (major RS injD) 1);
```
```    51 by (rtac selectI 1);
```
```    52 by (rtac refl 1);
```
```    53 qed "inj_select";
```
```    54
```
```    55 (*A one-to-one function has an inverse (given using select).*)
```
```    56 val [major] = goalw Fun.thy [inv_def] "inj(f) ==> inv f (f x) = x";
```
```    57 by (EVERY1 [rtac (major RS inj_select)]);
```
```    58 qed "inv_f_f";
```
```    59
```
```    60 (* Useful??? *)
```
```    61 val [oneone,minor] = goal Fun.thy
```
```    62     "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
```
```    63 by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
```
```    64 by (rtac (rangeI RS minor) 1);
```
```    65 qed "inj_transfer";
```
```    66
```
```    67
```
```    68 (*** inj_onto f A: f is one-to-one over A ***)
```
```    69
```
```    70 val prems = goalw Fun.thy [inj_onto_def]
```
```    71     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
```
```    72 by (blast_tac (!claset addIs prems) 1);
```
```    73 qed "inj_ontoI";
```
```    74
```
```    75 val [major] = goal Fun.thy
```
```    76     "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A";
```
```    77 by (rtac inj_ontoI 1);
```
```    78 by (etac (apply_inverse RS trans) 1);
```
```    79 by (REPEAT (eresolve_tac [asm_rl,major] 1));
```
```    80 qed "inj_onto_inverseI";
```
```    81
```
```    82 val major::prems = goalw Fun.thy [inj_onto_def]
```
```    83     "[| inj_onto f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
```
```    84 by (rtac (major RS bspec RS bspec RS mp) 1);
```
```    85 by (REPEAT (resolve_tac prems 1));
```
```    86 qed "inj_ontoD";
```
```    87
```
```    88 goal Fun.thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
```
```    89 by (blast_tac (!claset addSDs [inj_ontoD]) 1);
```
```    90 qed "inj_onto_iff";
```
```    91
```
```    92 val major::prems = goal Fun.thy
```
```    93     "[| inj_onto f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
```
```    94 by (rtac contrapos 1);
```
```    95 by (etac (major RS inj_ontoD) 2);
```
```    96 by (REPEAT (resolve_tac prems 1));
```
```    97 qed "inj_onto_contraD";
```
```    98
```
```    99 goalw Fun.thy [inj_onto_def]
```
```   100     "!!A B. [| A<=B; inj_onto f B |] ==> inj_onto f A";
```
```   101 by (Blast_tac 1);
```
```   102 qed "subset_inj_onto";
```
```   103
```
```   104
```
```   105 (*** Lemmas about inj ***)
```
```   106
```
```   107 goalw Fun.thy [o_def]
```
```   108     "!!f g. [| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
```
```   109 by (fast_tac (!claset addIs [injI] addEs [injD, inj_ontoD]) 1);
```
```   110 qed "comp_inj";
```
```   111
```
```   112 val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
```
```   113 by (blast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
```
```   114 qed "inj_imp";
```
```   115
```
```   116 val [prem] = goalw Fun.thy [inv_def] "y : range(f) ==> f(inv f y) = y";
```
```   117 by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
```
```   118 qed "f_inv_f";
```
```   119
```
```   120 val prems = goal Fun.thy
```
```   121     "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
```
```   122 by (rtac (arg_cong RS box_equals) 1);
```
```   123 by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
```
```   124 qed "inv_injective";
```
```   125
```
```   126 goal Fun.thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
```
```   127 by (fast_tac (!claset addIs [inj_ontoI]
```
```   128                       addEs [inv_injective,injD]) 1);
```
```   129 qed "inj_onto_inv";
```
```   130
```
```   131
```
```   132 val set_cs = !claset delrules [equalityI];
```