src/HOL/Inverse_Image.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10832 e33b47e4246d
permissions -rw-r--r--
improved theory reference in comment
     1 (*  Title:      HOL/Inverse_Image.ML
     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 (*** Equations ***)
    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 -` (Union A) = (UN X:A. f -` X)";
    63 by (Blast_tac 1);
    64 qed "vimage_Union";
    65 
    66 Goal "f-`(UN x:A. B x) = (UN x:A. f -` B x)";
    67 by (Blast_tac 1);
    68 qed "vimage_UN";
    69 
    70 Goal "f-`(INT x:A. B x) = (INT x:A. f -` B x)";
    71 by (Blast_tac 1);
    72 qed "vimage_INT";
    73 
    74 Goal "f -` Collect P = {y. P (f y)}";
    75 by (Blast_tac 1);
    76 qed "vimage_Collect_eq";
    77 Addsimps [vimage_Collect_eq];
    78 
    79 (*A strange result used in Tools/inductive_package*)
    80 val prems = Goal "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q";
    81 by (force_tac (claset(), simpset() addsimps prems) 1);
    82 qed "vimage_Collect";
    83 
    84 Addsimps [vimage_empty, vimage_Un, vimage_Int];
    85 
    86 (*NOT suitable for rewriting because of the recurrence of {a}*)
    87 Goal "f-`(insert a B) = (f-`{a}) Un (f-`B)";
    88 by (Blast_tac 1);
    89 qed "vimage_insert";
    90 
    91 Goal "f-`(A-B) = (f-`A) - (f-`B)";
    92 by (Blast_tac 1);
    93 qed "vimage_Diff";
    94 
    95 Goal "f-`UNIV = UNIV";
    96 by (Blast_tac 1);
    97 qed "vimage_UNIV";
    98 Addsimps [vimage_UNIV];
    99 
   100 (*NOT suitable for rewriting*)
   101 Goal "f-`B = (UN y: B. f-`{y})";
   102 by (Blast_tac 1);
   103 qed "vimage_eq_UN";
   104 
   105 (*monotonicity*)
   106 Goal "A<=B ==> f-`A <= f-`B";
   107 by (Blast_tac 1);
   108 qed "vimage_mono";