src/HOL/Fun.ML
 author paulson Wed Jul 15 10:15:13 1998 +0200 (1998-07-15) changeset 5143 b94cd208f073 parent 5069 3ea049f7979d child 5148 74919e8f221c permissions -rw-r--r--
Removal of leading "\!\!..." from most Goal commands
```     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
```
```    10 Goal "(f = g) = (!x. f(x)=g(x))";
```
```    11 by (rtac iffI 1);
```
```    12 by (Asm_simp_tac 1);
```
```    13 by (rtac ext 1 THEN Asm_simp_tac 1);
```
```    14 qed "expand_fun_eq";
```
```    15
```
```    16 val prems = goal thy
```
```    17     "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
```
```    18 by (rtac (arg_cong RS box_equals) 1);
```
```    19 by (REPEAT (resolve_tac (prems@[refl]) 1));
```
```    20 qed "apply_inverse";
```
```    21
```
```    22
```
```    23 (** "Axiom" of Choice, proved using the description operator **)
```
```    24
```
```    25 goal HOL.thy "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
```
```    26 by (fast_tac (claset() addEs [selectI]) 1);
```
```    27 qed "choice";
```
```    28
```
```    29 goal Set.thy "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
```
```    30 by (fast_tac (claset() addEs [selectI]) 1);
```
```    31 qed "bchoice";
```
```    32
```
```    33
```
```    34 (*** inj(f): f is a one-to-one function ***)
```
```    35
```
```    36 val prems = goalw thy [inj_def]
```
```    37     "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
```
```    38 by (blast_tac (claset() addIs prems) 1);
```
```    39 qed "injI";
```
```    40
```
```    41 val [major] = goal thy "(!!x. g(f(x)) = x) ==> inj(f)";
```
```    42 by (rtac injI 1);
```
```    43 by (etac (arg_cong RS box_equals) 1);
```
```    44 by (rtac major 1);
```
```    45 by (rtac major 1);
```
```    46 qed "inj_inverseI";
```
```    47
```
```    48 val [major,minor] = goalw thy [inj_def]
```
```    49     "[| inj(f); f(x) = f(y) |] ==> x=y";
```
```    50 by (rtac (major RS spec RS spec RS mp) 1);
```
```    51 by (rtac minor 1);
```
```    52 qed "injD";
```
```    53
```
```    54 (*Useful with the simplifier*)
```
```    55 val [major] = goal thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
```
```    56 by (rtac iffI 1);
```
```    57 by (etac (major RS injD) 1);
```
```    58 by (etac arg_cong 1);
```
```    59 qed "inj_eq";
```
```    60
```
```    61 val [major] = goal thy "inj(f) ==> (@x. f(x)=f(y)) = y";
```
```    62 by (rtac (major RS injD) 1);
```
```    63 by (rtac selectI 1);
```
```    64 by (rtac refl 1);
```
```    65 qed "inj_select";
```
```    66
```
```    67 (*A one-to-one function has an inverse (given using select).*)
```
```    68 val [major] = goalw thy [inv_def] "inj(f) ==> inv f (f x) = x";
```
```    69 by (EVERY1 [rtac (major RS inj_select)]);
```
```    70 qed "inv_f_f";
```
```    71
```
```    72 (* Useful??? *)
```
```    73 val [oneone,minor] = goal thy
```
```    74     "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
```
```    75 by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
```
```    76 by (rtac (rangeI RS minor) 1);
```
```    77 qed "inj_transfer";
```
```    78
```
```    79
```
```    80 (*** inj_on f A: f is one-to-one over A ***)
```
```    81
```
```    82 val prems = goalw thy [inj_on_def]
```
```    83     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
```
```    84 by (blast_tac (claset() addIs prems) 1);
```
```    85 qed "inj_onI";
```
```    86
```
```    87 val [major] = goal thy
```
```    88     "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
```
```    89 by (rtac inj_onI 1);
```
```    90 by (etac (apply_inverse RS trans) 1);
```
```    91 by (REPEAT (eresolve_tac [asm_rl,major] 1));
```
```    92 qed "inj_on_inverseI";
```
```    93
```
```    94 val major::prems = goalw thy [inj_on_def]
```
```    95     "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
```
```    96 by (rtac (major RS bspec RS bspec RS mp) 1);
```
```    97 by (REPEAT (resolve_tac prems 1));
```
```    98 qed "inj_onD";
```
```    99
```
```   100 Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
```
```   101 by (blast_tac (claset() addSDs [inj_onD]) 1);
```
```   102 qed "inj_on_iff";
```
```   103
```
```   104 val major::prems = goal thy
```
```   105     "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
```
```   106 by (rtac contrapos 1);
```
```   107 by (etac (major RS inj_onD) 2);
```
```   108 by (REPEAT (resolve_tac prems 1));
```
```   109 qed "inj_on_contraD";
```
```   110
```
```   111 Goalw [inj_on_def]
```
```   112     "!!A B. [| A<=B; inj_on f B |] ==> inj_on f A";
```
```   113 by (Blast_tac 1);
```
```   114 qed "subset_inj_on";
```
```   115
```
```   116
```
```   117 (*** Lemmas about inj ***)
```
```   118
```
```   119 Goalw [o_def]
```
```   120     "!!f g. [| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
```
```   121 by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
```
```   122 qed "comp_inj";
```
```   123
```
```   124 val [prem] = goal thy "inj(f) ==> inj_on f A";
```
```   125 by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1);
```
```   126 qed "inj_imp";
```
```   127
```
```   128 val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y";
```
```   129 by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
```
```   130 qed "f_inv_f";
```
```   131
```
```   132 val prems = goal thy
```
```   133     "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
```
```   134 by (rtac (arg_cong RS box_equals) 1);
```
```   135 by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
```
```   136 qed "inv_injective";
```
```   137
```
```   138 Goal "[| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
```
```   139 by (fast_tac (claset() addIs [inj_onI]
```
```   140                       addEs [inv_injective,injD]) 1);
```
```   141 qed "inj_on_inv";
```
```   142
```
```   143 Goalw [inj_on_def]
```
```   144    "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
```
```   145 by (Blast_tac 1);
```
```   146 qed "inj_on_image_Int";
```
```   147
```
```   148 Goalw [inj_on_def]
```
```   149    "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
```
```   150 by (Blast_tac 1);
```
```   151 qed "inj_on_image_set_diff";
```
```   152
```
```   153 Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B";
```
```   154 by (Blast_tac 1);
```
```   155 qed "image_Int";
```
```   156
```
```   157 Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B";
```
```   158 by (Blast_tac 1);
```
```   159 qed "image_set_diff";
```
```   160
```
```   161
```
```   162 val set_cs = claset() delrules [equalityI];
```