--- 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";
--- 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*)
--- 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];
--- 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;
--- 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";
--- 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]);