equal
deleted
inserted
replaced
396 |
396 |
397 lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)" |
397 lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)" |
398 apply(lifting test3) |
398 apply(lifting test3) |
399 done |
399 done |
400 |
400 |
|
401 lemma test4: "\<forall> (x :: 'a list, y, z) \<in> Respects( |
|
402 prod_rel (op \<approx>) (prod_rel (op \<approx>) (op \<approx>)) |
|
403 ). x = y \<and> y = z" |
|
404 sorry |
|
405 |
|
406 lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)" |
|
407 apply (lifting test4) |
|
408 sorry |
|
409 |
|
410 lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y, z) \<in> Respects( |
|
411 prod_rel (op \<approx> ===> op \<approx>) (prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>)) |
|
412 ). x = y \<and> y = z" |
|
413 sorry |
|
414 |
|
415 lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y, z). x = y \<and> y = z)" |
|
416 apply (lifting test5) |
|
417 sorry |
|
418 |
|
419 |
401 end |
420 end |