generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
authorpaulson
Wed Jun 21 10:31:34 2000 +0200 (2000-06-21)
changeset 909744cd0f9f8e5b
parent 9096 5c4d4364f854
child 9098 3a0912a127ec
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Wed Jun 21 10:30:36 2000 +0200
     1.2 +++ b/src/HOL/Relation.ML	Wed Jun 21 10:31:34 2000 +0200
     1.3 @@ -411,16 +411,21 @@
     1.4  qed "univalentD";
     1.5  
     1.6  
     1.7 -(** Graphs of partial functions **)
     1.8 +(** Graphs given by Collect **)
     1.9 +
    1.10 +Goal "Domain{(x,y). P x y} = {x. EX y. P x y}";
    1.11 +by Auto_tac; 
    1.12 +qed "Domain_Collect_split";
    1.13  
    1.14 -Goal "Domain{(x,y). y = f x & P x} = {x. P x}";
    1.15 -by (Blast_tac 1);
    1.16 -qed "Domain_partial_func";
    1.17 +Goal "Range{(x,y). P x y} = {y. EX x. P x y}";
    1.18 +by Auto_tac; 
    1.19 +qed "Range_Collect_split";
    1.20  
    1.21 -Goal "Range{(x,y). y = f x & P x} = f``{x. P x}";
    1.22 -by (Blast_tac 1);
    1.23 -qed "Range_partial_func";
    1.24 +Goal "{(x,y). P x y} ^^ A = {y. EX x:A. P x y}";
    1.25 +by Auto_tac; 
    1.26 +qed "Image_Collect_split";
    1.27  
    1.28 +Addsimps [Domain_Collect_split, Range_Collect_split, Image_Collect_split];
    1.29  
    1.30  (** Composition of function and relation **)
    1.31