255 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ |
255 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ |
256 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\ |
256 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\ |
257 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ |
257 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ |
258 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\ |
258 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\ |
259 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\ |
259 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\ |
260 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\ |
260 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\ |
261 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\ |
261 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\ |
262 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\ |
262 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\ |
263 @{lemma "listsum [1,2,3::nat] = 6" by simp} |
263 @{lemma "listsum [1,2,3::nat] = 6" by simp} |
264 \end{tabular}} |
264 \end{tabular}} |
265 \caption{Characteristic examples} |
265 \caption{Characteristic examples} |
266 \label{fig:Characteristic} |
266 \label{fig:Characteristic} |
267 \end{figure} |
267 \end{figure} |