the bij predicate (at last)
authorpaulson
Fri Aug 27 15:41:11 1999 +0200 (1999-08-27)
changeset 7374dec7b838f5cb
parent 7373 776d888472aa
child 7375 2cb340e66d15
the bij predicate (at last)
src/HOL/Fun.ML
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.ML	Fri Aug 27 10:54:31 1999 +0200
     1.2 +++ b/src/HOL/Fun.ML	Fri Aug 27 15:41:11 1999 +0200
     1.3 @@ -185,6 +185,21 @@
     1.4  qed "surjD";
     1.5  
     1.6  
     1.7 +(** Bijections **)
     1.8 +
     1.9 +Goalw [bij_def] "[| inj f; surj f |] ==> bij f";
    1.10 +by (Blast_tac 1);
    1.11 +qed "bijI";
    1.12 +
    1.13 +Goalw [bij_def] "bij f ==> inj f";
    1.14 +by (Blast_tac 1);
    1.15 +qed "bij_is_inj";
    1.16 +
    1.17 +Goalw [bij_def] "bij f ==> surj f";
    1.18 +by (Blast_tac 1);
    1.19 +qed "bij_is_surj";
    1.20 +
    1.21 +
    1.22  (*** Lemmas about injective functions and inv ***)
    1.23  
    1.24  Goalw [o_def] "[| inj_on f A;  inj_on g (f``A) |] ==> inj_on (g o f) A";
     2.1 --- a/src/HOL/Fun.thy	Fri Aug 27 10:54:31 1999 +0200
     2.2 +++ b/src/HOL/Fun.thy	Fri Aug 27 15:41:11 1999 +0200
     2.3 @@ -39,24 +39,27 @@
     2.4  
     2.5    o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
     2.6      "f o g == %x. f(g(x))"
     2.7 +  
     2.8 +  inv :: ('a => 'b) => ('b => 'a)
     2.9 +    "inv(f::'a=>'b) == % y. @x. f(x)=y"
    2.10  
    2.11    inj_on :: ['a => 'b, 'a set] => bool
    2.12      "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    2.13  
    2.14 -  surj :: ('a => 'b) => bool                   (*surjective*)
    2.15 -    "surj f == ! y. ? x. y=f(x)"
    2.16 -  
    2.17 -  inv :: ('a => 'b) => ('b => 'a)
    2.18 -    "inv(f::'a=>'b) == % y. @x. f(x)=y"
    2.19 -  
    2.20 -
    2.21 -
    2.22  syntax
    2.23    inj   :: ('a => 'b) => bool                   (*injective*)
    2.24  
    2.25  translations
    2.26    "inj f" == "inj_on f UNIV"
    2.27  
    2.28 +constdefs
    2.29 +  surj :: ('a => 'b) => bool                   (*surjective*)
    2.30 +    "surj f == ! y. ? x. y=f(x)"
    2.31 +  
    2.32 +  bij :: ('a => 'b) => bool                    (*bijective*)
    2.33 +    "bij f == inj f & surj f"
    2.34 +  
    2.35 +
    2.36  (*The Pi-operator, by Florian Kammueller*)
    2.37    
    2.38  constdefs