New theory of the inverse image of a function
authorpaulson
Tue Feb 24 11:35:33 1998 +0100 (1998-02-24)
changeset 4648f04da668581c
parent 4647 42af8ae6e2c1
child 4649 89ad3eb863a1
New theory of the inverse image of a function
src/HOL/Fun.thy
src/HOL/Vimage.ML
src/HOL/Vimage.thy
     1.1 --- a/src/HOL/Fun.thy	Tue Feb 24 10:44:53 1998 +0100
     1.2 +++ b/src/HOL/Fun.thy	Tue Feb 24 11:35:33 1998 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Notions about functions.
     1.5  *)
     1.6  
     1.7 -Fun = Set +
     1.8 +Fun = Vimage +
     1.9  
    1.10  instance set :: (term) order
    1.11                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Vimage.ML	Tue Feb 24 11:35:33 1998 +0100
     2.3 @@ -0,0 +1,72 @@
     2.4 +(*  Title:      HOL/Vimage
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1998  University of Cambridge
     2.8 +
     2.9 +Inverse image of a function
    2.10 +*)
    2.11 +
    2.12 +open Vimage;
    2.13 +
    2.14 +(** Basic rules **)
    2.15 +
    2.16 +qed_goalw "vimage_eq" thy [vimage_def]
    2.17 +    "(a : f-``B) = (f a : B)"
    2.18 + (fn _ => [ (Blast_tac 1) ]);
    2.19 +
    2.20 +qed_goal "vimage_singleton_eq" thy
    2.21 +    "(a : f-``{b}) = (f a = b)"
    2.22 + (fn _ => [ simp_tac (simpset() addsimps [vimage_eq]) 1 ]);
    2.23 +
    2.24 +qed_goalw "vimageI" thy [vimage_def]
    2.25 +    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B"
    2.26 + (fn _ => [ (Blast_tac 1) ]);
    2.27 +
    2.28 +qed_goalw "vimageE" thy [vimage_def]
    2.29 +    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P"
    2.30 + (fn major::prems=>
    2.31 +  [ (rtac (major RS CollectE) 1),
    2.32 +    (blast_tac (claset() addIs prems) 1) ]);
    2.33 +
    2.34 +AddIs  [vimageI];
    2.35 +AddSEs [vimageE];
    2.36 +
    2.37 +
    2.38 +(*** Simple equalities ***)
    2.39 +
    2.40 +goal thy "f-``{} = {}";
    2.41 +by (Blast_tac 1);
    2.42 +qed "vimage_empty";
    2.43 +
    2.44 +goal thy "f-``(A Un B) = (f-``A) Un (f-``B)";
    2.45 +by (Blast_tac 1);
    2.46 +qed "vimage_Un";
    2.47 +
    2.48 +(*NOT suitable for rewriting because of the recurrence of {a}*)
    2.49 +goal thy "f-``(insert a B) = (f-``{a}) Un (f-``B)";
    2.50 +by (Blast_tac 1);
    2.51 +qed "vimage_insert";
    2.52 +
    2.53 +goal thy "f-``(A Int B) <= (f-``A) Int (f-``B)";
    2.54 +by (Blast_tac 1);
    2.55 +qed "vimage_Int_subset";
    2.56 +
    2.57 +Addsimps [vimage_empty, vimage_Un];
    2.58 +
    2.59 +goal thy "f-``UNIV = UNIV";
    2.60 +by (Blast_tac 1);
    2.61 +qed "vimage_UNIV";
    2.62 +
    2.63 +Addsimps [vimage_UNIV];
    2.64 +
    2.65 +goal thy "(UN x:A. f -`` B x) = f -`` (UN x:A. B x)";
    2.66 +by (Blast_tac 1);
    2.67 +qed "UN_vimage";
    2.68 +Addsimps [UN_vimage];
    2.69 +
    2.70 +
    2.71 +(** monotonicity **)
    2.72 +
    2.73 +goal thy "!!f. A<=B ==> f-``A <= f-``B";
    2.74 +by (Blast_tac 1);
    2.75 +qed "vimage_mono";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Vimage.thy	Tue Feb 24 11:35:33 1998 +0100
     3.3 @@ -0,0 +1,9 @@
     3.4 +Vimage = Set +
     3.5 +
     3.6 +consts
     3.7 +  "-``"          :: ['a => 'b, 'b set] => ('a set)   (infixr 90)
     3.8 +
     3.9 +defs
    3.10 +  vimage_def     "f-``B           == {x. f(x) : B}"
    3.11 +
    3.12 +end