# HG changeset patch # User paulson # Date 918044767 -3600 # Node ID cd237a10cbf8210baa73deebaed72c2ff3be5506 # Parent 9a59cf8ae9b5a35d7d396f5fde99d83e4e034677 inj is now a translation of inj_on diff -r 9a59cf8ae9b5 -r cd237a10cbf8 src/HOL/Fun.ML --- a/src/HOL/Fun.ML Wed Feb 03 13:23:24 1999 +0100 +++ b/src/HOL/Fun.ML Wed Feb 03 13:26:07 1999 +0100 @@ -64,22 +64,17 @@ section "inj"; +(**NB: inj now just translates to inj_on**) (*** inj(f): f is a one-to-one function ***) -val prems = Goalw [inj_def] - "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)"; -by (blast_tac (claset() addIs prems) 1); -qed "injI"; +(*for Tools/datatype_rep_proofs*) +val [prem] = Goalw [inj_on_def] + "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"; +by (blast_tac (claset() addIs [prem RS spec RS mp]) 1); +qed "datatype_injI"; -val [major] = Goal "(!!x. g(f(x)) = x) ==> inj(f)"; -by (rtac injI 1); -by (etac (arg_cong RS box_equals) 1); -by (rtac major 1); -by (rtac major 1); -qed "inj_inverseI"; - -Goalw [inj_def] "[| inj(f); f(x) = f(y) |] ==> x=y"; +Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y"; by (Blast_tac 1); qed "injD"; @@ -116,6 +111,7 @@ "(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_on f A"; by (blast_tac (claset() addIs prems) 1); qed "inj_onI"; +val injI = inj_onI; (*for compatibility*) val [major] = Goal "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A"; @@ -123,6 +119,7 @@ by (etac (apply_inverse RS trans) 1); by (REPEAT (eresolve_tac [asm_rl,major] 1)); qed "inj_on_inverseI"; +val inj_inverseI = inj_on_inverseI; (*for compatibility*) Goalw [inj_on_def] "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y"; by (Blast_tac 1); @@ -141,21 +138,17 @@ qed "subset_inj_on"; -(*** Lemmas about inj ***) +(*** Lemmas about injective functions and inv ***) -Goalw [o_def] "[| inj(f); inj_on g (range f) |] ==> inj(g o f)"; -by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1); -qed "comp_inj"; - -Goal "inj(f) ==> inj_on f A"; -by (blast_tac (claset() addIs [injD, inj_onI]) 1); -qed "inj_imp"; +Goalw [o_def] "[| inj_on f A; inj_on g (range f) |] ==> inj_on (g o f) A"; +by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1); +qed "comp_inj_on"; Goalw [inv_def] "y : range(f) ==> f(inv f y) = y"; by (fast_tac (claset() addIs [selectI]) 1); qed "f_inv_f"; -Goal "[| inv f x=inv f y; x: range(f); y: range(f) |] ==> x=y"; +Goal "[| inv f x = inv f y; x: range(f); y: range(f) |] ==> x=y"; by (rtac (arg_cong RS box_equals) 1); by (REPEAT (ares_tac [f_inv_f] 1)); qed "inv_injective"; @@ -175,16 +168,15 @@ by (Blast_tac 1); qed "inj_on_image_set_diff"; -Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B"; +Goalw [inj_on_def] "inj f ==> f``(A Int B) = f``A Int f``B"; by (Blast_tac 1); qed "image_Int"; -Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B"; +Goalw [inj_on_def] "inj f ==> f``(A-B) = f``A - f``B"; by (Blast_tac 1); qed "image_set_diff"; - val [major] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g"; by (blast_tac (claset() addIs [major RS sym]) 1); qed "surjI"; diff -r 9a59cf8ae9b5 -r cd237a10cbf8 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Wed Feb 03 13:23:24 1999 +0100 +++ b/src/HOL/Fun.thy Wed Feb 03 13:26:07 1999 +0100 @@ -10,18 +10,12 @@ instance set :: (term) order (subset_refl,subset_trans,subset_antisym,psubset_eq) -consts - - id :: 'a => 'a - o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) - inj, surj :: ('a => 'b) => bool (*inj/surjective*) - inj_on :: ['a => 'b, 'a set] => bool - inv :: ('a => 'b) => ('b => 'a) - fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" - nonterminals updbinds updbind +consts + fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" + syntax (* Let expressions *) @@ -36,15 +30,32 @@ "f(x:=y)" == "fun_upd f x y" defs + fun_upd_def "f(a:=b) == % x. if x=a then b else f x" - id_def "id == %x. x" - o_def "f o g == %x. f(g(x))" - inj_def "inj f == ! x y. f(x)=f(y) --> x=y" - inj_on_def "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" - surj_def "surj f == ! y. ? x. y=f(x)" - inv_def "inv(f::'a=>'b) == % y. @x. f(x)=y" - fun_upd_def "f(a:=b) == % x. if x=a then b else f x" + +constdefs + id :: 'a => 'a + "id == %x. x" + + o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) + "f o g == %x. f(g(x))" + + inj_on :: ['a => 'b, 'a set] => bool + "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" + surj :: ('a => 'b) => bool (*surjective*) + "surj f == ! y. ? x. y=f(x)" + + inv :: ('a => 'b) => ('b => 'a) + "inv(f::'a=>'b) == % y. @x. f(x)=y" + + + +syntax + inj :: ('a => 'b) => bool (*injective*) + +translations + "inj f" == "inj_on f UNIV" (*The Pi-operator, by Florian Kammueller*) diff -r 9a59cf8ae9b5 -r cd237a10cbf8 src/HOL/Set.ML --- a/src/HOL/Set.ML Wed Feb 03 13:23:24 1999 +0100 +++ b/src/HOL/Set.ML Wed Feb 03 13:26:07 1999 +0100 @@ -6,8 +6,6 @@ Set theory for higher-order logic. A set is simply a predicate. *) -open Set; - section "Relating predicates and sets"; Addsimps [Collect_mem_eq]; diff -r 9a59cf8ae9b5 -r cd237a10cbf8 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Feb 03 13:23:24 1999 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Feb 03 13:26:07 1999 +0100 @@ -32,7 +32,6 @@ val image_name = Sign.intern_const (sign_of Set.thy) "op ``"; val UNIV_name = Sign.intern_const (sign_of Set.thy) "UNIV"; -val inj_name = Sign.intern_const (sign_of Fun.thy) "inj"; val inj_on_name = Sign.intern_const (sign_of Fun.thy) "inj_on"; val inv_name = Sign.intern_const (sign_of Fun.thy) "inv"; @@ -238,17 +237,25 @@ val AbsT = Univ_elT --> T; val Abs_name = Sign.intern_const sg ("Abs_" ^ s); - val inj_on_Abs_thm = prove_goalw_cterm [] (cterm_of sg - (HOLogic.mk_Trueprop (Const (inj_on_name, [AbsT, UnivT] ---> HOLogic.boolT) $ - Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))) + val inj_Abs_thm = + prove_goalw_cterm [] + (cterm_of sg + (HOLogic.mk_Trueprop + (Const (inj_on_name, [AbsT, UnivT] ---> HOLogic.boolT) $ + Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))) (fn _ => [rtac inj_on_inverseI 1, etac thm1 1]); - val inj_Rep_thm = prove_goalw_cterm [] (cterm_of sg - (HOLogic.mk_Trueprop (Const (inj_name, RepT --> HOLogic.boolT) $ - Const (Rep_name, RepT)))) + val setT = HOLogic.mk_setT T + + val inj_Rep_thm = + prove_goalw_cterm [] + (cterm_of sg + (HOLogic.mk_Trueprop + (Const (inj_on_name, [RepT, setT] ---> HOLogic.boolT) $ + Const (Rep_name, RepT) $ Const (UNIV_name, setT)))) (fn _ => [rtac inj_inverseI 1, rtac thm2 1]) - in (inj_on_Abs_thm, inj_Rep_thm) end; + in (inj_Abs_thm, inj_Rep_thm) end; val newT_iso_inj_thms = map prove_newT_iso_inj_thm (new_type_names ~~ newT_iso_axms ~~ newTs ~~ @@ -409,17 +416,20 @@ TRY (hyp_subst_tac 1), rtac refl 1])])])]); - val inj_thms'' = map (fn r => - r RS (allI RS (inj_def RS meta_eq_to_obj_eq RS iffD2))) - (split_conj_thm inj_thm); + val inj_thms'' = map (fn r => r RS datatype_injI) + (split_conj_thm inj_thm); - val elem_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5) - (HOLogic.mk_Trueprop (mk_conj ind_concl2))) (fn _ => - [indtac induction 1, - rewrite_goals_tac rewrites, - REPEAT (EVERY - [resolve_tac rep_intrs 1, - REPEAT ((atac 1) ORELSE (resolve_tac elem_thms 1))])]); + val elem_thm = + prove_goalw_cterm [] + (cterm_of (sign_of thy5) + (HOLogic.mk_Trueprop (mk_conj ind_concl2))) + (fn _ => + [indtac induction 1, + rewrite_goals_tac rewrites, + REPEAT (EVERY + [resolve_tac rep_intrs 1, + REPEAT ((atac 1) ORELSE + (resolve_tac elem_thms 1))])]); in (inj_thms @ inj_thms'', elem_thms @ (split_conj_thm elem_thm)) end; diff -r 9a59cf8ae9b5 -r cd237a10cbf8 src/HOL/Univ.ML --- a/src/HOL/Univ.ML Wed Feb 03 13:23:24 1999 +0100 +++ b/src/HOL/Univ.ML Wed Feb 03 13:26:07 1999 +0100 @@ -94,8 +94,8 @@ (** Atomic nodes **) -Goalw [Atom_def, inj_def] "inj(Atom)"; -by (blast_tac (claset() addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1); +Goalw [Atom_def] "inj(Atom)"; +by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1); qed "inj_Atom"; val Atom_inject = inj_Atom RS injD; @@ -367,12 +367,12 @@ AddIffs [In0_eq, In1_eq]; -Goalw [inj_def] "inj In0"; -by (Blast_tac 1); +Goal "inj In0"; +by (blast_tac (claset() addSIs [injI]) 1); qed "inj_In0"; -Goalw [inj_def] "inj In1"; -by (Blast_tac 1); +Goal "inj In1"; +by (blast_tac (claset() addSIs [injI]) 1); qed "inj_In1"; diff -r 9a59cf8ae9b5 -r cd237a10cbf8 src/HOL/ex/set.ML --- a/src/HOL/ex/set.ML Wed Feb 03 13:23:24 1999 +0100 +++ b/src/HOL/ex/set.ML Wed Feb 03 13:26:07 1999 +0100 @@ -112,21 +112,13 @@ by (Blast_tac 1); qed "surj_if_then_else"; -val [injf,injg,compl,bij] = -goal Lfp.thy - "[| inj_on f X; inj_on g (-X); -(f``X) = g``(-X); \ -\ bij = (%z. if z:X then f(z) else g(z)) |] ==> \ -\ inj(bij) & surj(bij)"; -val f_eq_gE = make_elim (compl RS disj_lemma); -by (stac bij 1); -by (rtac conjI 1); -by (rtac (compl RS surj_if_then_else) 2); -by (rewtac inj_def); -by (cut_facts_tac [injf,injg] 1); -by (EVERY1 [rtac allI, rtac allI, stac split_if, rtac conjI, stac split_if]); -by (fast_tac (claset() addEs [inj_onD, sym RS f_eq_gE]) 1); -by (stac split_if 1); -by (fast_tac (claset() addEs [inj_onD, f_eq_gE]) 1); +Goalw [inj_on_def] + "[| inj_on f X; inj_on g (-X); -(f``X) = g``(-X); \ +\ bij = (%z. if z:X then f(z) else g(z)) |] \ +\ ==> inj(bij) & surj(bij)"; +by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1); + (*PROOF FAILED if inj_onD*) +by (blast_tac (claset() addDs [disj_lemma, sym RSN (2,disj_lemma)]) 1); qed "bij_if_then_else"; Goal "? X. X = - (g``(- (f``X)))"; @@ -136,12 +128,13 @@ qed "decomposition"; val [injf,injg] = goal Lfp.thy - "[| inj(f:: 'a=>'b); inj(g:: 'b=>'a) |] ==> \ + "[| inj (f:: 'a=>'b); inj (g:: 'b=>'a) |] ==> \ \ ? h:: 'a=>'b. inj(h) & surj(h)"; by (rtac (decomposition RS exE) 1); by (rtac exI 1); by (rtac bij_if_then_else 1); -by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1, +by (rtac refl 4); +by (EVERY [rtac ([subset_UNIV,injf] MRS subset_inj_on) 1, rtac (injg RS inj_on_inv) 1]); by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, etac imageE, etac ssubst, rtac rangeI]);