# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267697796 -3600
# Node ID 95fb422bbb2bbb8c2501e39f0c011a8b45bdcd0f
# Parent  7ae031bd5d2f8ec40f8e5768afa14d259d29875f
A version that just leaves the supp/\supp goal. Obviously not true.

diff -r 7ae031bd5d2f -r 95fb422bbb2b Nominal/Fv.thy
--- a/Nominal/Fv.thy	Thu Mar 04 10:59:52 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 04 11:16:36 2010 +0100
@@ -184,8 +184,8 @@
               val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
               val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"})
             in
-              (*if length pi_supps > 1 then
-                HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen
+              if length pi_supps > 1 then
+                HOLogic.mk_conj (alpha_gen, pi_supps_eq) else alpha_gen
             (* TODO Add some test that is makes sense *)
             end else @{term "True"}
         end
diff -r 7ae031bd5d2f -r 95fb422bbb2b Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Mar 04 10:59:52 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 04 11:16:36 2010 +0100
@@ -71,20 +71,22 @@
 apply (simp_all add: weird_inj)
 apply (erule conjE)+
 apply (erule exE)+
+apply (erule conjE)+
+apply (erule exE)+
 apply (rule conjI)
 apply (rule_tac x="pica + pic" in exI)
 apply (erule alpha_gen_compose_trans)
 apply assumption
 apply (simp add: alpha_eqvt)
+apply (rule_tac x="pia + pib" in exI)
+apply (rule_tac x="piaa + piba" in exI)
+apply (rule conjI)
+apply (erule alpha_gen_compose_trans)
+apply assumption
+apply (simp add: alpha_eqvt)
 apply (rule conjI)
 defer
-apply (rule_tac x="pia + pi" in exI)
-apply (erule alpha_gen_compose_trans)
-apply assumption
-apply (simp add: alpha_eqvt)
-(* Normally: (pia + pb + (pib + pa)) *)
-apply (rule_tac x="piaa + pib" in exI)
-apply (rule_tac x="piab + piba" in exI)
+apply (rule_tac x="pid + pi" in exI)
 apply (erule alpha_gen_compose_trans)
 apply assumption
 apply (simp add: alpha_eqvt)