# HG changeset patch
# User haftmann
# Date 1236163445 -3600
# Node ID e67f42ac11570e832dd185e1797b6cf3e1f413f9
# Parent  48543b307e99a2496b9ae5e7e7bfd64f162c5235
consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun

diff -r 48543b307e99 -r e67f42ac1157 src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Wed Mar 04 11:37:50 2009 +0100
+++ b/src/HOL/Library/Code_Index.thy	Wed Mar 04 11:44:05 2009 +0100
@@ -87,12 +87,14 @@
   then show "P k" by simp
 qed simp_all
 
-lemmas [code 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]:
+lemma index_decr [termination_simp]:
+  "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
+  by (cases k) simp
+
+lemma [simp, code]:
   "index_size = nat_of"
 proof (rule ext)
   fix k
@@ -102,7 +104,7 @@
   finally show "index_size k = nat_of k" .
 qed
 
-lemma [code]:
+lemma [simp, code]:
   "size = nat_of"
 proof (rule ext)
   fix k
@@ -110,6 +112,8 @@
   by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
 qed
 
+lemmas [code del] = index.recs index.cases
+
 lemma [code]:
   "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
   by (cases k, cases l) (simp add: eq)