# HG changeset patch
# User haftmann
# Date 1204009197 -3600
# Node ID e453751350528d2ef6187530c7e8e58fd7a57139
# Parent  f7823a676ef735cf5811f44b549179a77feb5fc9
Zero/Suc recursion combinator for type index

diff -r f7823a676ef7 -r e45375135052 src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Tue Feb 26 07:59:56 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy	Tue Feb 26 07:59:57 2008 +0100
@@ -15,27 +15,17 @@
 
 subsection {* Datatype of indices *}
 
-datatype index = index_of_nat nat
-
-lemma [code func]:
-  "index_size k = 0"
-  by (cases k) simp
-
-lemmas [code func del] = index.recs index.cases
+typedef index = "UNIV \<Colon> nat set"
+  morphisms nat_of_index index_of_nat by rule
 
-primrec
-  nat_of_index :: "index \<Rightarrow> nat"
-where
-  "nat_of_index (index_of_nat k) = k"
-lemmas [code func del] = nat_of_index.simps
+lemma index_of_nat_nat_of_index [simp]:
+  "index_of_nat (nat_of_index k) = k"
+  by (rule nat_of_index_inverse)
 
-lemma index_id [simp]:
-  "index_of_nat (nat_of_index n) = n"
-  by (cases n) simp_all
-
-lemma nat_of_index_inject [simp]:
-  "nat_of_index n = nat_of_index m \<longleftrightarrow> n = m"
-  by (cases n) auto
+lemma nat_of_index_index_of_nat [simp]:
+  "nat_of_index (index_of_nat n) = n"
+  by (rule index_of_nat_inverse) 
+    (unfold index_def, rule UNIV_I)
 
 lemma index:
   "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"
@@ -50,8 +40,91 @@
   then show "PROP P n" by simp
 qed
 
-lemma [code func]: "size (n\<Colon>index) = 0"
-  by (cases n) simp_all
+lemma index_case:
+  assumes "\<And>n. k = index_of_nat n \<Longrightarrow> P"
+  shows P
+  by (rule assms [of "nat_of_index k"]) simp
+
+lemma index_induct:
+  assumes "\<And>n. P (index_of_nat n)"
+  shows "P k"
+proof -
+  from assms have "P (index_of_nat (nat_of_index k))" .
+  then show ?thesis by simp
+qed
+
+lemma nat_of_index_inject [simp]:
+  "nat_of_index k = nat_of_index l \<longleftrightarrow> k = l"
+  by (rule nat_of_index_inject)
+
+lemma index_of_nat_inject [simp]:
+  "index_of_nat n = index_of_nat m \<longleftrightarrow> n = m"
+  by (auto intro!: index_of_nat_inject simp add: index_def)
+
+instantiation index :: zero
+begin
+
+definition [simp, code func del]:
+  "0 = index_of_nat 0"
+
+instance ..
+
+end
+
+definition [simp]:
+  "Suc_index k = index_of_nat (Suc (nat_of_index k))"
+
+lemma index_induct: "P 0 \<Longrightarrow> (\<And>k. P k \<Longrightarrow> P (Suc_index k)) \<Longrightarrow> P k"
+proof -
+  assume "P 0" then have init: "P (index_of_nat 0)" by simp
+  assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
+    then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat (n)))" .
+    then have step: "\<And>n. P (index_of_nat n) \<Longrightarrow> P (index_of_nat (Suc n))" by simp
+  from init step have "P (index_of_nat (nat_of_index k))"
+    by (induct "nat_of_index k") simp_all
+  then show "P k" by simp
+qed
+
+lemma Suc_not_Zero_index: "Suc_index k \<noteq> 0"
+  by simp
+
+lemma Zero_not_Suc_index: "0 \<noteq> Suc_index k"
+  by simp
+
+lemma Suc_Suc_index_eq: "Suc_index k = Suc_index l \<longleftrightarrow> k = l"
+  by simp
+
+rep_datatype index
+  distinct  Suc_not_Zero_index Zero_not_Suc_index
+  inject    Suc_Suc_index_eq
+  induction index_induct
+
+lemmas [code func del] = index.recs index.cases
+
+declare index_case [case_names nat, cases type: index]
+declare index_induct [case_names nat, induct type: index]
+
+lemma [code func]:
+  "index_size = nat_of_index"
+proof (rule ext)
+  fix k
+  have "index_size k = nat_size (nat_of_index k)"
+    by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
+  also have "nat_size (nat_of_index k) = nat_of_index k" by (induct "nat_of_index k") simp_all
+  finally show "index_size k = nat_of_index k" .
+qed
+
+lemma [code func]:
+  "size = nat_of_index"
+proof (rule ext)
+  fix k
+  show "size k = nat_of_index k"
+  by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
+qed
+
+lemma [code func]:
+  "k = l \<longleftrightarrow> nat_of_index k = nat_of_index l"
+  by (cases k, cases l) simp
 
 
 subsection {* Indices as datatype of ints *}
@@ -74,9 +147,6 @@
 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
 begin
 
-definition [simp, code func del]:
-  "(0\<Colon>index) = index_of_nat 0"
-
 lemma zero_index_code [code inline, code func]:
   "(0\<Colon>index) = Numeral0"
   by (simp add: number_of_index_def Pls_def)
@@ -141,6 +211,8 @@
 
 end
 
+lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
+
 lemma index_of_nat_code [code]:
   "index_of_nat = of_nat"
 proof