(* Title: HOL/Library/FuncSet.thy ID: $Id$ Author: Florian Kammueller and Lawrence C Paulson *) header {* \title{Pi and Function Sets} \author{Florian Kammueller and Lawrence C Paulson} *} theory FuncSet = Main: constdefs Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" "Pi A B == {f. \x. x \ A --> f(x) \ B(x)}" extensional :: "'a set => ('a => 'b) set" "extensional A == {f. \x. x~:A --> f(x) = arbitrary}" restrict :: "['a => 'b, 'a set] => ('a => 'b)" "restrict f A == (%x. if x \ A then f x else arbitrary)" 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) "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\ _\_./ _)" 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 (HTML output) "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\ _\_./ _)" 10) "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\_\_./ _)" [0,0,3] 3) translations "PI x:A. B" => "Pi A (%x. B)" "A -> 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)" print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *} subsection{*Basic Properties of @{term Pi}*} lemma Pi_I: "(!!x. x \ A ==> f x \ B x) ==> f \ Pi A B" by (simp add: Pi_def) lemma funcsetI: "(!!x. x \ A ==> f x \ B) ==> f \ A -> B" by (simp add: Pi_def) lemma Pi_mem: "[|f: Pi A B; x \ A|] ==> f x \ B x" by (simp add: Pi_def) lemma funcset_mem: "[|f \ A -> B; x \ A|] ==> f x \ B" by (simp add: Pi_def) lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\x\A. B(x) = {})" apply (simp add: Pi_def, auto) txt{*Converse direction requires Axiom of Choice to exhibit a function picking an element from each non-empty @{term "B x"}*} apply (drule_tac x = "%u. SOME y. y \ B u" in spec, auto) apply (cut_tac P= "%y. y \ B x" in some_eq_ex, auto) done lemma Pi_empty [simp]: "Pi {} B = UNIV" by (simp add: Pi_def) lemma Pi_UNIV [simp]: "A -> UNIV = UNIV" by (simp add: Pi_def) text{*Covariance of Pi-sets in their second argument*} lemma Pi_mono: "(!!x. x \ A ==> B x <= C x) ==> Pi A B <= Pi A C" by (simp add: Pi_def, blast) text{*Contravariance of Pi-sets in their first argument*} lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B" by (simp add: Pi_def, blast) subsection{*Composition With a Restricted Domain: @{term compose}*} lemma funcset_compose: "[| f \ A -> B; g \ B -> C |]==> compose A g f \ A -> C" by (simp add: Pi_def compose_def restrict_def) lemma compose_assoc: "[| f \ A -> B; g \ B -> C; h \ C -> D |] ==> compose A h (compose A g f) = compose A (compose B h g) f" by (simp add: expand_fun_eq Pi_def compose_def restrict_def) lemma compose_eq: "x \ A ==> compose A g f x = g(f(x))" by (simp add: compose_def restrict_def) lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C" by (auto simp add: image_def compose_eq) lemma inj_on_compose: "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A" by (auto simp add: inj_on_def compose_eq) subsection{*Bounded Abstraction: @{term restrict}*} lemma restrict_in_funcset: "(!!x. x \ A ==> f x \ B) ==> (\x\A. f x) \ A -> B" by (simp add: Pi_def restrict_def) lemma restrictI: "(!!x. x \ A ==> f x \ B x) ==> (\x\A. f x) \ Pi A B" by (simp add: Pi_def restrict_def) lemma restrict_apply [simp]: "(\y\A. f y) x = (if x \ A then f x else arbitrary)" by (simp add: restrict_def) lemma restrict_ext: "(!!x. x \ A ==> f x = g x) ==> (\x\A. f x) = (\x\A. g x)" by (simp add: expand_fun_eq Pi_def Pi_def restrict_def) lemma inj_on_restrict_eq: "inj_on (restrict f A) A = inj_on f A" by (simp add: inj_on_def restrict_def) lemma Id_compose: "[|f \ A -> B; f \ extensional A|] ==> compose A (\y\B. y) f = f" by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) lemma compose_Id: "[|g \ A -> B; g \ extensional A|] ==> compose A g (\x\A. x) = g" by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) subsection{*Extensionality*} lemma extensional_arb: "[|f \ extensional A; x\ A|] ==> f x = arbitrary" by (simp add: extensional_def) lemma restrict_extensional [simp]: "restrict f A \ extensional A" by (simp add: restrict_def extensional_def) lemma compose_extensional [simp]: "compose A f g \ extensional A" by (simp add: compose_def) lemma extensionalityI: "[| f \ extensional A; g \ extensional A; !!x. x\A ==> f x = g x |] ==> f = g" by (force simp add: expand_fun_eq extensional_def) lemma Inv_funcset: "f ` A = B ==> (\x\B. Inv A f x) : B -> A" apply (unfold Inv_def) apply (fast intro: restrict_in_funcset someI2) done lemma compose_Inv_id: "[| inj_on f A; f ` A = B |] ==> compose A (\y\B. Inv A f y) f = (\x\A. x)" apply (simp add: compose_def) apply (rule restrict_ext, auto) apply (erule subst) apply (simp add: Inv_f_f) done lemma compose_id_Inv: "f ` A = B ==> compose B f (\y\B. Inv A f y) = (\x\B. x)" apply (simp add: compose_def) apply (rule restrict_ext) apply (simp add: f_Inv_f) done end