equal
deleted
inserted
replaced
382 apply(regularize) |
382 apply(regularize) |
383 apply(rule impI) |
383 apply(rule impI) |
384 apply(simp) |
384 apply(simp) |
385 apply(rule allI) |
385 apply(rule allI) |
386 apply(rule list_eq_refl) |
386 apply(rule list_eq_refl) |
387 apply(cleaning) |
|
388 apply(simp add: fun_map.simps expand_fun_eq) |
|
389 apply(cleaning) |
|
390 done |
387 done |
391 |
388 |
392 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
389 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
393 sorry |
390 sorry |
394 |
391 |
395 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
392 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
396 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
393 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
397 sorry |
394 sorry |
398 |
395 |
399 (* Always safe to apply, but not too helpful *) |
|
400 lemma app_prs2: |
|
401 assumes q1: "Quotient R1 abs1 rep1" |
|
402 and q2: "Quotient R2 abs2 rep2" |
|
403 shows "((abs1 ---> rep2) ((rep1 ---> abs2) f) (rep1 x)) = rep2 (((rep1 ---> abs2) f) x)" |
|
404 unfolding expand_fun_eq |
|
405 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
|
406 by simp |
|
407 |
|
408 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
396 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
409 sorry |
397 sorry |
410 |
398 |
411 (* PROBLEM *) |
399 (* PROBLEM *) |
412 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
400 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))" |
413 apply(lifting_setup hard) |
401 apply(lifting hard) |
414 defer |
|
415 apply(injection) |
|
416 apply(cleaning) |
|
417 sorry |
402 sorry |
418 |
403 |
419 end |
404 end |