# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268750294 -3600
# Node ID 0fae5608cd1ea8e5e15d5853e8d32356093061f8
# Parent  7c8cd6eae8e2c789b1ad46d3cbb2c962f816c641
alpha5_symp proved.

diff -r 7c8cd6eae8e2 -r 0fae5608cd1e Nominal/Term5.thy
--- a/Nominal/Term5.thy	Tue Mar 16 15:27:47 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 16 15:38:14 2010 +0100
@@ -48,12 +48,17 @@
   apply (simp_all add: eqvts atom_eqvt)
   done
 
-lemma alpha5_eqvt:
+(*lemma alpha5_eqvt:
   "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and>
   (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and>
   (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))"
 apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *})
-done
+done*)
+
+local_setup {*
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []),
+build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac  @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *}
+print_theorems
 
 lemma alpha5_reflp:
 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)"
@@ -69,7 +74,18 @@
 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)"
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
 apply (simp_all add: alpha5_inj)
-sorry
+apply (erule exE)
+apply (rule_tac x="- pi" in exI)
+apply clarify
+apply (erule alpha_gen_compose_sym)
+apply (simp add: alpha5_eqvt)
+apply(clarify)
+apply (rotate_tac 1)
+apply (frule_tac p="- pi" in alpha5_eqvt(1))
+apply simp
+done
+
+
 
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"