author wenzelm Sun, 03 Jan 2016 17:19:47 +0100 changeset 62046 2c9f68fbf047 parent 62045 75a7db3cae7e child 62047 1ae53588dcbb
tuned whitespace;
```--- a/src/HOL/Library/Nat_Bijection.thy	Sat Jan 02 21:33:57 2016 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy	Sun Jan 03 17:19:47 2016 +0100
@@ -16,10 +16,8 @@

text "Triangle numbers: 0, 1, 3, 6, 10, 15, ..."

-definition
-  triangle :: "nat \<Rightarrow> nat"
-where
-  "triangle n = n * Suc n div 2"
+definition triangle :: "nat \<Rightarrow> nat"
+  where "triangle n = (n * Suc n) div 2"

lemma triangle_0 [simp]: "triangle 0 = 0"
unfolding triangle_def by simp
@@ -27,25 +25,20 @@
lemma triangle_Suc [simp]: "triangle (Suc n) = triangle n + Suc n"
unfolding triangle_def by simp

-definition
-  prod_encode :: "nat \<times> nat \<Rightarrow> nat"
-where
-  "prod_encode = (\<lambda>(m, n). triangle (m + n) + m)"
+definition prod_encode :: "nat \<times> nat \<Rightarrow> nat"
+  where "prod_encode = (\<lambda>(m, n). triangle (m + n) + m)"

text \<open>In this auxiliary function, @{term "triangle k + m"} is an invariant.\<close>

-fun
-  prod_decode_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
+fun prod_decode_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
where
"prod_decode_aux k m =
(if m \<le> k then (m, k - m) else prod_decode_aux (Suc k) (m - Suc k))"

declare prod_decode_aux.simps [simp del]

-definition
-  prod_decode :: "nat \<Rightarrow> nat \<times> nat"
-where
-  "prod_decode = prod_decode_aux 0"
+definition prod_decode :: "nat \<Rightarrow> nat \<times> nat"
+  where "prod_decode = prod_decode_aux 0"

lemma prod_encode_prod_decode_aux:
"prod_encode (prod_decode_aux k m) = triangle k + m"
@@ -57,8 +50,7 @@
lemma prod_decode_inverse [simp]: "prod_encode (prod_decode n) = n"
unfolding prod_decode_def by (simp add: prod_encode_prod_decode_aux)

-  "prod_decode (triangle k + m) = prod_decode_aux k m"
+lemma prod_decode_triangle_add: "prod_decode (triangle k + m) = prod_decode_aux k m"
apply (induct k arbitrary: m)
@@ -96,6 +88,7 @@
lemma prod_decode_eq: "prod_decode x = prod_decode y \<longleftrightarrow> x = y"
by (rule inj_prod_decode [THEN inj_eq])

+
text \<open>Ordering properties\<close>

lemma le_prod_encode_1: "a \<le> prod_encode (a, b)"
@@ -107,13 +100,11 @@

subsection \<open>Type @{typ "nat + nat"}\<close>

-definition
-  sum_encode  :: "nat + nat \<Rightarrow> nat"
+definition sum_encode :: "nat + nat \<Rightarrow> nat"
where
"sum_encode x = (case x of Inl a \<Rightarrow> 2 * a | Inr b \<Rightarrow> Suc (2 * b))"

-definition
-  sum_decode  :: "nat \<Rightarrow> nat + nat"
+definition sum_decode :: "nat \<Rightarrow> nat + nat"
where
"sum_decode n = (if even n then Inl (n div 2) else Inr (n div 2))"

@@ -151,13 +142,11 @@

subsection \<open>Type @{typ "int"}\<close>

-definition
-  int_encode :: "int \<Rightarrow> nat"
+definition int_encode :: "int \<Rightarrow> nat"
where
"int_encode i = sum_encode (if 0 \<le> i then Inl (nat i) else Inr (nat (- i - 1)))"

-definition
-  int_decode :: "nat \<Rightarrow> int"
+definition int_decode :: "nat \<Rightarrow> int"
where
"int_decode n = (case sum_decode n of Inl a \<Rightarrow> int a | Inr b \<Rightarrow> - int b - 1)"

@@ -195,14 +184,12 @@

subsection \<open>Type @{typ "nat list"}\<close>

-fun
-  list_encode :: "nat list \<Rightarrow> nat"
+fun list_encode :: "nat list \<Rightarrow> nat"
where
"list_encode [] = 0"
| "list_encode (x # xs) = Suc (prod_encode (x, list_encode xs))"

-function
-  list_decode :: "nat \<Rightarrow> nat list"
+function list_decode :: "nat \<Rightarrow> nat list"
where
"list_decode 0 = []"
| "list_decode (Suc n) = (case prod_decode n of (x, y) \<Rightarrow> x # list_decode y)"
@@ -285,10 +272,8 @@

subsubsection \<open>From sets to naturals\<close>

-definition
-  set_encode :: "nat set \<Rightarrow> nat"
-where
-  "set_encode = setsum (op ^ 2)"
+definition set_encode :: "nat set \<Rightarrow> nat"
+  where "set_encode = setsum (op ^ 2)"

lemma set_encode_empty [simp]: "set_encode {} = 0"
@@ -314,12 +299,11 @@

lemmas set_encode_div_2 = set_encode_vimage_Suc [symmetric]

+
subsubsection \<open>From naturals to sets\<close>

-definition
-  set_decode :: "nat \<Rightarrow> nat set"
-where
-  "set_decode x = {n. odd (x div 2 ^ n)}"
+definition set_decode :: "nat \<Rightarrow> nat set"
+  where "set_decode x = {n. odd (x div 2 ^ n)}"

lemma set_decode_0 [simp]: "0 \<in> set_decode x \<longleftrightarrow> odd x"
@@ -358,6 +342,7 @@
done

+
subsubsection \<open>Proof of isomorphism\<close>

lemma set_decode_inverse [simp]: "set_encode (set_decode n) = n"
@@ -381,7 +366,9 @@
"\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> set_encode A = set_encode B \<longleftrightarrow> A = B"
by (rule iffI, simp add: inj_onD [OF inj_on_set_encode], simp)

-lemma subset_decode_imp_le: assumes "set_decode m \<subseteq> set_decode n" shows "m \<le> n"
+lemma subset_decode_imp_le:
+  assumes "set_decode m \<subseteq> set_decode n"
+  shows "m \<le> n"
proof -
have "n = m + set_encode (set_decode n - set_decode m)"
proof -```