--- a/Nominal/Term5.thy	Wed Mar 10 11:19:59 2010 +0100
+++ b/Nominal/Term5.thy	Wed Mar 10 11:39:28 2010 +0100
@@ -22,26 +22,16 @@
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *}
 print_theorems
 
-
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") [
-  [ [],
-    [],
-    [(SOME @{term rbv5}, 0, 1)] ],
-  [ [],
-    []]  ] *}
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5")
+  [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
 print_theorems
 
-(* Alternate version with additional binding of name in rlts in rLcons *)
-(*local_setup {* snd o define_fv_alpha "Term5.rtrm5" [
-  [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]]  ] *}
-print_theorems*)
-
 notation
   alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
   alpha_rlts ("_ \<approx>l _" [100, 100] 100)
-thm alpha_rtrm5_alpha_rlts.intros
+thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
 thm alpha5_inj
 
 lemma rbv5_eqvt[eqvt]:
@@ -60,8 +50,15 @@
 lemma alpha5_eqvt:
   "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
   "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
-  apply (induct rule: alpha_rtrm5_alpha_rlts.inducts)
-  apply (simp_all add: alpha5_inj)
+  "alpha_rbv5 a b c \<Longrightarrow> True"
+apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
+apply (simp_all add: alpha5_inj)
+apply (erule exE)
+apply (rule_tac x="pi" in exI)
+apply clarify
+apply (simp add: alpha_gen fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric])
+apply (subst eqvts[symmetric])
+apply (subst eqvts[symmetric])
 sorry
 
 lemma alpha5_equivp:
@@ -84,25 +81,25 @@
  |> 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 ("bv5", @{term rbv5})))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5})))
 *}
 print_theorems
 
 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)"
-  apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
+  "(t \<approx>5 s \<longrightarrow> fv_rtrm5 t = fv_rtrm5 s) \<and> (l \<approx>l m \<longrightarrow> fv_rlts l = fv_rlts m) \<and> (alpha_rbv5 a b c \<longrightarrow> True)"
+  apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
   apply(simp_all)
   apply(simp add: alpha_gen)
   apply(erule conjE)+
   apply(erule exE)
   apply(erule conjE)+
   apply(simp_all)
-  done
+  sorry
 
 lemma bv_list_rsp:
   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
-  apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2))
+  apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))
   apply(simp_all)
   apply(clarify)
   apply simp
@@ -118,11 +115,22 @@
   "(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"
   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)
-  done
-
+  defer
+  apply clarify
+  apply (erule alpha_rlts.cases)
+  apply (erule alpha_rlts.cases)
+  apply (simp_all)
+  defer
+  apply (erule alpha_rlts.cases)
+  apply (simp_all)
+  defer
+  apply clarify
+  apply (simp add: alpha5_inj)
+  sorry (* may be true? *)
 lemma
   shows "(alpha_rlts ===> op =) rbv5 rbv5"
   by (simp add: bv_list_rsp)
@@ -147,11 +155,10 @@
 
 end
 
-lemmas
-    permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
-and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
-and bv5[simp] = rbv5.simps[quot_lifted]
-and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
+lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
+lemmas bv5[simp] = rbv5.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]
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
@@ -159,6 +166,7 @@
 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:
@@ -170,10 +178,12 @@
 
 
 lemma lets_not_ok1:
-  "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)))"
+  "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
+   (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 fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1))
+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
 done
 
 lemma distinct_helper:
@@ -192,7 +202,7 @@
    (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)
+apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts)
 done
 
 end