# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268737717 -3600
# Node ID 49bdb8d475df5727fa3e62dc136aaf9c444a0208
# Parent  31f000d586bbe99f07125fd0d225a3637644e7df
The proof in 'Test' gets simpler.

diff -r 31f000d586bb -r 49bdb8d475df Nominal/Term5.thy
--- a/Nominal/Term5.thy	Tue Mar 16 12:06:22 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 16 12:08:37 2010 +0100
@@ -57,16 +57,20 @@
 lemma alpha5_reflp:
 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)"
 apply (rule rtrm5_rlts.induct)
+thm rtrm5_rlts.induct
+ alpha_rtrm5_alpha_rlts_alpha_rbv5.induct
 apply (simp_all add: alpha5_inj)
 apply (rule_tac x="0::perm" in exI)
 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)
 done
 
 lemma alpha5_symp:
-"(a \<approx>5 b \<longrightarrow> a \<approx>5 b) \<and>
+"(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)"
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct
+thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
 apply (simp_all add: alpha5_inj)
 sorry
 
diff -r 31f000d586bb -r 49bdb8d475df Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 16 12:06:22 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 16 12:08:37 2010 +0100
@@ -129,16 +129,9 @@
 apply(simp only: alpha_tst) 
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
-defer (* hacking *)
+apply simp
 apply(simp add: supp_Abs_tst)
 apply(simp add: fv_bi)
-apply(rule Collect_cong)
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-apply(simp)
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-apply(simp)
-apply(rule Collect_cong)
-apply(blast)
 done
 
 text {* example 2 *}