equal
deleted
inserted
replaced
211 by pat_completeness auto |
211 by pat_completeness auto |
212 |
212 |
213 termination list_decode |
213 termination list_decode |
214 apply (relation "measure id", simp_all) |
214 apply (relation "measure id", simp_all) |
215 apply (drule arg_cong [where f="prod_encode"]) |
215 apply (drule arg_cong [where f="prod_encode"]) |
|
216 apply (drule sym) |
216 apply (simp add: le_imp_less_Suc le_prod_encode_2) |
217 apply (simp add: le_imp_less_Suc le_prod_encode_2) |
217 done |
218 done |
218 |
219 |
219 lemma list_encode_inverse [simp]: "list_decode (list_encode x) = x" |
220 lemma list_encode_inverse [simp]: "list_decode (list_encode x) = x" |
220 by (induct x rule: list_encode.induct) simp_all |
221 by (induct x rule: list_encode.induct) simp_all |