equal
deleted
inserted
replaced
375 apply(drule fun_cong) |
375 apply(drule fun_cong) |
376 apply(drule fun_cong) |
376 apply(drule fun_cong) |
377 apply(assumption) |
377 apply(assumption) |
378 done |
378 done |
379 |
379 |
380 lemma [quot_respect]: |
|
381 "((op \<approx> ===> op \<approx> ===> op =) ===> prod_rel op \<approx> op \<approx> ===> op =) split split" |
|
382 apply(simp) |
|
383 done |
|
384 |
|
385 thm quot_preserve |
|
386 term split |
|
387 |
|
388 |
|
389 lemma [quot_preserve]: |
|
390 shows "(((abs_fset ---> abs_fset ---> id) ---> prod_fun rep_fset rep_fset ---> id) split) = split" |
|
391 apply(simp add: expand_fun_eq) |
|
392 apply(simp add: Quotient_abs_rep[OF Quotient_fset]) |
|
393 done |
|
394 |
|
395 |
|
396 lemma test: "All (\<lambda>(x::'a list, y). x = y)" |
380 lemma test: "All (\<lambda>(x::'a list, y). x = y)" |
397 sorry |
381 sorry |
398 |
382 |
399 lemma "All (\<lambda>(x::'a fset, y). x = y)" |
383 lemma "All (\<lambda>(x::'a fset, y). x = y)" |
400 apply(lifting test) |
384 apply(lifting test) |