# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1282875940 0
# Node ID fc3e8f79e698c98d25f303c804738ebc64edc74c
# Parent  0a36825b16c166a988b0e0f0538eb4e899b5013f
Ball Bex can be lifted after unfolding.

diff -r 0a36825b16c1 -r fc3e8f79e698 Attic/Quot/Examples/FSet_BallBex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Quot/Examples/FSet_BallBex.thy	Fri Aug 27 02:25:40 2010 +0000
@@ -0,0 +1,40 @@
+theory FSet_ballbex
+imports "../../../Nominal/FSet"
+begin
+
+notation
+  list_eq (infix "\<approx>" 50)
+
+lemma test:
+  "\<forall>xs \<in> (\<lambda>xs. memb x xs). memb x (y # xs)"
+  apply (simp add: memb_def)
+  apply (metis mem_def)
+  done
+
+(* Should not work and doesn't.
+thm test[quot_lifted]
+*)
+
+lemma "\<forall>xs \<in> (\<lambda>xs. x |\<in>| xs). x |\<in>| finsert y xs"
+  unfolding Ball_def mem_def
+  by (lifting test[unfolded Ball_def mem_def])
+
+ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def mem_def} @{thm test}*}
+
+lemma test2:
+  "\<exists>xs \<in> (\<lambda>xs. xs \<approx> []). xs \<approx> []"
+  apply (rule_tac x="[]" in bexI)
+  apply (auto simp add: mem_def)
+  done
+
+(* Should not work and doesn't
+thm test2[quot_lifted]
+*)
+
+lemma "\<exists>xs \<in> (\<lambda>xs. xs = {||}). xs = {||}"
+  unfolding Bex_def mem_def
+  by (lifting test2[unfolded Bex_def mem_def])
+
+ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def mem_def} @{thm test2}*}
+
+end