equal
deleted
inserted
replaced
10 |
10 |
11 theory Nat_Bijection |
11 theory Nat_Bijection |
12 imports Main |
12 imports Main |
13 begin |
13 begin |
14 |
14 |
15 subsection \<open>Type @{typ "nat \<times> nat"}\<close> |
15 subsection \<open>Type \<^typ>\<open>nat \<times> nat\<close>\<close> |
16 |
16 |
17 text \<open>Triangle numbers: 0, 1, 3, 6, 10, 15, ...\<close> |
17 text \<open>Triangle numbers: 0, 1, 3, 6, 10, 15, ...\<close> |
18 |
18 |
19 definition triangle :: "nat \<Rightarrow> nat" |
19 definition triangle :: "nat \<Rightarrow> nat" |
20 where "triangle n = (n * Suc n) div 2" |
20 where "triangle n = (n * Suc n) div 2" |
26 by (simp add: triangle_def) |
26 by (simp add: triangle_def) |
27 |
27 |
28 definition prod_encode :: "nat \<times> nat \<Rightarrow> nat" |
28 definition prod_encode :: "nat \<times> nat \<Rightarrow> nat" |
29 where "prod_encode = (\<lambda>(m, n). triangle (m + n) + m)" |
29 where "prod_encode = (\<lambda>(m, n). triangle (m + n) + m)" |
30 |
30 |
31 text \<open>In this auxiliary function, @{term "triangle k + m"} is an invariant.\<close> |
31 text \<open>In this auxiliary function, \<^term>\<open>triangle k + m\<close> is an invariant.\<close> |
32 |
32 |
33 fun prod_decode_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" |
33 fun prod_decode_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" |
34 where "prod_decode_aux k m = |
34 where "prod_decode_aux k m = |
35 (if m \<le> k then (m, k - m) else prod_decode_aux (Suc k) (m - Suc k))" |
35 (if m \<le> k then (m, k - m) else prod_decode_aux (Suc k) (m - Suc k))" |
36 |
36 |
96 |
96 |
97 lemma le_prod_encode_2: "b \<le> prod_encode (a, b)" |
97 lemma le_prod_encode_2: "b \<le> prod_encode (a, b)" |
98 by (induct b) (simp_all add: prod_encode_def) |
98 by (induct b) (simp_all add: prod_encode_def) |
99 |
99 |
100 |
100 |
101 subsection \<open>Type @{typ "nat + nat"}\<close> |
101 subsection \<open>Type \<^typ>\<open>nat + nat\<close>\<close> |
102 |
102 |
103 definition sum_encode :: "nat + nat \<Rightarrow> nat" |
103 definition sum_encode :: "nat + nat \<Rightarrow> nat" |
104 where "sum_encode x = (case x of Inl a \<Rightarrow> 2 * a | Inr b \<Rightarrow> Suc (2 * b))" |
104 where "sum_encode x = (case x of Inl a \<Rightarrow> 2 * a | Inr b \<Rightarrow> Suc (2 * b))" |
105 |
105 |
106 definition sum_decode :: "nat \<Rightarrow> nat + nat" |
106 definition sum_decode :: "nat \<Rightarrow> nat + nat" |
135 |
135 |
136 lemma sum_decode_eq: "sum_decode x = sum_decode y \<longleftrightarrow> x = y" |
136 lemma sum_decode_eq: "sum_decode x = sum_decode y \<longleftrightarrow> x = y" |
137 by (rule inj_sum_decode [THEN inj_eq]) |
137 by (rule inj_sum_decode [THEN inj_eq]) |
138 |
138 |
139 |
139 |
140 subsection \<open>Type @{typ "int"}\<close> |
140 subsection \<open>Type \<^typ>\<open>int\<close>\<close> |
141 |
141 |
142 definition int_encode :: "int \<Rightarrow> nat" |
142 definition int_encode :: "int \<Rightarrow> nat" |
143 where "int_encode i = sum_encode (if 0 \<le> i then Inl (nat i) else Inr (nat (- i - 1)))" |
143 where "int_encode i = sum_encode (if 0 \<le> i then Inl (nat i) else Inr (nat (- i - 1)))" |
144 |
144 |
145 definition int_decode :: "nat \<Rightarrow> int" |
145 definition int_decode :: "nat \<Rightarrow> int" |
175 |
175 |
176 lemma int_decode_eq: "int_decode x = int_decode y \<longleftrightarrow> x = y" |
176 lemma int_decode_eq: "int_decode x = int_decode y \<longleftrightarrow> x = y" |
177 by (rule inj_int_decode [THEN inj_eq]) |
177 by (rule inj_int_decode [THEN inj_eq]) |
178 |
178 |
179 |
179 |
180 subsection \<open>Type @{typ "nat list"}\<close> |
180 subsection \<open>Type \<^typ>\<open>nat list\<close>\<close> |
181 |
181 |
182 fun list_encode :: "nat list \<Rightarrow> nat" |
182 fun list_encode :: "nat list \<Rightarrow> nat" |
183 where |
183 where |
184 "list_encode [] = 0" |
184 "list_encode [] = 0" |
185 | "list_encode (x # xs) = Suc (prod_encode (x, list_encode xs))" |
185 | "list_encode (x # xs) = Suc (prod_encode (x, list_encode xs))" |