- Fixed bug in shrink
- Restored old behaviour of thm_proof
- Eliminated reference from theory data
(* Title: HOL/Inverse_Image.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
Inverse image of a function
*)
(** Basic rules **)
Goalw [vimage_def] "(a : f-`B) = (f a : B)";
by (Blast_tac 1) ;
qed "vimage_eq";
Addsimps [vimage_eq];
Goal "(a : f-`{b}) = (f a = b)";
by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
qed "vimage_singleton_eq";
Goalw [vimage_def]
"!!A B f. [| f a = b; b:B |] ==> a : f-`B";
by (Blast_tac 1) ;
qed "vimageI";
Goalw [vimage_def] "f a : A ==> a : f -` A";
by (Fast_tac 1);
qed "vimageI2";
val major::prems = Goalw [vimage_def]
"[| a: f-`B; !!x.[| f a = x; x:B |] ==> P |] ==> P";
by (rtac (major RS CollectE) 1);
by (blast_tac (claset() addIs prems) 1) ;
qed "vimageE";
Goalw [vimage_def] "a : f -` A ==> f a : A";
by (Fast_tac 1);
qed "vimageD";
AddIs [vimageI];
AddSEs [vimageE];
(*** Equations ***)
Goal "f-`{} = {}";
by (Blast_tac 1);
qed "vimage_empty";
Goal "f-`(-A) = -(f-`A)";
by (Blast_tac 1);
qed "vimage_Compl";
Goal "f-`(A Un B) = (f-`A) Un (f-`B)";
by (Blast_tac 1);
qed "vimage_Un";
Goal "f -` (A Int B) = (f -` A) Int (f -` B)";
by (Fast_tac 1);
qed "vimage_Int";
Goal "f -` (Union A) = (UN X:A. f -` X)";
by (Blast_tac 1);
qed "vimage_Union";
Goal "f-`(UN x:A. B x) = (UN x:A. f -` B x)";
by (Blast_tac 1);
qed "vimage_UN";
Goal "f-`(INT x:A. B x) = (INT x:A. f -` B x)";
by (Blast_tac 1);
qed "vimage_INT";
Goal "f -` Collect P = {y. P (f y)}";
by (Blast_tac 1);
qed "vimage_Collect_eq";
Addsimps [vimage_Collect_eq];
(*A strange result used in Tools/inductive_package*)
val prems = Goal "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q";
by (force_tac (claset(), simpset() addsimps prems) 1);
qed "vimage_Collect";
Addsimps [vimage_empty, vimage_Un, vimage_Int];
(*NOT suitable for rewriting because of the recurrence of {a}*)
Goal "f-`(insert a B) = (f-`{a}) Un (f-`B)";
by (Blast_tac 1);
qed "vimage_insert";
Goal "f-`(A-B) = (f-`A) - (f-`B)";
by (Blast_tac 1);
qed "vimage_Diff";
Goal "f-`UNIV = UNIV";
by (Blast_tac 1);
qed "vimage_UNIV";
Addsimps [vimage_UNIV];
(*NOT suitable for rewriting*)
Goal "f-`B = (UN y: B. f-`{y})";
by (Blast_tac 1);
qed "vimage_eq_UN";
(*monotonicity*)
Goal "A<=B ==> f-`A <= f-`B";
by (Blast_tac 1);
qed "vimage_mono";