--- 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";
--- 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
--- 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 \
--- 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";
--- 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"