# HG changeset patch # User paulson # Date 1033030289 -7200 # Node ID db4005b40cc65d6b6335ba4cd8ceb61f9120dbd5 # Parent 3736cf381e15d027a210b199823a4c58000b7171 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp" diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Bali/AxSem.thy --- 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\ {Q}" lemma inj_triple: "inj (\(P,t,Q). {P} t\ {Q})" -apply (rule injI) +apply (rule inj_onI) apply auto done diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Bali/DeclConcepts.thy --- 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 diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Bali/Table.thy --- 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 (\k. (k, C))" -apply (rule injI) +apply (rule inj_onI) apply auto done diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Fun.ML --- 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"; diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Fun.thy --- 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 "\\" 55) + comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\" 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 \ 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 "\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\\_\\_./ _)" [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\\ _\\_./ _)" 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"))]; diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Hilbert_Choice.thy --- 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 \ B |] ==> Inv A f x \ A" +apply (unfold Inv_def) +apply (fast intro: someI2) +done lemma tfl_some: "\P x. P x --> P (Eps P)" -- {* dynamically-scoped fact for TFL *} diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Hilbert_Choice_lemmas.ML --- 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"; diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Induct/LList.thy --- 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 diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/IsaMakefile --- 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 diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/List.thy --- 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 diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/MicroJava/J/WellForm.thy --- 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 diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Nat.thy --- 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]) diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Tools/datatype_prop.ML --- 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; diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/Tools/datatype_rep_proofs.ML --- 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, diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/ex/Tarski.thy --- 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" ("_ ." [90] 90) - "@order" :: "'a potype => ('a *'a)set" ("_ ." [90] 90) - -translations - "po." == "pset po" - "po." == "order po" - constdefs monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool" "monotone f A r == \x\A. \y\A. (x, y): r --> ((f x), (f y)) : r" least :: "['a => bool, 'a potype] => 'a" - "least P po == @ x. x: po. & P x & - (\y \ po.. P y --> (x,y): po.)" + "least P po == @ x. x: pset po & P x & + (\y \ pset po. P y --> (x,y): order po)" greatest :: "['a => bool, 'a potype] => 'a" - "greatest P po == @ x. x: po. & P x & - (\y \ po.. P y --> (y,x): po.)" + "greatest P po == @ x. x: pset po & P x & + (\y \ pset po. P y --> (y,x): order po)" lub :: "['a set, 'a potype] => 'a" - "lub S po == least (%x. \y\S. (y,x): po.) po" + "lub S po == least (%x. \y\S. (y,x): order po) po" glb :: "['a set, 'a potype] => 'a" - "glb S po == greatest (%x. \y\S. (x,y): po.) po" + "glb S po == greatest (%x. \y\S. (x,y): order po) po" isLub :: "['a set, 'a potype, 'a] => bool" - "isLub S po == %L. (L: po. & (\y\S. (y,L): po.) & - (\z\po.. (\y\S. (y,z): po.) --> (L,z): po.))" + "isLub S po == %L. (L: pset po & (\y\S. (y,L): order po) & + (\z\pset po. (\y\S. (y,z): order po) --> (L,z): order po))" isGlb :: "['a set, 'a potype, 'a] => bool" - "isGlb S po == %G. (G: po. & (\y\S. (G,y): po.) & - (\z \ po.. (\y\S. (z,y): po.) --> (z,G): po.))" + "isGlb S po == %G. (G: pset po & (\y\S. (G,y): order po) & + (\z \ pset po. (\y\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.) (P.) & antisym (P.) & - trans (P.)}" + "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) & + trans (order P)}" CompleteLattice :: "('a potype) set" "CompleteLattice == {cl. cl: PartialOrder & - (\S. S <= cl. --> (\L. isLub S cl L)) & - (\S. S <= cl. --> (\G. isGlb S cl G))}" + (\S. S <= pset cl --> (\L. isLub S cl L)) & + (\S. S <= pset cl --> (\G. isGlb S cl G))}" CLF :: "('a potype * ('a => 'a)) set" "CLF == SIGMA cl: CompleteLattice. - {f. f: cl. funcset cl. & monotone f (cl.) (cl.)}" + {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. & - (| pset = S, order = induced S (cl.) |): 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., order = converse (po.) |)" + "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." - and r_def: "r == cl." + 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 \ PartialOrder; (\S. S <= po. --> (\L. isLub S po L)); - (\S. S <= po. --> (\G. isGlb S po G))|] + "[| po \ PartialOrder; (\S. S <= pset po --> (\L. isLub S po L)); + (\S. S <= pset po --> (\G. isGlb S po G))|] ==> po \ CompleteLattice" apply (unfold CompleteLattice_def, blast) done @@ -268,19 +259,19 @@ dualPO) done -lemma (in PO) dualA_iff: "(dual cl.) = cl." +lemma (in PO) dualA_iff: "pset (dual cl) = pset cl" by (simp add: dual_def) -lemma (in PO) dualr_iff: "((x, y) \ (dual cl.)) = ((y, x) \ cl.)" +lemma (in PO) dualr_iff: "((x, y) \ (order(dual cl))) = ((y, x) \ order cl)" by (simp add: dual_def) lemma (in PO) monotone_dual: - "monotone f (cl.) (cl.) ==> monotone f (dual cl.) (dual cl.)" -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 \ A; y \ A|] ==> interval r x y = interval (dual cl.) y x" + "[| x \ A; y \ 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. funcset cl. & monotone f (cl.) (cl.)" + "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 \ A funcset A" +lemma (in CLF) f_in_funcset: "f \ 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) \ cl. to (x, f x)"}, *} +-- {* instantiates @{text "(x, ???z) \ 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)) \ r"} *} @@ -807,7 +798,7 @@ apply (simp add: intY1_def interval_def intY1_elem) done -lemma (in Tarski) intY1_func: "(%x: intY1. f x) \ intY1 funcset intY1" +lemma (in Tarski) intY1_func: "(%x: intY1. f x) \ intY1 -> intY1" apply (rule restrictI) apply (erule intY1_f_closed) done