equal
deleted
inserted
replaced
141 lemma one_index_code [code inline, code func]: |
141 lemma one_index_code [code inline, code func]: |
142 "(1\<Colon>index) = Numeral1" |
142 "(1\<Colon>index) = Numeral1" |
143 by simp |
143 by simp |
144 |
144 |
145 instance index :: abs |
145 instance index :: abs |
146 "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" .. |
146 "\<bar>k\<Colon>index\<bar> \<equiv> if k < 0 then -k else k" .. |
147 |
147 |
148 lemma index_of_int [code func]: |
148 lemma index_of_int [code func]: |
149 "index_of_int k = (if k = 0 then 0 |
149 "index_of_int k = (if k = 0 then 0 |
150 else if k = -1 then -1 |
150 else if k = -1 then -1 |
151 else let (l, m) = divAlg (k, 2) in 2 * index_of_int l + |
151 else let (l, m) = divAlg (k, 2) in 2 * index_of_int l + |