# HG changeset patch
# User wenzelm
# Date 1006299184 -3600
# Node ID e3f7d6fb55d76f735b3a60c21063b03a76e9abbb
# Parent  26243ebf2831d919c222db133cf26afba15e82ef
theory Inverse_Image converted and moved to Set;

diff -r 26243ebf2831 -r e3f7d6fb55d7 src/HOL/Inverse_Image.ML
--- a/src/HOL/Inverse_Image.ML	Wed Nov 21 00:32:10 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,108 +0,0 @@
-(*  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";
diff -r 26243ebf2831 -r e3f7d6fb55d7 src/HOL/Inverse_Image.thy
--- a/src/HOL/Inverse_Image.thy	Wed Nov 21 00:32:10 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      HOL/Inverse_Image.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Inverse image of a function
-*)
-
-Inverse_Image = Set +
-
-constdefs
-  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-`" 90)
-    "f-`B  == {x. f(x) : B}"
-
-end
diff -r 26243ebf2831 -r e3f7d6fb55d7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Nov 21 00:32:10 2001 +0100
+++ b/src/HOL/IsaMakefile	Wed Nov 21 00:33:04 2001 +0100
@@ -87,8 +87,7 @@
   Integ/nat_bin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
   Integ/NatSimprocs.thy Integ/int_arith1.ML Integ/int_arith2.ML \
   Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
-  Inverse_Image.ML Inverse_Image.thy Lfp.ML \
-  Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
+  Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
   Nat.thy NatArith.ML NatArith.thy NatDef.ML NatDef.thy Numeral.thy \
   Option.ML Option.thy Power.ML Power.thy PreList.thy \
   Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
diff -r 26243ebf2831 -r e3f7d6fb55d7 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Nov 21 00:32:10 2001 +0100
+++ b/src/HOL/Set.ML	Wed Nov 21 00:33:04 2001 +0100
@@ -24,3 +24,25 @@
   val set_diff_def = set_diff_def;
   val subset_def = subset_def;
 end;
+
+val vimageD = thm "vimageD";
+val vimageE = thm "vimageE";
+val vimageI = thm "vimageI";
+val vimageI2 = thm "vimageI2";
+val vimage_Collect = thm "vimage_Collect";
+val vimage_Collect_eq = thm "vimage_Collect_eq";
+val vimage_Compl = thm "vimage_Compl";
+val vimage_Diff = thm "vimage_Diff";
+val vimage_INT = thm "vimage_INT";
+val vimage_Int = thm "vimage_Int";
+val vimage_UN = thm "vimage_UN";
+val vimage_UNIV = thm "vimage_UNIV";
+val vimage_Un = thm "vimage_Un";
+val vimage_Union = thm "vimage_Union";
+val vimage_def = thm "vimage_def";
+val vimage_empty = thm "vimage_empty";
+val vimage_eq = thm "vimage_eq";
+val vimage_eq_UN = thm "vimage_eq_UN";
+val vimage_insert = thm "vimage_insert";
+val vimage_mono = thm "vimage_mono";
+val vimage_singleton_eq = thm "vimage_singleton_eq";
diff -r 26243ebf2831 -r e3f7d6fb55d7 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Nov 21 00:32:10 2001 +0100
+++ b/src/HOL/Set.thy	Wed Nov 21 00:33:04 2001 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Set.thy
     ID:         $Id$
-    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
+    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
@@ -187,11 +187,11 @@
   subset_def:   "A <= B         == ALL x:A. x:B"
   psubset_def:  "A < B          == (A::'a set) <= B & ~ A=B"
   Compl_def:    "- A            == {x. ~x:A}"
+  set_diff_def: "A - B          == {x. x:A & ~x:B}"
 
 defs
   Un_def:       "A Un B         == {x. x:A | x:B}"
   Int_def:      "A Int B        == {x. x:A & x:B}"
-  set_diff_def: "A - B          == {x. x:A & ~x:B}"
   INTER_def:    "INTER A B      == {y. ALL x:A. y: B(x)}"
   UNION_def:    "UNION A B      == {y. EX x:A. y: B(x)}"
   Inter_def:    "Inter S        == (INT x:S. x)"
@@ -207,26 +207,22 @@
 
 subsubsection {* Relating predicates and sets *}
 
-lemma CollectI [intro!]: "P(a) ==> a : {x. P(x)}"
+lemma CollectI: "P(a) ==> a : {x. P(x)}"
   by simp
 
 lemma CollectD: "a : {x. P(x)} ==> P(a)"
   by simp
 
-lemma set_ext: "(!!x. (x:A) = (x:B)) ==> A = B"
-proof -
-  case rule_context
-  show ?thesis
-    apply (rule prems [THEN ext, THEN arg_cong, THEN box_equals])
-     apply (rule Collect_mem_eq)
-    apply (rule Collect_mem_eq)
-    done
-qed
+lemma set_ext: (assumes prem: "(!!x. (x:A) = (x:B))") "A = B"
+  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
+   apply (rule Collect_mem_eq)
+  apply (rule Collect_mem_eq)
+  done
 
 lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
   by simp
 
-lemmas CollectE [elim!] = CollectD [elim_format]
+lemmas CollectE = CollectD [elim_format]
 
 
 subsubsection {* Bounded quantifiers *}
@@ -905,6 +901,82 @@
   done
 
 
+subsection {* Inverse image of a function *}
+
+constdefs
+  vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
+  "f -` B == {x. f x : B}"
+
+
+subsubsection {* Basic rules *}
+
+lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
+  by (unfold vimage_def) blast
+
+lemma vimage_singleton_eq: "(a : f -` {b}) = (f a = b)"
+  by simp
+
+lemma vimageI [intro]: "f a = b ==> b:B ==> a : f -` B"
+  by (unfold vimage_def) blast
+
+lemma vimageI2: "f a : A ==> a : f -` A"
+  by (unfold vimage_def) fast
+
+lemma vimageE [elim!]: "a: f -` B ==> (!!x. f a = x ==> x:B ==> P) ==> P"
+  by (unfold vimage_def) blast
+
+lemma vimageD: "a : f -` A ==> f a : A"
+  by (unfold vimage_def) fast
+
+
+subsubsection {* Equations *}
+
+lemma vimage_empty [simp]: "f -` {} = {}"
+  by blast
+
+lemma vimage_Compl: "f -` (-A) = -(f -` A)"
+  by blast
+
+lemma vimage_Un [simp]: "f -` (A Un B) = (f -` A) Un (f -` B)"
+  by blast
+
+lemma vimage_Int [simp]: "f -` (A Int B) = (f -` A) Int (f -` B)"
+  by fast
+
+lemma vimage_Union: "f -` (Union A) = (UN X:A. f -` X)"
+  by blast
+
+lemma vimage_UN: "f-`(UN x:A. B x) = (UN x:A. f -` B x)"
+  by blast
+
+lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)"
+  by blast
+
+lemma vimage_Collect_eq [simp]: "f -` Collect P = {y. P (f y)}"
+  by blast
+
+lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q"
+  by blast
+
+lemma vimage_insert: "f-`(insert a B) = (f-`{a}) Un (f-`B)"
+  -- {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *}
+  by blast
+
+lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)"
+  by blast
+
+lemma vimage_UNIV [simp]: "f -` UNIV = UNIV"
+  by blast
+
+lemma vimage_eq_UN: "f-`B = (UN y: B. f-`{y})"
+  -- {* NOT suitable for rewriting *}
+  by blast
+
+lemma vimage_mono: "A <= B ==> f -` A <= f -` B"
+  -- {* monotonicity *}
+  by blast
+
+
 subsection {* Transitivity rules for calculational reasoning *}
 
 lemma forw_subst: "a = b ==> P b ==> P a"