src/HOL/Fun.ML
changeset 4830 bd73675adbed
parent 4656 134d24ddaad3
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/Fun.ML	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/Fun.ML	Mon Apr 27 16:45:11 1998 +0200
     1.3 @@ -77,52 +77,52 @@
     1.4  qed "inj_transfer";
     1.5  
     1.6  
     1.7 -(*** inj_onto f A: f is one-to-one over A ***)
     1.8 +(*** inj_on f A: f is one-to-one over A ***)
     1.9  
    1.10 -val prems = goalw thy [inj_onto_def]
    1.11 -    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
    1.12 +val prems = goalw thy [inj_on_def]
    1.13 +    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
    1.14  by (blast_tac (claset() addIs prems) 1);
    1.15 -qed "inj_ontoI";
    1.16 +qed "inj_onI";
    1.17  
    1.18  val [major] = goal thy 
    1.19 -    "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A";
    1.20 -by (rtac inj_ontoI 1);
    1.21 +    "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
    1.22 +by (rtac inj_onI 1);
    1.23  by (etac (apply_inverse RS trans) 1);
    1.24  by (REPEAT (eresolve_tac [asm_rl,major] 1));
    1.25 -qed "inj_onto_inverseI";
    1.26 +qed "inj_on_inverseI";
    1.27  
    1.28 -val major::prems = goalw thy [inj_onto_def]
    1.29 -    "[| inj_onto f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
    1.30 +val major::prems = goalw thy [inj_on_def]
    1.31 +    "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
    1.32  by (rtac (major RS bspec RS bspec RS mp) 1);
    1.33  by (REPEAT (resolve_tac prems 1));
    1.34 -qed "inj_ontoD";
    1.35 +qed "inj_onD";
    1.36  
    1.37 -goal thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
    1.38 -by (blast_tac (claset() addSDs [inj_ontoD]) 1);
    1.39 -qed "inj_onto_iff";
    1.40 +goal thy "!!x y.[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
    1.41 +by (blast_tac (claset() addSDs [inj_onD]) 1);
    1.42 +qed "inj_on_iff";
    1.43  
    1.44  val major::prems = goal thy
    1.45 -    "[| inj_onto f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
    1.46 +    "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
    1.47  by (rtac contrapos 1);
    1.48 -by (etac (major RS inj_ontoD) 2);
    1.49 +by (etac (major RS inj_onD) 2);
    1.50  by (REPEAT (resolve_tac prems 1));
    1.51 -qed "inj_onto_contraD";
    1.52 +qed "inj_on_contraD";
    1.53  
    1.54 -goalw thy [inj_onto_def]
    1.55 -    "!!A B. [| A<=B; inj_onto f B |] ==> inj_onto f A";
    1.56 +goalw thy [inj_on_def]
    1.57 +    "!!A B. [| A<=B; inj_on f B |] ==> inj_on f A";
    1.58  by (Blast_tac 1);
    1.59 -qed "subset_inj_onto";
    1.60 +qed "subset_inj_on";
    1.61  
    1.62  
    1.63  (*** Lemmas about inj ***)
    1.64  
    1.65  goalw thy [o_def]
    1.66 -    "!!f g. [| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
    1.67 -by (fast_tac (claset() addIs [injI] addEs [injD, inj_ontoD]) 1);
    1.68 +    "!!f g. [| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
    1.69 +by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
    1.70  qed "comp_inj";
    1.71  
    1.72 -val [prem] = goal thy "inj(f) ==> inj_onto f A";
    1.73 -by (blast_tac (claset() addIs [prem RS injD, inj_ontoI]) 1);
    1.74 +val [prem] = goal thy "inj(f) ==> inj_on f A";
    1.75 +by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1);
    1.76  qed "inj_imp";
    1.77  
    1.78  val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y";
    1.79 @@ -135,20 +135,20 @@
    1.80  by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
    1.81  qed "inv_injective";
    1.82  
    1.83 -goal thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
    1.84 -by (fast_tac (claset() addIs [inj_ontoI] 
    1.85 +goal thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
    1.86 +by (fast_tac (claset() addIs [inj_onI] 
    1.87                        addEs [inv_injective,injD]) 1);
    1.88 -qed "inj_onto_inv";
    1.89 +qed "inj_on_inv";
    1.90  
    1.91 -goalw thy [inj_onto_def]
    1.92 -   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
    1.93 +goalw thy [inj_on_def]
    1.94 +   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
    1.95  by (Blast_tac 1);
    1.96 -qed "inj_onto_image_Int";
    1.97 +qed "inj_on_image_Int";
    1.98  
    1.99 -goalw thy [inj_onto_def]
   1.100 -   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
   1.101 +goalw thy [inj_on_def]
   1.102 +   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
   1.103  by (Blast_tac 1);
   1.104 -qed "inj_onto_image_set_diff";
   1.105 +qed "inj_on_image_set_diff";
   1.106  
   1.107  goalw thy [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B";
   1.108  by (Blast_tac 1);