1.1 --- a/src/HOL/Fun.thy Tue Feb 26 20:38:10 2008 +0100
1.2 +++ b/src/HOL/Fun.thy Tue Feb 26 20:38:12 2008 +0100
1.3 @@ -10,40 +10,45 @@
1.4 imports Set
1.5 begin
1.6
1.7 -constdefs
1.8 - fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
1.9 - "fun_upd f a b == % x. if x=a then b else f x"
1.10 +text{*As a simplification rule, it replaces all function equalities by
1.11 + first-order equalities.*}
1.12 +lemma expand_fun_eq: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
1.13 +apply (rule iffI)
1.14 +apply (simp (no_asm_simp))
1.15 +apply (rule ext)
1.16 +apply (simp (no_asm_simp))
1.17 +done
1.18
1.19 -nonterminals
1.20 - updbinds updbind
1.21 -syntax
1.22 - "_updbind" :: "['a, 'a] => updbind" ("(2_ :=/ _)")
1.23 - "" :: "updbind => updbinds" ("_")
1.24 - "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _")
1.25 - "_Update" :: "['a, updbinds] => 'a" ("_/'((_)')" [1000,0] 900)
1.26 +lemma apply_inverse:
1.27 + "f x =u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
1.28 + by auto
1.29
1.30 -translations
1.31 - "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
1.32 - "f(x:=y)" == "fun_upd f x y"
1.33
1.34 -(* Hint: to define the sum of two functions (or maps), use sum_case.
1.35 - A nice infix syntax could be defined (in Datatype.thy or below) by
1.36 -consts
1.37 - fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
1.38 -translations
1.39 - "fun_sum" == sum_case
1.40 -*)
1.41 -
1.42 -definition
1.43 - override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
1.44 -where
1.45 - "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
1.46 +subsection {* The Identity Function @{text id} *}
1.47
1.48 definition
1.49 id :: "'a \<Rightarrow> 'a"
1.50 where
1.51 "id = (\<lambda>x. x)"
1.52
1.53 +lemma id_apply [simp]: "id x = x"
1.54 + by (simp add: id_def)
1.55 +
1.56 +lemma image_ident [simp]: "(%x. x) ` Y = Y"
1.57 +by blast
1.58 +
1.59 +lemma image_id [simp]: "id ` Y = Y"
1.60 +by (simp add: id_def)
1.61 +
1.62 +lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
1.63 +by blast
1.64 +
1.65 +lemma vimage_id [simp]: "id -` A = A"
1.66 +by (simp add: id_def)
1.67 +
1.68 +
1.69 +subsection {* The Composition Operator @{text "f \<circ> g"} *}
1.70 +
1.71 definition
1.72 comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55)
1.73 where
1.74 @@ -58,63 +63,6 @@
1.75 text{*compatibility*}
1.76 lemmas o_def = comp_def
1.77
1.78 -constdefs
1.79 - inj_on :: "['a => 'b, 'a set] => bool" -- "injective"
1.80 - "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
1.81 -
1.82 -definition
1.83 - bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
1.84 - "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
1.85 -
1.86 -
1.87 -text{*A common special case: functions injective over the entire domain type.*}
1.88 -
1.89 -abbreviation
1.90 - "inj f == inj_on f UNIV"
1.91 -
1.92 -constdefs
1.93 - surj :: "('a => 'b) => bool" (*surjective*)
1.94 - "surj f == ! y. ? x. y=f(x)"
1.95 -
1.96 - bij :: "('a => 'b) => bool" (*bijective*)
1.97 - "bij f == inj f & surj f"
1.98 -
1.99 -
1.100 -
1.101 -text{*As a simplification rule, it replaces all function equalities by
1.102 - first-order equalities.*}
1.103 -lemma expand_fun_eq: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
1.104 -apply (rule iffI)
1.105 -apply (simp (no_asm_simp))
1.106 -apply (rule ext)
1.107 -apply (simp (no_asm_simp))
1.108 -done
1.109 -
1.110 -lemma apply_inverse:
1.111 - "[| f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) |] ==> x=g(u)"
1.112 -by auto
1.113 -
1.114 -
1.115 -text{*The Identity Function: @{term id}*}
1.116 -lemma id_apply [simp]: "id x = x"
1.117 -by (simp add: id_def)
1.118 -
1.119 -lemma inj_on_id[simp]: "inj_on id A"
1.120 -by (simp add: inj_on_def)
1.121 -
1.122 -lemma inj_on_id2[simp]: "inj_on (%x. x) A"
1.123 -by (simp add: inj_on_def)
1.124 -
1.125 -lemma surj_id[simp]: "surj id"
1.126 -by (simp add: surj_def)
1.127 -
1.128 -lemma bij_id[simp]: "bij id"
1.129 -by (simp add: bij_def inj_on_id surj_id)
1.130 -
1.131 -
1.132 -
1.133 -subsection{*The Composition Operator: @{term "f \<circ> g"}*}
1.134 -
1.135 lemma o_apply [simp]: "(f o g) x = f (g x)"
1.136 by (simp add: comp_def)
1.137
1.138 @@ -130,17 +78,36 @@
1.139 lemma image_compose: "(f o g) ` r = f`(g`r)"
1.140 by (simp add: comp_def, blast)
1.141
1.142 -lemma image_eq_UN: "f`A = (UN x:A. {f x})"
1.143 -by blast
1.144 -
1.145 lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
1.146 by (unfold comp_def, blast)
1.147
1.148
1.149 -subsection{*The Injectivity Predicate, @{term inj}*}
1.150 +subsection {* Injectivity and Surjectivity *}
1.151
1.152 -text{*NB: @{term inj} now just translates to @{term inj_on}*}
1.153 +constdefs
1.154 + inj_on :: "['a => 'b, 'a set] => bool" -- "injective"
1.155 + "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
1.156
1.157 +text{*A common special case: functions injective over the entire domain type.*}
1.158 +
1.159 +abbreviation
1.160 + "inj f == inj_on f UNIV"
1.161 +
1.162 +definition
1.163 + bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
1.164 + "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
1.165 +
1.166 +constdefs
1.167 + surj :: "('a => 'b) => bool" (*surjective*)
1.168 + "surj f == ! y. ? x. y=f(x)"
1.169 +
1.170 + bij :: "('a => 'b) => bool" (*bijective*)
1.171 + "bij f == inj f & surj f"
1.172 +
1.173 +lemma injI:
1.174 + assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
1.175 + shows "inj f"
1.176 + using assms unfolding inj_on_def by auto
1.177
1.178 text{*For Proofs in @{text "Tools/datatype_rep_proofs"}*}
1.179 lemma datatype_injI:
1.180 @@ -157,8 +124,17 @@
1.181 lemma inj_eq: "inj(f) ==> (f(x) = f(y)) = (x=y)"
1.182 by (force simp add: inj_on_def)
1.183
1.184 +lemma inj_on_id[simp]: "inj_on id A"
1.185 + by (simp add: inj_on_def)
1.186
1.187 -subsection{*The Predicate @{term inj_on}: Injectivity On A Restricted Domain*}
1.188 +lemma inj_on_id2[simp]: "inj_on (%x. x) A"
1.189 +by (simp add: inj_on_def)
1.190 +
1.191 +lemma surj_id[simp]: "surj id"
1.192 +by (simp add: surj_def)
1.193 +
1.194 +lemma bij_id[simp]: "bij id"
1.195 +by (simp add: bij_def inj_on_id surj_id)
1.196
1.197 lemma inj_onI:
1.198 "(!! x y. [| x:A; y:A; f(x) = f(y) |] ==> x=y) ==> inj_on f A"
1.199 @@ -218,9 +194,6 @@
1.200 apply (blast)
1.201 done
1.202
1.203 -
1.204 -subsection{*The Predicate @{term surj}: Surjectivity*}
1.205 -
1.206 lemma surjI: "(!! x. g(f x) = x) ==> surj g"
1.207 apply (simp add: surj_def)
1.208 apply (blast intro: sym)
1.209 @@ -241,9 +214,6 @@
1.210 apply (drule_tac x = x in spec, blast)
1.211 done
1.212
1.213 -
1.214 -subsection{*The Predicate @{const bij}: Bijectivity*}
1.215 -
1.216 lemma bijI: "[| inj f; surj f |] ==> bij f"
1.217 by (simp add: bij_def)
1.218
1.219 @@ -253,9 +223,6 @@
1.220 lemma bij_is_surj: "bij f ==> surj f"
1.221 by (simp add: bij_def)
1.222
1.223 -
1.224 -subsection{*The Predicate @{const bij_betw}: Bijectivity*}
1.225 -
1.226 lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
1.227 by (simp add: bij_betw_def)
1.228
1.229 @@ -290,34 +257,6 @@
1.230 ultimately show ?thesis by(auto simp:bij_betw_def)
1.231 qed
1.232
1.233 -
1.234 -subsection{*Facts About the Identity Function*}
1.235 -
1.236 -text{*We seem to need both the @{term id} forms and the @{term "\<lambda>x. x"}
1.237 -forms. The latter can arise by rewriting, while @{term id} may be used
1.238 -explicitly.*}
1.239 -
1.240 -lemma image_ident [simp]: "(%x. x) ` Y = Y"
1.241 -by blast
1.242 -
1.243 -lemma image_id [simp]: "id ` Y = Y"
1.244 -by (simp add: id_def)
1.245 -
1.246 -lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
1.247 -by blast
1.248 -
1.249 -lemma vimage_id [simp]: "id -` A = A"
1.250 -by (simp add: id_def)
1.251 -
1.252 -lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
1.253 -by (blast intro: sym)
1.254 -
1.255 -lemma image_vimage_subset: "f ` (f -` A) <= A"
1.256 -by blast
1.257 -
1.258 -lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
1.259 -by blast
1.260 -
1.261 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
1.262 by (simp add: surj_range)
1.263
1.264 @@ -337,12 +276,6 @@
1.265 apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
1.266 done
1.267
1.268 -lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
1.269 -by blast
1.270 -
1.271 -lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
1.272 -by blast
1.273 -
1.274 lemma inj_on_image_Int:
1.275 "[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B"
1.276 apply (simp add: inj_on_def, blast)
1.277 @@ -368,9 +301,6 @@
1.278 lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)"
1.279 by (blast dest: injD)
1.280
1.281 -lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
1.282 -by blast
1.283 -
1.284 (*injectivity's required. Left-to-right inclusion holds even if A is empty*)
1.285 lemma image_INT:
1.286 "[| inj_on f C; ALL x:A. B x <= C; j:A |]
1.287 @@ -400,6 +330,30 @@
1.288
1.289 subsection{*Function Updating*}
1.290
1.291 +constdefs
1.292 + fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
1.293 + "fun_upd f a b == % x. if x=a then b else f x"
1.294 +
1.295 +nonterminals
1.296 + updbinds updbind
1.297 +syntax
1.298 + "_updbind" :: "['a, 'a] => updbind" ("(2_ :=/ _)")
1.299 + "" :: "updbind => updbinds" ("_")
1.300 + "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _")
1.301 + "_Update" :: "['a, updbinds] => 'a" ("_/'((_)')" [1000,0] 900)
1.302 +
1.303 +translations
1.304 + "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
1.305 + "f(x:=y)" == "fun_upd f x y"
1.306 +
1.307 +(* Hint: to define the sum of two functions (or maps), use sum_case.
1.308 + A nice infix syntax could be defined (in Datatype.thy or below) by
1.309 +consts
1.310 + fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
1.311 +translations
1.312 + "fun_sum" == sum_case
1.313 +*)
1.314 +
1.315 lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)"
1.316 apply (simp add: fun_upd_def, safe)
1.317 apply (erule subst)
1.318 @@ -437,7 +391,13 @@
1.319 "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
1.320 by auto
1.321
1.322 -subsection{* @{text override_on} *}
1.323 +
1.324 +subsection {* @{text override_on} *}
1.325 +
1.326 +definition
1.327 + override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
1.328 +where
1.329 + "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
1.330
1.331 lemma override_on_emptyset[simp]: "override_on f g {} = f"
1.332 by(simp add:override_on_def)
1.333 @@ -448,7 +408,8 @@
1.334 lemma override_on_apply_in[simp]: "a : A ==> (override_on f g A) a = g a"
1.335 by(simp add:override_on_def)
1.336
1.337 -subsection{* swap *}
1.338 +
1.339 +subsection {* @{text swap} *}
1.340
1.341 definition
1.342 swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"