taken over from AFP / Gauss_Jordan
authorhaftmann
Wed Jul 18 20:51:17 2018 +0200 (11 months ago)
changeset 6865590652333fae2
parent 68654 81639cc48d0a
child 68656 297ca38c7da5
taken over from AFP / Gauss_Jordan
src/HOL/Library/IArray.thy
     1.1 --- a/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:16 2018 +0200
     1.2 +++ b/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:17 2018 +0200
     1.3 @@ -40,6 +40,10 @@
     1.4  "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
     1.5  by (cases as) (simp add: map_nth)
     1.6  
     1.7 +lemma of_fun_nth:
     1.8 +"IArray.of_fun f n !! i = f i" if "i < n"
     1.9 +using that by (simp add: map_nth)
    1.10 +
    1.11  end
    1.12  
    1.13