src/HOLCF/NatIso.thy
 author huffman Mon May 11 08:28:09 2009 -0700 (2009-05-11) changeset 31095 b79d140f6d0b parent 28952 15a4b2cf8c34 permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
```     1 (*  Title:      HOLCF/NatIso.thy
```
```     2     Author:     Brian Huffman
```
```     3 *)
```
```     4
```
```     5 header {* Isomorphisms of the Natural Numbers *}
```
```     6
```
```     7 theory NatIso
```
```     8 imports Parity
```
```     9 begin
```
```    10
```
```    11 subsection {* Isomorphism between naturals and sums of naturals *}
```
```    12
```
```    13 primrec
```
```    14   sum2nat  :: "nat + nat \<Rightarrow> nat"
```
```    15 where
```
```    16   "sum2nat (Inl a) = a + a"
```
```    17 | "sum2nat (Inr b) = Suc (b + b)"
```
```    18
```
```    19 primrec
```
```    20   nat2sum  :: "nat \<Rightarrow> nat + nat"
```
```    21 where
```
```    22   "nat2sum 0 = Inl 0"
```
```    23 | "nat2sum (Suc n) = (case nat2sum n of
```
```    24     Inl a \<Rightarrow> Inr a | Inr b \<Rightarrow> Inl (Suc b))"
```
```    25
```
```    26 lemma nat2sum_sum2nat [simp]: "nat2sum (sum2nat x) = x"
```
```    27 by (induct x, rule_tac [!] nat.induct, simp_all)
```
```    28
```
```    29 lemma sum2nat_nat2sum [simp]: "sum2nat (nat2sum n) = n"
```
```    30 by (induct n, auto split: sum.split)
```
```    31
```
```    32 lemma inj_sum2nat: "inj sum2nat"
```
```    33 by (rule inj_on_inverseI, rule nat2sum_sum2nat)
```
```    34
```
```    35 lemma sum2nat_eq_iff [simp]: "sum2nat x = sum2nat y \<longleftrightarrow> x = y"
```
```    36 by (rule inj_sum2nat [THEN inj_eq])
```
```    37
```
```    38 lemma inj_nat2sum: "inj nat2sum"
```
```    39 by (rule inj_on_inverseI, rule sum2nat_nat2sum)
```
```    40
```
```    41 lemma nat2sum_eq_iff [simp]: "nat2sum x = nat2sum y \<longleftrightarrow> x = y"
```
```    42 by (rule inj_nat2sum [THEN inj_eq])
```
```    43
```
```    44 declare sum2nat.simps [simp del]
```
```    45 declare nat2sum.simps [simp del]
```
```    46
```
```    47
```
```    48 subsection {* Isomorphism between naturals and pairs of naturals *}
```
```    49
```
```    50 function
```
```    51   prod2nat :: "nat \<times> nat \<Rightarrow> nat"
```
```    52 where
```
```    53   "prod2nat (0, 0) = 0"
```
```    54 | "prod2nat (0, Suc n) = Suc (prod2nat (n, 0))"
```
```    55 | "prod2nat (Suc m, n) = Suc (prod2nat (m, Suc n))"
```
```    56 by pat_completeness auto
```
```    57
```
```    58 termination by (relation
```
```    59   "inv_image (measure id <*lex*> measure id) (\<lambda>(x, y). (x+y, x))") auto
```
```    60
```
```    61 primrec
```
```    62   nat2prod :: "nat \<Rightarrow> nat \<times> nat"
```
```    63 where
```
```    64   "nat2prod 0 = (0, 0)"
```
```    65 | "nat2prod (Suc x) =
```
```    66     (case nat2prod x of (m, n) \<Rightarrow>
```
```    67       (case n of 0 \<Rightarrow> (0, Suc m) | Suc n \<Rightarrow> (Suc m, n)))"
```
```    68
```
```    69 lemma nat2prod_prod2nat [simp]: "nat2prod (prod2nat x) = x"
```
```    70 by (induct x, rule prod2nat.induct, simp_all)
```
```    71
```
```    72 lemma prod2nat_nat2prod [simp]: "prod2nat (nat2prod n) = n"
```
```    73 by (induct n, auto split: prod.split nat.split)
```
```    74
```
```    75 lemma inj_prod2nat: "inj prod2nat"
```
```    76 by (rule inj_on_inverseI, rule nat2prod_prod2nat)
```
```    77
```
```    78 lemma prod2nat_eq_iff [simp]: "prod2nat x = prod2nat y \<longleftrightarrow> x = y"
```
```    79 by (rule inj_prod2nat [THEN inj_eq])
```
```    80
```
```    81 lemma inj_nat2prod: "inj nat2prod"
```
```    82 by (rule inj_on_inverseI, rule prod2nat_nat2prod)
```
```    83
```
```    84 lemma nat2prod_eq_iff [simp]: "nat2prod x = nat2prod y \<longleftrightarrow> x = y"
```
```    85 by (rule inj_nat2prod [THEN inj_eq])
```
```    86
```
```    87 subsubsection {* Ordering properties *}
```
```    88
```
```    89 lemma fst_snd_le_prod2nat: "fst x \<le> prod2nat x \<and> snd x \<le> prod2nat x"
```
```    90 by (induct x rule: prod2nat.induct) auto
```
```    91
```
```    92 lemma fst_le_prod2nat: "fst x \<le> prod2nat x"
```
```    93 by (rule fst_snd_le_prod2nat [THEN conjunct1])
```
```    94
```
```    95 lemma snd_le_prod2nat: "snd x \<le> prod2nat x"
```
```    96 by (rule fst_snd_le_prod2nat [THEN conjunct2])
```
```    97
```
```    98 lemma le_prod2nat_1: "a \<le> prod2nat (a, b)"
```
```    99 using fst_le_prod2nat [where x="(a, b)"] by simp
```
```   100
```
```   101 lemma le_prod2nat_2: "b \<le> prod2nat (a, b)"
```
```   102 using snd_le_prod2nat [where x="(a, b)"] by simp
```
```   103
```
```   104 declare prod2nat.simps [simp del]
```
```   105 declare nat2prod.simps [simp del]
```
```   106
```
```   107
```
```   108 subsection {* Isomorphism between naturals and finite sets of naturals *}
```
```   109
```
```   110 subsubsection {* Preliminaries *}
```
```   111
```
```   112 lemma finite_vimage_Suc_iff: "finite (Suc -` F) \<longleftrightarrow> finite F"
```
```   113 apply (safe intro!: finite_vimageI inj_Suc)
```
```   114 apply (rule finite_subset [where B="insert 0 (Suc ` Suc -` F)"])
```
```   115 apply (rule subsetI, case_tac x, simp, simp)
```
```   116 apply (rule finite_insert [THEN iffD2])
```
```   117 apply (erule finite_imageI)
```
```   118 done
```
```   119
```
```   120 lemma vimage_Suc_insert_0: "Suc -` insert 0 A = Suc -` A"
```
```   121 by auto
```
```   122
```
```   123 lemma vimage_Suc_insert_Suc:
```
```   124   "Suc -` insert (Suc n) A = insert n (Suc -` A)"
```
```   125 by auto
```
```   126
```
```   127 lemma even_nat_Suc_div_2: "even x \<Longrightarrow> Suc x div 2 = x div 2"
```
```   128 by (simp only: numeral_2_eq_2 even_nat_plus_one_div_two)
```
```   129
```
```   130 lemma div2_even_ext_nat:
```
```   131   "\<lbrakk>x div 2 = y div 2; even x = even y\<rbrakk> \<Longrightarrow> (x::nat) = y"
```
```   132 apply (rule mod_div_equality [of x 2, THEN subst])
```
```   133 apply (rule mod_div_equality [of y 2, THEN subst])
```
```   134 apply (case_tac "even x")
```
```   135 apply (simp add: numeral_2_eq_2 even_nat_equiv_def)
```
```   136 apply (simp add: numeral_2_eq_2 odd_nat_equiv_def)
```
```   137 done
```
```   138
```
```   139 subsubsection {* From sets to naturals *}
```
```   140
```
```   141 definition
```
```   142   set2nat :: "nat set \<Rightarrow> nat" where
```
```   143   "set2nat = setsum (op ^ 2)"
```
```   144
```
```   145 lemma set2nat_empty [simp]: "set2nat {} = 0"
```
```   146 by (simp add: set2nat_def)
```
```   147
```
```   148 lemma set2nat_insert [simp]:
```
```   149   "\<lbrakk>finite A; n \<notin> A\<rbrakk> \<Longrightarrow> set2nat (insert n A) = 2^n + set2nat A"
```
```   150 by (simp add: set2nat_def)
```
```   151
```
```   152 lemma even_set2nat_iff: "finite A \<Longrightarrow> even (set2nat A) = (0 \<notin> A)"
```
```   153 by (unfold set2nat_def, erule finite_induct, auto)
```
```   154
```
```   155 lemma set2nat_vimage_Suc: "set2nat (Suc -` A) = set2nat A div 2"
```
```   156 apply (case_tac "finite A")
```
```   157 apply (erule finite_induct, simp)
```
```   158 apply (case_tac x)
```
```   159 apply (simp add: even_nat_Suc_div_2 even_set2nat_iff vimage_Suc_insert_0)
```
```   160 apply (simp add: finite_vimageI add_commute vimage_Suc_insert_Suc)
```
```   161 apply (simp add: set2nat_def finite_vimage_Suc_iff)
```
```   162 done
```
```   163
```
```   164 lemmas set2nat_div_2 = set2nat_vimage_Suc [symmetric]
```
```   165
```
```   166 subsubsection {* From naturals to sets *}
```
```   167
```
```   168 definition
```
```   169   nat2set :: "nat \<Rightarrow> nat set" where
```
```   170   "nat2set x = {n. odd (x div 2 ^ n)}"
```
```   171
```
```   172 lemma nat2set_0 [simp]: "0 \<in> nat2set x \<longleftrightarrow> odd x"
```
```   173 by (simp add: nat2set_def)
```
```   174
```
```   175 lemma nat2set_Suc [simp]:
```
```   176   "Suc n \<in> nat2set x \<longleftrightarrow> n \<in> nat2set (x div 2)"
```
```   177 by (simp add: nat2set_def div_mult2_eq)
```
```   178
```
```   179 lemma nat2set_zero [simp]: "nat2set 0 = {}"
```
```   180 by (simp add: nat2set_def)
```
```   181
```
```   182 lemma nat2set_div_2: "nat2set (x div 2) = Suc -` nat2set x"
```
```   183 by auto
```
```   184
```
```   185 lemma nat2set_plus_power_2:
```
```   186   "n \<notin> nat2set z \<Longrightarrow> nat2set (2 ^ n + z) = insert n (nat2set z)"
```
```   187  apply (induct n arbitrary: z, simp_all)
```
```   188   apply (rule set_ext, induct_tac x, simp, simp add: even_nat_Suc_div_2)
```
```   189  apply (rule set_ext, induct_tac x, simp, simp add: add_commute)
```
```   190 done
```
```   191
```
```   192 lemma finite_nat2set [simp]: "finite (nat2set n)"
```
```   193 apply (induct n rule: nat_less_induct)
```
```   194 apply (case_tac "n = 0", simp)
```
```   195 apply (drule_tac x="n div 2" in spec, simp)
```
```   196 apply (simp add: nat2set_div_2)
```
```   197 apply (simp add: finite_vimage_Suc_iff)
```
```   198 done
```
```   199
```
```   200 subsubsection {* Proof of isomorphism *}
```
```   201
```
```   202 lemma set2nat_nat2set [simp]: "set2nat (nat2set n) = n"
```
```   203 apply (induct n rule: nat_less_induct)
```
```   204 apply (case_tac "n = 0", simp)
```
```   205 apply (drule_tac x="n div 2" in spec, simp)
```
```   206 apply (simp add: nat2set_div_2 set2nat_vimage_Suc)
```
```   207 apply (erule div2_even_ext_nat)
```
```   208 apply (simp add: even_set2nat_iff)
```
```   209 done
```
```   210
```
```   211 lemma nat2set_set2nat [simp]: "finite A \<Longrightarrow> nat2set (set2nat A) = A"
```
```   212 apply (erule finite_induct, simp_all)
```
```   213 apply (simp add: nat2set_plus_power_2)
```
```   214 done
```
```   215
```
```   216 lemma inj_nat2set: "inj nat2set"
```
```   217 by (rule inj_on_inverseI, rule set2nat_nat2set)
```
```   218
```
```   219 lemma nat2set_eq_iff [simp]: "nat2set x = nat2set y \<longleftrightarrow> x = y"
```
```   220 by (rule inj_eq [OF inj_nat2set])
```
```   221
```
```   222 lemma inj_on_set2nat: "inj_on set2nat (Collect finite)"
```
```   223 by (rule inj_on_inverseI [where g="nat2set"], simp)
```
```   224
```
```   225 lemma set2nat_eq_iff [simp]:
```
```   226   "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> set2nat A = set2nat B \<longleftrightarrow> A = B"
```
```   227 by (rule iffI, simp add: inj_onD [OF inj_on_set2nat], simp)
```
```   228
```
```   229 subsubsection {* Ordering properties *}
```
```   230
```
```   231 lemma nat_less_power2: "n < 2^n"
```
```   232 by (induct n) simp_all
```
```   233
```
```   234 lemma less_set2nat: "\<lbrakk>finite A; x \<in> A\<rbrakk> \<Longrightarrow> x < set2nat A"
```
```   235 unfolding set2nat_def
```
```   236 apply (rule order_less_le_trans [where y="setsum (op ^ 2) {x}"])
```
```   237 apply (simp add: nat_less_power2)
```
```   238 apply (erule setsum_mono2, simp, simp)
```
```   239 done
```
```   240
```
`   241 end`