theory Inverse_Image converted and moved to Set;
authorwenzelm
Wed Nov 21 00:33:04 2001 +0100 (2001-11-21)
changeset 12257e3f7d6fb55d7
parent 12256 26243ebf2831
child 12258 5da24e7e9aba
theory Inverse_Image converted and moved to Set;
src/HOL/Inverse_Image.ML
src/HOL/Inverse_Image.thy
src/HOL/IsaMakefile
src/HOL/Set.ML
src/HOL/Set.thy
     1.1 --- a/src/HOL/Inverse_Image.ML	Wed Nov 21 00:32:10 2001 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,108 +0,0 @@
     1.4 -(*  Title:      HOL/Inverse_Image.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1998  University of Cambridge
     1.8 -
     1.9 -Inverse image of a function
    1.10 -*)
    1.11 -
    1.12 -(** Basic rules **)
    1.13 -
    1.14 -Goalw [vimage_def] "(a : f-`B) = (f a : B)";
    1.15 -by (Blast_tac 1) ;
    1.16 -qed "vimage_eq";
    1.17 -
    1.18 -Addsimps [vimage_eq];
    1.19 -
    1.20 -Goal "(a : f-`{b}) = (f a = b)";
    1.21 -by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
    1.22 -qed "vimage_singleton_eq";
    1.23 -
    1.24 -Goalw [vimage_def]
    1.25 -    "!!A B f. [| f a = b;  b:B |] ==> a : f-`B";
    1.26 -by (Blast_tac 1) ;
    1.27 -qed "vimageI";
    1.28 -
    1.29 -Goalw [vimage_def] "f a : A ==> a : f -` A";
    1.30 -by (Fast_tac 1);
    1.31 -qed "vimageI2";
    1.32 -
    1.33 -val major::prems = Goalw [vimage_def]
    1.34 -    "[| a: f-`B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
    1.35 -by (rtac (major RS CollectE) 1);
    1.36 -by (blast_tac (claset() addIs prems) 1) ;
    1.37 -qed "vimageE";
    1.38 -
    1.39 -Goalw [vimage_def] "a : f -` A ==> f a : A";
    1.40 -by (Fast_tac 1);
    1.41 -qed "vimageD";
    1.42 -
    1.43 -AddIs  [vimageI];
    1.44 -AddSEs [vimageE];
    1.45 -
    1.46 -
    1.47 -(*** Equations ***)
    1.48 -
    1.49 -Goal "f-`{} = {}";
    1.50 -by (Blast_tac 1);
    1.51 -qed "vimage_empty";
    1.52 -
    1.53 -Goal "f-`(-A) = -(f-`A)";
    1.54 -by (Blast_tac 1);
    1.55 -qed "vimage_Compl";
    1.56 -
    1.57 -Goal "f-`(A Un B) = (f-`A) Un (f-`B)";
    1.58 -by (Blast_tac 1);
    1.59 -qed "vimage_Un";
    1.60 -
    1.61 -Goal "f -` (A Int B) = (f -` A) Int (f -` B)";
    1.62 -by (Fast_tac 1);
    1.63 -qed "vimage_Int";
    1.64 -
    1.65 -Goal "f -` (Union A) = (UN X:A. f -` X)";
    1.66 -by (Blast_tac 1);
    1.67 -qed "vimage_Union";
    1.68 -
    1.69 -Goal "f-`(UN x:A. B x) = (UN x:A. f -` B x)";
    1.70 -by (Blast_tac 1);
    1.71 -qed "vimage_UN";
    1.72 -
    1.73 -Goal "f-`(INT x:A. B x) = (INT x:A. f -` B x)";
    1.74 -by (Blast_tac 1);
    1.75 -qed "vimage_INT";
    1.76 -
    1.77 -Goal "f -` Collect P = {y. P (f y)}";
    1.78 -by (Blast_tac 1);
    1.79 -qed "vimage_Collect_eq";
    1.80 -Addsimps [vimage_Collect_eq];
    1.81 -
    1.82 -(*A strange result used in Tools/inductive_package*)
    1.83 -val prems = Goal "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q";
    1.84 -by (force_tac (claset(), simpset() addsimps prems) 1);
    1.85 -qed "vimage_Collect";
    1.86 -
    1.87 -Addsimps [vimage_empty, vimage_Un, vimage_Int];
    1.88 -
    1.89 -(*NOT suitable for rewriting because of the recurrence of {a}*)
    1.90 -Goal "f-`(insert a B) = (f-`{a}) Un (f-`B)";
    1.91 -by (Blast_tac 1);
    1.92 -qed "vimage_insert";
    1.93 -
    1.94 -Goal "f-`(A-B) = (f-`A) - (f-`B)";
    1.95 -by (Blast_tac 1);
    1.96 -qed "vimage_Diff";
    1.97 -
    1.98 -Goal "f-`UNIV = UNIV";
    1.99 -by (Blast_tac 1);
   1.100 -qed "vimage_UNIV";
   1.101 -Addsimps [vimage_UNIV];
   1.102 -
   1.103 -(*NOT suitable for rewriting*)
   1.104 -Goal "f-`B = (UN y: B. f-`{y})";
   1.105 -by (Blast_tac 1);
   1.106 -qed "vimage_eq_UN";
   1.107 -
   1.108 -(*monotonicity*)
   1.109 -Goal "A<=B ==> f-`A <= f-`B";
   1.110 -by (Blast_tac 1);
   1.111 -qed "vimage_mono";
     2.1 --- a/src/HOL/Inverse_Image.thy	Wed Nov 21 00:32:10 2001 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,15 +0,0 @@
     2.4 -(*  Title:      HOL/Inverse_Image.thy
     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 -Inverse_Image = Set +
    2.13 -
    2.14 -constdefs
    2.15 -  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-`" 90)
    2.16 -    "f-`B  == {x. f(x) : B}"
    2.17 -
    2.18 -end
     3.1 --- a/src/HOL/IsaMakefile	Wed Nov 21 00:32:10 2001 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Wed Nov 21 00:33:04 2001 +0100
     3.3 @@ -87,8 +87,7 @@
     3.4    Integ/nat_bin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
     3.5    Integ/NatSimprocs.thy Integ/int_arith1.ML Integ/int_arith2.ML \
     3.6    Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
     3.7 -  Inverse_Image.ML Inverse_Image.thy Lfp.ML \
     3.8 -  Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
     3.9 +  Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
    3.10    Nat.thy NatArith.ML NatArith.thy NatDef.ML NatDef.thy Numeral.thy \
    3.11    Option.ML Option.thy Power.ML Power.thy PreList.thy \
    3.12    Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
     4.1 --- a/src/HOL/Set.ML	Wed Nov 21 00:32:10 2001 +0100
     4.2 +++ b/src/HOL/Set.ML	Wed Nov 21 00:33:04 2001 +0100
     4.3 @@ -24,3 +24,25 @@
     4.4    val set_diff_def = set_diff_def;
     4.5    val subset_def = subset_def;
     4.6  end;
     4.7 +
     4.8 +val vimageD = thm "vimageD";
     4.9 +val vimageE = thm "vimageE";
    4.10 +val vimageI = thm "vimageI";
    4.11 +val vimageI2 = thm "vimageI2";
    4.12 +val vimage_Collect = thm "vimage_Collect";
    4.13 +val vimage_Collect_eq = thm "vimage_Collect_eq";
    4.14 +val vimage_Compl = thm "vimage_Compl";
    4.15 +val vimage_Diff = thm "vimage_Diff";
    4.16 +val vimage_INT = thm "vimage_INT";
    4.17 +val vimage_Int = thm "vimage_Int";
    4.18 +val vimage_UN = thm "vimage_UN";
    4.19 +val vimage_UNIV = thm "vimage_UNIV";
    4.20 +val vimage_Un = thm "vimage_Un";
    4.21 +val vimage_Union = thm "vimage_Union";
    4.22 +val vimage_def = thm "vimage_def";
    4.23 +val vimage_empty = thm "vimage_empty";
    4.24 +val vimage_eq = thm "vimage_eq";
    4.25 +val vimage_eq_UN = thm "vimage_eq_UN";
    4.26 +val vimage_insert = thm "vimage_insert";
    4.27 +val vimage_mono = thm "vimage_mono";
    4.28 +val vimage_singleton_eq = thm "vimage_singleton_eq";
     5.1 --- a/src/HOL/Set.thy	Wed Nov 21 00:32:10 2001 +0100
     5.2 +++ b/src/HOL/Set.thy	Wed Nov 21 00:33:04 2001 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4  (*  Title:      HOL/Set.thy
     5.5      ID:         $Id$
     5.6 -    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     5.7 +    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     5.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5.9  *)
    5.10  
    5.11 @@ -187,11 +187,11 @@
    5.12    subset_def:   "A <= B         == ALL x:A. x:B"
    5.13    psubset_def:  "A < B          == (A::'a set) <= B & ~ A=B"
    5.14    Compl_def:    "- A            == {x. ~x:A}"
    5.15 +  set_diff_def: "A - B          == {x. x:A & ~x:B}"
    5.16  
    5.17  defs
    5.18    Un_def:       "A Un B         == {x. x:A | x:B}"
    5.19    Int_def:      "A Int B        == {x. x:A & x:B}"
    5.20 -  set_diff_def: "A - B          == {x. x:A & ~x:B}"
    5.21    INTER_def:    "INTER A B      == {y. ALL x:A. y: B(x)}"
    5.22    UNION_def:    "UNION A B      == {y. EX x:A. y: B(x)}"
    5.23    Inter_def:    "Inter S        == (INT x:S. x)"
    5.24 @@ -207,26 +207,22 @@
    5.25  
    5.26  subsubsection {* Relating predicates and sets *}
    5.27  
    5.28 -lemma CollectI [intro!]: "P(a) ==> a : {x. P(x)}"
    5.29 +lemma CollectI: "P(a) ==> a : {x. P(x)}"
    5.30    by simp
    5.31  
    5.32  lemma CollectD: "a : {x. P(x)} ==> P(a)"
    5.33    by simp
    5.34  
    5.35 -lemma set_ext: "(!!x. (x:A) = (x:B)) ==> A = B"
    5.36 -proof -
    5.37 -  case rule_context
    5.38 -  show ?thesis
    5.39 -    apply (rule prems [THEN ext, THEN arg_cong, THEN box_equals])
    5.40 -     apply (rule Collect_mem_eq)
    5.41 -    apply (rule Collect_mem_eq)
    5.42 -    done
    5.43 -qed
    5.44 +lemma set_ext: (assumes prem: "(!!x. (x:A) = (x:B))") "A = B"
    5.45 +  apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
    5.46 +   apply (rule Collect_mem_eq)
    5.47 +  apply (rule Collect_mem_eq)
    5.48 +  done
    5.49  
    5.50  lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
    5.51    by simp
    5.52  
    5.53 -lemmas CollectE [elim!] = CollectD [elim_format]
    5.54 +lemmas CollectE = CollectD [elim_format]
    5.55  
    5.56  
    5.57  subsubsection {* Bounded quantifiers *}
    5.58 @@ -905,6 +901,82 @@
    5.59    done
    5.60  
    5.61  
    5.62 +subsection {* Inverse image of a function *}
    5.63 +
    5.64 +constdefs
    5.65 +  vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
    5.66 +  "f -` B == {x. f x : B}"
    5.67 +
    5.68 +
    5.69 +subsubsection {* Basic rules *}
    5.70 +
    5.71 +lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
    5.72 +  by (unfold vimage_def) blast
    5.73 +
    5.74 +lemma vimage_singleton_eq: "(a : f -` {b}) = (f a = b)"
    5.75 +  by simp
    5.76 +
    5.77 +lemma vimageI [intro]: "f a = b ==> b:B ==> a : f -` B"
    5.78 +  by (unfold vimage_def) blast
    5.79 +
    5.80 +lemma vimageI2: "f a : A ==> a : f -` A"
    5.81 +  by (unfold vimage_def) fast
    5.82 +
    5.83 +lemma vimageE [elim!]: "a: f -` B ==> (!!x. f a = x ==> x:B ==> P) ==> P"
    5.84 +  by (unfold vimage_def) blast
    5.85 +
    5.86 +lemma vimageD: "a : f -` A ==> f a : A"
    5.87 +  by (unfold vimage_def) fast
    5.88 +
    5.89 +
    5.90 +subsubsection {* Equations *}
    5.91 +
    5.92 +lemma vimage_empty [simp]: "f -` {} = {}"
    5.93 +  by blast
    5.94 +
    5.95 +lemma vimage_Compl: "f -` (-A) = -(f -` A)"
    5.96 +  by blast
    5.97 +
    5.98 +lemma vimage_Un [simp]: "f -` (A Un B) = (f -` A) Un (f -` B)"
    5.99 +  by blast
   5.100 +
   5.101 +lemma vimage_Int [simp]: "f -` (A Int B) = (f -` A) Int (f -` B)"
   5.102 +  by fast
   5.103 +
   5.104 +lemma vimage_Union: "f -` (Union A) = (UN X:A. f -` X)"
   5.105 +  by blast
   5.106 +
   5.107 +lemma vimage_UN: "f-`(UN x:A. B x) = (UN x:A. f -` B x)"
   5.108 +  by blast
   5.109 +
   5.110 +lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)"
   5.111 +  by blast
   5.112 +
   5.113 +lemma vimage_Collect_eq [simp]: "f -` Collect P = {y. P (f y)}"
   5.114 +  by blast
   5.115 +
   5.116 +lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q"
   5.117 +  by blast
   5.118 +
   5.119 +lemma vimage_insert: "f-`(insert a B) = (f-`{a}) Un (f-`B)"
   5.120 +  -- {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *}
   5.121 +  by blast
   5.122 +
   5.123 +lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)"
   5.124 +  by blast
   5.125 +
   5.126 +lemma vimage_UNIV [simp]: "f -` UNIV = UNIV"
   5.127 +  by blast
   5.128 +
   5.129 +lemma vimage_eq_UN: "f-`B = (UN y: B. f-`{y})"
   5.130 +  -- {* NOT suitable for rewriting *}
   5.131 +  by blast
   5.132 +
   5.133 +lemma vimage_mono: "A <= B ==> f -` A <= f -` B"
   5.134 +  -- {* monotonicity *}
   5.135 +  by blast
   5.136 +
   5.137 +
   5.138  subsection {* Transitivity rules for calculational reasoning *}
   5.139  
   5.140  lemma forw_subst: "a = b ==> P b ==> P a"