conversion of equalities and WF to Isar
authorpaulson
Mon May 20 11:45:57 2002 +0200 (2002-05-20)
changeset 1316531d020705aff
parent 13164 dfc399c684e4
child 13166 9e9032657a0f
conversion of equalities and WF to Isar
src/ZF/IsaMakefile
src/ZF/WF.thy
src/ZF/equalities.thy
     1.1 --- a/src/ZF/IsaMakefile	Sat May 18 22:22:23 2002 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Mon May 20 11:45:57 2002 +0200
     1.3 @@ -44,9 +44,9 @@
     1.4    Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
     1.5    Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
     1.6    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
     1.7 -  Trancl.ML Trancl.thy Univ.thy Update.ML Update.thy WF.ML	\
     1.8 +  Trancl.ML Trancl.thy Univ.thy Update.ML Update.thy \
     1.9    WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML domrange.ML	\
    1.10 -  domrange.thy equalities.ML equalities.thy func.thy		\
    1.11 +  domrange.thy equalities.thy func.thy		\
    1.12    ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML		\
    1.13    subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
    1.14  	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
     2.1 --- a/src/ZF/WF.thy	Sat May 18 22:22:23 2002 +0200
     2.2 +++ b/src/ZF/WF.thy	Mon May 20 11:45:57 2002 +0200
     2.3 @@ -1,38 +1,394 @@
     2.4 -(*  Title:      ZF/wf.thy
     2.5 +(*  Title:      ZF/WF.thy
     2.6      ID:         $Id$
     2.7      Author:     Tobias Nipkow and Lawrence C Paulson
     2.8      Copyright   1994  University of Cambridge
     2.9  
    2.10  Well-founded Recursion
    2.11 +
    2.12 +Derived first for transitive relations, and finally for arbitrary WF relations
    2.13 +via wf_trancl and trans_trancl.
    2.14 +
    2.15 +It is difficult to derive this general case directly, using r^+ instead of
    2.16 +r.  In is_recfun, the two occurrences of the relation must have the same
    2.17 +form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
    2.18 +r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
    2.19 +principle, but harder to use, especially to prove wfrec_eclose_eq in
    2.20 +epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
    2.21 +a mess.
    2.22  *)
    2.23  
    2.24 -WF = Trancl + mono + equalities +
    2.25 -consts
    2.26 -  wf           :: i=>o
    2.27 -  wf_on        :: [i,i]=>o                      ("wf[_]'(_')")
    2.28 +theory WF = Trancl + mono + equalities:
    2.29 +
    2.30 +constdefs
    2.31 +  wf           :: "i=>o"
    2.32 +    (*r is a well-founded relation*)
    2.33 +    "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
    2.34 +
    2.35 +  wf_on        :: "[i,i]=>o"                      ("wf[_]'(_')")
    2.36 +    (*r is well-founded on A*)
    2.37 +    "wf_on(A,r) == wf(r Int A*A)"
    2.38 +
    2.39 +  is_recfun    :: "[i, i, [i,i]=>i, i] =>o"
    2.40 +    "is_recfun(r,a,H,f) == (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
    2.41 +
    2.42 +  the_recfun   :: "[i, i, [i,i]=>i] =>i"
    2.43 +    "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))"
    2.44 +
    2.45 +  wftrec :: "[i, i, [i,i]=>i] =>i"
    2.46 +    "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
    2.47 +
    2.48 +  wfrec :: "[i, i, [i,i]=>i] =>i"
    2.49 +    (*public version.  Does not require r to be transitive*)
    2.50 +    "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
    2.51 +
    2.52 +  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"       ("wfrec[_]'(_,_,_')")
    2.53 +    "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)"
    2.54 +
    2.55 +
    2.56 +(*** Well-founded relations ***)
    2.57 +
    2.58 +(** Equivalences between wf and wf_on **)
    2.59 +
    2.60 +lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
    2.61 +apply (unfold wf_def wf_on_def, clarify) (*needed for blast's efficiency*)
    2.62 +apply blast
    2.63 +done
    2.64 +
    2.65 +lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
    2.66 +by (unfold wf_def wf_on_def, fast)
    2.67 +
    2.68 +lemma wf_iff_wf_on_field: "wf(r) <-> wf[field(r)](r)"
    2.69 +by (blast intro: wf_imp_wf_on wf_on_field_imp_wf)
    2.70 +
    2.71 +lemma wf_on_subset_A: "[| wf[A](r);  B<=A |] ==> wf[B](r)"
    2.72 +by (unfold wf_on_def wf_def, fast)
    2.73 +
    2.74 +lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)"
    2.75 +by (unfold wf_on_def wf_def, fast)
    2.76 +
    2.77 +(** Introduction rules for wf_on **)
    2.78 +
    2.79 +lemma wf_onI:
    2.80 +(*If every non-empty subset of A has an r-minimal element then wf[A](r).*)
    2.81 + assumes prem: "!!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False"
    2.82 + shows         "wf[A](r)"
    2.83 +apply (unfold wf_on_def wf_def)
    2.84 +apply (rule equals0I [THEN disjCI, THEN allI])
    2.85 +apply (rule_tac Z = "Z" in prem, blast+)
    2.86 +done
    2.87 +
    2.88 +(*If r allows well-founded induction over A then wf[A](r)
    2.89 +  Premise is equivalent to
    2.90 +  !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B  *)
    2.91 +lemma wf_onI2:
    2.92 + assumes prem: "!!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A |]
    2.93 +                       ==> y:B"
    2.94 + shows         "wf[A](r)"
    2.95 +apply (rule wf_onI)
    2.96 +apply (rule_tac c=u in prem [THEN DiffE])
    2.97 +  prefer 3 apply blast 
    2.98 + apply fast+
    2.99 +done
   2.100 +
   2.101 +
   2.102 +(** Well-founded Induction **)
   2.103 +
   2.104 +(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
   2.105 +lemma wf_induct:
   2.106 +    "[| wf(r);
   2.107 +        !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x)
   2.108 +     |]  ==>  P(a)"
   2.109 +apply (unfold wf_def) 
   2.110 +apply (erule_tac x = "{z:domain (r) Un {a}. ~P (z) }" in allE)
   2.111 +apply blast 
   2.112 +done
   2.113  
   2.114 -  wftrec,wfrec :: [i, i, [i,i]=>i] =>i
   2.115 -  wfrec_on     :: [i, i, i, [i,i]=>i] =>i       ("wfrec[_]'(_,_,_')")
   2.116 -  is_recfun    :: [i, i, [i,i]=>i, i] =>o
   2.117 -  the_recfun   :: [i, i, [i,i]=>i] =>i
   2.118 +(*The form of this rule is designed to match wfI*)
   2.119 +lemma wf_induct2:
   2.120 +    "[| wf(r);  a:A;  field(r)<=A;
   2.121 +        !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) |]
   2.122 +     ==>  P(a)"
   2.123 +apply (erule_tac P="a:A" in rev_mp)
   2.124 +apply (erule_tac a=a in wf_induct, blast) 
   2.125 +done
   2.126 +
   2.127 +lemma field_Int_square: "field(r Int A*A) <= A"
   2.128 +by blast
   2.129 +
   2.130 +lemma wf_on_induct:
   2.131 +    "[| wf[A](r);  a:A;
   2.132 +        !!x.[| x: A;  ALL y:A. <y,x>: r --> P(y) |] ==> P(x)
   2.133 +     |]  ==>  P(a)"
   2.134 +apply (unfold wf_on_def) 
   2.135 +apply (erule wf_induct2, assumption)
   2.136 +apply (rule field_Int_square, blast)
   2.137 +done
   2.138 +
   2.139 +(*If r allows well-founded induction then wf(r)*)
   2.140 +lemma wfI:
   2.141 +    "[| field(r)<=A;
   2.142 +        !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;  y:A|]
   2.143 +               ==> y:B |]
   2.144 +     ==>  wf(r)"
   2.145 +apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf])
   2.146 +apply (rule wf_onI2)
   2.147 + prefer 2 apply blast  
   2.148 +apply blast 
   2.149 +done
   2.150 +
   2.151 +
   2.152 +(*** Properties of well-founded relations ***)
   2.153 +
   2.154 +lemma wf_not_refl: "wf(r) ==> <a,a> ~: r"
   2.155 +by (erule_tac a=a in wf_induct, blast)
   2.156 +
   2.157 +lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. <a,x>:r --> <x,a> ~: r"
   2.158 +by (erule_tac a=a in wf_induct, blast)
   2.159 +
   2.160 +(* [| wf(r);  <a,x> : r;  ~P ==> <x,a> : r |] ==> P *)
   2.161 +lemmas wf_asym = wf_not_sym [THEN swap, standard]
   2.162 +
   2.163 +lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r"
   2.164 +apply (erule_tac a=a in wf_on_induct, assumption)
   2.165 +apply blast
   2.166 +done
   2.167  
   2.168 -defs
   2.169 -  (*r is a well-founded relation*)
   2.170 -  wf_def         "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
   2.171 +lemma wf_on_not_sym [rule_format]:
   2.172 +     "[| wf[A](r);  a:A |] ==> ALL b:A. <a,b>:r --> <b,a>~:r"
   2.173 +apply (erule_tac a=a in wf_on_induct, assumption)
   2.174 +apply blast
   2.175 +done
   2.176 +
   2.177 +lemma wf_on_asym:
   2.178 +     "[| wf[A](r);  ~Z ==> <a,b> : r;
   2.179 +         <b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z"
   2.180 +by (blast dest: wf_on_not_sym); 
   2.181 +
   2.182 +
   2.183 +(*Needed to prove well_ordI.  Could also reason that wf[A](r) means
   2.184 +  wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
   2.185 +lemma wf_on_chain3:
   2.186 +     "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P"
   2.187 +apply (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P",
   2.188 +       blast) 
   2.189 +apply (erule_tac a=a in wf_on_induct, assumption)
   2.190 +apply blast
   2.191 +done
   2.192 +
   2.193 +
   2.194 +
   2.195 +
   2.196 +(*transitive closure of a WF relation is WF provided A is downwards closed*)
   2.197 +lemma wf_on_trancl:
   2.198 +    "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
   2.199 +apply (rule wf_onI2)
   2.200 +apply (frule bspec [THEN mp], assumption+)
   2.201 +apply (erule_tac a = "y" in wf_on_induct, assumption)
   2.202 +apply (blast elim: tranclE, blast) 
   2.203 +done
   2.204 +
   2.205 +lemma wf_trancl: "wf(r) ==> wf(r^+)"
   2.206 +apply (simp add: wf_iff_wf_on_field)
   2.207 +apply (rule wf_on_subset_A) 
   2.208 + apply (erule wf_on_trancl)
   2.209 + apply blast 
   2.210 +apply (rule trancl_type [THEN field_rel_subset])
   2.211 +done
   2.212 +
   2.213 +
   2.214 +
   2.215 +(** r-``{a} is the set of everything under a in r **)
   2.216 +
   2.217 +lemmas underI = vimage_singleton_iff [THEN iffD2, standard]
   2.218 +lemmas underD = vimage_singleton_iff [THEN iffD1, standard]
   2.219 +
   2.220 +(** is_recfun **)
   2.221  
   2.222 -  (*r is well-founded relation over A*)
   2.223 -  wf_on_def      "wf_on(A,r) == wf(r Int A*A)"
   2.224 +lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)"
   2.225 +apply (unfold is_recfun_def)
   2.226 +apply (erule ssubst)
   2.227 +apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
   2.228 +done
   2.229 +
   2.230 +lemma apply_recfun:
   2.231 +    "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
   2.232 +apply (unfold is_recfun_def) 
   2.233 +apply (erule_tac P = "%x.?t (x) = (?u::i) " in ssubst)
   2.234 +apply (erule underI [THEN beta])
   2.235 +done
   2.236 +
   2.237 +lemma is_recfun_equal [rule_format]:
   2.238 +     "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |]
   2.239 +      ==> <x,a>:r --> <x,b>:r --> f`x=g`x"
   2.240 +apply (frule_tac f = "f" in is_recfun_type)
   2.241 +apply (frule_tac f = "g" in is_recfun_type)
   2.242 +apply (simp add: is_recfun_def)
   2.243 +apply (erule_tac a=x in wf_induct)
   2.244 +apply (intro impI)
   2.245 +apply (elim ssubst)
   2.246 +apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
   2.247 +apply (rule_tac t = "%z. H (?x,z) " in subst_context)
   2.248 +apply (subgoal_tac "ALL y : r-``{x}. ALL z. <y,z>:f <-> <y,z>:g")
   2.249 + apply (blast dest: transD)
   2.250 +apply (simp add: apply_iff)
   2.251 +apply (blast dest: transD intro: sym)
   2.252 +done
   2.253 +
   2.254 +lemma is_recfun_cut:
   2.255 +     "[| wf(r);  trans(r);
   2.256 +         is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |]
   2.257 +      ==> restrict(f, r-``{b}) = g"
   2.258 +apply (frule_tac f = "f" in is_recfun_type)
   2.259 +apply (rule fun_extension)
   2.260 +  apply (blast dest: transD intro: restrict_type2)
   2.261 + apply (erule is_recfun_type, simp)
   2.262 +apply (blast dest: transD intro: is_recfun_equal)
   2.263 +done
   2.264 +
   2.265 +(*** Main Existence Lemma ***)
   2.266  
   2.267 -  is_recfun_def  "is_recfun(r,a,H,f) == 
   2.268 -                        (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
   2.269 +lemma is_recfun_functional:
   2.270 +     "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g"
   2.271 +by (blast intro: fun_extension is_recfun_type is_recfun_equal)
   2.272 +
   2.273 +(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
   2.274 +lemma is_the_recfun:
   2.275 +    "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]
   2.276 +     ==> is_recfun(r, a, H, the_recfun(r,a,H))"
   2.277 +apply (unfold the_recfun_def)
   2.278 +apply (rule ex1I [THEN theI], assumption)
   2.279 +apply (blast intro: is_recfun_functional)
   2.280 +done
   2.281 +
   2.282 +lemma unfold_the_recfun:
   2.283 +     "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"
   2.284 +apply (rule_tac a=a in wf_induct, assumption)
   2.285 +apply (rename_tac a1) 
   2.286 +apply (rule_tac f = "lam y: r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
   2.287 +  apply typecheck
   2.288 +apply (unfold is_recfun_def wftrec_def)
   2.289 +(*Applying the substitution: must keep the quantified assumption!!*)
   2.290 +apply (rule lam_cong [OF refl]) 
   2.291 +apply (drule underD) 
   2.292 +apply (fold is_recfun_def)
   2.293 +apply (rule_tac t = "%z. H(?x,z)" in subst_context)
   2.294 +apply (rule fun_extension)
   2.295 +  apply (blast intro: is_recfun_type)
   2.296 + apply (rule lam_type [THEN restrict_type2])
   2.297 +  apply blast
   2.298 + apply (blast dest: transD)
   2.299 +apply (frule spec [THEN mp], assumption)
   2.300 +apply (subgoal_tac "<xa,a1> : r")
   2.301 + apply (drule_tac x1 = "xa" in spec [THEN mp], assumption)
   2.302 +apply (simp add: vimage_singleton_iff  underI [THEN beta] 
   2.303 +                 apply_recfun is_recfun_cut)
   2.304 +apply (blast dest: transD)
   2.305 +done
   2.306 +
   2.307 +
   2.308 +(*** Unfolding wftrec ***)
   2.309 +
   2.310 +lemma the_recfun_cut:
   2.311 +     "[| wf(r);  trans(r);  <b,a>:r |]
   2.312 +      ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
   2.313 +by (blast intro: is_recfun_cut unfold_the_recfun);
   2.314  
   2.315 -  the_recfun_def "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))"
   2.316 +(*NOT SUITABLE FOR REWRITING: it is recursive!*)
   2.317 +lemma wftrec:
   2.318 +    "[| wf(r);  trans(r) |] ==>
   2.319 +          wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))"
   2.320 +apply (unfold wftrec_def)
   2.321 +apply (subst unfold_the_recfun [unfolded is_recfun_def])
   2.322 +apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
   2.323 +done
   2.324 +
   2.325 +(** Removal of the premise trans(r) **)
   2.326 +
   2.327 +(*NOT SUITABLE FOR REWRITING: it is recursive!*)
   2.328 +lemma wfrec:
   2.329 +    "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))"
   2.330 +apply (unfold wfrec_def) 
   2.331 +apply (erule wf_trancl [THEN wftrec, THEN ssubst])
   2.332 + apply (rule trans_trancl)
   2.333 +apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context])
   2.334 + apply (erule r_into_trancl)
   2.335 +apply (rule subset_refl)
   2.336 +done
   2.337  
   2.338 -  wftrec_def     "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
   2.339 +(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   2.340 +lemma def_wfrec:
   2.341 +    "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==>
   2.342 +     h(a) = H(a, lam x: r-``{a}. h(x))"
   2.343 +apply simp
   2.344 +apply (elim wfrec) 
   2.345 +done
   2.346 +
   2.347 +lemma wfrec_type:
   2.348 +    "[| wf(r);  a:A;  field(r)<=A;
   2.349 +        !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)
   2.350 +     |] ==> wfrec(r,a,H) : B(a)"
   2.351 +apply (rule_tac a = "a" in wf_induct2, assumption+)
   2.352 +apply (subst wfrec, assumption)
   2.353 +apply (simp add: lam_type underD)  
   2.354 +done
   2.355 +
   2.356 +
   2.357 +lemma wfrec_on:
   2.358 + "[| wf[A](r);  a: A |] ==>
   2.359 +         wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))"
   2.360 +apply (unfold wf_on_def wfrec_on_def)
   2.361 +apply (erule wfrec [THEN trans])
   2.362 +apply (simp add: vimage_Int_square cons_subset_iff)
   2.363 +done
   2.364  
   2.365 -  (*public version.  Does not require r to be transitive*)
   2.366 -  wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
   2.367 +(*Minimal-element characterization of well-foundedness*)
   2.368 +lemma wf_eq_minimal:
   2.369 +     "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q))"
   2.370 +apply (unfold wf_def, blast)
   2.371 +done
   2.372 +
   2.373 +ML
   2.374 +{*
   2.375 +val wf_def = thm "wf_def";
   2.376 +val wf_on_def = thm "wf_on_def";
   2.377  
   2.378 -  wfrec_on_def   "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)"
   2.379 +val wf_imp_wf_on = thm "wf_imp_wf_on";
   2.380 +val wf_on_field_imp_wf = thm "wf_on_field_imp_wf";
   2.381 +val wf_iff_wf_on_field = thm "wf_iff_wf_on_field";
   2.382 +val wf_on_subset_A = thm "wf_on_subset_A";
   2.383 +val wf_on_subset_r = thm "wf_on_subset_r";
   2.384 +val wf_onI = thm "wf_onI";
   2.385 +val wf_onI2 = thm "wf_onI2";
   2.386 +val wf_induct = thm "wf_induct";
   2.387 +val wf_induct2 = thm "wf_induct2";
   2.388 +val field_Int_square = thm "field_Int_square";
   2.389 +val wf_on_induct = thm "wf_on_induct";
   2.390 +val wfI = thm "wfI";
   2.391 +val wf_not_refl = thm "wf_not_refl";
   2.392 +val wf_not_sym = thm "wf_not_sym";
   2.393 +val wf_asym = thm "wf_asym";
   2.394 +val wf_on_not_refl = thm "wf_on_not_refl";
   2.395 +val wf_on_not_sym = thm "wf_on_not_sym";
   2.396 +val wf_on_asym = thm "wf_on_asym";
   2.397 +val wf_on_chain3 = thm "wf_on_chain3";
   2.398 +val wf_on_trancl = thm "wf_on_trancl";
   2.399 +val wf_trancl = thm "wf_trancl";
   2.400 +val underI = thm "underI";
   2.401 +val underD = thm "underD";
   2.402 +val is_recfun_type = thm "is_recfun_type";
   2.403 +val apply_recfun = thm "apply_recfun";
   2.404 +val is_recfun_equal = thm "is_recfun_equal";
   2.405 +val is_recfun_cut = thm "is_recfun_cut";
   2.406 +val is_recfun_functional = thm "is_recfun_functional";
   2.407 +val is_the_recfun = thm "is_the_recfun";
   2.408 +val unfold_the_recfun = thm "unfold_the_recfun";
   2.409 +val the_recfun_cut = thm "the_recfun_cut";
   2.410 +val wftrec = thm "wftrec";
   2.411 +val wfrec = thm "wfrec";
   2.412 +val def_wfrec = thm "def_wfrec";
   2.413 +val wfrec_type = thm "wfrec_type";
   2.414 +val wfrec_on = thm "wfrec_on";
   2.415 +val wf_eq_minimal = thm "wf_eq_minimal";
   2.416 +*}
   2.417  
   2.418  end
     3.1 --- a/src/ZF/equalities.thy	Sat May 18 22:22:23 2002 +0200
     3.2 +++ b/src/ZF/equalities.thy	Mon May 20 11:45:57 2002 +0200
     3.3 @@ -1,4 +1,761 @@
     3.4 -(*Dummy theory to document dependencies *)
     3.5 +(*  Title:      ZF/equalities
     3.6 +    ID:         $Id$
     3.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.8 +    Copyright   1992  University of Cambridge
     3.9 +
    3.10 +Set Theory examples: Union, Intersection, Inclusion, etc.
    3.11 +    (Thanks also to Philippe de Groote.)
    3.12 +*)
    3.13 +
    3.14 +theory equalities = domrange:
    3.15 +
    3.16 +(** Finite Sets **)
    3.17 +
    3.18 +(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
    3.19 +lemma cons_eq: "{a} Un B = cons(a,B)"
    3.20 +by blast
    3.21 +
    3.22 +lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))"
    3.23 +by blast
    3.24 +
    3.25 +lemma cons_absorb: "a: B ==> cons(a,B) = B"
    3.26 +by blast
    3.27 +
    3.28 +lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
    3.29 +by blast
    3.30 +
    3.31 +lemma equal_singleton [rule_format]: "[| a: C;  ALL y:C. y=b |] ==> C = {b}"
    3.32 +by blast
    3.33 +
    3.34 +
    3.35 +(** Binary Intersection **)
    3.36 +
    3.37 +(*NOT an equality, but it seems to belong here...*)
    3.38 +lemma Int_cons: "cons(a,B) Int C <= cons(a, B Int C)"
    3.39 +by blast
    3.40 +
    3.41 +lemma Int_absorb [simp]: "A Int A = A"
    3.42 +by blast
    3.43 +
    3.44 +lemma Int_left_absorb: "A Int (A Int B) = A Int B"
    3.45 +by blast
    3.46 +
    3.47 +lemma Int_commute: "A Int B = B Int A"
    3.48 +by blast
    3.49 +
    3.50 +lemma Int_left_commute: "A Int (B Int C) = B Int (A Int C)"
    3.51 +by blast
    3.52 +
    3.53 +lemma Int_assoc: "(A Int B) Int C  =  A Int (B Int C)"
    3.54 +by blast
    3.55 +
    3.56 +(*Intersection is an AC-operator*)
    3.57 +lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute
    3.58 +
    3.59 +lemma Int_Un_distrib: "A Int (B Un C) = (A Int B) Un (A Int C)"
    3.60 +by blast
    3.61 +
    3.62 +lemma Int_Un_distrib2: "(B Un C) Int A = (B Int A) Un (C Int A)"
    3.63 +by blast
    3.64 +
    3.65 +lemma subset_Int_iff: "A<=B <-> A Int B = A"
    3.66 +by (blast elim!: equalityE)
    3.67 +
    3.68 +lemma subset_Int_iff2: "A<=B <-> B Int A = A"
    3.69 +by (blast elim!: equalityE)
    3.70 +
    3.71 +lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B"
    3.72 +by blast
    3.73 +
    3.74 +(** Binary Union **)
    3.75 +
    3.76 +lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)"
    3.77 +by blast
    3.78 +
    3.79 +lemma Un_absorb [simp]: "A Un A = A"
    3.80 +by blast
    3.81 +
    3.82 +lemma Un_left_absorb: "A Un (A Un B) = A Un B"
    3.83 +by blast
    3.84 +
    3.85 +lemma Un_commute: "A Un B = B Un A"
    3.86 +by blast
    3.87 +
    3.88 +lemma Un_left_commute: "A Un (B Un C) = B Un (A Un C)"
    3.89 +by blast
    3.90 +
    3.91 +lemma Un_assoc: "(A Un B) Un C  =  A Un (B Un C)"
    3.92 +by blast
    3.93 +
    3.94 +(*Union is an AC-operator*)
    3.95 +lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
    3.96 +
    3.97 +lemma Un_Int_distrib: "(A Int B) Un C  =  (A Un C) Int (B Un C)"
    3.98 +by blast
    3.99 +
   3.100 +lemma subset_Un_iff: "A<=B <-> A Un B = B"
   3.101 +by (blast elim!: equalityE)
   3.102 +
   3.103 +lemma subset_Un_iff2: "A<=B <-> B Un A = B"
   3.104 +by (blast elim!: equalityE)
   3.105 +
   3.106 +lemma Un_empty [iff]: "(A Un B = 0) <-> (A = 0 & B = 0)"
   3.107 +by blast
   3.108 +
   3.109 +lemma Un_eq_Union: "A Un B = Union({A, B})"
   3.110 +by blast
   3.111 +
   3.112 +(** Simple properties of Diff -- set difference **)
   3.113 +
   3.114 +lemma Diff_cancel: "A - A = 0"
   3.115 +by blast
   3.116 +
   3.117 +lemma Diff_triv: "A  Int B = 0 ==> A - B = A"
   3.118 +by blast
   3.119 +
   3.120 +lemma empty_Diff [simp]: "0 - A = 0"
   3.121 +by blast
   3.122 +
   3.123 +lemma Diff_0 [simp]: "A - 0 = A"
   3.124 +by blast
   3.125 +
   3.126 +lemma Diff_eq_0_iff: "A - B = 0 <-> A <= B"
   3.127 +by (blast elim: equalityE)
   3.128 +
   3.129 +(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
   3.130 +lemma Diff_cons: "A - cons(a,B) = A - B - {a}"
   3.131 +by blast
   3.132 +
   3.133 +(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
   3.134 +lemma Diff_cons2: "A - cons(a,B) = A - {a} - B"
   3.135 +by blast
   3.136 +
   3.137 +lemma Diff_disjoint: "A Int (B-A) = 0"
   3.138 +by blast
   3.139 +
   3.140 +lemma Diff_partition: "A<=B ==> A Un (B-A) = B"
   3.141 +by blast
   3.142 +
   3.143 +lemma subset_Un_Diff: "A <= B Un (A - B)"
   3.144 +by blast
   3.145 +
   3.146 +lemma double_complement: "[| A<=B; B<=C |] ==> B-(C-A) = A"
   3.147 +by blast
   3.148 +
   3.149 +lemma double_complement_Un: "(A Un B) - (B-A) = A"
   3.150 +by blast
   3.151 +
   3.152 +lemma Un_Int_crazy: 
   3.153 + "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"
   3.154 +apply blast
   3.155 +done
   3.156 +
   3.157 +lemma Diff_Un: "A - (B Un C) = (A-B) Int (A-C)"
   3.158 +by blast
   3.159 +
   3.160 +lemma Diff_Int: "A - (B Int C) = (A-B) Un (A-C)"
   3.161 +by blast
   3.162 +
   3.163 +lemma Un_Diff: "(A Un B) - C = (A - C) Un (B - C)"
   3.164 +by blast
   3.165 +
   3.166 +lemma Int_Diff: "(A Int B) - C = A Int (B - C)"
   3.167 +by blast
   3.168 +
   3.169 +lemma Diff_Int_distrib: "C Int (A-B) = (C Int A) - (C Int B)"
   3.170 +by blast
   3.171 +
   3.172 +lemma Diff_Int_distrib2: "(A-B) Int C = (A Int C) - (B Int C)"
   3.173 +by blast
   3.174 +
   3.175 +(*Halmos, Naive Set Theory, page 16.*)
   3.176 +lemma Un_Int_assoc_iff: "(A Int B) Un C = A Int (B Un C)  <->  C<=A"
   3.177 +by (blast elim!: equalityE)
   3.178 +
   3.179 +
   3.180 +(** Big Union and Intersection **)
   3.181 +
   3.182 +lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)"
   3.183 +by blast
   3.184 +
   3.185 +lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"
   3.186 +by blast
   3.187 +
   3.188 +lemma Union_Int_subset: "Union(A Int B) <= Union(A) Int Union(B)"
   3.189 +by blast
   3.190 +
   3.191 +lemma Union_disjoint: "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)"
   3.192 +by (blast elim!: equalityE)
   3.193 +
   3.194 +lemma Union_empty_iff: "Union(A) = 0 <-> (ALL B:A. B=0)"
   3.195 +by blast
   3.196 +
   3.197 +lemma Inter_0: "Inter(0) = 0"
   3.198 +by (unfold Inter_def, blast)
   3.199 +
   3.200 +lemma Inter_Un_subset: "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)"
   3.201 +by blast
   3.202 +
   3.203 +(* A good challenge: Inter is ill-behaved on the empty set *)
   3.204 +lemma Inter_Un_distrib:
   3.205 +     "[| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)"
   3.206 +by blast
   3.207 +
   3.208 +lemma Union_singleton: "Union({b}) = b"
   3.209 +by blast
   3.210 +
   3.211 +lemma Inter_singleton: "Inter({b}) = b"
   3.212 +by blast
   3.213 +
   3.214 +lemma Inter_cons [simp]:
   3.215 +     "Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))"
   3.216 +by force
   3.217 +
   3.218 +(** Unions and Intersections of Families **)
   3.219 +
   3.220 +lemma Union_eq_UN: "Union(A) = (UN x:A. x)"
   3.221 +by blast
   3.222 +
   3.223 +lemma Inter_eq_INT: "Inter(A) = (INT x:A. x)"
   3.224 +by (unfold Inter_def, blast)
   3.225 +
   3.226 +lemma UN_0 [simp]: "(UN i:0. A(i)) = 0"
   3.227 +by blast
   3.228 +
   3.229 +lemma UN_singleton: "(UN x:A. {x}) = A"
   3.230 +by blast
   3.231 +
   3.232 +lemma UN_Un: "(UN i: A Un B. C(i)) = (UN i: A. C(i)) Un (UN i:B. C(i))"
   3.233 +by blast
   3.234 +
   3.235 +lemma INT_Un: "(INT i:I Un J. A(i)) = (if I=0 then INT j:J. A(j)  
   3.236 +                              else if J=0 then INT i:I. A(i)  
   3.237 +                              else ((INT i:I. A(i)) Int  (INT j:J. A(j))))"
   3.238 +apply auto
   3.239 +apply (blast intro!: equalityI)
   3.240 +done
   3.241 +
   3.242 +lemma UN_UN_flatten: "(UN x : (UN y:A. B(y)). C(x)) = (UN y:A. UN x: B(y). C(x))"
   3.243 +by blast
   3.244 +
   3.245 +(*Halmos, Naive Set Theory, page 35.*)
   3.246 +lemma Int_UN_distrib: "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"
   3.247 +by blast
   3.248 +
   3.249 +lemma Un_INT_distrib: "i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"
   3.250 +by blast
   3.251 +
   3.252 +lemma Int_UN_distrib2:
   3.253 +     "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"
   3.254 +by blast
   3.255 +
   3.256 +lemma Un_INT_distrib2: "[| i:I;  j:J |] ==>  
   3.257 +      (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"
   3.258 +by blast
   3.259 +
   3.260 +lemma UN_constant: "a: A ==> (UN y:A. c) = c"
   3.261 +by blast
   3.262 +
   3.263 +lemma INT_constant: "a: A ==> (INT y:A. c) = c"
   3.264 +by blast
   3.265 +
   3.266 +lemma UN_RepFun [simp]: "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))"
   3.267 +by blast
   3.268 +
   3.269 +lemma INT_RepFun [simp]: "(INT x:RepFun(A,f). B(x))    = (INT a:A. B(f(a)))"
   3.270 +by (auto simp add: Inter_def)
   3.271 +
   3.272 +lemma INT_Union_eq:
   3.273 +     "0 ~: A ==> (INT x: Union(A). B(x)) = (INT y:A. INT x:y. B(x))"
   3.274 +apply (simp add: Inter_def)
   3.275 +apply (subgoal_tac "ALL x:A. x~=0")
   3.276 +prefer 2 apply blast
   3.277 +apply force
   3.278 +done
   3.279 +
   3.280 +lemma INT_UN_eq: "(ALL x:A. B(x) ~= 0)  
   3.281 +      ==> (INT z: (UN x:A. B(x)). C(z)) = (INT x:A. INT z: B(x). C(z))"
   3.282 +apply (subst INT_Union_eq, blast)
   3.283 +apply (simp add: Inter_def)
   3.284 +done
   3.285 +
   3.286 +
   3.287 +(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
   3.288 +    Union of a family of unions **)
   3.289 +
   3.290 +lemma UN_Un_distrib:
   3.291 +     "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))"
   3.292 +by blast
   3.293 +
   3.294 +lemma INT_Int_distrib:
   3.295 +     "i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"
   3.296 +by blast
   3.297 +
   3.298 +lemma UN_Int_subset:
   3.299 +     "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))"
   3.300 +by blast
   3.301 +
   3.302 +(** Devlin, page 12, exercise 5: Complements **)
   3.303 +
   3.304 +lemma Diff_UN: "i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))"
   3.305 +by blast
   3.306 +
   3.307 +lemma Diff_INT: "i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))"
   3.308 +by blast
   3.309 +
   3.310 +(** Unions and Intersections with General Sum **)
   3.311 +
   3.312 +(*Not suitable for rewriting: LOOPS!*)
   3.313 +lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)"
   3.314 +by blast
   3.315 +
   3.316 +(*Not suitable for rewriting: LOOPS!*)
   3.317 +lemma Sigma_cons2: "A * cons(b,B) = A*{b} Un A*B"
   3.318 +by blast
   3.319 +
   3.320 +lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)"
   3.321 +by blast
   3.322 +
   3.323 +lemma Sigma_succ2: "A * succ(B) = A*{B} Un A*B"
   3.324 +by blast
   3.325 +
   3.326 +lemma SUM_UN_distrib1:
   3.327 +     "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))"
   3.328 +by blast
   3.329 +
   3.330 +lemma SUM_UN_distrib2:
   3.331 +     "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))"
   3.332 +by blast
   3.333 +
   3.334 +lemma SUM_Un_distrib1:
   3.335 +     "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))"
   3.336 +by blast
   3.337 +
   3.338 +lemma SUM_Un_distrib2:
   3.339 +     "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))"
   3.340 +by blast
   3.341 +
   3.342 +(*First-order version of the above, for rewriting*)
   3.343 +lemma prod_Un_distrib2: "I * (A Un B) = I*A Un I*B"
   3.344 +by (rule SUM_Un_distrib2)
   3.345 +
   3.346 +lemma SUM_Int_distrib1:
   3.347 +     "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))"
   3.348 +by blast
   3.349 +
   3.350 +lemma SUM_Int_distrib2:
   3.351 +     "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))"
   3.352 +by blast
   3.353 +
   3.354 +(*First-order version of the above, for rewriting*)
   3.355 +lemma prod_Int_distrib2: "I * (A Int B) = I*A Int I*B"
   3.356 +by (rule SUM_Int_distrib2)
   3.357 +
   3.358 +(*Cf Aczel, Non-Well-Founded Sets, page 115*)
   3.359 +lemma SUM_eq_UN: "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))"
   3.360 +by blast
   3.361 +
   3.362 +(** Domain **)
   3.363 +
   3.364 +lemma domain_of_prod: "b:B ==> domain(A*B) = A"
   3.365 +by blast
   3.366 +
   3.367 +lemma domain_0 [simp]: "domain(0) = 0"
   3.368 +by blast
   3.369 +
   3.370 +lemma domain_cons [simp]: "domain(cons(<a,b>,r)) = cons(a, domain(r))"
   3.371 +by blast
   3.372 +
   3.373 +lemma domain_Un_eq [simp]: "domain(A Un B) = domain(A) Un domain(B)"
   3.374 +by blast
   3.375 +
   3.376 +lemma domain_Int_subset: "domain(A Int B) <= domain(A) Int domain(B)"
   3.377 +by blast
   3.378 +
   3.379 +lemma domain_Diff_subset: "domain(A) - domain(B) <= domain(A - B)"
   3.380 +by blast
   3.381 +
   3.382 +lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
   3.383 +by blast
   3.384  
   3.385 -equalities = domrange
   3.386 +lemma domain_UN: "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))"
   3.387 +by blast
   3.388 +
   3.389 +lemma domain_Union: "domain(Union(A)) = (UN x:A. domain(x))"
   3.390 +by blast
   3.391 +
   3.392 +
   3.393 +(** Range **)
   3.394 +
   3.395 +lemma range_of_prod: "a:A ==> range(A*B) = B"
   3.396 +by blast
   3.397 +
   3.398 +lemma range_0 [simp]: "range(0) = 0"
   3.399 +by blast
   3.400 +
   3.401 +lemma range_cons [simp]: "range(cons(<a,b>,r)) = cons(b, range(r))"
   3.402 +by blast
   3.403 +
   3.404 +lemma range_Un_eq [simp]: "range(A Un B) = range(A) Un range(B)"
   3.405 +by blast
   3.406 +
   3.407 +lemma range_Int_subset: "range(A Int B) <= range(A) Int range(B)"
   3.408 +by blast
   3.409 +
   3.410 +lemma range_Diff_subset: "range(A) - range(B) <= range(A - B)"
   3.411 +by blast
   3.412 +
   3.413 +lemma range_converse [simp]: "range(converse(r)) = domain(r)"
   3.414 +by blast
   3.415 +
   3.416 +
   3.417 +(** Field **)
   3.418 +
   3.419 +lemma field_of_prod: "field(A*A) = A"
   3.420 +by blast
   3.421 +
   3.422 +lemma field_0 [simp]: "field(0) = 0"
   3.423 +by blast
   3.424 +
   3.425 +lemma field_cons [simp]: "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
   3.426 +by blast
   3.427 +
   3.428 +lemma field_Un_eq [simp]: "field(A Un B) = field(A) Un field(B)"
   3.429 +by blast
   3.430 +
   3.431 +lemma field_Int_subset: "field(A Int B) <= field(A) Int field(B)"
   3.432 +by blast
   3.433 +
   3.434 +lemma field_Diff_subset: "field(A) - field(B) <= field(A - B)"
   3.435 +by blast
   3.436 +
   3.437 +lemma field_converse [simp]: "field(converse(r)) = field(r)"
   3.438 +by blast
   3.439 +
   3.440 +
   3.441 +(** Image **)
   3.442 +
   3.443 +lemma image_0 [simp]: "r``0 = 0"
   3.444 +by blast
   3.445 +
   3.446 +lemma image_Un [simp]: "r``(A Un B) = (r``A) Un (r``B)"
   3.447 +by blast
   3.448 +
   3.449 +lemma image_Int_subset: "r``(A Int B) <= (r``A) Int (r``B)"
   3.450 +by blast
   3.451 +
   3.452 +lemma image_Int_square_subset: "(r Int A*A)``B <= (r``B) Int A"
   3.453 +by blast
   3.454 +
   3.455 +lemma image_Int_square: "B<=A ==> (r Int A*A)``B = (r``B) Int A"
   3.456 +by blast
   3.457 +
   3.458 +
   3.459 +(*Image laws for special relations*)
   3.460 +lemma image_0_left [simp]: "0``A = 0"
   3.461 +by blast
   3.462 +
   3.463 +lemma image_Un_left: "(r Un s)``A = (r``A) Un (s``A)"
   3.464 +by blast
   3.465 +
   3.466 +lemma image_Int_subset_left: "(r Int s)``A <= (r``A) Int (s``A)"
   3.467 +by blast
   3.468 +
   3.469 +
   3.470 +(** Inverse Image **)
   3.471 +
   3.472 +lemma vimage_0 [simp]: "r-``0 = 0"
   3.473 +by blast
   3.474 +
   3.475 +lemma vimage_Un [simp]: "r-``(A Un B) = (r-``A) Un (r-``B)"
   3.476 +by blast
   3.477 +
   3.478 +lemma vimage_Int_subset: "r-``(A Int B) <= (r-``A) Int (r-``B)"
   3.479 +by blast
   3.480 +
   3.481 +(*NOT suitable for rewriting*)
   3.482 +lemma vimage_eq_UN: "f -``B = (UN y:B. f-``{y})"
   3.483 +by blast
   3.484 +
   3.485 +lemma function_vimage_Int:
   3.486 +     "function(f) ==> f-``(A Int B) = (f-``A)  Int  (f-``B)"
   3.487 +by (unfold function_def, blast)
   3.488 +
   3.489 +lemma function_vimage_Diff: "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)"
   3.490 +by (unfold function_def, blast)
   3.491 +
   3.492 +lemma function_image_vimage: "function(f) ==> f `` (f-`` A) <= A"
   3.493 +by (unfold function_def, blast)
   3.494 +
   3.495 +lemma vimage_Int_square_subset: "(r Int A*A)-``B <= (r-``B) Int A"
   3.496 +by blast
   3.497 +
   3.498 +lemma vimage_Int_square: "B<=A ==> (r Int A*A)-``B = (r-``B) Int A"
   3.499 +by blast
   3.500 +
   3.501 +
   3.502 +
   3.503 +(*Invese image laws for special relations*)
   3.504 +lemma vimage_0_left [simp]: "0-``A = 0"
   3.505 +by blast
   3.506 +
   3.507 +lemma vimage_Un_left: "(r Un s)-``A = (r-``A) Un (s-``A)"
   3.508 +by blast
   3.509 +
   3.510 +lemma vimage_Int_subset_left: "(r Int s)-``A <= (r-``A) Int (s-``A)"
   3.511 +by blast
   3.512 +
   3.513 +
   3.514 +(** Converse **)
   3.515 +
   3.516 +lemma converse_Un [simp]: "converse(A Un B) = converse(A) Un converse(B)"
   3.517 +by blast
   3.518 +
   3.519 +lemma converse_Int [simp]: "converse(A Int B) = converse(A) Int converse(B)"
   3.520 +by blast
   3.521 +
   3.522 +lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"
   3.523 +by blast
   3.524 +
   3.525 +lemma converse_UN [simp]: "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))"
   3.526 +by blast
   3.527 +
   3.528 +(*Unfolding Inter avoids using excluded middle on A=0*)
   3.529 +lemma converse_INT [simp]:
   3.530 +     "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))"
   3.531 +apply (unfold Inter_def, blast)
   3.532 +done
   3.533 +
   3.534 +(** Pow **)
   3.535 +
   3.536 +lemma Pow_0 [simp]: "Pow(0) = {0}"
   3.537 +by blast
   3.538 +
   3.539 +lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}"
   3.540 +apply (rule equalityI, safe)
   3.541 +apply (erule swap)
   3.542 +apply (rule_tac a = "x-{a}" in RepFun_eqI, auto) 
   3.543 +done
   3.544 +
   3.545 +lemma Un_Pow_subset: "Pow(A) Un Pow(B) <= Pow(A Un B)"
   3.546 +by blast
   3.547 +
   3.548 +lemma UN_Pow_subset: "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))"
   3.549 +by blast
   3.550 +
   3.551 +lemma subset_Pow_Union: "A <= Pow(Union(A))"
   3.552 +by blast
   3.553 +
   3.554 +lemma Union_Pow_eq [simp]: "Union(Pow(A)) = A"
   3.555 +by blast
   3.556 +
   3.557 +lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)"
   3.558 +by blast
   3.559 +
   3.560 +lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))"
   3.561 +by blast
   3.562 +
   3.563 +(** RepFun **)
   3.564 +
   3.565 +lemma RepFun_eq_0_iff [simp]: "{f(x).x:A}=0 <-> A=0"
   3.566 +by blast
   3.567 +
   3.568 +lemma RepFun_constant [simp]: "{c. x:A} = (if A=0 then 0 else {c})"
   3.569 +apply auto
   3.570 +apply blast
   3.571 +done
   3.572 +
   3.573 +(** Collect **)
   3.574  
   3.575 +lemma Collect_Un: "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)"
   3.576 +by blast
   3.577 +
   3.578 +lemma Collect_Int: "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)"
   3.579 +by blast
   3.580 +
   3.581 +lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)"
   3.582 +by blast
   3.583 +
   3.584 +lemma Collect_cons: "{x:cons(a,B). P(x)} =  
   3.585 +      (if P(a) then cons(a, {x:B. P(x)}) else {x:B. P(x)})"
   3.586 +by (simp, blast)
   3.587 +
   3.588 +lemma Int_Collect_self_eq: "A Int Collect(A,P) = Collect(A,P)"
   3.589 +by blast
   3.590 +
   3.591 +lemma Collect_Collect_eq [simp]:
   3.592 +     "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))"
   3.593 +by blast
   3.594 +
   3.595 +lemma Collect_Int_Collect_eq:
   3.596 +     "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
   3.597 +by blast
   3.598 +
   3.599 +ML
   3.600 +{*
   3.601 +val cons_eq = thm "cons_eq";
   3.602 +val cons_commute = thm "cons_commute";
   3.603 +val cons_absorb = thm "cons_absorb";
   3.604 +val cons_Diff = thm "cons_Diff";
   3.605 +val equal_singleton = thm "equal_singleton";
   3.606 +val Int_cons = thm "Int_cons";
   3.607 +val Int_absorb = thm "Int_absorb";
   3.608 +val Int_left_absorb = thm "Int_left_absorb";
   3.609 +val Int_commute = thm "Int_commute";
   3.610 +val Int_left_commute = thm "Int_left_commute";
   3.611 +val Int_assoc = thm "Int_assoc";
   3.612 +val Int_Un_distrib = thm "Int_Un_distrib";
   3.613 +val Int_Un_distrib2 = thm "Int_Un_distrib2";
   3.614 +val subset_Int_iff = thm "subset_Int_iff";
   3.615 +val subset_Int_iff2 = thm "subset_Int_iff2";
   3.616 +val Int_Diff_eq = thm "Int_Diff_eq";
   3.617 +val Un_cons = thm "Un_cons";
   3.618 +val Un_absorb = thm "Un_absorb";
   3.619 +val Un_left_absorb = thm "Un_left_absorb";
   3.620 +val Un_commute = thm "Un_commute";
   3.621 +val Un_left_commute = thm "Un_left_commute";
   3.622 +val Un_assoc = thm "Un_assoc";
   3.623 +val Un_Int_distrib = thm "Un_Int_distrib";
   3.624 +val subset_Un_iff = thm "subset_Un_iff";
   3.625 +val subset_Un_iff2 = thm "subset_Un_iff2";
   3.626 +val Un_empty = thm "Un_empty";
   3.627 +val Un_eq_Union = thm "Un_eq_Union";
   3.628 +val Diff_cancel = thm "Diff_cancel";
   3.629 +val Diff_triv = thm "Diff_triv";
   3.630 +val empty_Diff = thm "empty_Diff";
   3.631 +val Diff_0 = thm "Diff_0";
   3.632 +val Diff_eq_0_iff = thm "Diff_eq_0_iff";
   3.633 +val Diff_cons = thm "Diff_cons";
   3.634 +val Diff_cons2 = thm "Diff_cons2";
   3.635 +val Diff_disjoint = thm "Diff_disjoint";
   3.636 +val Diff_partition = thm "Diff_partition";
   3.637 +val subset_Un_Diff = thm "subset_Un_Diff";
   3.638 +val double_complement = thm "double_complement";
   3.639 +val double_complement_Un = thm "double_complement_Un";
   3.640 +val Un_Int_crazy = thm "Un_Int_crazy";
   3.641 +val Diff_Un = thm "Diff_Un";
   3.642 +val Diff_Int = thm "Diff_Int";
   3.643 +val Un_Diff = thm "Un_Diff";
   3.644 +val Int_Diff = thm "Int_Diff";
   3.645 +val Diff_Int_distrib = thm "Diff_Int_distrib";
   3.646 +val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
   3.647 +val Un_Int_assoc_iff = thm "Un_Int_assoc_iff";
   3.648 +val Union_cons = thm "Union_cons";
   3.649 +val Union_Un_distrib = thm "Union_Un_distrib";
   3.650 +val Union_Int_subset = thm "Union_Int_subset";
   3.651 +val Union_disjoint = thm "Union_disjoint";
   3.652 +val Union_empty_iff = thm "Union_empty_iff";
   3.653 +val Inter_0 = thm "Inter_0";
   3.654 +val Inter_Un_subset = thm "Inter_Un_subset";
   3.655 +val Inter_Un_distrib = thm "Inter_Un_distrib";
   3.656 +val Union_singleton = thm "Union_singleton";
   3.657 +val Inter_singleton = thm "Inter_singleton";
   3.658 +val Inter_cons = thm "Inter_cons";
   3.659 +val Union_eq_UN = thm "Union_eq_UN";
   3.660 +val Inter_eq_INT = thm "Inter_eq_INT";
   3.661 +val UN_0 = thm "UN_0";
   3.662 +val UN_singleton = thm "UN_singleton";
   3.663 +val UN_Un = thm "UN_Un";
   3.664 +val INT_Un = thm "INT_Un";
   3.665 +val UN_UN_flatten = thm "UN_UN_flatten";
   3.666 +val Int_UN_distrib = thm "Int_UN_distrib";
   3.667 +val Un_INT_distrib = thm "Un_INT_distrib";
   3.668 +val Int_UN_distrib2 = thm "Int_UN_distrib2";
   3.669 +val Un_INT_distrib2 = thm "Un_INT_distrib2";
   3.670 +val UN_constant = thm "UN_constant";
   3.671 +val INT_constant = thm "INT_constant";
   3.672 +val UN_RepFun = thm "UN_RepFun";
   3.673 +val INT_RepFun = thm "INT_RepFun";
   3.674 +val INT_Union_eq = thm "INT_Union_eq";
   3.675 +val INT_UN_eq = thm "INT_UN_eq";
   3.676 +val UN_Un_distrib = thm "UN_Un_distrib";
   3.677 +val INT_Int_distrib = thm "INT_Int_distrib";
   3.678 +val UN_Int_subset = thm "UN_Int_subset";
   3.679 +val Diff_UN = thm "Diff_UN";
   3.680 +val Diff_INT = thm "Diff_INT";
   3.681 +val Sigma_cons1 = thm "Sigma_cons1";
   3.682 +val Sigma_cons2 = thm "Sigma_cons2";
   3.683 +val Sigma_succ1 = thm "Sigma_succ1";
   3.684 +val Sigma_succ2 = thm "Sigma_succ2";
   3.685 +val SUM_UN_distrib1 = thm "SUM_UN_distrib1";
   3.686 +val SUM_UN_distrib2 = thm "SUM_UN_distrib2";
   3.687 +val SUM_Un_distrib1 = thm "SUM_Un_distrib1";
   3.688 +val SUM_Un_distrib2 = thm "SUM_Un_distrib2";
   3.689 +val prod_Un_distrib2 = thm "prod_Un_distrib2";
   3.690 +val SUM_Int_distrib1 = thm "SUM_Int_distrib1";
   3.691 +val SUM_Int_distrib2 = thm "SUM_Int_distrib2";
   3.692 +val prod_Int_distrib2 = thm "prod_Int_distrib2";
   3.693 +val SUM_eq_UN = thm "SUM_eq_UN";
   3.694 +val domain_of_prod = thm "domain_of_prod";
   3.695 +val domain_0 = thm "domain_0";
   3.696 +val domain_cons = thm "domain_cons";
   3.697 +val domain_Un_eq = thm "domain_Un_eq";
   3.698 +val domain_Int_subset = thm "domain_Int_subset";
   3.699 +val domain_Diff_subset = thm "domain_Diff_subset";
   3.700 +val domain_converse = thm "domain_converse";
   3.701 +val domain_UN = thm "domain_UN";
   3.702 +val domain_Union = thm "domain_Union";
   3.703 +val range_of_prod = thm "range_of_prod";
   3.704 +val range_0 = thm "range_0";
   3.705 +val range_cons = thm "range_cons";
   3.706 +val range_Un_eq = thm "range_Un_eq";
   3.707 +val range_Int_subset = thm "range_Int_subset";
   3.708 +val range_Diff_subset = thm "range_Diff_subset";
   3.709 +val range_converse = thm "range_converse";
   3.710 +val field_of_prod = thm "field_of_prod";
   3.711 +val field_0 = thm "field_0";
   3.712 +val field_cons = thm "field_cons";
   3.713 +val field_Un_eq = thm "field_Un_eq";
   3.714 +val field_Int_subset = thm "field_Int_subset";
   3.715 +val field_Diff_subset = thm "field_Diff_subset";
   3.716 +val field_converse = thm "field_converse";
   3.717 +val image_0 = thm "image_0";
   3.718 +val image_Un = thm "image_Un";
   3.719 +val image_Int_subset = thm "image_Int_subset";
   3.720 +val image_Int_square_subset = thm "image_Int_square_subset";
   3.721 +val image_Int_square = thm "image_Int_square";
   3.722 +val image_0_left = thm "image_0_left";
   3.723 +val image_Un_left = thm "image_Un_left";
   3.724 +val image_Int_subset_left = thm "image_Int_subset_left";
   3.725 +val vimage_0 = thm "vimage_0";
   3.726 +val vimage_Un = thm "vimage_Un";
   3.727 +val vimage_Int_subset = thm "vimage_Int_subset";
   3.728 +val vimage_eq_UN = thm "vimage_eq_UN";
   3.729 +val function_vimage_Int = thm "function_vimage_Int";
   3.730 +val function_vimage_Diff = thm "function_vimage_Diff";
   3.731 +val function_image_vimage = thm "function_image_vimage";
   3.732 +val vimage_Int_square_subset = thm "vimage_Int_square_subset";
   3.733 +val vimage_Int_square = thm "vimage_Int_square";
   3.734 +val vimage_0_left = thm "vimage_0_left";
   3.735 +val vimage_Un_left = thm "vimage_Un_left";
   3.736 +val vimage_Int_subset_left = thm "vimage_Int_subset_left";
   3.737 +val converse_Un = thm "converse_Un";
   3.738 +val converse_Int = thm "converse_Int";
   3.739 +val converse_Diff = thm "converse_Diff";
   3.740 +val converse_UN = thm "converse_UN";
   3.741 +val converse_INT = thm "converse_INT";
   3.742 +val Pow_0 = thm "Pow_0";
   3.743 +val Pow_insert = thm "Pow_insert";
   3.744 +val Un_Pow_subset = thm "Un_Pow_subset";
   3.745 +val UN_Pow_subset = thm "UN_Pow_subset";
   3.746 +val subset_Pow_Union = thm "subset_Pow_Union";
   3.747 +val Union_Pow_eq = thm "Union_Pow_eq";
   3.748 +val Pow_Int_eq = thm "Pow_Int_eq";
   3.749 +val Pow_INT_eq = thm "Pow_INT_eq";
   3.750 +val RepFun_eq_0_iff = thm "RepFun_eq_0_iff";
   3.751 +val RepFun_constant = thm "RepFun_constant";
   3.752 +val Collect_Un = thm "Collect_Un";
   3.753 +val Collect_Int = thm "Collect_Int";
   3.754 +val Collect_Diff = thm "Collect_Diff";
   3.755 +val Collect_cons = thm "Collect_cons";
   3.756 +val Int_Collect_self_eq = thm "Int_Collect_self_eq";
   3.757 +val Collect_Collect_eq = thm "Collect_Collect_eq";
   3.758 +val Collect_Int_Collect_eq = thm "Collect_Int_Collect_eq";
   3.759 +
   3.760 +val Int_ac = thms "Int_ac";
   3.761 +val Un_ac = thms "Un_ac";
   3.762 +
   3.763 +*}
   3.764 +
   3.765 +end
   3.766 +