inj is now a translation of inj_on
authorpaulson
Wed Feb 03 13:26:07 1999 +0100 (1999-02-03)
changeset 6171cd237a10cbf8
parent 6170 9a59cf8ae9b5
child 6172 8a505e0694d0
inj is now a translation of inj_on
src/HOL/Fun.ML
src/HOL/Fun.thy
src/HOL/Set.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Univ.ML
src/HOL/ex/set.ML
     1.1 --- a/src/HOL/Fun.ML	Wed Feb 03 13:23:24 1999 +0100
     1.2 +++ b/src/HOL/Fun.ML	Wed Feb 03 13:26:07 1999 +0100
     1.3 @@ -64,22 +64,17 @@
     1.4  
     1.5  
     1.6  section "inj";
     1.7 +(**NB: inj now just translates to inj_on**)
     1.8  
     1.9  (*** inj(f): f is a one-to-one function ***)
    1.10  
    1.11 -val prems = Goalw [inj_def]
    1.12 -    "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
    1.13 -by (blast_tac (claset() addIs prems) 1);
    1.14 -qed "injI";
    1.15 +(*for Tools/datatype_rep_proofs*)
    1.16 +val [prem] = Goalw [inj_on_def]
    1.17 +    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)";
    1.18 +by (blast_tac (claset() addIs [prem RS spec RS mp]) 1);
    1.19 +qed "datatype_injI";
    1.20  
    1.21 -val [major] = Goal "(!!x. g(f(x)) = x) ==> inj(f)";
    1.22 -by (rtac injI 1);
    1.23 -by (etac (arg_cong RS box_equals) 1);
    1.24 -by (rtac major 1);
    1.25 -by (rtac major 1);
    1.26 -qed "inj_inverseI";
    1.27 -
    1.28 -Goalw [inj_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
    1.29 +Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
    1.30  by (Blast_tac 1);
    1.31  qed "injD";
    1.32  
    1.33 @@ -116,6 +111,7 @@
    1.34      "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
    1.35  by (blast_tac (claset() addIs prems) 1);
    1.36  qed "inj_onI";
    1.37 +val injI = inj_onI;                  (*for compatibility*)
    1.38  
    1.39  val [major] = Goal 
    1.40      "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
    1.41 @@ -123,6 +119,7 @@
    1.42  by (etac (apply_inverse RS trans) 1);
    1.43  by (REPEAT (eresolve_tac [asm_rl,major] 1));
    1.44  qed "inj_on_inverseI";
    1.45 +val inj_inverseI = inj_on_inverseI;   (*for compatibility*)
    1.46  
    1.47  Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
    1.48  by (Blast_tac 1);
    1.49 @@ -141,21 +138,17 @@
    1.50  qed "subset_inj_on";
    1.51  
    1.52  
    1.53 -(*** Lemmas about inj ***)
    1.54 +(*** Lemmas about injective functions and inv ***)
    1.55  
    1.56 -Goalw [o_def] "[| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
    1.57 -by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
    1.58 -qed "comp_inj";
    1.59 -
    1.60 -Goal "inj(f) ==> inj_on f A";
    1.61 -by (blast_tac (claset() addIs [injD, inj_onI]) 1);
    1.62 -qed "inj_imp";
    1.63 +Goalw [o_def] "[| inj_on f A;  inj_on g (range f) |] ==> inj_on (g o f) A";
    1.64 +by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
    1.65 +qed "comp_inj_on";
    1.66  
    1.67  Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
    1.68  by (fast_tac (claset() addIs [selectI]) 1);
    1.69  qed "f_inv_f";
    1.70  
    1.71 -Goal "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
    1.72 +Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
    1.73  by (rtac (arg_cong RS box_equals) 1);
    1.74  by (REPEAT (ares_tac [f_inv_f] 1));
    1.75  qed "inv_injective";
    1.76 @@ -175,16 +168,15 @@
    1.77  by (Blast_tac 1);
    1.78  qed "inj_on_image_set_diff";
    1.79  
    1.80 -Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B";
    1.81 +Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B";
    1.82  by (Blast_tac 1);
    1.83  qed "image_Int";
    1.84  
    1.85 -Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B";
    1.86 +Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B";
    1.87  by (Blast_tac 1);
    1.88  qed "image_set_diff";
    1.89  
    1.90  
    1.91 -
    1.92  val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
    1.93  by (blast_tac (claset() addIs [major RS sym]) 1);
    1.94  qed "surjI";
     2.1 --- a/src/HOL/Fun.thy	Wed Feb 03 13:23:24 1999 +0100
     2.2 +++ b/src/HOL/Fun.thy	Wed Feb 03 13:26:07 1999 +0100
     2.3 @@ -10,18 +10,12 @@
     2.4  
     2.5  instance set :: (term) order
     2.6                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
     2.7 -consts
     2.8 -
     2.9 -  id          ::  'a => 'a
    2.10 -  o           :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    2.11 -  inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
    2.12 -  inj_on      :: ['a => 'b, 'a set] => bool
    2.13 -  inv         :: ('a => 'b) => ('b => 'a)
    2.14 -  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    2.15 -
    2.16  nonterminals
    2.17    updbinds  updbind
    2.18  
    2.19 +consts
    2.20 +  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    2.21 +
    2.22  syntax
    2.23  
    2.24    (* Let expressions *)
    2.25 @@ -36,15 +30,32 @@
    2.26    "f(x:=y)"                     == "fun_upd f x y"
    2.27  
    2.28  defs
    2.29 +  fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
    2.30  
    2.31 -  id_def	"id             == %x. x"
    2.32 -  o_def   	"f o g          == %x. f(g(x))"
    2.33 -  inj_def	"inj f          == ! x y. f(x)=f(y) --> x=y"
    2.34 -  inj_on_def	"inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    2.35 -  surj_def	"surj f         == ! y. ? x. y=f(x)"
    2.36 -  inv_def	"inv(f::'a=>'b) == % y. @x. f(x)=y"
    2.37 -  fun_upd_def	"f(a:=b)        == % x. if x=a then b else f x"
    2.38 +  
    2.39 +constdefs
    2.40 +  id ::  'a => 'a
    2.41 +    "id == %x. x"
    2.42 +
    2.43 +  o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    2.44 +    "f o g == %x. f(g(x))"
    2.45 +
    2.46 +  inj_on :: ['a => 'b, 'a set] => bool
    2.47 +    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    2.48  
    2.49 +  surj :: ('a => 'b) => bool                   (*surjective*)
    2.50 +    "surj f == ! y. ? x. y=f(x)"
    2.51 +  
    2.52 +  inv :: ('a => 'b) => ('b => 'a)
    2.53 +    "inv(f::'a=>'b) == % y. @x. f(x)=y"
    2.54 +  
    2.55 +
    2.56 +
    2.57 +syntax
    2.58 +  inj   :: ('a => 'b) => bool                   (*injective*)
    2.59 +
    2.60 +translations
    2.61 +  "inj f" == "inj_on f UNIV"
    2.62  
    2.63  (*The Pi-operator, by Florian Kammueller*)
    2.64    
     3.1 --- a/src/HOL/Set.ML	Wed Feb 03 13:23:24 1999 +0100
     3.2 +++ b/src/HOL/Set.ML	Wed Feb 03 13:26:07 1999 +0100
     3.3 @@ -6,8 +6,6 @@
     3.4  Set theory for higher-order logic.  A set is simply a predicate.
     3.5  *)
     3.6  
     3.7 -open Set;
     3.8 -
     3.9  section "Relating predicates and sets";
    3.10  
    3.11  Addsimps [Collect_mem_eq];
     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Feb 03 13:23:24 1999 +0100
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Feb 03 13:26:07 1999 +0100
     4.3 @@ -32,7 +32,6 @@
     4.4  
     4.5  val image_name = Sign.intern_const (sign_of Set.thy) "op ``";
     4.6  val UNIV_name = Sign.intern_const (sign_of Set.thy) "UNIV";
     4.7 -val inj_name = Sign.intern_const (sign_of Fun.thy) "inj";
     4.8  val inj_on_name = Sign.intern_const (sign_of Fun.thy) "inj_on";
     4.9  val inv_name = Sign.intern_const (sign_of Fun.thy) "inv";
    4.10  
    4.11 @@ -238,17 +237,25 @@
    4.12          val AbsT = Univ_elT --> T;
    4.13          val Abs_name = Sign.intern_const sg ("Abs_" ^ s);
    4.14  
    4.15 -        val inj_on_Abs_thm = prove_goalw_cterm [] (cterm_of sg
    4.16 -          (HOLogic.mk_Trueprop (Const (inj_on_name, [AbsT, UnivT] ---> HOLogic.boolT) $
    4.17 -            Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT))))
    4.18 +        val inj_Abs_thm = 
    4.19 +	    prove_goalw_cterm [] 
    4.20 +	      (cterm_of sg
    4.21 +	       (HOLogic.mk_Trueprop 
    4.22 +		(Const (inj_on_name, [AbsT, UnivT] ---> HOLogic.boolT) $
    4.23 +		 Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT))))
    4.24                (fn _ => [rtac inj_on_inverseI 1, etac thm1 1]);
    4.25  
    4.26 -        val inj_Rep_thm = prove_goalw_cterm [] (cterm_of sg
    4.27 -          (HOLogic.mk_Trueprop (Const (inj_name, RepT --> HOLogic.boolT) $
    4.28 -            Const (Rep_name, RepT))))
    4.29 +        val setT = HOLogic.mk_setT T
    4.30 +
    4.31 +        val inj_Rep_thm =
    4.32 +	    prove_goalw_cterm []
    4.33 +	      (cterm_of sg
    4.34 +	       (HOLogic.mk_Trueprop
    4.35 +		(Const (inj_on_name, [RepT, setT] ---> HOLogic.boolT) $
    4.36 +		 Const (Rep_name, RepT) $ Const (UNIV_name, setT))))
    4.37                (fn _ => [rtac inj_inverseI 1, rtac thm2 1])
    4.38  
    4.39 -      in (inj_on_Abs_thm, inj_Rep_thm) end;
    4.40 +      in (inj_Abs_thm, inj_Rep_thm) end;
    4.41  
    4.42      val newT_iso_inj_thms = map prove_newT_iso_inj_thm
    4.43        (new_type_names ~~ newT_iso_axms ~~ newTs ~~
    4.44 @@ -409,17 +416,20 @@
    4.45                        TRY (hyp_subst_tac 1),
    4.46                        rtac refl 1])])])]);
    4.47  
    4.48 -        val inj_thms'' = map (fn r =>
    4.49 -          r RS (allI RS (inj_def RS meta_eq_to_obj_eq RS iffD2)))
    4.50 -            (split_conj_thm inj_thm);
    4.51 +        val inj_thms'' = map (fn r => r RS datatype_injI)
    4.52 +                             (split_conj_thm inj_thm);
    4.53  
    4.54 -        val elem_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
    4.55 -          (HOLogic.mk_Trueprop (mk_conj ind_concl2))) (fn _ =>
    4.56 -            [indtac induction 1,
    4.57 -             rewrite_goals_tac rewrites,
    4.58 -             REPEAT (EVERY
    4.59 -               [resolve_tac rep_intrs 1,
    4.60 -                REPEAT ((atac 1) ORELSE (resolve_tac elem_thms 1))])]);
    4.61 +        val elem_thm = 
    4.62 +	    prove_goalw_cterm []
    4.63 +	      (cterm_of (sign_of thy5)
    4.64 +	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
    4.65 +	      (fn _ =>
    4.66 +	       [indtac induction 1,
    4.67 +		rewrite_goals_tac rewrites,
    4.68 +		REPEAT (EVERY
    4.69 +			[resolve_tac rep_intrs 1,
    4.70 +			 REPEAT ((atac 1) ORELSE
    4.71 +				 (resolve_tac elem_thms 1))])]);
    4.72  
    4.73        in (inj_thms @ inj_thms'', elem_thms @ (split_conj_thm elem_thm))
    4.74        end;
     5.1 --- a/src/HOL/Univ.ML	Wed Feb 03 13:23:24 1999 +0100
     5.2 +++ b/src/HOL/Univ.ML	Wed Feb 03 13:26:07 1999 +0100
     5.3 @@ -94,8 +94,8 @@
     5.4  
     5.5  (** Atomic nodes **)
     5.6  
     5.7 -Goalw [Atom_def, inj_def] "inj(Atom)";
     5.8 -by (blast_tac (claset() addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
     5.9 +Goalw [Atom_def] "inj(Atom)";
    5.10 +by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1);
    5.11  qed "inj_Atom";
    5.12  val Atom_inject = inj_Atom RS injD;
    5.13  
    5.14 @@ -367,12 +367,12 @@
    5.15  
    5.16  AddIffs [In0_eq, In1_eq];
    5.17  
    5.18 -Goalw [inj_def] "inj In0";
    5.19 -by (Blast_tac 1);
    5.20 +Goal "inj In0";
    5.21 +by (blast_tac (claset() addSIs [injI]) 1);
    5.22  qed "inj_In0";
    5.23  
    5.24 -Goalw [inj_def] "inj In1";
    5.25 -by (Blast_tac 1);
    5.26 +Goal "inj In1";
    5.27 +by (blast_tac (claset() addSIs [injI]) 1);
    5.28  qed "inj_In1";
    5.29  
    5.30  
     6.1 --- a/src/HOL/ex/set.ML	Wed Feb 03 13:23:24 1999 +0100
     6.2 +++ b/src/HOL/ex/set.ML	Wed Feb 03 13:26:07 1999 +0100
     6.3 @@ -112,21 +112,13 @@
     6.4  by (Blast_tac 1);
     6.5  qed "surj_if_then_else";
     6.6  
     6.7 -val [injf,injg,compl,bij] = 
     6.8 -goal Lfp.thy
     6.9 -    "[| inj_on f X;  inj_on g (-X);  -(f``X) = g``(-X); \
    6.10 -\       bij = (%z. if z:X then f(z) else g(z)) |] ==> \
    6.11 -\       inj(bij) & surj(bij)";
    6.12 -val f_eq_gE = make_elim (compl RS disj_lemma);
    6.13 -by (stac bij 1);
    6.14 -by (rtac conjI 1);
    6.15 -by (rtac (compl RS surj_if_then_else) 2);
    6.16 -by (rewtac inj_def);
    6.17 -by (cut_facts_tac [injf,injg] 1);
    6.18 -by (EVERY1 [rtac allI, rtac allI, stac split_if, rtac conjI, stac split_if]);
    6.19 -by (fast_tac (claset() addEs  [inj_onD, sym RS f_eq_gE]) 1);
    6.20 -by (stac split_if 1);
    6.21 -by (fast_tac (claset() addEs  [inj_onD, f_eq_gE]) 1);
    6.22 +Goalw [inj_on_def]
    6.23 +     "[| inj_on f X;  inj_on g (-X);  -(f``X) = g``(-X); \
    6.24 +\        bij = (%z. if z:X then f(z) else g(z)) |]       \
    6.25 +\     ==> inj(bij) & surj(bij)";
    6.26 +by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1);
    6.27 +   (*PROOF FAILED if inj_onD*)
    6.28 +by (blast_tac (claset() addDs [disj_lemma, sym RSN (2,disj_lemma)]) 1);
    6.29  qed "bij_if_then_else";
    6.30  
    6.31  Goal "? X. X = - (g``(- (f``X)))";
    6.32 @@ -136,12 +128,13 @@
    6.33  qed "decomposition";
    6.34  
    6.35  val [injf,injg] = goal Lfp.thy 
    6.36 -   "[| inj(f:: 'a=>'b);  inj(g:: 'b=>'a) |] ==> \
    6.37 +   "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |] ==> \
    6.38  \   ? h:: 'a=>'b. inj(h) & surj(h)";
    6.39  by (rtac (decomposition RS exE) 1);
    6.40  by (rtac exI 1);
    6.41  by (rtac bij_if_then_else 1);
    6.42 -by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1,
    6.43 +by (rtac refl 4);
    6.44 +by (EVERY [rtac ([subset_UNIV,injf] MRS subset_inj_on) 1,
    6.45             rtac (injg RS inj_on_inv) 1]);
    6.46  by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI,
    6.47              etac imageE, etac ssubst, rtac rangeI]);