# HG changeset patch # User haftmann # Date 1531939877 -7200 # Node ID 90652333fae21244d2f6728661776091ffbbb41c # Parent 81639cc48d0a7c98d7f874b45087b2b8043ba040 taken over from AFP / Gauss_Jordan diff -r 81639cc48d0a -r 90652333fae2 src/HOL/Library/IArray.thy --- a/src/HOL/Library/IArray.thy Wed Jul 18 20:51:16 2018 +0200 +++ b/src/HOL/Library/IArray.thy Wed Jul 18 20:51:17 2018 +0200 @@ -40,6 +40,10 @@ "IArray.list_of as = map (\n. as !! n) [0 ..< IArray.length as]" by (cases as) (simp add: map_nth) +lemma of_fun_nth: +"IArray.of_fun f n !! i = f i" if "i < n" +using that by (simp add: map_nth) + end