src/HOL/Cardinals/Fun_More.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 63167 0909deb8059b
child 69735 8230dca028eb
permissions -rw-r--r--
tuned;
blanchet@49310
     1
(*  Title:      HOL/Cardinals/Fun_More.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
More on injections, bijections and inverses.
blanchet@48975
     6
*)
blanchet@48975
     7
wenzelm@63167
     8
section \<open>More on Injections, Bijections and Inverses\<close>
blanchet@48975
     9
blanchet@48975
    10
theory Fun_More
blanchet@55020
    11
imports Main
blanchet@48975
    12
begin
blanchet@48975
    13
wenzelm@63167
    14
subsection \<open>Purely functional properties\<close>
blanchet@48975
    15
blanchet@48975
    16
(* unused *)
blanchet@48975
    17
(*1*)lemma notIn_Un_bij_betw2:
blanchet@48975
    18
assumes NIN: "b \<notin> A" and NIN': "b' \<notin> A'" and
blanchet@48975
    19
        BIJ: "bij_betw f A A'"
blanchet@48975
    20
shows "bij_betw f (A \<union> {b}) (A' \<union> {b'}) = (f b = b')"
blanchet@48975
    21
proof
blanchet@48975
    22
  assume "f b = b'"
blanchet@48975
    23
  thus "bij_betw f (A \<union> {b}) (A' \<union> {b'})"
blanchet@48975
    24
  using assms notIn_Un_bij_betw[of b A f A'] by auto
blanchet@48975
    25
next
blanchet@48975
    26
  assume *: "bij_betw f (A \<union> {b}) (A' \<union> {b'})"
blanchet@48975
    27
  hence "f b \<in> A' \<union> {b'}"
blanchet@48975
    28
  unfolding bij_betw_def by auto
blanchet@48975
    29
  moreover
blanchet@48975
    30
  {assume "f b \<in> A'"
blanchet@48975
    31
   then obtain b1 where 1: "b1 \<in> A" and 2: "f b1 = f b" using BIJ
blanchet@48975
    32
   by (auto simp add: bij_betw_def)
blanchet@48975
    33
   hence "b = b1" using *
blanchet@48975
    34
   by (auto simp add: bij_betw_def inj_on_def)
blanchet@48975
    35
   with 1 NIN have False by auto
blanchet@48975
    36
  }
blanchet@48975
    37
  ultimately show "f b = b'" by blast
blanchet@48975
    38
qed
blanchet@48975
    39
blanchet@48975
    40
(* unused *)
blanchet@48975
    41
(*1*)lemma bij_betw_ball:
blanchet@48975
    42
assumes BIJ: "bij_betw f A B"
blanchet@48975
    43
shows "(\<forall>b \<in> B. phi b) = (\<forall>a \<in> A. phi(f a))"
blanchet@48975
    44
using assms unfolding bij_betw_def inj_on_def by blast
blanchet@48975
    45
blanchet@48975
    46
(* unused *)
blanchet@48975
    47
(*1*)lemma bij_betw_diff_singl:
blanchet@48975
    48
assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
blanchet@48975
    49
shows "bij_betw f (A - {a}) (A' - {f a})"
blanchet@48975
    50
proof-
blanchet@48975
    51
  let ?B = "A - {a}"   let ?B' = "A' - {f a}"
blanchet@48975
    52
  have "f a \<in> A'" using IN BIJ unfolding bij_betw_def by blast
blanchet@48975
    53
  hence "a \<notin> ?B \<and> f a \<notin> ?B' \<and> A = ?B \<union> {a} \<and> A' = ?B' \<union> {f a}"
blanchet@48975
    54
  using IN by blast
blanchet@48975
    55
  thus ?thesis using notIn_Un_bij_betw3[of a ?B f ?B'] BIJ by simp
blanchet@48975
    56
qed
blanchet@48975
    57
blanchet@48975
    58
wenzelm@63167
    59
subsection \<open>Properties involving finite and infinite sets\<close>
blanchet@48975
    60
blanchet@48975
    61
(*3*)lemma inj_on_image_Pow:
blanchet@48975
    62
assumes "inj_on f A"
blanchet@48975
    63
shows "inj_on (image f) (Pow A)"
blanchet@48975
    64
unfolding Pow_def inj_on_def proof(clarsimp)
blanchet@48975
    65
  fix X Y assume *: "X \<le> A" and **: "Y \<le> A" and
blanchet@48975
    66
                 ***: "f ` X = f ` Y"
blanchet@48975
    67
  show "X = Y"
blanchet@48975
    68
  proof(auto)
blanchet@48975
    69
    fix x assume ****: "x \<in> X"
blanchet@48975
    70
    with *** obtain y where "y \<in> Y \<and> f x = f y" by blast
blanchet@48975
    71
    with **** * ** assms show "x \<in> Y"
blanchet@48975
    72
    unfolding inj_on_def by auto
blanchet@48975
    73
  next
blanchet@48975
    74
    fix y assume ****: "y \<in> Y"
traytel@51764
    75
    with *** obtain x where "x \<in> X \<and> f x = f y" by atomize_elim force
blanchet@48975
    76
    with **** * ** assms show "y \<in> X"
blanchet@48975
    77
    unfolding inj_on_def by auto
blanchet@48975
    78
  qed
blanchet@48975
    79
qed
blanchet@48975
    80
blanchet@48975
    81
(*2*)lemma bij_betw_image_Pow:
blanchet@48975
    82
assumes "bij_betw f A B"
blanchet@48975
    83
shows "bij_betw (image f) (Pow A) (Pow B)"
blanchet@48975
    84
using assms unfolding bij_betw_def
blanchet@48975
    85
by (auto simp add: inj_on_image_Pow image_Pow_surj)
blanchet@48975
    86
blanchet@48975
    87
(* unused *)
blanchet@48975
    88
(*1*)lemma bij_betw_inv_into_RIGHT:
blanchet@48975
    89
assumes BIJ: "bij_betw f A A'" and SUB: "B' \<le> A'"
blanchet@48975
    90
shows "f `((inv_into A f)`B') = B'"
blanchet@48975
    91
using assms
blanchet@48975
    92
proof(auto simp add: bij_betw_inv_into_right)
blanchet@48975
    93
  let ?f' = "(inv_into A f)"
blanchet@48975
    94
  fix a' assume *: "a' \<in> B'"
blanchet@48975
    95
  hence "a' \<in> A'" using SUB by auto
blanchet@48975
    96
  hence "a' = f (?f' a')"
blanchet@48975
    97
  using BIJ by (auto simp add: bij_betw_inv_into_right)
blanchet@48975
    98
  thus "a' \<in> f ` (?f' ` B')" using * by blast
blanchet@48975
    99
qed
blanchet@48975
   100
blanchet@48975
   101
(* unused *)
blanchet@48975
   102
(*1*)lemma bij_betw_inv_into_RIGHT_LEFT:
blanchet@48975
   103
assumes BIJ: "bij_betw f A A'" and SUB: "B' \<le> A'" and
blanchet@48975
   104
        IM: "(inv_into A f) ` B' = B"
blanchet@48975
   105
shows "f ` B = B'"
blanchet@48975
   106
proof-
blanchet@48975
   107
  have "f`((inv_into A f)` B') = B'"
blanchet@48975
   108
  using assms bij_betw_inv_into_RIGHT[of f A A' B'] by auto
blanchet@48975
   109
  thus ?thesis using IM by auto
blanchet@48975
   110
qed
blanchet@48975
   111
blanchet@48975
   112
(* unused *)
blanchet@48975
   113
(*2*)lemma bij_betw_inv_into_twice:
blanchet@48975
   114
assumes "bij_betw f A A'"
blanchet@48975
   115
shows "\<forall>a \<in> A. inv_into A' (inv_into A f) a = f a"
blanchet@48975
   116
proof
blanchet@48975
   117
  let ?f' = "inv_into A f"   let ?f'' = "inv_into A' ?f'"
blanchet@48975
   118
  have 1: "bij_betw ?f' A' A" using assms
blanchet@48975
   119
  by (auto simp add: bij_betw_inv_into)
blanchet@48975
   120
  fix a assume *: "a \<in> A"
blanchet@48975
   121
  then obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a"
blanchet@48975
   122
  using 1 unfolding bij_betw_def by force
blanchet@48975
   123
  hence "?f'' a = a'"
blanchet@48975
   124
  using * 1 3 by (auto simp add: bij_betw_inv_into_left)
blanchet@48975
   125
  moreover have "f a = a'" using assms 2 3
blanchet@48975
   126
  by (auto simp add: bij_betw_inv_into_right)
blanchet@48975
   127
  ultimately show "?f'' a = f a" by simp
blanchet@48975
   128
qed
blanchet@48975
   129
blanchet@48975
   130
wenzelm@63167
   131
subsection \<open>Properties involving Hilbert choice\<close>
blanchet@48975
   132
blanchet@54478
   133
(*1*)lemma bij_betw_inv_into_LEFT:
blanchet@54478
   134
assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A"
blanchet@54478
   135
shows "(inv_into A f)`(f ` B) = B"
blanchet@54478
   136
using assms unfolding bij_betw_def using inv_into_image_cancel by force
blanchet@54478
   137
blanchet@54478
   138
(*1*)lemma bij_betw_inv_into_LEFT_RIGHT:
blanchet@54478
   139
assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A" and
blanchet@54478
   140
        IM: "f ` B = B'"
blanchet@54478
   141
shows "(inv_into A f) ` B' = B"
blanchet@54478
   142
using assms bij_betw_inv_into_LEFT[of f A A' B] by fast
blanchet@54478
   143
blanchet@54478
   144
wenzelm@63167
   145
subsection \<open>Other facts\<close>
blanchet@48975
   146
blanchet@48975
   147
(*3*)lemma atLeastLessThan_injective:
blanchet@48975
   148
assumes "{0 ..< m::nat} = {0 ..< n}"
blanchet@48975
   149
shows "m = n"
blanchet@48975
   150
proof-
blanchet@48975
   151
  {assume "m < n"
blanchet@48975
   152
   hence "m \<in> {0 ..< n}" by auto
blanchet@48975
   153
   hence "{0 ..< m} < {0 ..< n}" by auto
blanchet@48975
   154
   hence False using assms by blast
blanchet@48975
   155
  }
blanchet@48975
   156
  moreover
blanchet@48975
   157
  {assume "n < m"
blanchet@48975
   158
   hence "n \<in> {0 ..< m}" by auto
blanchet@48975
   159
   hence "{0 ..< n} < {0 ..< m}" by auto
blanchet@48975
   160
   hence False using assms by blast
blanchet@48975
   161
  }
blanchet@48975
   162
  ultimately show ?thesis by force
blanchet@48975
   163
qed
blanchet@48975
   164
blanchet@48975
   165
(*2*)lemma atLeastLessThan_injective2:
blanchet@48975
   166
"bij_betw f {0 ..< m::nat} {0 ..< n} \<Longrightarrow> m = n"
blanchet@48975
   167
using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
blanchet@48975
   168
      card_atLeastLessThan[of m] card_atLeastLessThan[of n]
blanchet@48975
   169
      bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto
blanchet@48975
   170
traytel@54581
   171
(*2*)lemma atLeastLessThan_less_eq:
traytel@54581
   172
"({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)"
traytel@54581
   173
unfolding ivl_subset by arith
traytel@54581
   174
traytel@54581
   175
(*2*)lemma atLeastLessThan_less_eq2:
traytel@54581
   176
assumes "inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}"
traytel@54581
   177
shows "m \<le> n"
traytel@54581
   178
using assms
traytel@54581
   179
using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n]
traytel@54581
   180
      card_atLeastLessThan[of m] card_atLeastLessThan[of n]
traytel@54581
   181
      card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce
traytel@54581
   182
blanchet@48975
   183
(* unused *)
blanchet@48975
   184
(*2*)lemma atLeastLessThan_less_eq3:
blanchet@48975
   185
"(\<exists>f. inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}) = (m \<le> n)"
blanchet@48975
   186
using atLeastLessThan_less_eq2
blanchet@48975
   187
proof(auto)
blanchet@48975
   188
  assume "m \<le> n"
blanchet@48975
   189
  hence "inj_on id {0..<m} \<and> id ` {0..<m} \<subseteq> {0..<n}" unfolding inj_on_def by force
blanchet@48975
   190
  thus "\<exists>f. inj_on f {0..<m} \<and> f ` {0..<m} \<subseteq> {0..<n}" by blast
blanchet@48975
   191
qed
blanchet@48975
   192
blanchet@48975
   193
(* unused *)
blanchet@48975
   194
(*3*)lemma atLeastLessThan_less:
blanchet@48975
   195
"({0..<m} < {0..<n}) = ((m::nat) < n)"
blanchet@48975
   196
proof-
blanchet@48975
   197
  have "({0..<m} < {0..<n}) = ({0..<m} \<le> {0..<n} \<and> {0..<m} ~= {0..<n})"
blanchet@48975
   198
  using subset_iff_psubset_eq by blast
blanchet@48975
   199
  also have "\<dots> = (m \<le> n \<and> m ~= n)"
blanchet@48975
   200
  using atLeastLessThan_less_eq atLeastLessThan_injective by blast
blanchet@48975
   201
  also have "\<dots> = (m < n)" by auto
blanchet@48975
   202
  finally show ?thesis .
blanchet@48975
   203
qed
blanchet@48975
   204
blanchet@48975
   205
end