equal
deleted
inserted
replaced
371 |
371 |
372 lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))" |
372 lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))" |
373 apply (lifting ttt) |
373 apply (lifting ttt) |
374 done |
374 done |
375 |
375 |
|
376 |
376 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))" |
377 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))" |
377 sorry |
378 sorry |
378 |
379 |
379 (* PROBLEM *) |
|
380 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))" |
380 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))" |
381 apply(lifting ttt2) |
381 apply(lifting ttt2) |
382 apply(regularize) |
382 apply(regularize) |
383 apply(rule impI) |
383 apply(rule impI) |
384 apply(simp) |
384 apply(simp) |
387 done |
387 done |
388 |
388 |
389 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))" |
390 sorry |
390 sorry |
391 |
391 |
|
392 |
392 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
393 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
393 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
394 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
394 sorry |
395 sorry |
395 |
396 |
396 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
397 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))" |
397 sorry |
398 sorry |
398 |
399 |
399 (* PROBLEM *) |
|
400 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)))" |
401 apply(lifting hard) |
401 apply(lifting hard) |
|
402 apply(regularize) |
|
403 apply(auto) |
402 sorry |
404 sorry |
403 |
405 |
404 end |
406 end |