src/HOL/Vimage.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7516 a1d476251238
child 7823 742715638a01
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Vimage
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Inverse image of a function
     7 *)
     8 
     9 (** Basic rules **)
    10 
    11 Goalw [vimage_def] "(a : f-``B) = (f a : B)";
    12 by (Blast_tac 1) ;
    13 qed "vimage_eq";
    14 
    15 Addsimps [vimage_eq];
    16 
    17 Goal "(a : f-``{b}) = (f a = b)";
    18 by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
    19 qed "vimage_singleton_eq";
    20 
    21 Goalw [vimage_def]
    22     "!!A B f. [| f a = b;  b:B |] ==> a : f-``B";
    23 by (Blast_tac 1) ;
    24 qed "vimageI";
    25 
    26 Goalw [vimage_def] "f a : A ==> a : f -`` A";
    27 by (Fast_tac 1);
    28 qed "vimageI2";
    29 
    30 val major::prems = Goalw [vimage_def]
    31     "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
    32 by (rtac (major RS CollectE) 1);
    33 by (blast_tac (claset() addIs prems) 1) ;
    34 qed "vimageE";
    35 
    36 Goalw [vimage_def] "a : f -`` A ==> f a : A";
    37 by (Fast_tac 1);
    38 qed "vimageD";
    39 
    40 AddIs  [vimageI];
    41 AddSEs [vimageE];
    42 
    43 
    44 (*** Simple equalities ***)
    45 
    46 Goal "f-``{} = {}";
    47 by (Blast_tac 1);
    48 qed "vimage_empty";
    49 
    50 Goal "f-``(-A) = -(f-``A)";
    51 by (Blast_tac 1);
    52 qed "vimage_Compl";
    53 
    54 Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
    55 by (Blast_tac 1);
    56 qed "vimage_Un";
    57 
    58 Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
    59 by (Fast_tac 1);
    60 qed "vimage_Int";
    61 
    62 Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
    63 by (Blast_tac 1);
    64 qed "vimage_UN";
    65 
    66 bind_thm ("vimage_Collect", allI RS prove_goalw thy [vimage_def]
    67   "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
    68     (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
    69 
    70 Addsimps [vimage_empty, vimage_Un, vimage_Int];
    71 
    72 (*NOT suitable for rewriting because of the recurrence of {a}*)
    73 Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
    74 by (Blast_tac 1);
    75 qed "vimage_insert";
    76 
    77 Goal "f-``(A-B) = (f-``A) - (f-``B)";
    78 by (Blast_tac 1);
    79 qed "vimage_Diff";
    80 
    81 Goal "f-``UNIV = UNIV";
    82 by (Blast_tac 1);
    83 qed "vimage_UNIV";
    84 Addsimps [vimage_UNIV];
    85 
    86 Goal "(UN x:A. f -`` B x) = f -`` (UN x:A. B x)";
    87 by (Blast_tac 1);
    88 qed "UN_vimage";
    89 Addsimps [UN_vimage];
    90 
    91 (*NOT suitable for rewriting*)
    92 Goal "f-``B = (UN y: B. f-``{y})";
    93 by (Blast_tac 1);
    94 qed "vimage_eq_UN";
    95 
    96 
    97 (** monotonicity **)
    98 
    99 Goal "A<=B ==> f-``A <= f-``B";
   100 by (Blast_tac 1);
   101 qed "vimage_mono";