--- a/Nominal/Term5.thy	Tue Mar 16 18:19:00 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 16 20:07:13 2010 +0100
@@ -43,7 +43,6 @@
 lemma fv_rtrm5_rlts_eqvt[eqvt]:
   "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
   "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
-  "pi \<bullet> (fv_rbv5 l) = fv_rbv5 (pi \<bullet> l)"
   apply (induct x and l)
   apply (simp_all add: eqvts atom_eqvt)
   done
@@ -134,7 +133,6 @@
  |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
  |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_bv5", @{term fv_rbv5}))
  |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))
  |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5})))
 *}
@@ -142,14 +140,14 @@
 
 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 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)"
+  "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
+  "(alpha_rbv5 b c \<Longrightarrow> True)"
   apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
   apply(simp_all add: eqvts)
   apply(simp add: alpha_gen)
   apply(clarify)
   apply(simp)
-  sorry
+done
 
 lemma bv_list_rsp:
   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
@@ -159,9 +157,38 @@
   apply simp
   done
 
+local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
+print_theorems
+
+
+lemma alpha_rbv_rsp_pre:
+  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 x z = alpha_rbv5 y z"
+  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply (case_tac [!] z)
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply auto
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
+
+lemma alpha_rbv_rsp_pre2:
+  "x \<approx>l y \<Longrightarrow> \<forall>z. alpha_rbv5 z x = alpha_rbv5 z y"
+  apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply (case_tac [!] z)
+  apply (simp_all add: alpha_dis alpha5_inj)
+  apply clarify
+  apply auto
+  apply (meson alpha5_symp alpha5_transp)
+  apply (meson alpha5_symp alpha5_transp)
+  done
+
 lemma [quot_respect]:
   "(alpha_rlts ===> op =) fv_rlts fv_rlts"
-  "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5"
   "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
   "(alpha_rlts ===> op =) rbv5 rbv5"
   "(op = ===> alpha_rtrm5) rVr5 rVr5"
@@ -176,15 +203,9 @@
   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
-  apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
-  apply simp_all
-  defer defer (* Both sides false, so equal when we have distinct *)
-  apply (erule conjE)+
-  apply clarify
-  apply (simp add: alpha5_inj)
-  sorry (* may be true? *)
+  apply (simp add: alpha_rbv_rsp_pre2)
+  apply (simp add: alpha_rbv_rsp_pre)
+done
 
 lemma
   shows "(alpha_rlts ===> op =) rbv5 rbv5"
@@ -212,9 +233,9 @@
 
 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
 lemmas bv5[simp] = rbv5.simps[quot_lifted]
-lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted]
-lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted]
+lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas alpha5_DIS = alpha_dis[quot_lifted]
 
 lemma lets_bla:
   "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))"
@@ -235,7 +256,6 @@
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
-apply (metis flip_at_simps(1) supp_at_base supp_eqvt)
 done
 
 lemma lets_ok3:
@@ -252,27 +272,15 @@
    (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 apply (simp add: alpha5_INJ alpha_gen)
 apply (simp add: permute_trm5_lts eqvts)
-apply (simp add: alpha5_INJ(5))
-apply (simp add: alpha5_INJ(1))
+apply (simp add: alpha5_INJ)
 done
 
-lemma distinct_helper:
-  shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
-  apply auto
-  apply (erule alpha_rtrm5.cases)
-  apply (simp_all only: rtrm5.distinct)
-  done
-
-lemma distinct_helper2:
-  shows "(Vr5 x) \<noteq> (Ap5 y z)"
-  by (lifting distinct_helper)
-
 lemma lets_nok:
   "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
    (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
    (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
-apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts)
+apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts)
 done
 
 end