# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1324272025 -32400
# Node ID df1055004f5294fec08848fc565634913f090a4c
# Parent  2b1b8404fe0dee91a6f9fcb134adf52dc19b31fd
Disproved the property described as 'Tzevelakos'.

diff -r 2b1b8404fe0d -r df1055004f52 Nominal/Ex/Beta.thy
--- a/Nominal/Ex/Beta.thy	Sun Dec 18 00:42:32 2011 +0000
+++ b/Nominal/Ex/Beta.thy	Mon Dec 19 14:20:25 2011 +0900
@@ -401,7 +401,6 @@
   }
   ultimately show "supp x = A" by blast
 qed
-      
 
 lemma
   "(supp x) ssupp x"
@@ -415,6 +414,19 @@
 (*Tzevelekos 2008, section 2.1.2 property 2.5*)
 oops
 
+(* The above is not true. Take p=(a\<leftrightarrow>b) and x={a,b}, then the goal is provably false *)
+lemma
+  "b \<noteq> a \<Longrightarrow> \<not>(supp {a :: name,b}) ssupp {a,b}"
+unfolding ssupp_def
+apply (auto)
+apply (intro exI[of _ "(a\<leftrightarrow>b) :: perm"])
+apply (subgoal_tac "(a \<leftrightarrow> b) \<bullet> {a, b} = {a, b}")
+apply simp
+apply (subgoal_tac "supp {a, b} = {atom a, atom b}")
+apply (simp add: flip_def)
+apply (simp add: supp_of_finite_insert supp_at_base supp_set_empty)
+apply blast
+by (smt empty_eqvt flip_at_simps(1) flip_at_simps(2) insert_commute insert_eqvt)
 
 function
   qsubst :: "qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam"  ("_ [_ ::qq= _]" [90, 90, 90] 90)