author hoelzl Thu Sep 02 18:45:23 2010 +0200 (2010-09-02) changeset 39079 bddc3d3f6e53 parent 39071 928c5a5bdc93 parent 39078 39f8f6d1eb74 child 39100 e9467adb8b52 child 39103 a9d710bf6074
merged
 NEWS file | annotate | diff | revisions
```     1.1 --- a/NEWS	Thu Sep 02 17:02:00 2010 +0200
1.2 +++ b/NEWS	Thu Sep 02 18:45:23 2010 +0200
1.3 @@ -200,6 +200,9 @@
1.4  derive instantiated and simplified equations for inductive predicates,
1.5  similar to inductive_cases.
1.6
1.7 +* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
1.8 +generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
1.9 +The theorems bij_def and surj_def are unchanged.
1.10
1.11  *** FOL ***
1.12
```
```     2.1 --- a/src/HOL/Fun.thy	Thu Sep 02 17:02:00 2010 +0200
2.2 +++ b/src/HOL/Fun.thy	Thu Sep 02 18:45:23 2010 +0200
2.3 @@ -117,31 +117,27 @@
2.4  no_notation fcomp (infixl "\<circ>>" 60)
2.5
2.6
2.7 -subsection {* Injectivity and Surjectivity *}
2.8 +subsection {* Injectivity, Surjectivity and Bijectivity *}
2.9 +
2.10 +definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
2.11 +  "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
2.12
2.13 -definition
2.14 -  inj_on :: "['a => 'b, 'a set] => bool" where
2.15 -  -- "injective"
2.16 -  "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
2.17 +definition surj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> bool" where -- "surjective"
2.18 +  "surj_on f B \<longleftrightarrow> B \<subseteq> range f"
2.19 +
2.20 +definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
2.21 +  "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
2.22
2.23  text{*A common special case: functions injective over the entire domain type.*}
2.24
2.25  abbreviation
2.26 -  "inj f == inj_on f UNIV"
2.27 -
2.28 -definition
2.29 -  bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
2.30 -  "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
2.31 +  "inj f \<equiv> inj_on f UNIV"
2.32
2.33 -definition
2.34 -  surj :: "('a => 'b) => bool" where
2.35 -  -- "surjective"
2.36 -  "surj f == ! y. ? x. y=f(x)"
2.37 +abbreviation
2.38 +  "surj f \<equiv> surj_on f UNIV"
2.39
2.40 -definition
2.41 -  bij :: "('a => 'b) => bool" where
2.42 -  -- "bijective"
2.43 -  "bij f == inj f & surj f"
2.44 +abbreviation
2.45 +  "bij f \<equiv> bij_betw f UNIV UNIV"
2.46
2.47  lemma injI:
2.48    assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
2.49 @@ -173,16 +169,16 @@
2.51
2.52  lemma inj_on_id[simp]: "inj_on id A"
2.53 -  by (simp add: inj_on_def)
2.54 +  by (simp add: inj_on_def)
2.55
2.56  lemma inj_on_id2[simp]: "inj_on (%x. x) A"
2.59
2.60 -lemma surj_id[simp]: "surj id"
2.62 +lemma surj_id[simp]: "surj_on id A"
2.64
2.65 -lemma bij_id[simp]: "bij id"
2.67 +lemma bij_id[simp]: "bij_betw id A A"
2.69
2.70  lemma inj_onI:
2.71      "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A"
2.72 @@ -242,19 +238,26 @@
2.73  apply (blast)
2.74  done
2.75
2.76 -lemma surjI: "(!! x. g(f x) = x) ==> surj g"
2.78 -apply (blast intro: sym)
2.79 -done
2.80 +lemma surj_onI: "(\<And>x. x \<in> B \<Longrightarrow> g (f x) = x) \<Longrightarrow> surj_on g B"
2.81 +  by (simp add: surj_on_def) (blast intro: sym)
2.82 +
2.83 +lemma surj_onD: "surj_on f B \<Longrightarrow> y \<in> B \<Longrightarrow> \<exists>x. y = f x"
2.84 +  by (auto simp: surj_on_def)
2.85 +
2.86 +lemma surj_on_range_iff: "surj_on f B \<longleftrightarrow> (\<exists>A. f ` A = B)"
2.87 +  unfolding surj_on_def by (auto intro!: exI[of _ "f -` B"])
2.88
2.89 -lemma surj_range: "surj f ==> range f = UNIV"
2.90 -by (auto simp add: surj_def)
2.91 +lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
2.92 +  by (simp add: surj_on_def subset_eq image_iff)
2.93 +
2.94 +lemma surjI: "(\<And> x. g (f x) = x) \<Longrightarrow> surj g"
2.95 +  by (blast intro: surj_onI)
2.96
2.97 -lemma surjD: "surj f ==> EX x. y = f x"
2.99 +lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
2.100 +  by (simp add: surj_def)
2.101
2.102 -lemma surjE: "surj f ==> (!!x. y = f x ==> C) ==> C"
2.103 -by (simp add: surj_def, blast)
2.104 +lemma surjE: "surj f \<Longrightarrow> (\<And>x. y = f x \<Longrightarrow> C) \<Longrightarrow> C"
2.105 +  by (simp add: surj_def, blast)
2.106
2.107  lemma comp_surj: "[| surj f;  surj g |] ==> surj (g o f)"
2.108  apply (simp add: comp_def surj_def, clarify)
2.109 @@ -262,6 +265,18 @@
2.110  apply (drule_tac x = x in spec, blast)
2.111  done
2.112
2.113 +lemma surj_range: "surj f \<Longrightarrow> range f = UNIV"
2.114 +  by (auto simp add: surj_on_def)
2.115 +
2.116 +lemma surj_range_iff: "surj f \<longleftrightarrow> range f = UNIV"
2.117 +  unfolding surj_on_def by auto
2.118 +
2.119 +lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
2.120 +  unfolding bij_betw_def surj_range_iff by auto
2.121 +
2.122 +lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
2.123 +  unfolding surj_range_iff bij_betw_def ..
2.124 +
2.125  lemma bijI: "[| inj f; surj f |] ==> bij f"
2.127
2.128 @@ -274,6 +289,9 @@
2.129  lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
2.131
2.132 +lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> surj_on f B"
2.133 +by (auto simp: bij_betw_def surj_on_range_iff)
2.134 +
2.135  lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
2.136  by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
2.137
2.138 @@ -312,6 +330,11 @@
2.139    ultimately show ?thesis by(auto simp:bij_betw_def)
2.140  qed
2.141
2.142 +lemma bij_betw_combine:
2.143 +  assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
2.144 +  shows "bij_betw f (A \<union> C) (B \<union> D)"
2.145 +  using assms unfolding bij_betw_def inj_on_Un image_Un by auto
2.146 +
2.147  lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
2.149
2.150 @@ -497,44 +520,46 @@
2.151  lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
2.152  by (rule ext, simp add: fun_upd_def swap_def)
2.153
2.154 +lemma swap_image_eq [simp]:
2.155 +  assumes "a \<in> A" "b \<in> A" shows "swap a b f ` A = f ` A"
2.156 +proof -
2.157 +  have subset: "\<And>f. swap a b f ` A \<subseteq> f ` A"
2.158 +    using assms by (auto simp: image_iff swap_def)
2.159 +  then have "swap a b (swap a b f) ` A \<subseteq> (swap a b f) ` A" .
2.160 +  with subset[of f] show ?thesis by auto
2.161 +qed
2.162 +
2.163  lemma inj_on_imp_inj_on_swap:
2.164 -  "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
2.165 -by (simp add: inj_on_def swap_def, blast)
2.166 +  "\<lbrakk>inj_on f A; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> inj_on (swap a b f) A"
2.167 +  by (simp add: inj_on_def swap_def, blast)
2.168
2.169  lemma inj_on_swap_iff [simp]:
2.170 -  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
2.171 -proof
2.172 +  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A \<longleftrightarrow> inj_on f A"
2.173 +proof
2.174    assume "inj_on (swap a b f) A"
2.175 -  with A have "inj_on (swap a b (swap a b f)) A"
2.176 -    by (iprover intro: inj_on_imp_inj_on_swap)
2.177 -  thus "inj_on f A" by simp
2.178 +  with A have "inj_on (swap a b (swap a b f)) A"
2.179 +    by (iprover intro: inj_on_imp_inj_on_swap)
2.180 +  thus "inj_on f A" by simp
2.181  next
2.182    assume "inj_on f A"
2.183    with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
2.184  qed
2.185
2.186 -lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
2.187 -apply (simp add: surj_def swap_def, clarify)
2.188 -apply (case_tac "y = f b", blast)
2.189 -apply (case_tac "y = f a", auto)
2.190 -done
2.191 +lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
2.192 +  unfolding surj_range_iff by simp
2.193 +
2.194 +lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
2.195 +  unfolding surj_range_iff by simp
2.196
2.197 -lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
2.198 -proof
2.199 -  assume "surj (swap a b f)"
2.200 -  hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap)
2.201 -  thus "surj f" by simp
2.202 -next
2.203 -  assume "surj f"
2.204 -  thus "surj (swap a b f)" by (rule surj_imp_surj_swap)
2.205 -qed
2.206 +lemma bij_betw_swap_iff [simp]:
2.207 +  "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
2.208 +  by (auto simp: bij_betw_def)
2.209
2.210 -lemma bij_swap_iff: "bij (swap a b f) = bij f"
2.212 +lemma bij_swap_iff [simp]: "bij (swap a b f) \<longleftrightarrow> bij f"
2.213 +  by simp
2.214
2.215  hide_const (open) swap
2.216
2.217 -
2.218  subsection {* Inversion of injective functions *}
2.219
2.220  definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
```
```     3.1 --- a/src/HOL/Library/Permutation.thy	Thu Sep 02 17:02:00 2010 +0200
3.2 +++ b/src/HOL/Library/Permutation.thy	Thu Sep 02 18:45:23 2010 +0200
3.3 @@ -183,4 +183,55 @@
3.4  lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
3.5    by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
3.6
3.7 +lemma permutation_Ex_bij:
3.8 +  assumes "xs <~~> ys"
3.9 +  shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
3.10 +using assms proof induct
3.11 +  case Nil then show ?case unfolding bij_betw_def by simp
3.12 +next
3.13 +  case (swap y x l)
3.14 +  show ?case
3.15 +  proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
3.16 +    show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
3.17 +      by (auto simp: bij_betw_def bij_betw_swap_iff)
3.18 +    fix i assume "i < length(y#x#l)"
3.19 +    show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
3.20 +      by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
3.21 +  qed
3.22 +next
3.23 +  case (Cons xs ys z)
3.24 +  then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and
3.25 +    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast
3.26 +  let "?f i" = "case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
3.27 +  show ?case
3.28 +  proof (intro exI[of _ ?f] allI conjI impI)
3.29 +    have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"
3.30 +            "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"
3.31 +      by (simp_all add: lessThan_Suc_eq_insert_0)
3.32 +    show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" unfolding *
3.33 +    proof (rule bij_betw_combine)
3.34 +      show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
3.35 +        using bij unfolding bij_betw_def
3.36 +        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
3.37 +    qed (auto simp: bij_betw_def)
3.38 +    fix i assume "i < length (z#xs)"
3.39 +    then show "(z # xs) ! i = (z # ys) ! (?f i)"
3.40 +      using perm by (cases i) auto
3.41 +  qed
3.42 +next
3.43 +  case (trans xs ys zs)
3.44 +  then obtain f g where
3.45 +    bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and
3.46 +    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast
3.47 +  show ?case
3.48 +  proof (intro exI[of _ "g\<circ>f"] conjI allI impI)
3.49 +    show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
3.50 +      using bij by (rule bij_betw_trans)
3.51 +    fix i assume "i < length xs"
3.52 +    with bij have "f i < length ys" unfolding bij_betw_def by force
3.53 +    with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
3.54 +      using trans(1,3)[THEN perm_length] perm by force
3.55 +  qed
3.56 +qed
3.57 +
3.58  end
```
```     4.1 --- a/src/HOL/List.thy	Thu Sep 02 17:02:00 2010 +0200
4.2 +++ b/src/HOL/List.thy	Thu Sep 02 18:45:23 2010 +0200
4.3 @@ -3076,6 +3076,10 @@
4.4    "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
4.5  by(induct xs) auto
4.6
4.7 +lemma filter_remove1:
4.8 +  "filter Q (remove1 x xs) = remove1 x (filter Q xs)"
4.9 +by (induct xs) auto
4.10 +
4.11  lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
4.12  apply(insert set_remove1_subset)
4.13  apply fast
```
```     5.1 --- a/src/HOL/SetInterval.thy	Thu Sep 02 17:02:00 2010 +0200
5.2 +++ b/src/HOL/SetInterval.thy	Thu Sep 02 18:45:23 2010 +0200
5.3 @@ -304,6 +304,17 @@
5.4  lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)"
5.5  by (simp add: lessThan_def less_Suc_eq, blast)
5.6
5.7 +text {* The following proof is convinient in induction proofs where
5.8 +new elements get indices at the beginning. So it is used to transform
5.9 +@{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}. *}
5.10 +
5.11 +lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})"
5.12 +proof safe
5.13 +  fix x assume "x < Suc n" "x \<notin> Suc ` {..<n}"
5.14 +  then have "x \<noteq> Suc (x - 1)" by auto
5.15 +  with `x < Suc n` show "x = 0" by auto
5.16 +qed
5.17 +
5.18  lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
5.19  by (simp add: lessThan_def atMost_def less_Suc_eq_le)
5.20
```