src/HOL/Fun.ML
author paulson
Thu Feb 26 11:07:37 1998 +0100 (1998-02-26)
changeset 4656 134d24ddaad3
parent 4089 96fba19bcbe2
child 4830 bd73675adbed
permissions -rw-r--r--
Proved choice and bchoice; changed Fun.thy -> thy
     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 thy "(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_onto f A: f is one-to-one over A ***)
    81 
    82 val prems = goalw thy [inj_onto_def]
    83     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
    84 by (blast_tac (claset() addIs prems) 1);
    85 qed "inj_ontoI";
    86 
    87 val [major] = goal thy 
    88     "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A";
    89 by (rtac inj_ontoI 1);
    90 by (etac (apply_inverse RS trans) 1);
    91 by (REPEAT (eresolve_tac [asm_rl,major] 1));
    92 qed "inj_onto_inverseI";
    93 
    94 val major::prems = goalw thy [inj_onto_def]
    95     "[| inj_onto 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_ontoD";
    99 
   100 goal thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   101 by (blast_tac (claset() addSDs [inj_ontoD]) 1);
   102 qed "inj_onto_iff";
   103 
   104 val major::prems = goal thy
   105     "[| inj_onto f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   106 by (rtac contrapos 1);
   107 by (etac (major RS inj_ontoD) 2);
   108 by (REPEAT (resolve_tac prems 1));
   109 qed "inj_onto_contraD";
   110 
   111 goalw thy [inj_onto_def]
   112     "!!A B. [| A<=B; inj_onto f B |] ==> inj_onto f A";
   113 by (Blast_tac 1);
   114 qed "subset_inj_onto";
   115 
   116 
   117 (*** Lemmas about inj ***)
   118 
   119 goalw thy [o_def]
   120     "!!f g. [| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
   121 by (fast_tac (claset() addIs [injI] addEs [injD, inj_ontoD]) 1);
   122 qed "comp_inj";
   123 
   124 val [prem] = goal thy "inj(f) ==> inj_onto f A";
   125 by (blast_tac (claset() addIs [prem RS injD, inj_ontoI]) 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 thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
   139 by (fast_tac (claset() addIs [inj_ontoI] 
   140                       addEs [inv_injective,injD]) 1);
   141 qed "inj_onto_inv";
   142 
   143 goalw thy [inj_onto_def]
   144    "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
   145 by (Blast_tac 1);
   146 qed "inj_onto_image_Int";
   147 
   148 goalw thy [inj_onto_def]
   149    "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
   150 by (Blast_tac 1);
   151 qed "inj_onto_image_set_diff";
   152 
   153 goalw thy [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B";
   154 by (Blast_tac 1);
   155 qed "image_Int";
   156 
   157 goalw thy [inj_def] "!!f. 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];