53 | constant IArray \<rightharpoonup> (SML) "Vector.fromList" |
53 | constant IArray \<rightharpoonup> (SML) "Vector.fromList" |
54 | constant IArray.all \<rightharpoonup> (SML) "Vector.all" |
54 | constant IArray.all \<rightharpoonup> (SML) "Vector.all" |
55 | constant IArray.exists \<rightharpoonup> (SML) "Vector.exists" |
55 | constant IArray.exists \<rightharpoonup> (SML) "Vector.exists" |
56 |
56 |
57 lemma [code]: |
57 lemma [code]: |
58 "size (as :: 'a iarray) = Suc (length (IArray.list_of as))" |
58 "size (as :: 'a iarray) = Suc (length (IArray.list_of as))" |
59 by (cases as) simp |
59 by (cases as) simp |
60 |
60 |
61 lemma [code]: |
61 lemma [code]: |
62 "size_iarray f as = Suc (size_list f (IArray.list_of as))" |
62 "size_iarray f as = Suc (size_list f (IArray.list_of as))" |
63 by (cases as) simp |
63 by (cases as) simp |
64 |
64 |
65 lemma [code]: |
65 lemma [code]: |
66 "rec_iarray f as = f (IArray.list_of as)" |
66 "rec_iarray f as = f (IArray.list_of as)" |
67 by (cases as) simp |
67 by (cases as) simp |
68 |
68 |
69 lemma [code]: |
69 lemma [code]: |
70 "case_iarray f as = f (IArray.list_of as)" |
70 "case_iarray f as = f (IArray.list_of as)" |
71 by (cases as) simp |
71 by (cases as) simp |
72 |
72 |
73 lemma [code]: |
73 lemma [code]: |
74 "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)" |
74 "set_iarray as = set (IArray.list_of as)" |
75 by (cases as, cases bs) (simp add: equal) |
75 by (case_tac as) auto |
|
76 |
|
77 lemma [code]: |
|
78 "map_iarray f as = IArray (map f (IArray.list_of as))" |
|
79 by (case_tac as) auto |
|
80 |
|
81 lemma [code]: |
|
82 "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)" |
|
83 by (case_tac as) (case_tac bs, auto) |
|
84 |
|
85 lemma [code]: |
|
86 "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)" |
|
87 by (cases as, cases bs) (simp add: equal) |
76 |
88 |
77 primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where |
89 primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where |
78 "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])" |
90 "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])" |
|
91 |
79 hide_const (open) tabulate |
92 hide_const (open) tabulate |
80 |
93 |
81 lemma [code]: |
94 lemma [code]: |
82 "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)" |
95 "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)" |
83 by simp |
96 by simp |
84 |
97 |
85 code_printing |
98 code_printing |
86 constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate" |
99 constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate" |
87 |
100 |
88 primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where |
101 primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where |
89 [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n" |
102 [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n" |
|
103 |
90 hide_const (open) sub' |
104 hide_const (open) sub' |
91 |
105 |
92 lemma [code]: |
106 lemma [code]: |
93 "IArray.sub' (IArray as, n) = as ! nat_of_integer n" |
107 "IArray.sub' (IArray as, n) = as ! nat_of_integer n" |
94 by simp |
108 by simp |
95 |
109 |
96 lemma [code]: |
110 lemma [code]: |
97 "as !! n = IArray.sub' (as, integer_of_nat n)" |
111 "as !! n = IArray.sub' (as, integer_of_nat n)" |
98 by simp |
112 by simp |
99 |
113 |
100 code_printing |
114 code_printing |
101 constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub" |
115 constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub" |
102 |
116 |
103 definition length' :: "'a iarray \<Rightarrow> integer" where |
117 definition length' :: "'a iarray \<Rightarrow> integer" where |
104 [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))" |
118 [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))" |
|
119 |
105 hide_const (open) length' |
120 hide_const (open) length' |
106 |
121 |
107 lemma [code]: |
122 lemma [code]: |
108 "IArray.length' (IArray as) = integer_of_nat (List.length as)" |
123 "IArray.length' (IArray as) = integer_of_nat (List.length as)" |
109 by simp |
124 by simp |
110 |
125 |
111 lemma [code]: |
126 lemma [code]: |
112 "IArray.length as = nat_of_integer (IArray.length' as)" |
127 "IArray.length as = nat_of_integer (IArray.length' as)" |
113 by simp |
128 by simp |
114 |
129 |
115 code_printing |
130 code_printing |
116 constant IArray.length' \<rightharpoonup> (SML) "Vector.length" |
131 constant IArray.length' \<rightharpoonup> (SML) "Vector.length" |
117 |
132 |
118 end |
133 end |