# HG changeset patch # User paulson # Date 918553555 -3600 # Node ID a3098667b9b65e5d4fbcf3bf354b7f7d35b68cb5 # Parent a5f9fa6b6d7c343dc2f952008d108e99bf1cff5a new lemma surjD diff -r a5f9fa6b6d7c -r a3098667b9b6 src/HOL/Fun.ML --- a/src/HOL/Fun.ML Mon Feb 08 17:33:47 1999 +0100 +++ b/src/HOL/Fun.ML Tue Feb 09 10:45:55 1999 +0100 @@ -142,14 +142,18 @@ (** surj **) -val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; -by (blast_tac (claset() addIs [major RS sym]) 1); +val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; +by (blast_tac (claset() addIs [prem RS sym]) 1); qed "surjI"; Goalw [surj_def] "surj f ==> range f = UNIV"; by Auto_tac; qed "surj_range"; +Goalw [surj_def] "surj f ==> EX x. y = f x"; +by (Blast_tac 1); +qed "surjD"; + (*** Lemmas about injective functions and inv ***)