src/HOL/Fun.ML
changeset 2912 3fac3e8d5d3e
parent 2890 f27002fc531d
child 2922 580647a879cf
     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 -