moved inj and surj from Set to Fun and Inv -> inv.
authornipkow
Fri Apr 04 16:33:28 1997 +0200 (1997-04-04)
changeset 29123fac3e8d5d3e
parent 2911 8a680e310f04
child 2913 ce271fa4d8e2
moved inj and surj from Set to Fun and Inv -> inv.
src/HOL/Fun.ML
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Set.ML
src/HOL/Set.thy
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Fun.ML	Fri Apr 04 16:27:39 1997 +0200
     1.2 +++ b/src/HOL/Fun.ML	Fri Apr 04 16:33:28 1997 +0200
     1.3 @@ -19,48 +19,6 @@
     1.4  qed "apply_inverse";
     1.5  
     1.6  
     1.7 -(*** Image of a set under a function ***)
     1.8 -
     1.9 -(*Frequently b does not have the syntactic form of f(x).*)
    1.10 -val prems = goalw Fun.thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
    1.11 -by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
    1.12 -qed "image_eqI";
    1.13 -
    1.14 -bind_thm ("imageI", refl RS image_eqI);
    1.15 -
    1.16 -(*The eta-expansion gives variable-name preservation.*)
    1.17 -val major::prems = goalw Fun.thy [image_def]
    1.18 -    "[| b : (%x.f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
    1.19 -by (rtac (major RS CollectD RS bexE) 1);
    1.20 -by (REPEAT (ares_tac prems 1));
    1.21 -qed "imageE";
    1.22 -
    1.23 -AddIs  [image_eqI];
    1.24 -AddSEs [imageE]; 
    1.25 -
    1.26 -goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
    1.27 -by (Fast_tac 1);
    1.28 -qed "image_compose";
    1.29 -
    1.30 -goal Fun.thy "f``(A Un B) = f``A Un f``B";
    1.31 -by (Fast_tac 1);
    1.32 -qed "image_Un";
    1.33 -
    1.34 -(*** Range of a function -- just a translation for image! ***)
    1.35 -
    1.36 -goal Fun.thy "!!b. b=f(x) ==> b : range(f)";
    1.37 -by (EVERY1 [etac image_eqI, rtac UNIV_I]);
    1.38 -bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
    1.39 -
    1.40 -bind_thm ("rangeI", UNIV_I RS imageI);
    1.41 -
    1.42 -val [major,minor] = goal Fun.thy 
    1.43 -    "[| b : range(%x.f(x));  !!x. b=f(x) ==> P |] ==> P"; 
    1.44 -by (rtac (major RS imageE) 1);
    1.45 -by (etac minor 1);
    1.46 -qed "rangeE";
    1.47 -
    1.48 -
    1.49  (*** inj(f): f is a one-to-one function ***)
    1.50  
    1.51  val prems = goalw Fun.thy [inj_def]
    1.52 @@ -95,14 +53,14 @@
    1.53  qed "inj_select";
    1.54  
    1.55  (*A one-to-one function has an inverse (given using select).*)
    1.56 -val [major] = goalw Fun.thy [Inv_def] "inj(f) ==> Inv f (f x) = x";
    1.57 +val [major] = goalw Fun.thy [inv_def] "inj(f) ==> inv f (f x) = x";
    1.58  by (EVERY1 [rtac (major RS inj_select)]);
    1.59 -qed "Inv_f_f";
    1.60 +qed "inv_f_f";
    1.61  
    1.62  (* Useful??? *)
    1.63  val [oneone,minor] = goal Fun.thy
    1.64 -    "[| inj(f); !!y. y: range(f) ==> P(Inv f y) |] ==> P(x)";
    1.65 -by (res_inst_tac [("t", "x")] (oneone RS (Inv_f_f RS subst)) 1);
    1.66 +    "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
    1.67 +by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
    1.68  by (rtac (rangeI RS minor) 1);
    1.69  qed "inj_transfer";
    1.70  
    1.71 @@ -152,27 +110,22 @@
    1.72  by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
    1.73  qed "inj_imp";
    1.74  
    1.75 -val [prem] = goalw Fun.thy [Inv_def] "y : range(f) ==> f(Inv f y) = y";
    1.76 +val [prem] = goalw Fun.thy [inv_def] "y : range(f) ==> f(inv f y) = y";
    1.77  by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
    1.78 -qed "f_Inv_f";
    1.79 -
    1.80 -val prems = goal Fun.thy
    1.81 -    "[| Inv f x=Inv f y; x: range(f);  y: range(f) |] ==> x=y";
    1.82 -by (rtac (arg_cong RS box_equals) 1);
    1.83 -by (REPEAT (resolve_tac (prems @ [f_Inv_f]) 1));
    1.84 -qed "Inv_injective";
    1.85 +qed "f_inv_f";
    1.86  
    1.87  val prems = goal Fun.thy
    1.88 -    "[| inj(f);  A<=range(f) |] ==> inj_onto (Inv f) A";
    1.89 +    "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
    1.90 +by (rtac (arg_cong RS box_equals) 1);
    1.91 +by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
    1.92 +qed "inv_injective";
    1.93 +
    1.94 +val prems = goal Fun.thy
    1.95 +    "[| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
    1.96  by (cut_facts_tac prems 1);
    1.97  by (fast_tac (!claset addIs [inj_ontoI] 
    1.98 -                      addEs [Inv_injective,injD]) 1);
    1.99 -qed "inj_onto_Inv";
   1.100 +                      addEs [inv_injective,injD]) 1);
   1.101 +qed "inj_onto_inv";
   1.102  
   1.103  
   1.104 -AddIs  [rangeI]; 
   1.105 -AddSEs [rangeE]; 
   1.106 -
   1.107  val set_cs = !claset delrules [equalityI];
   1.108 -
   1.109 -
     2.1 --- a/src/HOL/Fun.thy	Fri Apr 04 16:27:39 1997 +0200
     2.2 +++ b/src/HOL/Fun.thy	Fri Apr 04 16:33:28 1997 +0200
     2.3 @@ -3,7 +3,22 @@
     2.4      Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     2.5      Copyright   1994  University of Cambridge
     2.6  
     2.7 -Lemmas about functions.
     2.8 +Notions about functions.
     2.9  *)
    2.10  
    2.11 -Fun = Set
    2.12 +Fun = Set +
    2.13 +
    2.14 +consts
    2.15 +
    2.16 +  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
    2.17 +  inj_onto      :: ['a => 'b, 'a set] => bool
    2.18 +  inv           :: ('a => 'b) => ('b => 'a)
    2.19 +
    2.20 +defs
    2.21 +
    2.22 +  inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
    2.23 +  inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    2.24 +  surj_def      "surj f         == ! y. ? x. y=f(x)"
    2.25 +  inv_def       "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
    2.26 +
    2.27 +end
     3.1 --- a/src/HOL/HOL.thy	Fri Apr 04 16:27:39 1997 +0200
     3.2 +++ b/src/HOL/HOL.thy	Fri Apr 04 16:33:28 1997 +0200
     3.3 @@ -33,7 +33,6 @@
     3.4    Not           :: bool => bool                     ("~ _" [40] 40)
     3.5    True, False   :: bool
     3.6    If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
     3.7 -  Inv           :: ('a => 'b) => ('b => 'a)
     3.8  
     3.9    (* Binders *)
    3.10  
    3.11 @@ -170,7 +169,6 @@
    3.12    (* Misc Definitions *)
    3.13  
    3.14    Let_def       "Let s f == f(s)"
    3.15 -  Inv_def       "Inv(f::'a=>'b)  == (% y. @x. f(x)=y)"
    3.16    o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
    3.17    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
    3.18  
     4.1 --- a/src/HOL/Set.ML	Fri Apr 04 16:27:39 1997 +0200
     4.2 +++ b/src/HOL/Set.ML	Fri Apr 04 16:33:28 1997 +0200
     4.3 @@ -602,6 +602,51 @@
     4.4  AddEs  [InterD, InterE];
     4.5  
     4.6  
     4.7 +(*** Image of a set under a function ***)
     4.8 +
     4.9 +(*Frequently b does not have the syntactic form of f(x).*)
    4.10 +val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
    4.11 +by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
    4.12 +qed "image_eqI";
    4.13 +
    4.14 +bind_thm ("imageI", refl RS image_eqI);
    4.15 +
    4.16 +(*The eta-expansion gives variable-name preservation.*)
    4.17 +val major::prems = goalw thy [image_def]
    4.18 +    "[| b : (%x.f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
    4.19 +by (rtac (major RS CollectD RS bexE) 1);
    4.20 +by (REPEAT (ares_tac prems 1));
    4.21 +qed "imageE";
    4.22 +
    4.23 +AddIs  [image_eqI];
    4.24 +AddSEs [imageE]; 
    4.25 +
    4.26 +goalw thy [o_def] "(f o g)``r = f``(g``r)";
    4.27 +by (Fast_tac 1);
    4.28 +qed "image_compose";
    4.29 +
    4.30 +goal thy "f``(A Un B) = f``A Un f``B";
    4.31 +by (Fast_tac 1);
    4.32 +qed "image_Un";
    4.33 +
    4.34 +
    4.35 +(*** Range of a function -- just a translation for image! ***)
    4.36 +
    4.37 +goal thy "!!b. b=f(x) ==> b : range(f)";
    4.38 +by (EVERY1 [etac image_eqI, rtac UNIV_I]);
    4.39 +bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
    4.40 +
    4.41 +bind_thm ("rangeI", UNIV_I RS imageI);
    4.42 +
    4.43 +val [major,minor] = goal thy 
    4.44 +    "[| b : range(%x.f(x));  !!x. b=f(x) ==> P |] ==> P"; 
    4.45 +by (rtac (major RS imageE) 1);
    4.46 +by (etac minor 1);
    4.47 +qed "rangeE";
    4.48 +
    4.49 +AddIs  [rangeI]; 
    4.50 +AddSEs [rangeE]; 
    4.51 +
    4.52  
    4.53  (*** Set reasoning tools ***)
    4.54  
     5.1 --- a/src/HOL/Set.thy	Fri Apr 04 16:27:39 1997 +0200
     5.2 +++ b/src/HOL/Set.thy	Fri Apr 04 16:33:28 1997 +0200
     5.3 @@ -32,8 +32,6 @@
     5.4    Pow           :: 'a set => 'a set set                 (*powerset*)
     5.5    range         :: ('a => 'b) => 'b set                 (*of function*)
     5.6    Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
     5.7 -  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
     5.8 -  inj_onto      :: ['a => 'b, 'a set] => bool
     5.9    "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
    5.10    (*membership*)
    5.11    "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
    5.12 @@ -149,9 +147,6 @@
    5.13    empty_def     "{}             == {x. False}"
    5.14    insert_def    "insert a B     == {x.x=a} Un B"
    5.15    image_def     "f``A           == {y. ? x:A. y=f(x)}"
    5.16 -  inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
    5.17 -  inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    5.18 -  surj_def      "surj f         == ! y. ? x. y=f(x)"
    5.19  
    5.20  end
    5.21  
     6.1 --- a/src/HOL/equalities.ML	Fri Apr 04 16:27:39 1997 +0200
     6.2 +++ b/src/HOL/equalities.ML	Fri Apr 04 16:33:28 1997 +0200
     6.3 @@ -412,7 +412,7 @@
     6.4  by (Blast_tac 1);
     6.5  qed "Int_Union";
     6.6  
     6.7 -(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
     6.8 +(* Devlin, Setdamentals of Contemporary Set Theory, page 12, exercise 5: 
     6.9     Union of a family of unions **)
    6.10  goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
    6.11  by (Blast_tac 1);