equal
deleted
inserted
replaced
232 (* PROBLEM: these lemmas needs to be restated, since *) |
232 (* PROBLEM: these lemmas needs to be restated, since *) |
233 (* concat.simps(1) and concat.simps(2) contain the *) |
233 (* concat.simps(1) and concat.simps(2) contain the *) |
234 (* type variables ?'a1.0 (which are turned into frees *) |
234 (* type variables ?'a1.0 (which are turned into frees *) |
235 (* 'a_1 *) |
235 (* 'a_1 *) |
236 lemma concat1: |
236 lemma concat1: |
237 shows "concat [] = []" |
237 shows "concat [] \<approx> []" |
238 by (simp) |
238 by (simp) |
239 |
239 |
240 lemma concat2: |
240 lemma concat2: |
241 shows "concat (x # xs) = x @ concat xs" |
241 shows "concat (x # xs) \<approx> x @ concat xs" |
242 by (simp) |
242 by (simp) |
243 |
243 |
244 lemma fconcat_empty: |
244 lemma fconcat_empty: |
245 shows "fconcat {||} = {||}" |
245 shows "fconcat {||} = {||}" |
246 apply(lifting concat1) |
246 apply(lifting_setup concat1) |
|
247 apply(regularize) |
247 apply(injection) |
248 apply(injection) |
248 defer |
249 defer |
249 apply(cleaning) |
250 apply(cleaning) |
250 apply(simp add: comp_def) |
251 apply(simp add: comp_def) |
251 apply(cleaning) |
252 apply(cleaning) |