author haftmann Fri, 30 May 2014 08:23:07 +0200 changeset 57117 a2eb1bdb9270 parent 57116 85e55ea7e06d child 57118 4760ac85b3f0
terminating code equations
```--- a/src/HOL/Library/IArray.thy	Thu May 29 22:46:21 2014 +0200
+++ b/src/HOL/Library/IArray.thy	Fri May 30 08:23:07 2014 +0200
@@ -86,10 +86,14 @@
constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"

primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
-"sub' (as, n) = IArray.list_of as ! nat_of_integer n"
+[code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
hide_const (open) sub'

lemma [code]:
+  "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
+  by simp
+
+lemma [code]:
"as !! n = IArray.sub' (as, integer_of_nat n)"
by simp

@@ -97,10 +101,14 @@
constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"

definition length' :: "'a iarray \<Rightarrow> integer" where
-[simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
+[code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
hide_const (open) length'

lemma [code]:
+  "IArray.length' (IArray as) = integer_of_nat (List.length as)"
+  by simp
+
+lemma [code]:
"IArray.length as = nat_of_integer (IArray.length' as)"
by simp
```