1.1 --- a/src/HOL/Library/FuncSet.thy Thu May 06 12:43:00 2004 +0200
1.2 +++ b/src/HOL/Library/FuncSet.thy Thu May 06 14:14:18 2004 +0200
1.3 @@ -3,22 +3,19 @@
1.4 Author: Florian Kammueller and Lawrence C Paulson
1.5 *)
1.6
1.7 -header {*
1.8 - \title{Pi and Function Sets}
1.9 - \author{Florian Kammueller and Lawrence C Paulson}
1.10 -*}
1.11 +header {* Pi and Function Sets *}
1.12
1.13 theory FuncSet = Main:
1.14
1.15 constdefs
1.16 - Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
1.17 - "Pi A B == {f. \<forall>x. x \<in> A --> f(x) \<in> B(x)}"
1.18 + Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
1.19 + "Pi A B == {f. \<forall>x. x \<in> A --> f x \<in> B x}"
1.20
1.21 extensional :: "'a set => ('a => 'b) set"
1.22 - "extensional A == {f. \<forall>x. x~:A --> f(x) = arbitrary}"
1.23 + "extensional A == {f. \<forall>x. x~:A --> f x = arbitrary}"
1.24
1.25 - restrict :: "['a => 'b, 'a set] => ('a => 'b)"
1.26 - "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
1.27 + "restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
1.28 + "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
1.29
1.30 syntax
1.31 "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
1.32 @@ -27,7 +24,7 @@
1.33
1.34 syntax (xsymbols)
1.35 "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
1.36 - funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "\<rightarrow>" 60)
1.37 + funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "\<rightarrow>" 60)
1.38 "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
1.39
1.40 syntax (HTML output)
1.41 @@ -36,11 +33,11 @@
1.42
1.43 translations
1.44 "PI x:A. B" => "Pi A (%x. B)"
1.45 - "A -> B" => "Pi A (_K B)"
1.46 - "%x:A. f" == "restrict (%x. f) A"
1.47 + "A -> B" => "Pi A (_K B)"
1.48 + "%x:A. f" == "restrict (%x. f) A"
1.49
1.50 constdefs
1.51 - compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
1.52 + "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
1.53 "compose A g f == \<lambda>x\<in>A. g (f x)"
1.54
1.55 print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
1.56 @@ -49,126 +46,123 @@
1.57 subsection{*Basic Properties of @{term Pi}*}
1.58
1.59 lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
1.60 -by (simp add: Pi_def)
1.61 + by (simp add: Pi_def)
1.62
1.63 lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
1.64 -by (simp add: Pi_def)
1.65 + by (simp add: Pi_def)
1.66
1.67 lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
1.68 -by (simp add: Pi_def)
1.69 + by (simp add: Pi_def)
1.70
1.71 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
1.72 -by (simp add: Pi_def)
1.73 + by (simp add: Pi_def)
1.74
1.75 lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
1.76 apply (simp add: Pi_def, auto)
1.77 txt{*Converse direction requires Axiom of Choice to exhibit a function
1.78 picking an element from each non-empty @{term "B x"}*}
1.79 apply (drule_tac x = "%u. SOME y. y \<in> B u" in spec, auto)
1.80 -apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto)
1.81 +apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto)
1.82 done
1.83
1.84 lemma Pi_empty [simp]: "Pi {} B = UNIV"
1.85 -by (simp add: Pi_def)
1.86 + by (simp add: Pi_def)
1.87
1.88 lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
1.89 -by (simp add: Pi_def)
1.90 + by (simp add: Pi_def)
1.91
1.92 text{*Covariance of Pi-sets in their second argument*}
1.93 lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
1.94 -by (simp add: Pi_def, blast)
1.95 + by (simp add: Pi_def, blast)
1.96
1.97 text{*Contravariance of Pi-sets in their first argument*}
1.98 lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
1.99 -by (simp add: Pi_def, blast)
1.100 + by (simp add: Pi_def, blast)
1.101
1.102
1.103 subsection{*Composition With a Restricted Domain: @{term compose}*}
1.104
1.105 -lemma funcset_compose:
1.106 - "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C"
1.107 -by (simp add: Pi_def compose_def restrict_def)
1.108 +lemma funcset_compose:
1.109 + "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C"
1.110 + by (simp add: Pi_def compose_def restrict_def)
1.111
1.112 lemma compose_assoc:
1.113 - "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
1.114 + "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
1.115 ==> compose A h (compose A g f) = compose A (compose B h g) f"
1.116 -by (simp add: expand_fun_eq Pi_def compose_def restrict_def)
1.117 + by (simp add: expand_fun_eq Pi_def compose_def restrict_def)
1.118
1.119 lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))"
1.120 -by (simp add: compose_def restrict_def)
1.121 + by (simp add: compose_def restrict_def)
1.122
1.123 lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C"
1.124 -by (auto simp add: image_def compose_eq)
1.125 + by (auto simp add: image_def compose_eq)
1.126
1.127 lemma inj_on_compose:
1.128 - "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A"
1.129 -by (auto simp add: inj_on_def compose_eq)
1.130 + "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A"
1.131 + by (auto simp add: inj_on_def compose_eq)
1.132
1.133
1.134 subsection{*Bounded Abstraction: @{term restrict}*}
1.135
1.136 lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
1.137 -by (simp add: Pi_def restrict_def)
1.138 + by (simp add: Pi_def restrict_def)
1.139
1.140 lemma restrictI: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
1.141 -by (simp add: Pi_def restrict_def)
1.142 + by (simp add: Pi_def restrict_def)
1.143
1.144 lemma restrict_apply [simp]:
1.145 - "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
1.146 -by (simp add: restrict_def)
1.147 + "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
1.148 + by (simp add: restrict_def)
1.149
1.150 -lemma restrict_ext:
1.151 +lemma restrict_ext:
1.152 "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
1.153 -by (simp add: expand_fun_eq Pi_def Pi_def restrict_def)
1.154 + by (simp add: expand_fun_eq Pi_def Pi_def restrict_def)
1.155
1.156 lemma inj_on_restrict_eq: "inj_on (restrict f A) A = inj_on f A"
1.157 -by (simp add: inj_on_def restrict_def)
1.158 -
1.159 + by (simp add: inj_on_def restrict_def)
1.160
1.161 lemma Id_compose:
1.162 - "[|f \<in> A -> B; f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
1.163 -by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
1.164 + "[|f \<in> A -> B; f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
1.165 + by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
1.166
1.167 lemma compose_Id:
1.168 - "[|g \<in> A -> B; g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
1.169 -by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
1.170 + "[|g \<in> A -> B; g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
1.171 + by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
1.172
1.173
1.174 subsection{*Extensionality*}
1.175
1.176 lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
1.177 -by (simp add: extensional_def)
1.178 + by (simp add: extensional_def)
1.179
1.180 lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
1.181 -by (simp add: restrict_def extensional_def)
1.182 + by (simp add: restrict_def extensional_def)
1.183
1.184 lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
1.185 -by (simp add: compose_def)
1.186 + by (simp add: compose_def)
1.187
1.188 lemma extensionalityI:
1.189 - "[| f \<in> extensional A; g \<in> extensional A;
1.190 - !!x. x\<in>A ==> f x = g x |] ==> f = g"
1.191 -by (force simp add: expand_fun_eq extensional_def)
1.192 + "[| f \<in> extensional A; g \<in> extensional A;
1.193 + !!x. x\<in>A ==> f x = g x |] ==> f = g"
1.194 + by (force simp add: expand_fun_eq extensional_def)
1.195
1.196 lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
1.197 -apply (unfold Inv_def)
1.198 -apply (fast intro: restrict_in_funcset someI2)
1.199 -done
1.200 + by (unfold Inv_def) (fast intro: restrict_in_funcset someI2)
1.201
1.202 lemma compose_Inv_id:
1.203 - "[| inj_on f A; f ` A = B |]
1.204 + "[| inj_on f A; f ` A = B |]
1.205 ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
1.206 -apply (simp add: compose_def)
1.207 -apply (rule restrict_ext, auto)
1.208 -apply (erule subst)
1.209 -apply (simp add: Inv_f_f)
1.210 -done
1.211 + apply (simp add: compose_def)
1.212 + apply (rule restrict_ext, auto)
1.213 + apply (erule subst)
1.214 + apply (simp add: Inv_f_f)
1.215 + done
1.216
1.217 lemma compose_id_Inv:
1.218 - "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
1.219 -apply (simp add: compose_def)
1.220 -apply (rule restrict_ext)
1.221 -apply (simp add: f_Inv_f)
1.222 -done
1.223 + "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
1.224 + apply (simp add: compose_def)
1.225 + apply (rule restrict_ext)
1.226 + apply (simp add: f_Inv_f)
1.227 + done
1.228
1.229 end