--- a/Nominal/Fv.thy	Wed Mar 03 17:51:47 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 04 10:59:52 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

--- a/Nominal/Test.thy	Wed Mar 03 17:51:47 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 04 10:59:52 2010 +0100
@@ -46,9 +46,7 @@
   )
 *}
 
-
-prove {* (snd o snd) (build_alpha_refl_gl [@{term alpha_weird_raw}] ("x","y","z")) *}
-ML_prf {*
+ML {*
 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
   ind_tac induct THEN_ALL_NEW
   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
@@ -56,23 +54,62 @@
   split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt)
   THEN_ALL_NEW split_conjs
 *}
+(*apply (tactic {* transp_tac @{context} @{thm alpha_weird_raw.induct} @{thms weird_inj}  @{thms weird_raw.inject} @{thms weird_raw.distinct} @{thms alpha_weird_raw.cases} @{thms alpha_eqvt} 1 *})*)
 
-apply (tactic {* transp_tac @{context} @{thm alpha_weird_raw.induct} @{thms weird_inj}  @{thms weird_raw.inject} @{thms weird_raw.distinct} @{thms alpha_weird_raw.cases} @{thms alpha_eqvt} 1 *})
-apply (simp_all)
+lemma "alpha_weird_raw x y \<longrightarrow> (\<forall>z. alpha_weird_raw y z \<longrightarrow> alpha_weird_raw x z)"
+apply (rule impI)
+apply (erule alpha_weird_raw.induct)
+apply (simp_all add: weird_inj)
+defer
+apply (rule allI)
+apply (rule impI)
+apply (erule alpha_weird_raw.cases)
+apply (simp_all add: weird_inj)
+apply (rule allI)
+apply (rule impI)
+apply (erule alpha_weird_raw.cases)
+apply (simp_all add: weird_inj)
+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 conjI)
+defer
+apply (rule_tac x="pia + pi" in exI)
 apply (erule alpha_gen_compose_trans)
 apply assumption
 apply (simp add: alpha_eqvt)
-defer defer
+(* Normally: (pia + pb + (pib + pa)) *)
+apply (rule_tac x="piaa + pib" in exI)
+apply (rule_tac x="piab + piba" in exI)
 apply (erule alpha_gen_compose_trans)
 apply assumption
 apply (simp add: alpha_eqvt)
-apply (subgoal_tac "pia + pb + (pib + pa) = (pia + pib) + (pb + pa)")
-apply simp
-apply (erule alpha_gen_compose_trans)
-apply assumption
-apply (simp add: alpha_eqvt)
-sorry
+done
 
+lemma "alpha_weird_raw x y \<Longrightarrow> alpha_weird_raw y x"
+apply (erule alpha_weird_raw.induct)
+apply (simp_all add: weird_inj)
+apply (erule conjE)+
+apply (erule exE)+
+apply (rule conjI)
+defer (* simple *)
+apply (rule conjI)
+apply (rule_tac x="- pia" in exI)
+apply (rule_tac x="- pib" in exI)
+apply (simp add: minus_add[symmetric])
+apply (erule alpha_gen_compose_sym)
+apply (simp_all add: alpha_eqvt)
+apply (rule_tac x="- pi" in exI)
+apply (erule alpha_gen_compose_sym)
+apply (simp_all add: alpha_eqvt)
+apply (rule_tac x="- pic" in exI)
+apply (erule alpha_gen_compose_sym)
+apply (simp_all add: alpha_eqvt)
+done
 
 
 abbreviation "WBind \<equiv> WBind_raw"