--- a/Nominal/Term5.thy	Tue Mar 16 17:20:46 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 16 18:18:08 2010 +0100
@@ -61,7 +61,7 @@
 print_theorems
 
 lemma alpha5_reflp:
-"y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)"
+"y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 x x)"
 apply (rule rtrm5_rlts.induct)
 apply (simp_all add: alpha5_inj)
 apply (rule_tac x="0::perm" in exI)
@@ -71,25 +71,21 @@
 lemma alpha5_symp:
 "(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)"
+(alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
 apply (simp_all add: alpha5_inj)
 apply (erule exE)
 apply (rule_tac x="- pi" in exI)
 apply clarify
-apply (erule alpha_gen_compose_sym)
-apply (simp add: alpha5_eqvt)
-(* Works for non-recursive, proof is done here *)
-apply(clarify)
-apply (rotate_tac 1)
-apply (frule_tac p="- pi" in alpha5_eqvt(1))
-apply simp
+apply (rule conjI)
+apply (erule_tac [!] alpha_gen_compose_sym)
+apply (simp_all add: 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 p k l \<longrightarrow> (\<forall>m q. alpha_rbv5 q l m \<longrightarrow> alpha_rbv5 (q + p) k m))"
+(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)
@@ -101,27 +97,17 @@
 apply (simp_all add: alpha5_inj)
 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
 apply clarify
-apply simp
+apply (rule conjI)
+apply (erule alpha_gen_compose_trans)
+apply (assumption)
+apply (simp add: alpha5_eqvt)
 apply (erule alpha_gen_compose_trans)
 apply (assumption)
 apply (simp add: alpha5_eqvt)
 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
 apply (simp_all add: alpha5_inj)
-apply (rule 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 (rule allI)
 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
 apply (simp_all add: alpha5_inj)
-(* Works for non-recursive, proof is done here *)
-apply clarify
-apply (rotate_tac 1)
-apply (frule_tac p="- pia" in alpha5_eqvt(1))
-apply (erule_tac x="- pia \<bullet> rtrm5aa" in allE)
-apply simp
-apply (rotate_tac -1)
-apply (frule_tac p="pia" in alpha5_eqvt(1))
-apply simp
 done
 
 lemma alpha5_equivp:
@@ -157,10 +143,9 @@
 lemma alpha5_rfv:
   "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
   "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))"
-  "(alpha_rbv5 p b c \<Longrightarrow> fv_rbv5 (p \<bullet> b) = fv_rbv5 c)"
+  "(alpha_rbv5 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)"
   apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
   apply(simp_all add: eqvts)
-  thm alpha5_inj
   apply(simp add: alpha_gen)
   apply(clarify)
   apply(simp)
@@ -185,13 +170,11 @@
   "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"
   "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
   "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
-  "(op = ===> alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5"
+  "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5"
   apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
   apply (clarify)
-  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
-  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply (simp_all add: alpha5_inj)
-  apply clarify
+  apply (rule_tac x="0" in exI)
+  apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
   apply clarify
   apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
   apply simp_all
@@ -234,14 +217,16 @@
 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemma lets_bla:
-  "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
+  "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
 apply (simp only: alpha5_INJ)
 apply (simp only: bv5)
 apply simp
-apply (rule_tac x="(z \<leftrightarrow> y)" in exI)
+apply (rule allI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts)
-done
+apply (rule impI)
+apply (rule impI)
+sorry (* The assumption is false, so it is true *)
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
@@ -262,12 +247,13 @@
 
 
 lemma lets_not_ok1:
-  "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
+  "x \<noteq> y \<Longrightarrow>
+   (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
    (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 apply (simp add: alpha5_INJ alpha_gen)
-apply (rule_tac x="0::perm" in exI)
-apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts)
-apply auto
+apply (simp add: permute_trm5_lts eqvts)
+apply (simp add: alpha5_INJ(5))
+apply (simp add: alpha5_INJ(1))
 done
 
 lemma distinct_helper: