equal
deleted
inserted
replaced
84 |
84 |
85 code_printing |
85 code_printing |
86 constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate" |
86 constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate" |
87 |
87 |
88 primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where |
88 primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where |
89 "sub' (as, n) = IArray.list_of as ! nat_of_integer n" |
89 [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n" |
90 hide_const (open) sub' |
90 hide_const (open) sub' |
|
91 |
|
92 lemma [code]: |
|
93 "IArray.sub' (IArray as, n) = as ! nat_of_integer n" |
|
94 by simp |
91 |
95 |
92 lemma [code]: |
96 lemma [code]: |
93 "as !! n = IArray.sub' (as, integer_of_nat n)" |
97 "as !! n = IArray.sub' (as, integer_of_nat n)" |
94 by simp |
98 by simp |
95 |
99 |
96 code_printing |
100 code_printing |
97 constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub" |
101 constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub" |
98 |
102 |
99 definition length' :: "'a iarray \<Rightarrow> integer" where |
103 definition length' :: "'a iarray \<Rightarrow> integer" where |
100 [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))" |
104 [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))" |
101 hide_const (open) length' |
105 hide_const (open) length' |
|
106 |
|
107 lemma [code]: |
|
108 "IArray.length' (IArray as) = integer_of_nat (List.length as)" |
|
109 by simp |
102 |
110 |
103 lemma [code]: |
111 lemma [code]: |
104 "IArray.length as = nat_of_integer (IArray.length' as)" |
112 "IArray.length as = nat_of_integer (IArray.length' as)" |
105 by simp |
113 by simp |
106 |
114 |