# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260306214 -3600
# Node ID 10d04ee5210184be07a5567d3d627e2fdf1c7fca
# Parent  97a397ba57437df184ae3a63f19464eff5551745
An example which is hard to lift because of the interplay between lambda_prs and unfolding.

diff -r 97a397ba5743 -r 10d04ee52101 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 20:55:55 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 22:03:34 2009 +0100
@@ -444,4 +444,22 @@
 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
 sorry
 
+lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
+sorry
+
+lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
+apply(lifting_setup hard)
+defer
+apply(injection)
+apply(subst babs_prs)
+defer defer
+apply(subst babs_prs)
+defer defer
+apply(subst babs_prs)
+defer defer
+apply(subst babs_prs)
+defer defer
+apply(tactic {* lambda_prs_tac @{context} 1 *})
+(* Until here is ok *)
+apply(cleaning)
 end