equal
deleted
inserted
replaced
407 apply (lifting test4) |
407 apply (lifting test4) |
408 sorry |
408 sorry |
409 |
409 |
410 lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y) \<in> Respects( |
410 lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y) \<in> Respects( |
411 prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>) |
411 prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>) |
412 ). x = y" |
412 ). (op \<approx> ===> op \<approx>) x y" |
413 sorry |
413 sorry |
414 |
414 |
415 lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y). x = y)" |
415 lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y). x = y)" |
416 apply (lifting test5) |
416 apply (lifting test5) |
417 sorry |
417 done |
418 |
418 |
|
419 lemma test6: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y, z) \<in> Respects( |
|
420 prod_rel (op \<approx> ===> op \<approx>) (prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>)) |
|
421 ). (op \<approx> ===> op \<approx>) x y \<and> (op \<approx> ===> op \<approx>) y z" |
|
422 sorry |
|
423 |
|
424 lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y, z). x = y \<and> y = z)" |
|
425 apply (lifting test6) |
|
426 done |
419 |
427 |
420 end |
428 end |