src/HOL/Vimage.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5490 85855f65d0c6
child 7031 972b5f62f476
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     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 open Vimage;
    10 
    11 (** Basic rules **)
    12 
    13 qed_goalw "vimage_eq" thy [vimage_def]
    14     "(a : f-``B) = (f a : B)"
    15  (fn _ => [ (Blast_tac 1) ]);
    16 
    17 Addsimps [vimage_eq];
    18 
    19 qed_goal "vimage_singleton_eq" thy
    20     "(a : f-``{b}) = (f a = b)"
    21  (fn _ => [ simp_tac (simpset() addsimps [vimage_eq]) 1 ]);
    22 
    23 qed_goalw "vimageI" thy [vimage_def]
    24     "!!A B f. [| f a = b;  b:B |] ==> a : f-``B"
    25  (fn _ => [ (Blast_tac 1) ]);
    26 
    27 Goalw [vimage_def] "f a : A ==> a : f -`` A";
    28 by (Fast_tac 1);
    29 qed "vimageI2";
    30 
    31 qed_goalw "vimageE" thy [vimage_def]
    32     "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P"
    33  (fn major::prems=>
    34   [ (rtac (major RS CollectE) 1),
    35     (blast_tac (claset() addIs prems) 1) ]);
    36 
    37 Goalw [vimage_def] "a : f -`` A ==> f a : A";
    38 by (Fast_tac 1);
    39 qed "vimageD";
    40 
    41 AddIs  [vimageI];
    42 AddSEs [vimageE];
    43 
    44 
    45 (*** Simple equalities ***)
    46 
    47 Goal "(%x. x) -`` B = B";
    48 by (Blast_tac 1);
    49 qed "ident_vimage";
    50 Addsimps [ident_vimage];
    51 
    52 Goal "f-``{} = {}";
    53 by (Blast_tac 1);
    54 qed "vimage_empty";
    55 
    56 Goal "f-``(-A) = -(f-``A)";
    57 by (Blast_tac 1);
    58 qed "vimage_Compl";
    59 
    60 Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
    61 by (Blast_tac 1);
    62 qed "vimage_Un";
    63 
    64 Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
    65 by (Fast_tac 1);
    66 qed "vimage_Int";
    67 
    68 Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
    69 by (Blast_tac 1);
    70 qed "vimage_UN";
    71 
    72 bind_thm ("vimage_Collect", allI RS prove_goalw thy [vimage_def]
    73   "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
    74     (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
    75 
    76 Addsimps [vimage_empty, vimage_Un, vimage_Int];
    77 
    78 (*NOT suitable for rewriting because of the recurrence of {a}*)
    79 Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
    80 by (Blast_tac 1);
    81 qed "vimage_insert";
    82 
    83 Goal "f-``(A-B) = (f-``A) - (f-``B)";
    84 by (Blast_tac 1);
    85 qed "vimage_Diff";
    86 
    87 Goal "f-``UNIV = UNIV";
    88 by (Blast_tac 1);
    89 qed "vimage_UNIV";
    90 Addsimps [vimage_UNIV];
    91 
    92 Goal "(UN x:A. f -`` B x) = f -`` (UN x:A. B x)";
    93 by (Blast_tac 1);
    94 qed "UN_vimage";
    95 Addsimps [UN_vimage];
    96 
    97 (*NOT suitable for rewriting*)
    98 Goal "f-``B = (UN y: B. f-``{y})";
    99 by (Blast_tac 1);
   100 qed "vimage_eq_UN";
   101 
   102 
   103 (** monotonicity **)
   104 
   105 Goal "A<=B ==> f-``A <= f-``B";
   106 by (Blast_tac 1);
   107 qed "vimage_mono";