converted domrange to Isar and merged with equalities
authorpaulson
Tue May 21 13:06:36 2002 +0200 (2002-05-21)
changeset 13168afcbca3498b0
parent 13167 7157c6d47aa4
child 13169 394a6c649547
converted domrange to Isar and merged with equalities
src/ZF/Fixedpt.thy
src/ZF/IsaMakefile
src/ZF/Rel.thy
src/ZF/equalities.thy
src/ZF/func.thy
     1.1 --- a/src/ZF/Fixedpt.thy	Mon May 20 12:59:59 2002 +0200
     1.2 +++ b/src/ZF/Fixedpt.thy	Tue May 21 13:06:36 2002 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  Least and greatest fixed points
     1.5  *)
     1.6  
     1.7 -Fixedpt = domrange +
     1.8 +Fixedpt = equalities +
     1.9  
    1.10  consts
    1.11    bnd_mono    :: [i,i=>i]=>o
     2.1 --- a/src/ZF/IsaMakefile	Mon May 20 12:59:59 2002 +0200
     2.2 +++ b/src/ZF/IsaMakefile	Tue May 21 13:06:36 2002 +0200
     2.3 @@ -45,8 +45,7 @@
     2.4    Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
     2.5    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
     2.6    Trancl.ML Trancl.thy Univ.thy Update.ML Update.thy \
     2.7 -  WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML domrange.ML	\
     2.8 -  domrange.thy equalities.thy func.thy		\
     2.9 +  WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy	\
    2.10    ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML		\
    2.11    subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
    2.12  	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
     3.1 --- a/src/ZF/Rel.thy	Mon May 20 12:59:59 2002 +0200
     3.2 +++ b/src/ZF/Rel.thy	Tue May 21 13:06:36 2002 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  Relations in Zermelo-Fraenkel Set Theory 
     3.5  *)
     3.6  
     3.7 -Rel = domrange +
     3.8 +Rel = equalities +
     3.9  consts
    3.10      refl,irrefl,equiv      :: [i,i]=>o
    3.11      sym,asym,antisym,trans :: i=>o
     4.1 --- a/src/ZF/equalities.thy	Mon May 20 12:59:59 2002 +0200
     4.2 +++ b/src/ZF/equalities.thy	Tue May 21 13:06:36 2002 +0200
     4.3 @@ -3,11 +3,228 @@
     4.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.5      Copyright   1992  University of Cambridge
     4.6  
     4.7 -Set Theory examples: Union, Intersection, Inclusion, etc.
     4.8 +Converse, domain, range of a relation or function.
     4.9 +
    4.10 +And set theory equalities involving Union, Intersection, Inclusion, etc.
    4.11      (Thanks also to Philippe de Groote.)
    4.12  *)
    4.13  
    4.14 -theory equalities = domrange:
    4.15 +theory equalities = pair + subset:
    4.16 +
    4.17 +
    4.18 +(*** converse ***)
    4.19 +
    4.20 +lemma converse_iff [iff]: "<a,b>: converse(r) <-> <b,a>:r"
    4.21 +apply (unfold converse_def)
    4.22 +apply blast
    4.23 +done
    4.24 +
    4.25 +lemma converseI: "<a,b>:r ==> <b,a>:converse(r)"
    4.26 +apply (unfold converse_def)
    4.27 +apply blast
    4.28 +done
    4.29 +
    4.30 +lemma converseD: "<a,b> : converse(r) ==> <b,a> : r"
    4.31 +apply (unfold converse_def)
    4.32 +apply blast
    4.33 +done
    4.34 +
    4.35 +lemma converseE [elim!]:
    4.36 +    "[| yx : converse(r);   
    4.37 +        !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P |]
    4.38 +     ==> P"
    4.39 +apply (unfold converse_def)
    4.40 +apply (blast intro: elim:); 
    4.41 +done
    4.42 +
    4.43 +lemma converse_converse: "r<=Sigma(A,B) ==> converse(converse(r)) = r"
    4.44 +apply blast
    4.45 +done
    4.46 +
    4.47 +lemma converse_type: "r<=A*B ==> converse(r)<=B*A"
    4.48 +apply blast
    4.49 +done
    4.50 +
    4.51 +lemma converse_prod [simp]: "converse(A*B) = B*A"
    4.52 +apply blast
    4.53 +done
    4.54 +
    4.55 +lemma converse_empty [simp]: "converse(0) = 0"
    4.56 +apply blast
    4.57 +done
    4.58 +
    4.59 +lemma converse_subset_iff: "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
    4.60 +apply blast
    4.61 +done
    4.62 +
    4.63 +
    4.64 +(*** domain ***)
    4.65 +
    4.66 +lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>: r)"
    4.67 +apply (unfold domain_def)
    4.68 +apply blast
    4.69 +done
    4.70 +
    4.71 +lemma domainI [intro]: "<a,b>: r ==> a: domain(r)"
    4.72 +apply (unfold domain_def)
    4.73 +apply blast
    4.74 +done
    4.75 +
    4.76 +lemma domainE [elim!]:
    4.77 +    "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
    4.78 +apply (unfold domain_def)
    4.79 +apply blast
    4.80 +done
    4.81 +
    4.82 +lemma domain_subset: "domain(Sigma(A,B)) <= A"
    4.83 +apply blast
    4.84 +done
    4.85 +
    4.86 +(*** range ***)
    4.87 +
    4.88 +lemma rangeI [intro]: "<a,b>: r ==> b : range(r)"
    4.89 +apply (unfold range_def)
    4.90 +apply (erule converseI [THEN domainI])
    4.91 +done
    4.92 +
    4.93 +lemma rangeE [elim!]: "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
    4.94 +apply (unfold range_def)
    4.95 +apply (blast intro: elim:); 
    4.96 +done
    4.97 +
    4.98 +lemma range_subset: "range(A*B) <= B"
    4.99 +apply (unfold range_def)
   4.100 +apply (subst converse_prod)
   4.101 +apply (rule domain_subset)
   4.102 +done
   4.103 +
   4.104 +
   4.105 +(*** field ***)
   4.106 +
   4.107 +lemma fieldI1: "<a,b>: r ==> a : field(r)"
   4.108 +apply (unfold field_def)
   4.109 +apply blast
   4.110 +done
   4.111 +
   4.112 +lemma fieldI2: "<a,b>: r ==> b : field(r)"
   4.113 +apply (unfold field_def)
   4.114 +apply blast
   4.115 +done
   4.116 +
   4.117 +lemma fieldCI [intro]: 
   4.118 +    "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
   4.119 +apply (unfold field_def)
   4.120 +apply blast
   4.121 +done
   4.122 +
   4.123 +lemma fieldE [elim!]: 
   4.124 +     "[| a : field(r);   
   4.125 +         !!x. <a,x>: r ==> P;   
   4.126 +         !!x. <x,a>: r ==> P        |] ==> P"
   4.127 +apply (unfold field_def)
   4.128 +apply blast
   4.129 +done
   4.130 +
   4.131 +lemma field_subset: "field(A*B) <= A Un B"
   4.132 +apply blast
   4.133 +done
   4.134 +
   4.135 +lemma domain_subset_field: "domain(r) <= field(r)"
   4.136 +apply (unfold field_def)
   4.137 +apply (rule Un_upper1)
   4.138 +done
   4.139 +
   4.140 +lemma range_subset_field: "range(r) <= field(r)"
   4.141 +apply (unfold field_def)
   4.142 +apply (rule Un_upper2)
   4.143 +done
   4.144 +
   4.145 +lemma domain_times_range: "r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
   4.146 +apply blast
   4.147 +done
   4.148 +
   4.149 +lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)"
   4.150 +apply blast
   4.151 +done
   4.152 +
   4.153 +
   4.154 +(*** Image of a set under a function/relation ***)
   4.155 +
   4.156 +lemma image_iff: "b : r``A <-> (EX x:A. <x,b>:r)"
   4.157 +apply (unfold image_def)
   4.158 +apply blast
   4.159 +done
   4.160 +
   4.161 +lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r"
   4.162 +apply (rule image_iff [THEN iff_trans])
   4.163 +apply blast
   4.164 +done
   4.165 +
   4.166 +lemma imageI [intro]: "[| <a,b>: r;  a:A |] ==> b : r``A"
   4.167 +apply (unfold image_def)
   4.168 +apply blast
   4.169 +done
   4.170 +
   4.171 +lemma imageE [elim!]: 
   4.172 +    "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
   4.173 +apply (unfold image_def)
   4.174 +apply blast
   4.175 +done
   4.176 +
   4.177 +lemma image_subset: "r <= A*B ==> r``C <= B"
   4.178 +apply blast
   4.179 +done
   4.180 +
   4.181 +
   4.182 +(*** Inverse image of a set under a function/relation ***)
   4.183 +
   4.184 +lemma vimage_iff: 
   4.185 +    "a : r-``B <-> (EX y:B. <a,y>:r)"
   4.186 +apply (unfold vimage_def image_def converse_def)
   4.187 +apply blast
   4.188 +done
   4.189 +
   4.190 +lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r"
   4.191 +apply (rule vimage_iff [THEN iff_trans])
   4.192 +apply blast
   4.193 +done
   4.194 +
   4.195 +lemma vimageI [intro]: "[| <a,b>: r;  b:B |] ==> a : r-``B"
   4.196 +apply (unfold vimage_def)
   4.197 +apply blast
   4.198 +done
   4.199 +
   4.200 +lemma vimageE [elim!]: 
   4.201 +    "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P"
   4.202 +apply (unfold vimage_def)
   4.203 +apply blast
   4.204 +done
   4.205 +
   4.206 +lemma vimage_subset: "r <= A*B ==> r-``C <= A"
   4.207 +apply (unfold vimage_def)
   4.208 +apply (erule converse_type [THEN image_subset])
   4.209 +done
   4.210 +
   4.211 +
   4.212 +(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
   4.213 +lemma rel_Union: "(ALL x:S. EX A B. x <= A*B) ==>   
   4.214 +                  Union(S) <= domain(Union(S)) * range(Union(S))"
   4.215 +by blast
   4.216 +
   4.217 +(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
   4.218 +lemma rel_Un: "[| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
   4.219 +apply blast
   4.220 +done
   4.221 +
   4.222 +lemma domain_Diff_eq: "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
   4.223 +apply blast
   4.224 +done
   4.225 +
   4.226 +lemma range_Diff_eq: "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)"
   4.227 +apply blast
   4.228 +done
   4.229 +
   4.230 +
   4.231  
   4.232  (** Finite Sets **)
   4.233  
   4.234 @@ -593,6 +810,47 @@
   4.235  
   4.236  ML
   4.237  {*
   4.238 +val ZF_cs = claset() delrules [equalityI];
   4.239 +
   4.240 +val converse_iff = thm "converse_iff";
   4.241 +val converseI = thm "converseI";
   4.242 +val converseD = thm "converseD";
   4.243 +val converseE = thm "converseE";
   4.244 +val converse_converse = thm "converse_converse";
   4.245 +val converse_type = thm "converse_type";
   4.246 +val converse_prod = thm "converse_prod";
   4.247 +val converse_empty = thm "converse_empty";
   4.248 +val converse_subset_iff = thm "converse_subset_iff";
   4.249 +val domain_iff = thm "domain_iff";
   4.250 +val domainI = thm "domainI";
   4.251 +val domainE = thm "domainE";
   4.252 +val domain_subset = thm "domain_subset";
   4.253 +val rangeI = thm "rangeI";
   4.254 +val rangeE = thm "rangeE";
   4.255 +val range_subset = thm "range_subset";
   4.256 +val fieldI1 = thm "fieldI1";
   4.257 +val fieldI2 = thm "fieldI2";
   4.258 +val fieldCI = thm "fieldCI";
   4.259 +val fieldE = thm "fieldE";
   4.260 +val field_subset = thm "field_subset";
   4.261 +val domain_subset_field = thm "domain_subset_field";
   4.262 +val range_subset_field = thm "range_subset_field";
   4.263 +val domain_times_range = thm "domain_times_range";
   4.264 +val field_times_field = thm "field_times_field";
   4.265 +val image_iff = thm "image_iff";
   4.266 +val image_singleton_iff = thm "image_singleton_iff";
   4.267 +val imageI = thm "imageI";
   4.268 +val imageE = thm "imageE";
   4.269 +val image_subset = thm "image_subset";
   4.270 +val vimage_iff = thm "vimage_iff";
   4.271 +val vimage_singleton_iff = thm "vimage_singleton_iff";
   4.272 +val vimageI = thm "vimageI";
   4.273 +val vimageE = thm "vimageE";
   4.274 +val vimage_subset = thm "vimage_subset";
   4.275 +val rel_Union = thm "rel_Union";
   4.276 +val rel_Un = thm "rel_Un";
   4.277 +val domain_Diff_eq = thm "domain_Diff_eq";
   4.278 +val range_Diff_eq = thm "range_Diff_eq";
   4.279  val cons_eq = thm "cons_eq";
   4.280  val cons_commute = thm "cons_commute";
   4.281  val cons_absorb = thm "cons_absorb";
     5.1 --- a/src/ZF/func.thy	Mon May 20 12:59:59 2002 +0200
     5.2 +++ b/src/ZF/func.thy	Tue May 21 13:06:36 2002 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  Functions in Zermelo-Fraenkel Set Theory
     5.5  *)
     5.6  
     5.7 -theory func = domrange + equalities:
     5.8 +theory func = equalities:
     5.9  
    5.10  (*** The Pi operator -- dependent function space ***)
    5.11