Converted Fun to Isar style.
Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy.
Renamed constant "Fun.op o" to "Fun.comp"
--- a/src/HOL/Bali/AxSem.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Bali/AxSem.thy Thu Sep 26 10:51:29 2002 +0200
@@ -413,7 +413,7 @@
"{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
-apply (rule injI)
+apply (rule inj_onI)
apply auto
done
--- a/src/HOL/Bali/DeclConcepts.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Thu Sep 26 10:51:29 2002 +0200
@@ -2369,9 +2369,8 @@
unique (fields G C)"
apply (rule ws_subcls1_induct, assumption, assumption)
apply (subst fields_rec, assumption)
-apply (auto intro!: unique_map_inj injI
- elim!: unique_append ws_unique_fields_lemma fields_norec
- )
+apply (auto intro!: unique_map_inj inj_onI
+ elim!: unique_append ws_unique_fields_lemma fields_norec)
done
--- a/src/HOL/Bali/Table.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Bali/Table.thy Thu Sep 26 10:51:29 2002 +0200
@@ -213,7 +213,7 @@
done
lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
-apply (rule injI)
+apply (rule inj_onI)
apply auto
done
--- a/src/HOL/Fun.ML Thu Sep 26 10:43:43 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,507 +0,0 @@
-(* Title: HOL/Fun
- ID: $Id$
- Author: Tobias Nipkow, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Lemmas about functions.
-*)
-
-Goal "(f = g) = (! x. f(x)=g(x))";
-by (rtac iffI 1);
-by (Asm_simp_tac 1);
-by (rtac ext 1 THEN Asm_simp_tac 1);
-qed "expand_fun_eq";
-
-val prems = Goal
- "[| f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) |] ==> x=g(u)";
-by (rtac (arg_cong RS box_equals) 1);
-by (REPEAT (resolve_tac (prems@[refl]) 1));
-qed "apply_inverse";
-
-
-section "id";
-
-Goalw [id_def] "id x = x";
-by (rtac refl 1);
-qed "id_apply";
-Addsimps [id_apply];
-
-
-section "o";
-
-Goalw [o_def] "(f o g) x = f (g x)";
-by (rtac refl 1);
-qed "o_apply";
-Addsimps [o_apply];
-
-Goalw [o_def] "f o (g o h) = f o g o h";
-by (rtac ext 1);
-by (rtac refl 1);
-qed "o_assoc";
-
-Goalw [id_def] "id o g = g";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "id_o";
-Addsimps [id_o];
-
-Goalw [id_def] "f o id = f";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "o_id";
-Addsimps [o_id];
-
-Goalw [o_def] "(f o g)`r = f`(g`r)";
-by (Blast_tac 1);
-qed "image_compose";
-
-Goal "f`A = (UN x:A. {f x})";
-by (Blast_tac 1);
-qed "image_eq_UN";
-
-Goalw [o_def] "UNION A (g o f) = UNION (f`A) g";
-by (Blast_tac 1);
-qed "UN_o";
-
-(** lemma for proving injectivity of representation functions for **)
-(** datatypes involving function types **)
-
-Goalw [o_def]
- "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
-by (rtac ext 1);
-by (etac allE 1);
-by (etac allE 1);
-by (etac mp 1);
-by (etac fun_cong 1);
-qed "inj_fun_lemma";
-
-
-section "inj";
-(**NB: inj now just translates to inj_on**)
-
-(*** inj(f): f is a one-to-one function ***)
-
-(*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";
-
-Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
-by (Blast_tac 1);
-qed "injD";
-
-(*Useful with the simplifier*)
-Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
-by (rtac iffI 1);
-by (etac arg_cong 2);
-by (etac injD 1);
-by (assume_tac 1);
-qed "inj_eq";
-
-Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
-by (rtac ext 1);
-by (etac injD 1);
-by (etac fun_cong 1);
-qed "inj_o";
-
-(*** inj_on f A: f is one-to-one over A ***)
-
-val prems = Goalw [inj_on_def]
- "(!! x y. [| x:A; y:A; f(x) = f(y) |] ==> x=y) ==> inj_on f A";
-by (blast_tac (claset() addIs prems) 1);
-qed "inj_onI";
-bind_thm ("injI", inj_onI); (*for compatibility*)
-
-val [major] = Goal
- "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
-by (rtac inj_onI 1);
-by (etac (apply_inverse RS trans) 1);
-by (REPEAT (eresolve_tac [asm_rl,major] 1));
-qed "inj_on_inverseI";
-bind_thm ("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);
-qed "inj_onD";
-
-Goal "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)";
-by (blast_tac (claset() addSDs [inj_onD]) 1);
-qed "inj_on_iff";
-
-Goalw [o_def, inj_on_def]
- "[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A";
-by (Blast_tac 1);
-qed "comp_inj_on";
-
-Goalw [inj_on_def] "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)";
-by (Blast_tac 1);
-qed "inj_on_contraD";
-
-Goal "inj (%s. {s})";
-by (rtac injI 1);
-by (etac singleton_inject 1);
-qed "inj_singleton";
-
-Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
-by (Blast_tac 1);
-qed "subset_inj_on";
-
-
-(** surj **)
-
-val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
-by (blast_tac (claset() addIs [prem RS sym]) 1);
-qed "surjI";
-
-Goalw [surj_def] "surj f ==> range f = UNIV";
-by Auto_tac;
-qed "surj_range";
-
-Goalw [surj_def] "surj f ==> EX x. y = f x";
-by (Blast_tac 1);
-qed "surjD";
-
-val [p1, p2] = Goal "surj f ==> (!!x. y = f x ==> C) ==> C";
-by (cut_facts_tac [p1 RS surjD] 1);
-by (etac exE 1);
-by (rtac p2 1);
-by (atac 1);
-qed "surjE";
-
-Goalw [o_def, surj_def] "[| surj f; surj g |] ==> surj (g o f)";
-by (Clarify_tac 1);
-by (dres_inst_tac [("x","y")] spec 1);
-by (Clarify_tac 1);
-by (dres_inst_tac [("x","x")] spec 1);
-by (Blast_tac 1);
-qed "comp_surj";
-
-
-(** Bijections **)
-
-Goalw [bij_def] "[| inj f; surj f |] ==> bij f";
-by (Blast_tac 1);
-qed "bijI";
-
-Goalw [bij_def] "bij f ==> inj f";
-by (Blast_tac 1);
-qed "bij_is_inj";
-
-Goalw [bij_def] "bij f ==> surj f";
-by (Blast_tac 1);
-qed "bij_is_surj";
-
-
-(** We seem to need both the id-forms and the (%x. x) forms; the latter can
- arise by rewriting, while id may be used explicitly. **)
-
-Goal "(%x. x) ` Y = Y";
-by (Blast_tac 1);
-qed "image_ident";
-
-Goalw [id_def] "id ` Y = Y";
-by (Blast_tac 1);
-qed "image_id";
-Addsimps [image_ident, image_id];
-
-Goal "(%x. x) -` Y = Y";
-by (Blast_tac 1);
-qed "vimage_ident";
-
-Goalw [id_def] "id -` A = A";
-by Auto_tac;
-qed "vimage_id";
-Addsimps [vimage_ident, vimage_id];
-
-Goal "f -` (f ` A) = {y. EX x:A. f x = f y}";
-by (blast_tac (claset() addIs [sym]) 1);
-qed "vimage_image_eq";
-
-Goal "f ` (f -` A) <= A";
-by (Blast_tac 1);
-qed "image_vimage_subset";
-
-Goal "f ` (f -` A) = A Int range f";
-by (Blast_tac 1);
-qed "image_vimage_eq";
-Addsimps [image_vimage_eq];
-
-Goal "surj f ==> f ` (f -` A) = A";
-by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
-qed "surj_image_vimage_eq";
-
-Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A";
-by (Blast_tac 1);
-qed "inj_vimage_image_eq";
-
-Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A";
-by (blast_tac (claset() addIs [sym]) 1);
-qed "vimage_subsetD";
-
-Goalw [inj_on_def] "inj f ==> B <= f ` A ==> f -` B <= A";
-by (Blast_tac 1);
-qed "vimage_subsetI";
-
-Goalw [bij_def] "bij f ==> (f -` B <= A) = (B <= f ` A)";
-by (blast_tac (claset() delrules [subsetI]
- addIs [vimage_subsetI, vimage_subsetD]) 1);
-qed "vimage_subset_eq";
-
-Goal "f`(A Int B) <= f`A Int f`B";
-by (Blast_tac 1);
-qed "image_Int_subset";
-
-Goal "f`A - f`B <= f`(A - B)";
-by (Blast_tac 1);
-qed "image_diff_subset";
-
-Goalw [inj_on_def]
- "[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B";
-by (Blast_tac 1);
-qed "inj_on_image_Int";
-
-Goalw [inj_on_def]
- "[| inj_on f C; A<=C; B<=C |] ==> f`(A-B) = f`A - f`B";
-by (Blast_tac 1);
-qed "inj_on_image_set_diff";
-
-Goalw [inj_on_def] "inj f ==> f`(A Int B) = f`A Int f`B";
-by (Blast_tac 1);
-qed "image_Int";
-
-Goalw [inj_on_def] "inj f ==> f`(A-B) = f`A - f`B";
-by (Blast_tac 1);
-qed "image_set_diff";
-
-Goal "inj f ==> (f a : f`A) = (a : A)";
-by (blast_tac (claset() addDs [injD]) 1);
-qed "inj_image_mem_iff";
-
-Goalw [inj_on_def] "inj f ==> (f`A <= f`B) = (A<=B)";
-by (Blast_tac 1);
-qed "inj_image_subset_iff";
-
-Goal "inj f ==> (f`A = f`B) = (A = B)";
-by (blast_tac (claset() addDs [injD]) 1);
-qed "inj_image_eq_iff";
-
-Goal "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))";
-by (Blast_tac 1);
-qed "image_UN";
-
-(*injectivity's required. Left-to-right inclusion holds even if A is empty*)
-Goalw [inj_on_def]
- "[| inj_on f C; ALL x:A. B x <= C; j:A |] \
-\ ==> f ` (INTER A B) = (INT x:A. f ` B x)";
-by (Blast_tac 1);
-qed "image_INT";
-
-(*Compare with image_INT: no use of inj_on, and if f is surjective then
- it doesn't matter whether A is empty*)
-Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)";
-by (asm_full_simp_tac (simpset() addsimps [inj_on_def, surj_def]) 1);
-by (Blast_tac 1);
-qed "bij_image_INT";
-
-Goal "surj f ==> -(f`A) <= f`(-A)";
-by (auto_tac (claset(), simpset() addsimps [surj_def]));
-qed "surj_Compl_image_subset";
-
-Goal "inj f ==> f`(-A) <= -(f`A)";
-by (auto_tac (claset(), simpset() addsimps [inj_on_def]));
-qed "inj_image_Compl_subset";
-
-Goalw [bij_def] "bij f ==> f`(-A) = -(f`A)";
-by (rtac equalityI 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset,
- surj_Compl_image_subset])));
-qed "bij_image_Compl_eq";
-
-val set_cs = claset() delrules [equalityI];
-
-
-section "fun_upd";
-
-Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
-by Safe_tac;
-by (etac subst 1);
-by (rtac ext 2);
-by Auto_tac;
-qed "fun_upd_idem_iff";
-
-(* f x = y ==> f(x:=y) = f *)
-bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
-
-(* f(x := f x) = f *)
-AddIffs [refl RS fun_upd_idem];
-
-Goal "(f(x:=y))z = (if z=x then y else f z)";
-by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
-qed "fun_upd_apply";
-Addsimps [fun_upd_apply];
-
-(* fun_upd_apply supersedes these two, but they are useful
- if fun_upd_apply is intentionally removed from the simpset *)
-Goal "(f(x:=y)) x = y";
-by (Simp_tac 1);
-qed "fun_upd_same";
-
-Goal "z~=x ==> (f(x:=y)) z = f z";
-by (Asm_simp_tac 1);
-qed "fun_upd_other";
-
-Goal "f(x:=y,x:=z) = f(x:=z)";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "fun_upd_upd";
-Addsimps [fun_upd_upd];
-
-(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
-local
- fun gen_fun_upd None T _ _ = None
- | gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y);
- fun dest_fun_T1 (Type (_, T :: Ts)) = T;
- fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) =
- let
- fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) =
- if v aconv x then Some g else gen_fun_upd (find g) T v w
- | find t = None;
- in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end;
-
- val ss = simpset ();
- val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1);
-in
- val fun_upd2_simproc =
- Simplifier.simproc (Theory.sign_of (the_context ()))
- "fun_upd2" ["f(v := w, x := y)"]
- (fn sg => fn _ => fn t =>
- case find_double t of (T, None) => None
- | (T, Some rhs) => Some (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover));
-end;
-Addsimprocs[fun_upd2_simproc];
-
-Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)";
-by (rtac ext 1);
-by Auto_tac;
-qed "fun_upd_twist";
-
-
-(*** -> and Pi, by Florian Kammueller and LCP ***)
-
-val prems = Goalw [Pi_def]
-"[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = arbitrary|] \
-\ ==> f: Pi A B";
-by (auto_tac (claset(), simpset() addsimps prems));
-qed "Pi_I";
-
-val prems = Goal
-"[| !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = arbitrary|] ==> f: A funcset B";
-by (blast_tac (claset() addIs Pi_I::prems) 1);
-qed "funcsetI";
-
-Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
-by Auto_tac;
-qed "Pi_mem";
-
-Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
-by Auto_tac;
-qed "funcset_mem";
-
-Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = arbitrary";
-by Auto_tac;
-qed "apply_arb";
-
-Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
-by (rtac ext 1);
-by Auto_tac;
-bind_thm ("Pi_extensionality", ballI RSN (3, result()));
-
-
-(*** compose ***)
-
-Goalw [Pi_def, compose_def, restrict_def]
- "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
-by Auto_tac;
-qed "funcset_compose";
-
-Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
-\ ==> compose A h (compose A g f) = compose A (compose B h g) f";
-by (res_inst_tac [("A","A")] Pi_extensionality 1);
-by (blast_tac (claset() addIs [funcset_compose]) 1);
-by (blast_tac (claset() addIs [funcset_compose]) 1);
-by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);
-by Auto_tac;
-qed "compose_assoc";
-
-Goal "x : A ==> compose A g f x = g(f(x))";
-by (asm_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
-qed "compose_eq";
-
-Goal "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C";
-by (auto_tac (claset(), simpset() addsimps [image_def, compose_eq]));
-qed "surj_compose";
-
-Goal "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A";
-by (auto_tac (claset(), simpset() addsimps [inj_on_def, compose_eq]));
-qed "inj_on_compose";
-
-
-(*** restrict / bounded abstraction ***)
-
-Goal "f`A <= B ==> (%x:A. f x) : A funcset B";
-by (auto_tac (claset(),
- simpset() addsimps [restrict_def, Pi_def]));
-qed "restrict_in_funcset";
-
-val prems = Goalw [restrict_def, Pi_def]
- "(!!x. x: A ==> f x: B x) ==> (%x:A. f x) : Pi A B";
-by (asm_simp_tac (simpset() addsimps prems) 1);
-qed "restrictI";
-
-Goal "(%y:A. f y) x = (if x : A then f x else arbitrary)";
-by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
-qed "restrict_apply";
-Addsimps [restrict_apply];
-
-val prems = Goal
- "(!!x. x: A ==> f x = g x) ==> (%x:A. f x) = (%x:A. g x)";
-by (rtac ext 1);
-by (auto_tac (claset(),
- simpset() addsimps prems@[restrict_def, Pi_def]));
-qed "restrict_ext";
-
-Goalw [inj_on_def, restrict_def] "inj_on (restrict f A) A = inj_on f A";
-by Auto_tac;
-qed "inj_on_restrict_eq";
-
-
-Goal "f : A funcset B ==> compose A (%y:B. y) f = f";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def]));
-qed "Id_compose";
-
-Goal "g : A funcset B ==> compose A g (%x:A. x) = g";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def]));
-qed "compose_Id";
-
-
-(*** Pi ***)
-
-Goalw [Pi_def] "[| B(x) = {}; x: A |] ==> (PI x: A. B x) = {}";
-by Auto_tac;
-qed "Pi_eq_empty";
-
-Goal "[| (PI x: A. B x) ~= {}; x: A |] ==> B(x) ~= {}";
-by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
-qed "Pi_total1";
-
-Goal "Pi {} B = { %x. arbitrary }";
-by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
-qed "Pi_empty";
-
-val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
-by (auto_tac (claset(),
- simpset() addsimps [impOfSubs major]));
-qed "Pi_mono";
--- a/src/HOL/Fun.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Fun.thy Thu Sep 26 10:51:29 2002 +0200
@@ -6,94 +6,447 @@
Notions about functions.
*)
-Fun = Typedef +
+theory Fun = Typedef:
instance set :: (type) order
- (subset_refl,subset_trans,subset_antisym,psubset_eq)
-consts
- fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+ by (intro_classes,
+ (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
+
+constdefs
+ fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+ "fun_upd f a b == % x. if x=a then b else f x"
nonterminals
updbinds updbind
syntax
- "_updbind" :: ['a, 'a] => updbind ("(2_ :=/ _)")
- "" :: updbind => updbinds ("_")
- "_updbinds" :: [updbind, updbinds] => updbinds ("_,/ _")
- "_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [1000,0] 900)
+ "_updbind" :: "['a, 'a] => updbind" ("(2_ :=/ _)")
+ "" :: "updbind => updbinds" ("_")
+ "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _")
+ "_Update" :: "['a, updbinds] => 'a" ("_/'((_)')" [1000,0] 900)
translations
"_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
"f(x:=y)" == "fun_upd f x y"
-defs
- fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
-
(* Hint: to define the sum of two functions (or maps), use sum_case.
A nice infix syntax could be defined (in Datatype.thy or below) by
consts
fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
translations
- "fun_sum" == "sum_case"
+ "fun_sum" == sum_case
*)
constdefs
- id :: 'a => 'a
+ id :: "'a => 'a"
"id == %x. x"
- o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55)
+ comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "o" 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"
+text{*compatibility*}
+lemmas o_def = comp_def
syntax (xsymbols)
- "op o" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\\<circ>" 55)
+ comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\<circ>" 55)
+
-syntax
- inj :: ('a => 'b) => bool (*injective*)
+constdefs
+ inj_on :: "['a => 'b, 'a set] => bool" (*injective*)
+ "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
+text{*A common special case: functions injective over the entire domain type.*}
+syntax inj :: "('a => 'b) => bool"
translations
"inj f" == "inj_on f UNIV"
constdefs
- surj :: ('a => 'b) => bool (*surjective*)
+ surj :: "('a => 'b) => bool" (*surjective*)
"surj f == ! y. ? x. y=f(x)"
- bij :: ('a => 'b) => bool (*bijective*)
+ bij :: "('a => 'b) => bool" (*bijective*)
"bij f == inj f & surj f"
-(*The Pi-operator, by Florian Kammueller*)
+
+text{*As a simplification rule, it replaces all function equalities by
+ first-order equalities.*}
+lemma expand_fun_eq: "(f = g) = (! x. f(x)=g(x))"
+apply (rule iffI)
+apply (simp (no_asm_simp))
+apply (rule ext, simp (no_asm_simp))
+done
+
+lemma apply_inverse:
+ "[| f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) |] ==> x=g(u)"
+by auto
+
+
+text{*The Identity Function: @{term id}*}
+lemma id_apply [simp]: "id x = x"
+by (simp add: id_def)
+
+
+subsection{*The Composition Operator: @{term "f \<circ> g"}*}
+
+lemma o_apply [simp]: "(f o g) x = f (g x)"
+by (simp add: comp_def)
+
+lemma o_assoc: "f o (g o h) = f o g o h"
+by (simp add: comp_def)
+
+lemma id_o [simp]: "id o g = g"
+by (simp add: comp_def)
+
+lemma o_id [simp]: "f o id = f"
+by (simp add: comp_def)
+
+lemma image_compose: "(f o g) ` r = f`(g`r)"
+by (simp add: comp_def, blast)
+
+lemma image_eq_UN: "f`A = (UN x:A. {f x})"
+by blast
+
+lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
+by (unfold comp_def, blast)
+
+text{*Lemma for proving injectivity of representation functions for
+datatypes involving function types*}
+lemma inj_fun_lemma:
+ "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa"
+by (simp add: comp_def expand_fun_eq)
+
+
+subsection{*The Injectivity Predicate, @{term inj}*}
+
+text{*NB: @{term inj} now just translates to @{term inj_on}*}
+
+
+text{*For Proofs in @{text "Tools/datatype_rep_proofs"}*}
+lemma datatype_injI:
+ "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
+by (simp add: inj_on_def)
+
+lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
+by (simp add: inj_on_def)
+
+(*Useful with the simplifier*)
+lemma inj_eq: "inj(f) ==> (f(x) = f(y)) = (x=y)"
+by (force simp add: inj_on_def)
+
+lemma inj_o: "[| inj f; f o g = f o h |] ==> g = h"
+by (simp add: comp_def inj_on_def expand_fun_eq)
+
+
+subsection{*The Predicate @{term inj_on}: Injectivity On A Restricted Domain*}
+
+lemma inj_onI:
+ "(!! x y. [| x:A; y:A; f(x) = f(y) |] ==> x=y) ==> inj_on f A"
+by (simp add: inj_on_def)
+
+lemma inj_on_inverseI: "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A"
+by (auto dest: arg_cong [of concl: g] simp add: inj_on_def)
+
+lemma inj_onD: "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y"
+by (unfold inj_on_def, blast)
+
+lemma inj_on_iff: "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"
+by (blast dest!: inj_onD)
+
+lemma comp_inj_on:
+ "[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A"
+by (simp add: comp_def inj_on_def)
+
+lemma inj_on_contraD: "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"
+by (unfold inj_on_def, blast)
-constdefs
- Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
- "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = arbitrary}"
+lemma inj_singleton: "inj (%s. {s})"
+by (simp add: inj_on_def)
+
+lemma subset_inj_on: "[| A<=B; inj_on f B |] ==> inj_on f A"
+by (unfold inj_on_def, blast)
+
+
+subsection{*The Predicate @{term surj}: Surjectivity*}
+
+lemma surjI: "(!! x. g(f x) = x) ==> surj g"
+apply (simp add: surj_def)
+apply (blast intro: sym)
+done
+
+lemma surj_range: "surj f ==> range f = UNIV"
+by (auto simp add: surj_def)
+
+lemma surjD: "surj f ==> EX x. y = f x"
+by (simp add: surj_def)
+
+lemma surjE: "surj f ==> (!!x. y = f x ==> C) ==> C"
+by (simp add: surj_def, blast)
+
+lemma comp_surj: "[| surj f; surj g |] ==> surj (g o f)"
+apply (simp add: comp_def surj_def, clarify)
+apply (drule_tac x = y in spec, clarify)
+apply (drule_tac x = x in spec, blast)
+done
+
+
+
+subsection{*The Predicate @{term bij}: Bijectivity*}
+
+lemma bijI: "[| inj f; surj f |] ==> bij f"
+by (simp add: bij_def)
+
+lemma bij_is_inj: "bij f ==> inj f"
+by (simp add: bij_def)
+
+lemma bij_is_surj: "bij f ==> surj f"
+by (simp add: bij_def)
+
+
+subsection{*Facts About the Identity Function*}
- restrict :: "['a => 'b, 'a set] => ('a => 'b)"
- "restrict f A == (%x. if x : A then f x else arbitrary)"
+text{*We seem to need both the @{term id} forms and the @{term "\<lambda>x. x"}
+forms. The latter can arise by rewriting, while @{term id} may be used
+explicitly.*}
+
+lemma image_ident [simp]: "(%x. x) ` Y = Y"
+by blast
+
+lemma image_id [simp]: "id ` Y = Y"
+by (simp add: id_def)
+
+lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
+by blast
+
+lemma vimage_id [simp]: "id -` A = A"
+by (simp add: id_def)
+
+lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
+by (blast intro: sym)
+
+lemma image_vimage_subset: "f ` (f -` A) <= A"
+by blast
+
+lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
+by blast
+
+lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
+by (simp add: surj_range)
+
+lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
+by (simp add: inj_on_def, blast)
+
+lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A"
+apply (unfold surj_def)
+apply (blast intro: sym)
+done
+
+lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A"
+by (unfold inj_on_def, blast)
+
+lemma vimage_subset_eq: "bij f ==> (f -` B <= A) = (B <= f ` A)"
+apply (unfold bij_def)
+apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
+done
+
+lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
+by blast
+
+lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
+by blast
-syntax
- "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
- funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr 60)
- "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3%_:_./ _)" [0, 0, 3] 3)
-syntax (xsymbols)
- "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3\\<lambda>_\\<in>_./ _)" [0, 0, 3] 3)
+lemma inj_on_image_Int:
+ "[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B"
+apply (simp add: inj_on_def, blast)
+done
+
+lemma inj_on_image_set_diff:
+ "[| inj_on f C; A<=C; B<=C |] ==> f`(A-B) = f`A - f`B"
+apply (simp add: inj_on_def, blast)
+done
+
+lemma image_Int: "inj f ==> f`(A Int B) = f`A Int f`B"
+by (simp add: inj_on_def, blast)
+
+lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B"
+by (simp add: inj_on_def, blast)
+
+lemma inj_image_mem_iff: "inj f ==> (f a : f`A) = (a : A)"
+by (blast dest: injD)
+
+lemma inj_image_subset_iff: "inj f ==> (f`A <= f`B) = (A<=B)"
+by (simp add: inj_on_def, blast)
+
+lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)"
+by (blast dest: injD)
+
+lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
+by blast
+
+(*injectivity's required. Left-to-right inclusion holds even if A is empty*)
+lemma image_INT:
+ "[| inj_on f C; ALL x:A. B x <= C; j:A |]
+ ==> f ` (INTER A B) = (INT x:A. f ` B x)"
+apply (simp add: inj_on_def, blast)
+done
+
+(*Compare with image_INT: no use of inj_on, and if f is surjective then
+ it doesn't matter whether A is empty*)
+lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"
+apply (simp add: bij_def)
+apply (simp add: inj_on_def surj_def, blast)
+done
+
+lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
+by (auto simp add: surj_def)
+
+lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)"
+by (auto simp add: inj_on_def)
- (*Giving funcset an arrow syntax (-> or =>) clashes with many existing theories*)
+lemma bij_image_Compl_eq: "bij f ==> f`(-A) = -(f`A)"
+apply (simp add: bij_def)
+apply (rule equalityI)
+apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset)
+done
+
+
+subsection{*Function Updating*}
+
+lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)"
+apply (simp add: fun_upd_def, safe)
+apply (erule subst)
+apply (rule_tac [2] ext, auto)
+done
+
+(* f x = y ==> f(x:=y) = f *)
+lemmas fun_upd_idem = fun_upd_idem_iff [THEN iffD2, standard]
+
+(* f(x := f x) = f *)
+declare refl [THEN fun_upd_idem, iff]
+
+lemma fun_upd_apply [simp]: "(f(x:=y))z = (if z=x then y else f z)"
+apply (simp (no_asm) add: fun_upd_def)
+done
+
+(* fun_upd_apply supersedes these two, but they are useful
+ if fun_upd_apply is intentionally removed from the simpset *)
+lemma fun_upd_same: "(f(x:=y)) x = y"
+by simp
+
+lemma fun_upd_other: "z~=x ==> (f(x:=y)) z = f z"
+by simp
+
+lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)"
+by (simp add: expand_fun_eq)
+
+lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
+by (rule ext, auto)
+
+text{*The ML section includes some compatibility bindings and a simproc
+for function updates, in addition to the usual ML-bindings of theorems.*}
+ML
+{*
+val id_def = thm "id_def";
+val inj_on_def = thm "inj_on_def";
+val surj_def = thm "surj_def";
+val bij_def = thm "bij_def";
+val fun_upd_def = thm "fun_upd_def";
-syntax (xsymbols)
- "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<Pi> _\\<in>_./ _)" 10)
+val o_def = thm "comp_def";
+val injI = thm "inj_onI";
+val inj_inverseI = thm "inj_on_inverseI";
+val set_cs = claset() delrules [equalityI];
+
+val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];
+
+(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
+local
+ fun gen_fun_upd None T _ _ = None
+ | gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y)
+ fun dest_fun_T1 (Type (_, T :: Ts)) = T
+ fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) =
+ let
+ fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) =
+ if v aconv x then Some g else gen_fun_upd (find g) T v w
+ | find t = None
+ in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
+
+ val ss = simpset ()
+ val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1)
+in
+ val fun_upd2_simproc =
+ Simplifier.simproc (Theory.sign_of (the_context ()))
+ "fun_upd2" ["f(v := w, x := y)"]
+ (fn sg => fn _ => fn t =>
+ case find_double t of (T, None) => None
+ | (T, Some rhs) => Some (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover))
+end;
+Addsimprocs[fun_upd2_simproc];
-translations
- "PI x:A. B" => "Pi A (%x. B)"
- "A funcset B" => "Pi A (_K B)"
- "%x:A. f" == "restrict (%x. f) A"
-
-constdefs
- compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
- "compose A g f == %x:A. g (f x)"
+val expand_fun_eq = thm "expand_fun_eq";
+val apply_inverse = thm "apply_inverse";
+val id_apply = thm "id_apply";
+val o_apply = thm "o_apply";
+val o_assoc = thm "o_assoc";
+val id_o = thm "id_o";
+val o_id = thm "o_id";
+val image_compose = thm "image_compose";
+val image_eq_UN = thm "image_eq_UN";
+val UN_o = thm "UN_o";
+val inj_fun_lemma = thm "inj_fun_lemma";
+val datatype_injI = thm "datatype_injI";
+val injD = thm "injD";
+val inj_eq = thm "inj_eq";
+val inj_o = thm "inj_o";
+val inj_onI = thm "inj_onI";
+val inj_on_inverseI = thm "inj_on_inverseI";
+val inj_onD = thm "inj_onD";
+val inj_on_iff = thm "inj_on_iff";
+val comp_inj_on = thm "comp_inj_on";
+val inj_on_contraD = thm "inj_on_contraD";
+val inj_singleton = thm "inj_singleton";
+val subset_inj_on = thm "subset_inj_on";
+val surjI = thm "surjI";
+val surj_range = thm "surj_range";
+val surjD = thm "surjD";
+val surjE = thm "surjE";
+val comp_surj = thm "comp_surj";
+val bijI = thm "bijI";
+val bij_is_inj = thm "bij_is_inj";
+val bij_is_surj = thm "bij_is_surj";
+val image_ident = thm "image_ident";
+val image_id = thm "image_id";
+val vimage_ident = thm "vimage_ident";
+val vimage_id = thm "vimage_id";
+val vimage_image_eq = thm "vimage_image_eq";
+val image_vimage_subset = thm "image_vimage_subset";
+val image_vimage_eq = thm "image_vimage_eq";
+val surj_image_vimage_eq = thm "surj_image_vimage_eq";
+val inj_vimage_image_eq = thm "inj_vimage_image_eq";
+val vimage_subsetD = thm "vimage_subsetD";
+val vimage_subsetI = thm "vimage_subsetI";
+val vimage_subset_eq = thm "vimage_subset_eq";
+val image_Int_subset = thm "image_Int_subset";
+val image_diff_subset = thm "image_diff_subset";
+val inj_on_image_Int = thm "inj_on_image_Int";
+val inj_on_image_set_diff = thm "inj_on_image_set_diff";
+val image_Int = thm "image_Int";
+val image_set_diff = thm "image_set_diff";
+val inj_image_mem_iff = thm "inj_image_mem_iff";
+val inj_image_subset_iff = thm "inj_image_subset_iff";
+val inj_image_eq_iff = thm "inj_image_eq_iff";
+val image_UN = thm "image_UN";
+val image_INT = thm "image_INT";
+val bij_image_INT = thm "bij_image_INT";
+val surj_Compl_image_subset = thm "surj_Compl_image_subset";
+val inj_image_Compl_subset = thm "inj_image_Compl_subset";
+val bij_image_Compl_eq = thm "bij_image_Compl_eq";
+val fun_upd_idem_iff = thm "fun_upd_idem_iff";
+val fun_upd_idem = thm "fun_upd_idem";
+val fun_upd_apply = thm "fun_upd_apply";
+val fun_upd_same = thm "fun_upd_same";
+val fun_upd_other = thm "fun_upd_other";
+val fun_upd_upd = thm "fun_upd_upd";
+val fun_upd_twist = thm "fun_upd_twist";
+*}
end
-
-ML
-val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];
--- a/src/HOL/Hilbert_Choice.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Hilbert_Choice.thy Thu Sep 26 10:51:29 2002 +0200
@@ -39,6 +39,10 @@
use "Hilbert_Choice_lemmas.ML"
declare someI_ex [elim?];
+lemma Inv_mem: "[| f ` A = B; x \<in> B |] ==> Inv A f x \<in> A"
+apply (unfold Inv_def)
+apply (fast intro: someI2)
+done
lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
-- {* dynamically-scoped fact for TFL *}
--- a/src/HOL/Hilbert_Choice_lemmas.ML Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Hilbert_Choice_lemmas.ML Thu Sep 26 10:51:29 2002 +0200
@@ -212,10 +212,6 @@
section "Inverse of a PI-function (restricted domain)";
-Goalw [Inv_def] "f ` A = B ==> (%x:B. (Inv A f) x) : B funcset A";
-by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
-qed "Inv_funcset";
-
Goal "[| inj_on f A; x : A |] ==> Inv A f (f x) = x";
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
by (blast_tac (claset() addIs [someI2]) 1);
@@ -236,15 +232,6 @@
by (blast_tac (claset() addIs [inj_onI] addDs [Inv_injective, injD]) 1);
qed "inj_on_Inv";
-Goal "[| inj_on f A; f ` A = B |] \
-\ ==> compose A (%y:B. (Inv A f) y) f = (%x:A. x)";
-by (asm_simp_tac (simpset() addsimps [compose_def]) 1);
-by (rtac restrict_ext 1);
-by Auto_tac;
-by (etac subst 1);
-by (asm_full_simp_tac (simpset() addsimps [Inv_f_f]) 1);
-qed "compose_Inv_id";
-
section "split and SOME";
--- a/src/HOL/Induct/LList.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Induct/LList.thy Thu Sep 26 10:51:29 2002 +0200
@@ -1,7 +1,6 @@
(* Title: HOL/Induct/LList.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
Shares NIL, CONS, List_case with List.thy
@@ -445,7 +444,7 @@
subsection{* Isomorphisms *}
lemma inj_Rep_LList: "inj Rep_LList"
-apply (rule inj_inverseI)
+apply (rule inj_on_inverseI)
apply (rule Rep_LList_inverse)
done
--- a/src/HOL/IsaMakefile Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/IsaMakefile Thu Sep 26 10:51:29 2002 +0200
@@ -83,7 +83,7 @@
$(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
- Fun.ML Fun.thy Gfp.ML Gfp.thy \
+ Fun.thy Gfp.ML Gfp.thy \
Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
Integ/Equiv.ML Integ/Equiv.thy Integ/int.ML Integ/Int.thy \
@@ -197,7 +197,8 @@
HOL-Library: HOL $(LOG)/HOL-Library.gz
$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
- Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
+ Library/FuncSet.thy Library/Library.thy \
+ Library/List_Prefix.thy Library/Multiset.thy \
Library/Permutation.thy Library/Primes.thy \
Library/Quotient.thy Library/Ring_and_Field.thy \
Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
@@ -275,20 +276,16 @@
HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz
$(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
- Library/Primes.thy \
- GroupTheory/Bij.thy GroupTheory/Bij.ML\
- GroupTheory/Coset.thy GroupTheory/Coset.ML\
- GroupTheory/DirProd.thy GroupTheory/DirProd.ML\
- GroupTheory/Exponent.thy GroupTheory/Exponent.ML\
- GroupTheory/FactGroup.thy GroupTheory/FactGroup.ML\
- GroupTheory/Group.thy GroupTheory/Group.ML\
- GroupTheory/Homomorphism.thy GroupTheory/Homomorphism.ML\
- GroupTheory/PiSets.ML GroupTheory/PiSets.thy \
- GroupTheory/Ring.thy GroupTheory/Ring.ML\
- GroupTheory/RingConstr.thy GroupTheory/RingConstr.ML\
- GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
- GroupTheory/ROOT.ML
- @$(ISATOOL) usedir $(OUT)/HOL GroupTheory
+ Library/Primes.thy Library/FuncSet.thy \
+ GroupTheory/Bij.thy \
+ GroupTheory/Coset.thy \
+ GroupTheory/Exponent.thy \
+ GroupTheory/Group.thy \
+ GroupTheory/Ring.thy \
+ GroupTheory/Sylow.thy \
+ GroupTheory/ROOT.ML \
+ GroupTheory/document/root.tex
+ @$(ISATOOL) usedir -g true $(OUT)/HOL GroupTheory
## HOL-Hoare
--- a/src/HOL/List.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/List.thy Thu Sep 26 10:51:29 2002 +0200
@@ -451,7 +451,7 @@
by (induct ys) (auto simp add: map_eq_Cons)
lemma inj_mapI: "inj f ==> inj (map f)"
-by (rules dest: map_injective injD intro: injI)
+by (rules dest: map_injective injD intro: inj_onI)
lemma inj_mapD: "inj (map f) ==> inj f"
apply (unfold inj_on_def)
@@ -1241,7 +1241,7 @@
apply(rule wf_subset)
prefer 2 apply (rule Int_lower1)
apply(rule wf_prod_fun_image)
- prefer 2 apply (rule injI)
+ prefer 2 apply (rule inj_onI)
apply auto
done
--- a/src/HOL/MicroJava/J/WellForm.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Thu Sep 26 10:51:29 2002 +0200
@@ -230,7 +230,7 @@
apply( simp add: wf_cdecl_def)
apply( rule unique_map_inj)
apply( simp)
-apply( rule injI)
+apply( rule inj_onI)
apply( simp)
apply( safe dest!: wf_cdecl_supD)
apply( drule subcls1_wfD)
@@ -244,7 +244,7 @@
apply( erule unique_append)
apply( rule unique_map_inj)
apply( clarsimp)
-apply (rule injI)
+apply (rule inj_onI)
apply( simp)
apply(auto dest!: widen_fields_defpl)
done
--- a/src/HOL/Nat.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Nat.thy Thu Sep 26 10:51:29 2002 +0200
@@ -80,7 +80,7 @@
text {* Isomorphisms: @{text Abs_Nat} and @{text Rep_Nat} *}
lemma inj_Rep_Nat: "inj Rep_Nat"
- apply (rule inj_inverseI)
+ apply (rule inj_on_inverseI)
apply (rule Rep_Nat_inverse)
done
@@ -111,7 +111,7 @@
lemma inj_Suc: "inj Suc"
apply (unfold Suc_def)
- apply (rule injI)
+ apply (rule inj_onI)
apply (drule inj_on_Abs_Nat [THEN inj_onD])
apply (rule Rep_Nat Nat.Suc_RepI)+
apply (drule inj_Suc_Rep [THEN injD])
--- a/src/HOL/Tools/datatype_prop.ML Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Thu Sep 26 10:51:29 2002 +0200
@@ -168,7 +168,7 @@
fun make_primrecs new_type_names descr sorts thy =
let
- val o_name = "Fun.op o";
+ val o_name = "Fun.comp";
val sign = Theory.sign_of thy;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Sep 26 10:51:29 2002 +0200
@@ -55,7 +55,7 @@
val Numb_name = "Datatype_Universe.Numb";
val Lim_name = "Datatype_Universe.Lim";
val Funs_name = "Datatype_Universe.Funs";
- val o_name = "Fun.op o";
+ val o_name = "Fun.comp";
val sum_case_name = "Datatype.sum.sum_case";
val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
--- a/src/HOL/ex/Tarski.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/ex/Tarski.thy Thu Sep 26 10:51:29 2002 +0200
@@ -1,12 +1,11 @@
(* Title: HOL/ex/Tarski.thy
ID: $Id$
Author: Florian Kammüller, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
*)
-header {* The full theorem of Tarski *}
+header {* The Full Theorem of Tarski *}
-theory Tarski = Main:
+theory Tarski = Main + FuncSet:
text {*
Minimal version of lattice theory plus the full theorem of Tarski:
@@ -21,39 +20,31 @@
pset :: "'a set"
order :: "('a * 'a) set"
-syntax
- "@pset" :: "'a potype => 'a set" ("_ .<A>" [90] 90)
- "@order" :: "'a potype => ('a *'a)set" ("_ .<r>" [90] 90)
-
-translations
- "po.<A>" == "pset po"
- "po.<r>" == "order po"
-
constdefs
monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
"monotone f A r == \<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r"
least :: "['a => bool, 'a potype] => 'a"
- "least P po == @ x. x: po.<A> & P x &
- (\<forall>y \<in> po.<A>. P y --> (x,y): po.<r>)"
+ "least P po == @ x. x: pset po & P x &
+ (\<forall>y \<in> pset po. P y --> (x,y): order po)"
greatest :: "['a => bool, 'a potype] => 'a"
- "greatest P po == @ x. x: po.<A> & P x &
- (\<forall>y \<in> po.<A>. P y --> (y,x): po.<r>)"
+ "greatest P po == @ x. x: pset po & P x &
+ (\<forall>y \<in> pset po. P y --> (y,x): order po)"
lub :: "['a set, 'a potype] => 'a"
- "lub S po == least (%x. \<forall>y\<in>S. (y,x): po.<r>) po"
+ "lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po"
glb :: "['a set, 'a potype] => 'a"
- "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): po.<r>) po"
+ "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
isLub :: "['a set, 'a potype, 'a] => bool"
- "isLub S po == %L. (L: po.<A> & (\<forall>y\<in>S. (y,L): po.<r>) &
- (\<forall>z\<in>po.<A>. (\<forall>y\<in>S. (y,z): po.<r>) --> (L,z): po.<r>))"
+ "isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
+ (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po))"
isGlb :: "['a set, 'a potype, 'a] => bool"
- "isGlb S po == %G. (G: po.<A> & (\<forall>y\<in>S. (G,y): po.<r>) &
- (\<forall>z \<in> po.<A>. (\<forall>y\<in>S. (z,y): po.<r>) --> (z,G): po.<r>))"
+ "isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
+ (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po))"
"fix" :: "[('a => 'a), 'a set] => 'a set"
"fix f A == {x. x: A & f x = x}"
@@ -70,17 +61,17 @@
"Top po == greatest (%x. True) po"
PartialOrder :: "('a potype) set"
- "PartialOrder == {P. refl (P.<A>) (P.<r>) & antisym (P.<r>) &
- trans (P.<r>)}"
+ "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) &
+ trans (order P)}"
CompleteLattice :: "('a potype) set"
"CompleteLattice == {cl. cl: PartialOrder &
- (\<forall>S. S <= cl.<A> --> (\<exists>L. isLub S cl L)) &
- (\<forall>S. S <= cl.<A> --> (\<exists>G. isGlb S cl G))}"
+ (\<forall>S. S <= pset cl --> (\<exists>L. isLub S cl L)) &
+ (\<forall>S. S <= pset cl --> (\<exists>G. isGlb S cl G))}"
CLF :: "('a potype * ('a => 'a)) set"
"CLF == SIGMA cl: CompleteLattice.
- {f. f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)}"
+ {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)}"
induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
"induced A r == {(a,b). a : A & b: A & (a,b): r}"
@@ -90,8 +81,8 @@
sublattice :: "('a potype * 'a set)set"
"sublattice ==
SIGMA cl: CompleteLattice.
- {S. S <= cl.<A> &
- (| pset = S, order = induced S (cl.<r>) |): CompleteLattice }"
+ {S. S <= pset cl &
+ (| pset = S, order = induced S (order cl) |): CompleteLattice }"
syntax
"@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
@@ -101,15 +92,15 @@
constdefs
dual :: "'a potype => 'a potype"
- "dual po == (| pset = po.<A>, order = converse (po.<r>) |)"
+ "dual po == (| pset = pset po, order = converse (order po) |)"
locale (open) PO =
fixes cl :: "'a potype"
and A :: "'a set"
and r :: "('a * 'a) set"
assumes cl_po: "cl : PartialOrder"
- defines A_def: "A == cl.<A>"
- and r_def: "r == cl.<r>"
+ defines A_def: "A == pset cl"
+ and r_def: "r == order cl"
locale (open) CL = PO +
assumes cl_co: "cl : CompleteLattice"
@@ -254,8 +245,8 @@
by (rule PO_imp_trans)
lemma CompleteLatticeI:
- "[| po \<in> PartialOrder; (\<forall>S. S <= po.<A> --> (\<exists>L. isLub S po L));
- (\<forall>S. S <= po.<A> --> (\<exists>G. isGlb S po G))|]
+ "[| po \<in> PartialOrder; (\<forall>S. S <= pset po --> (\<exists>L. isLub S po L));
+ (\<forall>S. S <= pset po --> (\<exists>G. isGlb S po G))|]
==> po \<in> CompleteLattice"
apply (unfold CompleteLattice_def, blast)
done
@@ -268,19 +259,19 @@
dualPO)
done
-lemma (in PO) dualA_iff: "(dual cl.<A>) = cl.<A>"
+lemma (in PO) dualA_iff: "pset (dual cl) = pset cl"
by (simp add: dual_def)
-lemma (in PO) dualr_iff: "((x, y) \<in> (dual cl.<r>)) = ((y, x) \<in> cl.<r>)"
+lemma (in PO) dualr_iff: "((x, y) \<in> (order(dual cl))) = ((y, x) \<in> order cl)"
by (simp add: dual_def)
lemma (in PO) monotone_dual:
- "monotone f (cl.<A>) (cl.<r>) ==> monotone f (dual cl.<A>) (dual cl.<r>)"
-apply (simp add: monotone_def dualA_iff dualr_iff)
-done
+ "monotone f (pset cl) (order cl)
+ ==> monotone f (pset (dual cl)) (order(dual cl))"
+by (simp add: monotone_def dualA_iff dualr_iff)
lemma (in PO) interval_dual:
- "[| x \<in> A; y \<in> A|] ==> interval r x y = interval (dual cl.<r>) y x"
+ "[| x \<in> A; y \<in> A|] ==> interval r x y = interval (order(dual cl)) y x"
apply (simp add: interval_def dualr_iff)
apply (fold r_def, fast)
done
@@ -416,7 +407,7 @@
*}
lemma (in CLF) [simp]:
- "f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)"
+ "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
apply (insert f_cl)
apply (simp add: CLF_def)
done
@@ -424,7 +415,7 @@
declare (in CLF) f_cl [simp]
-lemma (in CLF) f_in_funcset: "f \<in> A funcset A"
+lemma (in CLF) f_in_funcset: "f \<in> A -> A"
by (simp add: A_def)
lemma (in CLF) monotone_f: "monotone f A r"
@@ -460,7 +451,7 @@
apply (rule ballI)
apply (rule transE)
apply (rule CO_trans)
--- {* instantiates @{text "(x, ???z) \<in> cl.<r> to (x, f x)"}, *}
+-- {* instantiates @{text "(x, ???z) \<in> order cl to (x, f x)"}, *}
-- {* because of the def of @{text H} *}
apply fast
-- {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *}
@@ -807,7 +798,7 @@
apply (simp add: intY1_def interval_def intY1_elem)
done
-lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 funcset intY1"
+lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
apply (rule restrictI)
apply (erule intY1_f_closed)
done