new theory Library/Nat_Bijection.thy
authorhuffman
Wed Mar 10 14:57:13 2010 -0800 (2010-03-10)
changeset 35700951974ce903e
parent 35699 9ed327529a44
child 35701 0f5bf989da42
new theory Library/Nat_Bijection.thy
src/HOL/IsaMakefile
src/HOL/Library/Countable.thy
src/HOL/Library/Nat_Bijection.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Mar 10 19:21:59 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Mar 10 14:57:13 2010 -0800
     1.3 @@ -415,6 +415,7 @@
     1.4    Library/Enum.thy Library/Float.thy Library/Quotient_List.thy          \
     1.5    Library/Quotient_Option.thy Library/Quotient_Product.thy              \
     1.6    Library/Quotient_Sum.thy Library/Quotient_Syntax.thy                  \
     1.7 +  Library/Nat_Bijection.thy						\
     1.8    $(SRC)/Tools/float.ML                                                 \
     1.9    $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML		\
    1.10    Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy	\
     2.1 --- a/src/HOL/Library/Countable.thy	Wed Mar 10 19:21:59 2010 +0100
     2.2 +++ b/src/HOL/Library/Countable.thy	Wed Mar 10 14:57:13 2010 -0800
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Encoding (almost) everything into natural numbers *}
     2.5  
     2.6  theory Countable
     2.7 -imports Main Rat Nat_Int_Bij
     2.8 +imports Main Rat Nat_Bijection
     2.9  begin
    2.10  
    2.11  subsection {* The class of countable types *}
    2.12 @@ -48,7 +48,7 @@
    2.13  subsection {* Countable types *}
    2.14  
    2.15  instance nat :: countable
    2.16 -  by (rule countable_classI [of "id"]) simp 
    2.17 +  by (rule countable_classI [of "id"]) simp
    2.18  
    2.19  subclass (in finite) countable
    2.20  proof
    2.21 @@ -63,47 +63,9 @@
    2.22  
    2.23  text {* Pairs *}
    2.24  
    2.25 -primrec sum :: "nat \<Rightarrow> nat"
    2.26 -where
    2.27 -  "sum 0 = 0"
    2.28 -| "sum (Suc n) = Suc n + sum n"
    2.29 -
    2.30 -lemma sum_arith: "sum n = n * Suc n div 2"
    2.31 -  by (induct n) auto
    2.32 -
    2.33 -lemma sum_mono: "n \<ge> m \<Longrightarrow> sum n \<ge> sum m"
    2.34 -  by (induct n m rule: diff_induct) auto
    2.35 -
    2.36 -definition
    2.37 -  "pair_encode = (\<lambda>(m, n). sum (m + n) + m)"
    2.38 -
    2.39 -lemma inj_pair_cencode: "inj pair_encode"
    2.40 -  unfolding pair_encode_def
    2.41 -proof (rule injI, simp only: split_paired_all split_conv)
    2.42 -  fix a b c d
    2.43 -  assume eq: "sum (a + b) + a = sum (c + d) + c"
    2.44 -  have "a + b = c + d \<or> a + b \<ge> Suc (c + d) \<or> c + d \<ge> Suc (a + b)" by arith
    2.45 -  then
    2.46 -  show "(a, b) = (c, d)"
    2.47 -  proof (elim disjE)
    2.48 -    assume sumeq: "a + b = c + d"
    2.49 -    then have "a = c" using eq by auto
    2.50 -    moreover from sumeq this have "b = d" by auto
    2.51 -    ultimately show ?thesis by simp
    2.52 -  next
    2.53 -    assume "a + b \<ge> Suc (c + d)"
    2.54 -    from sum_mono[OF this] eq
    2.55 -    show ?thesis by auto
    2.56 -  next
    2.57 -    assume "c + d \<ge> Suc (a + b)"
    2.58 -    from sum_mono[OF this] eq
    2.59 -    show ?thesis by auto
    2.60 -  qed
    2.61 -qed
    2.62 -
    2.63  instance "*" :: (countable, countable) countable
    2.64 -by (rule countable_classI [of "\<lambda>(x, y). pair_encode (to_nat x, to_nat y)"])
    2.65 -  (auto dest: injD [OF inj_pair_cencode] injD [OF inj_to_nat])
    2.66 +  by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
    2.67 +    (auto simp add: prod_encode_eq)
    2.68  
    2.69  
    2.70  text {* Sums *}
    2.71 @@ -111,76 +73,28 @@
    2.72  instance "+":: (countable, countable) countable
    2.73    by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
    2.74                                       | Inr b \<Rightarrow> to_nat (True, to_nat b))"])
    2.75 -    (auto split:sum.splits)
    2.76 +    (simp split: sum.split_asm)
    2.77  
    2.78  
    2.79  text {* Integers *}
    2.80  
    2.81 -lemma int_cases: "(i::int) = 0 \<or> i < 0 \<or> i > 0"
    2.82 -by presburger
    2.83 -
    2.84 -lemma int_pos_neg_zero:
    2.85 -  obtains (zero) "(z::int) = 0" "sgn z = 0" "abs z = 0"
    2.86 -  | (pos) n where "z = of_nat n" "sgn z = 1" "abs z = of_nat n"
    2.87 -  | (neg) n where "z = - (of_nat n)" "sgn z = -1" "abs z = of_nat n"
    2.88 -apply atomize_elim
    2.89 -apply (insert int_cases[of z])
    2.90 -apply (auto simp:zsgn_def)
    2.91 -apply (rule_tac x="nat (-z)" in exI, simp)
    2.92 -apply (rule_tac x="nat z" in exI, simp)
    2.93 -done
    2.94 -
    2.95  instance int :: countable
    2.96 -proof (rule countable_classI [of "(\<lambda>i. to_nat (nat (sgn i + 1), nat (abs i)))"], 
    2.97 -    auto dest: injD [OF inj_to_nat])
    2.98 -  fix x y 
    2.99 -  assume a: "nat (sgn x + 1) = nat (sgn y + 1)" "nat (abs x) = nat (abs y)"
   2.100 -  show "x = y"
   2.101 -  proof (cases rule: int_pos_neg_zero[of x])
   2.102 -    case zero 
   2.103 -    with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
   2.104 -  next
   2.105 -    case (pos n)
   2.106 -    with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
   2.107 -  next
   2.108 -    case (neg n)
   2.109 -    with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
   2.110 -  qed
   2.111 -qed
   2.112 +  by (rule countable_classI [of "int_encode"])
   2.113 +    (simp add: int_encode_eq)
   2.114  
   2.115  
   2.116  text {* Options *}
   2.117  
   2.118  instance option :: (countable) countable
   2.119 -by (rule countable_classI[of "\<lambda>x. case x of None \<Rightarrow> 0
   2.120 -                                     | Some y \<Rightarrow> Suc (to_nat y)"])
   2.121 - (auto split:option.splits)
   2.122 +  by (rule countable_classI [of "option_case 0 (Suc \<circ> to_nat)"])
   2.123 +    (simp split: option.split_asm)
   2.124  
   2.125  
   2.126  text {* Lists *}
   2.127  
   2.128 -lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs"
   2.129 -  by (simp add: comp_def)
   2.130 -
   2.131 -primrec
   2.132 -  list_encode :: "'a\<Colon>countable list \<Rightarrow> nat"
   2.133 -where
   2.134 -  "list_encode [] = 0"
   2.135 -| "list_encode (x#xs) = Suc (to_nat (x, list_encode xs))"
   2.136 -
   2.137  instance list :: (countable) countable
   2.138 -proof (rule countable_classI [of "list_encode"])
   2.139 -  fix xs ys :: "'a list"
   2.140 -  assume cenc: "list_encode xs = list_encode ys"
   2.141 -  then show "xs = ys"
   2.142 -  proof (induct xs arbitrary: ys)
   2.143 -    case (Nil ys)
   2.144 -    with cenc show ?case by (cases ys, auto)
   2.145 -  next
   2.146 -    case (Cons x xs' ys)
   2.147 -    thus ?case by (cases ys) auto
   2.148 -  qed
   2.149 -qed
   2.150 +  by (rule countable_classI [of "list_encode \<circ> map to_nat"])
   2.151 +    (simp add: list_encode_eq)
   2.152  
   2.153  
   2.154  text {* Functions *}
   2.155 @@ -200,8 +114,8 @@
   2.156  subsection {* The Rationals are Countably Infinite *}
   2.157  
   2.158  definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
   2.159 -"nat_to_rat_surj n = (let (a,b) = nat_to_nat2 n
   2.160 -                      in Fract (nat_to_int_bij a) (nat_to_int_bij b))"
   2.161 +"nat_to_rat_surj n = (let (a,b) = prod_decode n
   2.162 +                      in Fract (int_decode a) (int_decode b))"
   2.163  
   2.164  lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
   2.165  unfolding surj_def
   2.166 @@ -210,10 +124,9 @@
   2.167    show "\<exists>n. r = nat_to_rat_surj n"
   2.168    proof (cases r)
   2.169      fix i j assume [simp]: "r = Fract i j" and "j > 0"
   2.170 -    have "r = (let m = inv nat_to_int_bij i; n = inv nat_to_int_bij j
   2.171 -               in nat_to_rat_surj(nat2_to_nat (m,n)))"
   2.172 -      using nat2_to_nat_inj surj_f_inv_f[OF surj_nat_to_int_bij]
   2.173 -      by(simp add:Let_def nat_to_rat_surj_def nat_to_nat2_def)
   2.174 +    have "r = (let m = int_encode i; n = int_encode j
   2.175 +               in nat_to_rat_surj(prod_encode (m,n)))"
   2.176 +      by (simp add: Let_def nat_to_rat_surj_def)
   2.177      thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
   2.178    qed
   2.179  qed
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Wed Mar 10 14:57:13 2010 -0800
     3.3 @@ -0,0 +1,370 @@
     3.4 +(*  Title:      HOL/Nat_Bijection.thy
     3.5 +    Author:     Brian Huffman
     3.6 +    Author:     Florian Haftmann
     3.7 +    Author:     Stefan Richter
     3.8 +    Author:     Tobias Nipkow
     3.9 +    Author:     Alexander Krauss
    3.10 +*)
    3.11 +
    3.12 +header {* Bijections between natural numbers and other types *}
    3.13 +
    3.14 +theory Nat_Bijection
    3.15 +imports Main Parity
    3.16 +begin
    3.17 +
    3.18 +subsection {* Type @{typ "nat \<times> nat"} *}
    3.19 +
    3.20 +text "Triangle numbers: 0, 1, 3, 6, 10, 15, ..."
    3.21 +
    3.22 +definition
    3.23 +  triangle :: "nat \<Rightarrow> nat"
    3.24 +where
    3.25 +  "triangle n = n * Suc n div 2"
    3.26 +
    3.27 +lemma triangle_0 [simp]: "triangle 0 = 0"
    3.28 +unfolding triangle_def by simp
    3.29 +
    3.30 +lemma triangle_Suc [simp]: "triangle (Suc n) = triangle n + Suc n"
    3.31 +unfolding triangle_def by simp
    3.32 +
    3.33 +definition
    3.34 +  prod_encode :: "nat \<times> nat \<Rightarrow> nat"
    3.35 +where
    3.36 +  "prod_encode = (\<lambda>(m, n). triangle (m + n) + m)"
    3.37 +
    3.38 +text {* In this auxiliary function, @{term "triangle k + m"} is an invariant. *}
    3.39 +
    3.40 +fun
    3.41 +  prod_decode_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
    3.42 +where
    3.43 +  "prod_decode_aux k m =
    3.44 +    (if m \<le> k then (m, k - m) else prod_decode_aux (Suc k) (m - Suc k))"
    3.45 +
    3.46 +declare prod_decode_aux.simps [simp del]
    3.47 +
    3.48 +definition
    3.49 +  prod_decode :: "nat \<Rightarrow> nat \<times> nat"
    3.50 +where
    3.51 +  "prod_decode = prod_decode_aux 0"
    3.52 +
    3.53 +lemma prod_encode_prod_decode_aux:
    3.54 +  "prod_encode (prod_decode_aux k m) = triangle k + m"
    3.55 +apply (induct k m rule: prod_decode_aux.induct)
    3.56 +apply (subst prod_decode_aux.simps)
    3.57 +apply (simp add: prod_encode_def)
    3.58 +done
    3.59 +
    3.60 +lemma prod_decode_inverse [simp]: "prod_encode (prod_decode n) = n"
    3.61 +unfolding prod_decode_def by (simp add: prod_encode_prod_decode_aux)
    3.62 +
    3.63 +lemma prod_decode_triangle_add:
    3.64 +  "prod_decode (triangle k + m) = prod_decode_aux k m"
    3.65 +apply (induct k arbitrary: m)
    3.66 +apply (simp add: prod_decode_def)
    3.67 +apply (simp only: triangle_Suc add_assoc)
    3.68 +apply (subst prod_decode_aux.simps, simp)
    3.69 +done
    3.70 +
    3.71 +lemma prod_encode_inverse [simp]: "prod_decode (prod_encode x) = x"
    3.72 +unfolding prod_encode_def
    3.73 +apply (induct x)
    3.74 +apply (simp add: prod_decode_triangle_add)
    3.75 +apply (subst prod_decode_aux.simps, simp)
    3.76 +done
    3.77 +
    3.78 +lemma inj_prod_encode: "inj_on prod_encode A"
    3.79 +by (rule inj_on_inverseI, rule prod_encode_inverse)
    3.80 +
    3.81 +lemma inj_prod_decode: "inj_on prod_decode A"
    3.82 +by (rule inj_on_inverseI, rule prod_decode_inverse)
    3.83 +
    3.84 +lemma surj_prod_encode: "surj prod_encode"
    3.85 +by (rule surjI, rule prod_decode_inverse)
    3.86 +
    3.87 +lemma surj_prod_decode: "surj prod_decode"
    3.88 +by (rule surjI, rule prod_encode_inverse)
    3.89 +
    3.90 +lemma bij_prod_encode: "bij prod_encode"
    3.91 +by (rule bijI [OF inj_prod_encode surj_prod_encode])
    3.92 +
    3.93 +lemma bij_prod_decode: "bij prod_decode"
    3.94 +by (rule bijI [OF inj_prod_decode surj_prod_decode])
    3.95 +
    3.96 +lemma prod_encode_eq: "prod_encode x = prod_encode y \<longleftrightarrow> x = y"
    3.97 +by (rule inj_prod_encode [THEN inj_eq])
    3.98 +
    3.99 +lemma prod_decode_eq: "prod_decode x = prod_decode y \<longleftrightarrow> x = y"
   3.100 +by (rule inj_prod_decode [THEN inj_eq])
   3.101 +
   3.102 +text {* Ordering properties *}
   3.103 +
   3.104 +lemma le_prod_encode_1: "a \<le> prod_encode (a, b)"
   3.105 +unfolding prod_encode_def by simp
   3.106 +
   3.107 +lemma le_prod_encode_2: "b \<le> prod_encode (a, b)"
   3.108 +unfolding prod_encode_def by (induct b, simp_all)
   3.109 +
   3.110 +
   3.111 +subsection {* Type @{typ "nat + nat"} *}
   3.112 +
   3.113 +definition
   3.114 +  sum_encode  :: "nat + nat \<Rightarrow> nat"
   3.115 +where
   3.116 +  "sum_encode x = (case x of Inl a \<Rightarrow> 2 * a | Inr b \<Rightarrow> Suc (2 * b))"
   3.117 +
   3.118 +definition
   3.119 +  sum_decode  :: "nat \<Rightarrow> nat + nat"
   3.120 +where
   3.121 +  "sum_decode n = (if even n then Inl (n div 2) else Inr (n div 2))"
   3.122 +
   3.123 +lemma sum_encode_inverse [simp]: "sum_decode (sum_encode x) = x"
   3.124 +unfolding sum_decode_def sum_encode_def
   3.125 +by (induct x) simp_all
   3.126 +
   3.127 +lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n"
   3.128 +unfolding sum_decode_def sum_encode_def numeral_2_eq_2
   3.129 +by (simp add: even_nat_div_two_times_two odd_nat_div_two_times_two_plus_one
   3.130 +         del: mult_Suc)
   3.131 +
   3.132 +lemma inj_sum_encode: "inj_on sum_encode A"
   3.133 +by (rule inj_on_inverseI, rule sum_encode_inverse)
   3.134 +
   3.135 +lemma inj_sum_decode: "inj_on sum_decode A"
   3.136 +by (rule inj_on_inverseI, rule sum_decode_inverse)
   3.137 +
   3.138 +lemma surj_sum_encode: "surj sum_encode"
   3.139 +by (rule surjI, rule sum_decode_inverse)
   3.140 +
   3.141 +lemma surj_sum_decode: "surj sum_decode"
   3.142 +by (rule surjI, rule sum_encode_inverse)
   3.143 +
   3.144 +lemma bij_sum_encode: "bij sum_encode"
   3.145 +by (rule bijI [OF inj_sum_encode surj_sum_encode])
   3.146 +
   3.147 +lemma bij_sum_decode: "bij sum_decode"
   3.148 +by (rule bijI [OF inj_sum_decode surj_sum_decode])
   3.149 +
   3.150 +lemma sum_encode_eq: "sum_encode x = sum_encode y \<longleftrightarrow> x = y"
   3.151 +by (rule inj_sum_encode [THEN inj_eq])
   3.152 +
   3.153 +lemma sum_decode_eq: "sum_decode x = sum_decode y \<longleftrightarrow> x = y"
   3.154 +by (rule inj_sum_decode [THEN inj_eq])
   3.155 +
   3.156 +
   3.157 +subsection {* Type @{typ "int"} *}
   3.158 +
   3.159 +definition
   3.160 +  int_encode :: "int \<Rightarrow> nat"
   3.161 +where
   3.162 +  "int_encode i = sum_encode (if 0 \<le> i then Inl (nat i) else Inr (nat (- i - 1)))"
   3.163 +
   3.164 +definition
   3.165 +  int_decode :: "nat \<Rightarrow> int"
   3.166 +where
   3.167 +  "int_decode n = (case sum_decode n of Inl a \<Rightarrow> int a | Inr b \<Rightarrow> - int b - 1)"
   3.168 +
   3.169 +lemma int_encode_inverse [simp]: "int_decode (int_encode x) = x"
   3.170 +unfolding int_decode_def int_encode_def by simp
   3.171 +
   3.172 +lemma int_decode_inverse [simp]: "int_encode (int_decode n) = n"
   3.173 +unfolding int_decode_def int_encode_def using sum_decode_inverse [of n]
   3.174 +by (cases "sum_decode n", simp_all)
   3.175 +
   3.176 +lemma inj_int_encode: "inj_on int_encode A"
   3.177 +by (rule inj_on_inverseI, rule int_encode_inverse)
   3.178 +
   3.179 +lemma inj_int_decode: "inj_on int_decode A"
   3.180 +by (rule inj_on_inverseI, rule int_decode_inverse)
   3.181 +
   3.182 +lemma surj_int_encode: "surj int_encode"
   3.183 +by (rule surjI, rule int_decode_inverse)
   3.184 +
   3.185 +lemma surj_int_decode: "surj int_decode"
   3.186 +by (rule surjI, rule int_encode_inverse)
   3.187 +
   3.188 +lemma bij_int_encode: "bij int_encode"
   3.189 +by (rule bijI [OF inj_int_encode surj_int_encode])
   3.190 +
   3.191 +lemma bij_int_decode: "bij int_decode"
   3.192 +by (rule bijI [OF inj_int_decode surj_int_decode])
   3.193 +
   3.194 +lemma int_encode_eq: "int_encode x = int_encode y \<longleftrightarrow> x = y"
   3.195 +by (rule inj_int_encode [THEN inj_eq])
   3.196 +
   3.197 +lemma int_decode_eq: "int_decode x = int_decode y \<longleftrightarrow> x = y"
   3.198 +by (rule inj_int_decode [THEN inj_eq])
   3.199 +
   3.200 +
   3.201 +subsection {* Type @{typ "nat list"} *}
   3.202 +
   3.203 +fun
   3.204 +  list_encode :: "nat list \<Rightarrow> nat"
   3.205 +where
   3.206 +  "list_encode [] = 0"
   3.207 +| "list_encode (x # xs) = Suc (prod_encode (x, list_encode xs))"
   3.208 +
   3.209 +function
   3.210 +  list_decode :: "nat \<Rightarrow> nat list"
   3.211 +where
   3.212 +  "list_decode 0 = []"
   3.213 +| "list_decode (Suc n) = (case prod_decode n of (x, y) \<Rightarrow> x # list_decode y)"
   3.214 +by pat_completeness auto
   3.215 +
   3.216 +termination list_decode
   3.217 +apply (relation "measure id", simp_all)
   3.218 +apply (drule arg_cong [where f="prod_encode"])
   3.219 +apply (simp add: le_imp_less_Suc le_prod_encode_2)
   3.220 +done
   3.221 +
   3.222 +lemma list_encode_inverse [simp]: "list_decode (list_encode x) = x"
   3.223 +by (induct x rule: list_encode.induct) simp_all
   3.224 +
   3.225 +lemma list_decode_inverse [simp]: "list_encode (list_decode n) = n"
   3.226 +apply (induct n rule: list_decode.induct, simp)
   3.227 +apply (simp split: prod.split)
   3.228 +apply (simp add: prod_decode_eq [symmetric])
   3.229 +done
   3.230 +
   3.231 +lemma inj_list_encode: "inj_on list_encode A"
   3.232 +by (rule inj_on_inverseI, rule list_encode_inverse)
   3.233 +
   3.234 +lemma inj_list_decode: "inj_on list_decode A"
   3.235 +by (rule inj_on_inverseI, rule list_decode_inverse)
   3.236 +
   3.237 +lemma surj_list_encode: "surj list_encode"
   3.238 +by (rule surjI, rule list_decode_inverse)
   3.239 +
   3.240 +lemma surj_list_decode: "surj list_decode"
   3.241 +by (rule surjI, rule list_encode_inverse)
   3.242 +
   3.243 +lemma bij_list_encode: "bij list_encode"
   3.244 +by (rule bijI [OF inj_list_encode surj_list_encode])
   3.245 +
   3.246 +lemma bij_list_decode: "bij list_decode"
   3.247 +by (rule bijI [OF inj_list_decode surj_list_decode])
   3.248 +
   3.249 +lemma list_encode_eq: "list_encode x = list_encode y \<longleftrightarrow> x = y"
   3.250 +by (rule inj_list_encode [THEN inj_eq])
   3.251 +
   3.252 +lemma list_decode_eq: "list_decode x = list_decode y \<longleftrightarrow> x = y"
   3.253 +by (rule inj_list_decode [THEN inj_eq])
   3.254 +
   3.255 +
   3.256 +subsection {* Finite sets of naturals *}
   3.257 +
   3.258 +subsubsection {* Preliminaries *}
   3.259 +
   3.260 +lemma finite_vimage_Suc_iff: "finite (Suc -` F) \<longleftrightarrow> finite F"
   3.261 +apply (safe intro!: finite_vimageI inj_Suc)
   3.262 +apply (rule finite_subset [where B="insert 0 (Suc ` Suc -` F)"])
   3.263 +apply (rule subsetI, case_tac x, simp, simp)
   3.264 +apply (rule finite_insert [THEN iffD2])
   3.265 +apply (erule finite_imageI)
   3.266 +done
   3.267 +
   3.268 +lemma vimage_Suc_insert_0: "Suc -` insert 0 A = Suc -` A"
   3.269 +by auto
   3.270 +
   3.271 +lemma vimage_Suc_insert_Suc:
   3.272 +  "Suc -` insert (Suc n) A = insert n (Suc -` A)"
   3.273 +by auto
   3.274 +
   3.275 +lemma even_nat_Suc_div_2: "even x \<Longrightarrow> Suc x div 2 = x div 2"
   3.276 +by (simp only: numeral_2_eq_2 even_nat_plus_one_div_two)
   3.277 +
   3.278 +lemma div2_even_ext_nat:
   3.279 +  "\<lbrakk>x div 2 = y div 2; even x = even y\<rbrakk> \<Longrightarrow> (x::nat) = y"
   3.280 +apply (rule mod_div_equality [of x 2, THEN subst])
   3.281 +apply (rule mod_div_equality [of y 2, THEN subst])
   3.282 +apply (case_tac "even x")
   3.283 +apply (simp add: numeral_2_eq_2 even_nat_equiv_def)
   3.284 +apply (simp add: numeral_2_eq_2 odd_nat_equiv_def)
   3.285 +done
   3.286 +
   3.287 +subsubsection {* From sets to naturals *}
   3.288 +
   3.289 +definition
   3.290 +  set_encode :: "nat set \<Rightarrow> nat"
   3.291 +where
   3.292 +  "set_encode = setsum (op ^ 2)"
   3.293 +
   3.294 +lemma set_encode_empty [simp]: "set_encode {} = 0"
   3.295 +by (simp add: set_encode_def)
   3.296 +
   3.297 +lemma set_encode_insert [simp]:
   3.298 +  "\<lbrakk>finite A; n \<notin> A\<rbrakk> \<Longrightarrow> set_encode (insert n A) = 2^n + set_encode A"
   3.299 +by (simp add: set_encode_def)
   3.300 +
   3.301 +lemma even_set_encode_iff: "finite A \<Longrightarrow> even (set_encode A) \<longleftrightarrow> 0 \<notin> A"
   3.302 +unfolding set_encode_def by (induct set: finite, auto)
   3.303 +
   3.304 +lemma set_encode_vimage_Suc: "set_encode (Suc -` A) = set_encode A div 2"
   3.305 +apply (cases "finite A")
   3.306 +apply (erule finite_induct, simp)
   3.307 +apply (case_tac x)
   3.308 +apply (simp add: even_nat_Suc_div_2 even_set_encode_iff vimage_Suc_insert_0)
   3.309 +apply (simp add: finite_vimageI add_commute vimage_Suc_insert_Suc)
   3.310 +apply (simp add: set_encode_def finite_vimage_Suc_iff)
   3.311 +done
   3.312 +
   3.313 +lemmas set_encode_div_2 = set_encode_vimage_Suc [symmetric]
   3.314 +
   3.315 +subsubsection {* From naturals to sets *}
   3.316 +
   3.317 +definition
   3.318 +  set_decode :: "nat \<Rightarrow> nat set"
   3.319 +where
   3.320 +  "set_decode x = {n. odd (x div 2 ^ n)}"
   3.321 +
   3.322 +lemma set_decode_0 [simp]: "0 \<in> set_decode x \<longleftrightarrow> odd x"
   3.323 +by (simp add: set_decode_def)
   3.324 +
   3.325 +lemma set_decode_Suc [simp]:
   3.326 +  "Suc n \<in> set_decode x \<longleftrightarrow> n \<in> set_decode (x div 2)"
   3.327 +by (simp add: set_decode_def div_mult2_eq)
   3.328 +
   3.329 +lemma set_decode_zero [simp]: "set_decode 0 = {}"
   3.330 +by (simp add: set_decode_def)
   3.331 +
   3.332 +lemma set_decode_div_2: "set_decode (x div 2) = Suc -` set_decode x"
   3.333 +by auto
   3.334 +
   3.335 +lemma set_decode_plus_power_2:
   3.336 +  "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)"
   3.337 + apply (induct n arbitrary: z, simp_all)
   3.338 +  apply (rule set_ext, induct_tac x, simp, simp add: even_nat_Suc_div_2)
   3.339 + apply (rule set_ext, induct_tac x, simp, simp add: add_commute)
   3.340 +done
   3.341 +
   3.342 +lemma finite_set_decode [simp]: "finite (set_decode n)"
   3.343 +apply (induct n rule: nat_less_induct)
   3.344 +apply (case_tac "n = 0", simp)
   3.345 +apply (drule_tac x="n div 2" in spec, simp)
   3.346 +apply (simp add: set_decode_div_2)
   3.347 +apply (simp add: finite_vimage_Suc_iff)
   3.348 +done
   3.349 +
   3.350 +subsubsection {* Proof of isomorphism *}
   3.351 +
   3.352 +lemma set_decode_inverse [simp]: "set_encode (set_decode n) = n"
   3.353 +apply (induct n rule: nat_less_induct)
   3.354 +apply (case_tac "n = 0", simp)
   3.355 +apply (drule_tac x="n div 2" in spec, simp)
   3.356 +apply (simp add: set_decode_div_2 set_encode_vimage_Suc)
   3.357 +apply (erule div2_even_ext_nat)
   3.358 +apply (simp add: even_set_encode_iff)
   3.359 +done
   3.360 +
   3.361 +lemma set_encode_inverse [simp]: "finite A \<Longrightarrow> set_decode (set_encode A) = A"
   3.362 +apply (erule finite_induct, simp_all)
   3.363 +apply (simp add: set_decode_plus_power_2)
   3.364 +done
   3.365 +
   3.366 +lemma inj_on_set_encode: "inj_on set_encode (Collect finite)"
   3.367 +by (rule inj_on_inverseI [where g="set_decode"], simp)
   3.368 +
   3.369 +lemma set_encode_eq:
   3.370 +  "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> set_encode A = set_encode B \<longleftrightarrow> A = B"
   3.371 +by (rule iffI, simp add: inj_onD [OF inj_on_set_encode], simp)
   3.372 +
   3.373 +end