# HG changeset patch # User paulson # Date 961576294 -7200 # Node ID 44cd0f9f8e5b0cff2c2b16f943362ba0dbcb3a29 # Parent 5c4d4364f854540b2900fade8abbebadf74f92d9 generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split diff -r 5c4d4364f854 -r 44cd0f9f8e5b src/HOL/Relation.ML --- a/src/HOL/Relation.ML Wed Jun 21 10:30:36 2000 +0200 +++ b/src/HOL/Relation.ML Wed Jun 21 10:31:34 2000 +0200 @@ -411,16 +411,21 @@ qed "univalentD"; -(** Graphs of partial functions **) +(** Graphs given by Collect **) + +Goal "Domain{(x,y). P x y} = {x. EX y. P x y}"; +by Auto_tac; +qed "Domain_Collect_split"; -Goal "Domain{(x,y). y = f x & P x} = {x. P x}"; -by (Blast_tac 1); -qed "Domain_partial_func"; +Goal "Range{(x,y). P x y} = {y. EX x. P x y}"; +by Auto_tac; +qed "Range_Collect_split"; -Goal "Range{(x,y). y = f x & P x} = f``{x. P x}"; -by (Blast_tac 1); -qed "Range_partial_func"; +Goal "{(x,y). P x y} ^^ A = {y. EX x:A. P x y}"; +by Auto_tac; +qed "Image_Collect_split"; +Addsimps [Domain_Collect_split, Range_Collect_split, Image_Collect_split]; (** Composition of function and relation **)