Replace surj by abbreviation; remove surj_on.
--- a/NEWS Wed Nov 24 10:52:02 2010 +0100
+++ b/NEWS Mon Nov 22 10:34:33 2010 +0100
@@ -291,9 +291,10 @@
derive instantiated and simplified equations for inductive predicates,
similar to inductive_cases.
-* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
-generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
-The theorems bij_def and surj_def are unchanged.
+* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f" is now an
+abbreviation of "range f = UIV". The theorems bij_def and surj_def are
+unchanged.
+INCOMPATIBILITY.
* Function package: .psimps rules are no longer implicitly declared [simp].
INCOMPATIBILITY.
--- a/src/HOL/Finite_Set.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Finite_Set.thy Mon Nov 22 10:34:33 2010 +0100
@@ -2286,7 +2286,7 @@
lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
-by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
+by (blast intro: finite_surj_inj subset_UNIV)
lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
--- a/src/HOL/Fun.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Fun.thy Mon Nov 22 10:34:33 2010 +0100
@@ -130,24 +130,22 @@
by (simp_all add: fun_eq_iff)
-subsection {* Injectivity, Surjectivity and Bijectivity *}
+subsection {* Injectivity and Bijectivity *}
definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
"inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
-definition surj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> bool" where -- "surjective"
- "surj_on f B \<longleftrightarrow> B \<subseteq> range f"
-
definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
"bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
-text{*A common special case: functions injective over the entire domain type.*}
+text{*A common special case: functions injective, surjective or bijective over
+the entire domain type.*}
abbreviation
"inj f \<equiv> inj_on f UNIV"
-abbreviation
- "surj f \<equiv> surj_on f UNIV"
+abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where -- "surjective"
+ "surj f \<equiv> (range f = UNIV)"
abbreviation
"bij f \<equiv> bij_betw f UNIV UNIV"
@@ -187,8 +185,8 @@
lemma inj_on_id2[simp]: "inj_on (%x. x) A"
by (simp add: inj_on_def)
-lemma surj_id[simp]: "surj_on id A"
-by (simp add: surj_on_def)
+lemma surj_id: "surj id"
+by simp
lemma bij_id[simp]: "bij id"
by (simp add: bij_betw_def)
@@ -251,20 +249,11 @@
apply (blast)
done
-lemma surj_onI: "(\<And>x. x \<in> B \<Longrightarrow> g (f x) = x) \<Longrightarrow> surj_on g B"
- by (simp add: surj_on_def) (blast intro: sym)
-
-lemma surj_onD: "surj_on f B \<Longrightarrow> y \<in> B \<Longrightarrow> \<exists>x. y = f x"
- by (auto simp: surj_on_def)
+lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
+ by auto
-lemma surj_on_range_iff: "surj_on f B \<longleftrightarrow> (\<exists>A. f ` A = B)"
- unfolding surj_on_def by (auto intro!: exI[of _ "f -` B"])
-
-lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
- by (simp add: surj_on_def subset_eq image_iff)
-
-lemma surjI: "(\<And> x. g (f x) = x) \<Longrightarrow> surj g"
- by (blast intro: surj_onI)
+lemma surjI: assumes *: "\<And> x. g (f x) = x" shows "surj g"
+ using *[symmetric] by auto
lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
by (simp add: surj_def)
@@ -278,17 +267,11 @@
apply (drule_tac x = x in spec, blast)
done
-lemma surj_range: "surj f \<Longrightarrow> range f = UNIV"
- by (auto simp add: surj_on_def)
-
-lemma surj_range_iff: "surj f \<longleftrightarrow> range f = UNIV"
- unfolding surj_on_def by auto
-
lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
- unfolding bij_betw_def surj_range_iff by auto
+ unfolding bij_betw_def by auto
lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
- unfolding surj_range_iff bij_betw_def ..
+ unfolding bij_betw_def ..
lemma bijI: "[| inj f; surj f |] ==> bij f"
by (simp add: bij_def)
@@ -302,16 +285,13 @@
lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
by (simp add: bij_betw_def)
-lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> surj_on f B"
-by (auto simp: bij_betw_def surj_on_range_iff)
-
-lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
-by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
-
lemma bij_betw_trans:
"bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
by(auto simp add:bij_betw_def comp_inj_on)
+lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
+ by (rule bij_betw_trans)
+
lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
proof -
have i: "inj_on f A" and s: "f ` A = B"
@@ -349,15 +329,13 @@
using assms unfolding bij_betw_def inj_on_Un image_Un by auto
lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
-by (simp add: surj_range)
+by simp
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
+by (blast intro: sym)
lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A"
by (unfold inj_on_def, blast)
@@ -410,7 +388,7 @@
done
lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
-by (auto simp add: surj_def)
+by auto
lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)"
by (auto simp add: inj_on_def)
@@ -559,10 +537,10 @@
qed
lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
- unfolding surj_range_iff by simp
+ by simp
lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
- unfolding surj_range_iff by simp
+ by simp
lemma bij_betw_swap_iff [simp]:
"\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
--- a/src/HOL/Hilbert_Choice.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Hilbert_Choice.thy Mon Nov 22 10:34:33 2010 +0100
@@ -151,10 +151,10 @@
by(fastsimp simp: image_def)
lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
-by (blast intro: surjI inv_into_f_f)
+by (blast intro!: surjI inv_into_f_f)
lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
-by (simp add: f_inv_into_f surj_range)
+by (simp add: f_inv_into_f)
lemma inv_into_injective:
assumes eq: "inv_into A f x = inv_into A f y"
@@ -173,12 +173,13 @@
by (auto simp add: bij_betw_def inj_on_inv_into)
lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
-by (simp add: inj_on_inv_into surj_range)
+by (simp add: inj_on_inv_into)
lemma surj_iff: "(surj f) = (f o inv f = id)"
-apply (simp add: o_def fun_eq_iff)
-apply (blast intro: surjI surj_f_inv_f)
-done
+by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
+
+lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)"
+ unfolding surj_iff by (simp add: o_def fun_eq_iff)
lemma surj_imp_inv_eq: "[| surj f; \<forall>x. g(f x) = x |] ==> inv f = g"
apply (rule ext)
--- a/src/HOL/Lattice/Orders.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Lattice/Orders.thy Mon Nov 22 10:34:33 2010 +0100
@@ -118,8 +118,8 @@
qed
qed
-lemma range_dual [simp]: "dual ` UNIV = UNIV"
-proof (rule surj_range)
+lemma range_dual [simp]: "surj dual"
+proof -
have "\<And>x'. dual (undual x') = x'" by simp
thus "surj dual" by (rule surjI)
qed
--- a/src/HOL/Library/ContNotDenum.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Library/ContNotDenum.thy Mon Nov 22 10:34:33 2010 +0100
@@ -565,8 +565,7 @@
shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
proof -- "by contradiction"
assume "\<exists>f::nat\<Rightarrow>real. surj f"
- then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
- hence rangeF: "range f = UNIV" by (rule surj_range)
+ then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
-- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
--- a/src/HOL/Library/Countable.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Library/Countable.thy Mon Nov 22 10:34:33 2010 +0100
@@ -165,7 +165,7 @@
qed
lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
-by (simp add: Rats_def surj_nat_to_rat_surj surj_range)
+by (simp add: Rats_def surj_nat_to_rat_surj)
context field_char_0
begin
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Nov 22 10:34:33 2010 +0100
@@ -948,14 +948,12 @@
assumes lf: "linear f" and gf: "f o g = id"
shows "linear g"
proof-
- from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def fun_eq_iff)
- by metis
+ from gf have fi: "surj f" by (auto simp add: surj_def o_def id_def) metis
from linear_surjective_isomorphism[OF lf fi]
obtain h:: "'a => 'a" where
h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" by blast
have "h = g" apply (rule ext) using gf h(2,3)
- apply (simp add: o_def id_def fun_eq_iff)
- by metis
+ by (simp add: o_def id_def fun_eq_iff) metis
with h(1) show ?thesis by blast
qed
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Nov 22 10:34:33 2010 +0100
@@ -2843,7 +2843,7 @@
h: "linear h" "\<forall> x\<in> basis ` {..<DIM('b)}. h x = inv f x" by blast
from h(2)
have th: "\<forall>i<DIM('b). (f o h) (basis i) = id (basis i)"
- using sf by(auto simp add: surj_iff o_def fun_eq_iff)
+ using sf by(auto simp add: surj_iff_all)
from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
have "f o h = id" .
then show ?thesis using h(1) by blast
@@ -2995,7 +2995,7 @@
{fix f f':: "'a => 'a"
assume lf: "linear f" "linear f'" and f: "f o f' = id"
from f have sf: "surj f"
- apply (auto simp add: o_def fun_eq_iff id_def surj_def)
+ apply (auto simp add: o_def id_def surj_def)
by metis
from linear_surjective_isomorphism[OF lf(1) sf] lf f
have "f' o f = id" unfolding fun_eq_iff o_def id_def
--- a/src/HOL/Nominal/Examples/Support.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy Mon Nov 22 10:34:33 2010 +0100
@@ -47,7 +47,7 @@
also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i \<or> n = 2*i+1})" by auto
also have "\<dots> = (\<lambda>n. atom n) ` (UNIV::nat set)" using even_or_odd by auto
also have "\<dots> = (UNIV::atom set)" using atom.exhaust
- by (rule_tac surj_range) (auto simp add: surj_def)
+ by (auto simp add: surj_def)
finally show "EVEN \<union> ODD = UNIV" by simp
qed
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Nov 22 10:34:33 2010 +0100
@@ -132,7 +132,7 @@
by (auto intro!: exI[of _ "from_nat i"])
qed
have **: "range ?A' = range A"
- using surj_range[OF surj_from_nat]
+ using surj_from_nat
by (auto simp: image_compose intro!: imageI)
show ?thesis unfolding * ** ..
qed
--- a/src/HOL/Product_Type.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Product_Type.thy Mon Nov 22 10:34:33 2010 +0100
@@ -1135,6 +1135,7 @@
qed
lemma map_pair_surj:
+ fixes f :: "'a \<Rightarrow> 'b" and g :: "'c \<Rightarrow> 'd"
assumes "surj f" and "surj g"
shows "surj (map_pair f g)"
unfolding surj_def
--- a/src/HOL/UNITY/Comp/Alloc.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Nov 22 10:34:33 2010 +0100
@@ -358,7 +358,7 @@
done
lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc"
- apply (simp add: surj_iff fun_eq_iff o_apply)
+ apply (simp add: surj_iff_all)
apply record_auto
done
@@ -386,7 +386,7 @@
done
lemma surj_sysOfClient [iff]: "surj sysOfClient"
- apply (simp add: surj_iff fun_eq_iff o_apply)
+ apply (simp add: surj_iff_all)
apply record_auto
done
@@ -410,7 +410,7 @@
done
lemma surj_client_map [iff]: "surj client_map"
- apply (simp add: surj_iff fun_eq_iff o_apply)
+ apply (simp add: surj_iff_all)
apply record_auto
done
@@ -682,7 +682,7 @@
lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x"
apply (insert fst_o_lift_map [of i])
apply (drule fun_cong [where x=x])
-apply (simp add: o_def);
+apply (simp add: o_def)
done
lemma fst_o_lift_map' [simp]:
@@ -702,7 +702,7 @@
RS guarantees_PLam_I
RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
|> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
- surj_rename RS surj_range])
+ surj_rename])
However, the "preserves" property remains to be discharged, and the unfolding
of "o" and "sub" complicates subsequent reasoning.
@@ -723,7 +723,7 @@
asm_simp_tac
(ss addsimps [@{thm lift_guarantees_eq_lift_inv},
@{thm rename_guarantees_eq_rename_inv},
- @{thm bij_imp_bij_inv}, @{thm surj_rename} RS @{thm surj_range},
+ @{thm bij_imp_bij_inv}, @{thm surj_rename},
@{thm inv_inv_eq}]) 1,
asm_simp_tac
(@{simpset} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
@@ -798,9 +798,9 @@
lemmas rename_Alloc_Increasing =
Alloc_Increasing
[THEN rename_guarantees_sysOfAlloc_I,
- simplified surj_rename [THEN surj_range] o_def sub_apply
+ simplified surj_rename o_def sub_apply
rename_image_Increasing bij_sysOfAlloc
- allocGiv_o_inv_sysOfAlloc_eq'];
+ allocGiv_o_inv_sysOfAlloc_eq']
lemma System_Increasing_allocGiv:
"i < Nclients ==> System : Increasing (sub i o allocGiv)"
@@ -879,7 +879,7 @@
\<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
apply (simp add: o_apply)
apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])
- apply (simp add: o_def);
+ apply (simp add: o_def)
apply (erule component_guaranteesD)
apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
done
--- a/src/HOL/UNITY/Extend.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/UNITY/Extend.thy Mon Nov 22 10:34:33 2010 +0100
@@ -127,7 +127,7 @@
assumes surj_h: "surj h"
and prem: "!! x y. g (h(x,y)) = x"
shows "fst (inv h z) = g z"
-by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h surj_range)
+by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h)
subsection{*Trivial properties of f, g, h*}
--- a/src/HOL/UNITY/Rename.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/UNITY/Rename.thy Mon Nov 22 10:34:33 2010 +0100
@@ -60,7 +60,8 @@
lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))"
apply (rule bijI)
apply (rule Extend.inj_extend_act)
-apply (auto simp add: bij_extend_act_eq_project_act)
+apply simp
+apply (simp add: bij_extend_act_eq_project_act)
apply (rule surjI)
apply (rule Extend.extend_act_inverse)
apply (blast intro: bij_imp_bij_inv good_map_bij)
@@ -75,7 +76,7 @@
project_act (%(x,u::'c). h x)"
apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric])
apply (rule surj_imp_inv_eq)
-apply (blast intro: bij_extend_act bij_is_surj)
+apply (blast intro!: bij_extend_act bij_is_surj)
apply (simp (no_asm_simp) add: Extend.extend_act_inverse)
done