merged
authorhoelzl
Thu Sep 02 18:45:23 2010 +0200 (2010-09-02)
changeset 39079bddc3d3f6e53
parent 39071 928c5a5bdc93
parent 39078 39f8f6d1eb74
child 39100 e9467adb8b52
child 39103 a9d710bf6074
merged
NEWS
     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.50  by (simp add: inj_on_eq_iff)
    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.57 -by (simp add: inj_on_def) 
    2.58 +by (simp add: inj_on_def)
    2.59  
    2.60 -lemma surj_id[simp]: "surj id"
    2.61 -by (simp add: surj_def) 
    2.62 +lemma surj_id[simp]: "surj_on id A"
    2.63 +by (simp add: surj_on_def)
    2.64  
    2.65 -lemma bij_id[simp]: "bij id"
    2.66 -by (simp add: bij_def)
    2.67 +lemma bij_id[simp]: "bij_betw id A A"
    2.68 +by (simp add: bij_betw_def)
    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.77 -apply (simp add: surj_def)
    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.98 -by (simp add: surj_def)
    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.126  by (simp add: bij_def)
   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.130  by (simp add: bij_betw_def)
   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.148  by (simp add: surj_range)
   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.211 -by (simp add: bij_def)
   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