--- a/Nominal/Fv.thy	Tue Mar 16 17:20:46 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 16 18:18:08 2010 +0100
@@ -210,11 +210,10 @@
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
   val alpha_bn_type = 
-    if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}
-    else nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool};
+    (*if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} else*)
+    nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool};
   val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type);
   val pi = Free("pi", @{typ perm})
-  val alpha_bn_pi = if is_rec then alpha_bn_free $ pi else alpha_bn_free;
   fun alpha_bn_constr (cname, dts) args_in_bn =
   let
     val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -224,19 +223,18 @@
     val args2 = map Free (names2 ~~ Ts);
     val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
     val rhs = HOLogic.mk_Trueprop
-      (alpha_bn_pi $ (list_comb (c, args)) $ (list_comb (c, args2)));
+      (alpha_bn_free $ (list_comb (c, args)) $ (list_comb (c, args2)));
     fun lhs_arg ((dt, arg_no), (arg, arg2)) =
       let
         val argty = fastype_of arg;
         val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty);
-        val permarg = if is_rec then permute $ pi $ arg else arg
       in
       if is_rec_type dt then
-        if arg_no mem args_in_bn then alpha_bn_pi $ arg $ arg2
-        else (nth alpha_frees (body_index dt)) $ permarg $ arg2
+        if arg_no mem args_in_bn then alpha_bn_free $ arg $ arg2
+        else (nth alpha_frees (body_index dt)) $ arg $ arg2
       else
         if arg_no mem args_in_bn then @{term True}
-        else HOLogic.mk_eq (permarg, arg2)
+        else HOLogic.mk_eq (arg, arg2)
       end
     val arg_nos = 0 upto (length dts - 1)
     val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
@@ -355,19 +353,31 @@
               else (HOLogic.mk_eq (arg, arg2))
           | (_, [], []) => @{term True}
           | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) =>
-            let
-              val alpha_bn_const =
-                nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns)
-              val alpha_bn =
-                if is_rec then alpha_bn_const $ pi $ arg $ arg2 else alpha_bn_const $ arg $ arg2
-              val ty = fastype_of (bn $ arg)
-              val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty)
-            in
-              if bns_same rel_in_comp_binds then
-                alpha_bn
-(*                HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))*)
-              else error "incompatible bindings for one argument"
-            end
+            if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else
+            if is_rec then
+              let
+                val (rbinds, rpis) = split_list rel_in_comp_binds
+                val lhs_binds = fv_binds args rbinds
+                val lhs = mk_pair (lhs_binds, arg);
+                val rhs_binds = fv_binds args2 rbinds;
+                val rhs = mk_pair (rhs_binds, arg2);
+                val alpha = nth alpha_frees (body_index dt);
+                val fv = nth fv_frees (body_index dt);
+                val pi = foldr1 add_perm (distinct (op =) rpis);
+                val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
+                val alpha_gen = Syntax.check_term lthy alpha_gen_pre
+              in
+                alpha_gen
+              end
+            else
+              let
+                val alpha_bn_const =
+                  nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns)
+                val ty = fastype_of (bn $ arg)
+                val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty)
+              in
+                alpha_bn_const $ arg $ arg2
+              end
           | ([], [], relevant) =>
             let
               val (rbinds, rpis) = split_list relevant
@@ -380,10 +390,7 @@
               val pi = foldr1 add_perm (distinct (op =) rpis);
               val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
               val alpha_gen = Syntax.check_term lthy alpha_gen_pre
-(*              val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
-              val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *)
             in
-(*              if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
               alpha_gen
             end
           | _ => error "Fv.alpha: not supported binding structure"

--- 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: