# HG changeset patch
# User haftmann
# Date 1401430987 -7200
# Node ID a2eb1bdb9270ef1991898ac2217e125f4fb7fc28
# Parent  85e55ea7e06da111b1b298b5d1ea6d3b5b9c6a91
terminating code equations

diff -r 85e55ea7e06d -r a2eb1bdb9270 src/HOL/Library/IArray.thy
--- 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