# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269280595 -3600
# Node ID 67936ae789972deeef846851f8759eb79bcd11c7
# Parent  ed54632fab4a7718e80e10ac2293b9f18ba5ad4d
sym proof with compose.

diff -r ed54632fab4a -r 67936ae78997 Nominal/Term5.thy
--- a/Nominal/Term5.thy	Mon Mar 22 18:38:59 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 22 18:56:35 2010 +0100
@@ -71,66 +71,21 @@
 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
-apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *})
-(*
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
-apply (simp_all add: alpha5_inj)
+apply (simp only: alpha5_inj)
+apply (simp add: alpha5_inj)
 apply (erule exE)
+apply (simp only: alpha5_inj)
 apply (rule_tac x="- pi" in exI)
-apply (simp add: alpha_gen)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-apply clarify
-apply (rule conjI)
-apply (rotate_tac 3)
-apply (frule_tac p="- pi" in alpha5_eqvt(2))
-apply simp
-apply (rule conjI)
-apply (rotate_tac 5)
-apply (frule_tac p="- pi" in alpha5_eqvt(1))
-apply simp
-apply (rotate_tac 6)
-apply simp
-apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1])
-apply (simp)*)
+apply (erule alpha_gen_compose_sym2)
+apply (simp_all add: alpha5_inj eqvts alpha5_eqvt)
 done
 
 lemma alpha5_transp:
 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and>
 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and>
 (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))"
-(*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*)
-apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
-apply (rule_tac [!] allI)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-defer
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
-apply (simp_all add: alpha5_inj)
-apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
-(* HERE *)
-apply (simp add: alpha_gen)
-apply clarify
-apply(simp add: fresh_star_plus)
-apply (rule conjI)
-apply (erule_tac x="- pi \<bullet> rltsaa" in allE)
-apply (rotate_tac 5)
-apply (drule_tac p="- pi" in alpha5_eqvt(2))
-apply simp
-apply (drule_tac p="pi" in alpha5_eqvt(2))
-apply simp
-apply (erule_tac x="- pi \<bullet> rtrm5aa" in allE)
-apply (rotate_tac 7)
-apply (drule_tac p="- pi" in alpha5_eqvt(1))
-apply simp
-apply (rotate_tac 3)
-apply (drule_tac p="pi" in alpha5_eqvt(1))
-apply simp
+apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})
 done
 
 lemma alpha5_equivp: