new theorems and comment
authorpaulson
Sat Sep 23 16:11:38 2000 +0200 (2000-09-23)
changeset 100662f5686cf8c9a
parent 10065 ddb3a014f721
child 10067 ab03cfd6be3a
new theorems and comment
src/HOL/Fun.ML
     1.1 --- a/src/HOL/Fun.ML	Sat Sep 23 16:08:23 2000 +0200
     1.2 +++ b/src/HOL/Fun.ML	Sat Sep 23 16:11:38 2000 +0200
     1.3 @@ -130,6 +130,10 @@
     1.4  by (etac inv_f_f 1);
     1.5  qed "inv_f_eq";
     1.6  
     1.7 +Goal "[| inj f; ALL x. f(g x) = x |] ==> inv f = g";
     1.8 +by (blast_tac (claset() addIs [ext, inv_f_eq]) 1); 
     1.9 +qed "inj_imp_inv_eq";
    1.10 +
    1.11  (* Useful??? *)
    1.12  val [oneone,minor] = Goal
    1.13      "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
    1.14 @@ -238,6 +242,12 @@
    1.15  by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
    1.16  qed "surj_iff";
    1.17  
    1.18 +Goal "[| surj f; ALL x. g(f x) = x |] ==> inv f = g";
    1.19 +by (rtac ext 1);
    1.20 +by (dres_inst_tac [("x","inv f x")] spec 1); 
    1.21 +by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); 
    1.22 +qed "surj_imp_inv_eq";
    1.23 +
    1.24  
    1.25  (** Bijections **)
    1.26  
    1.27 @@ -268,6 +278,13 @@
    1.28  by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
    1.29  qed "inv_inv_eq";
    1.30  
    1.31 +(** bij(inv f) implies little about f.  Consider f::bool=>bool such that
    1.32 +    f(True)=f(False)=True.  Then it's consistent with axiom someI that
    1.33 +    inv(f) could be any function at all, including the identity function.
    1.34 +    If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and
    1.35 +    inv(inv(f))=f all fail.
    1.36 +**)
    1.37 +
    1.38  Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f";
    1.39  by (rtac (inv_equality) 1);
    1.40  by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));