--- a/Nominal/Fv.thy	Wed Mar 10 12:48:38 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 12:48:55 2010 +0100
@@ -193,6 +193,51 @@
 end
 *}
 
+ML {*
+fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) =
+let
+  val {descr, sorts, ...} = dt_info;
+  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 = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}
+  val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type);
+  fun alpha_bn_constr (cname, dts) args_in_bn =
+  let
+    val Ts = map (typ_of_dtyp descr sorts) dts;
+    val pi = Free("pi", @{typ perm})
+    val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
+    val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
+    val args = map Free (names ~~ Ts);
+    val args2 = map Free (names2 ~~ Ts);
+    val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
+    val rhs = HOLogic.mk_Trueprop
+      (alpha_bn_free $ pi $ (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_free $ pi $ arg $ arg2
+        else (nth alpha_frees (body_index dt)) $ permarg $ arg2
+      else
+        if arg_no mem args_in_bn then @{term True}
+        else HOLogic.mk_eq (permarg, arg2)
+      end
+    val arg_nos = 0 upto (length dts - 1)
+    val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
+    val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs)
+  in
+    eq
+  end
+  val (_, (_, _, constrs)) = nth descr ith_dtyp;
+  val eqs = map2i alpha_bn_constr constrs args_in_bns
+in
+  ((bn, alpha_bn_free), (alpha_bn_name, eqs))
+end
+*}
+
 ML {* fn x => split_list(flat x) *}
 ML {* fn x => apsnd flat (split_list (map split_list x)) *}
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
@@ -209,12 +254,17 @@
   val nr_bns = non_rec_binds bindsall;
   val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
   val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);
-  val fv_bns = map snd bn_fv_bns;
   val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
   val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
   val alpha_frees = map Free (alpha_names ~~ alpha_types);
+  (* We assume that a bn is either recursive or not *)
+  val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
+  val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec))
+  val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs;
+  val alpha_bn_frees = map snd bn_alpha_bns;
+  val alpha_bn_types = map fastype_of alpha_bn_frees;
   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -269,14 +319,26 @@
         HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
       fun alpha_arg ((dt, arg_no), (arg, arg2)) =
         let
-          val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) bind_pis;
+          val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis;
+          val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis;
+          val rel_has_binds = filter (fn ((SOME _, _, j), _) => j = arg_no | _ => false) bind_pis;
         in
-          if relevant = [] then (
-            if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
-            else (HOLogic.mk_eq (arg, arg2)))
-          else
-            if is_rec_type dt then let
-              (* THE HARD CASE *)
+          case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of
+            ([], [], []) =>
+              if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
+              else (HOLogic.mk_eq (arg, arg2))
+            (* TODO: if more then check and accept *)
+          | (_, [], []) => @{term True}
+          | ([], [(((SOME (bn, _)), _, _), pi)], []) =>
+            let
+              val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2
+              val ty = fastype_of (bn $ arg)
+              val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty)
+            in
+              HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))
+            end
+          | ([], [], relevant) =>
+            let
               val (rbinds, rpis) = split_list relevant
               val lhs_binds = fv_binds args rbinds
               val lhs = mk_pair (lhs_binds, arg);
@@ -290,10 +352,10 @@
 (*              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*)
+(*              if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
               alpha_gen
-            (* TODO Add some test that is makes sense *)
-            end else @{term "True"}
+            end
+          | _ => error "Fv.alpha: not supported binding structure"
         end
       val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2))
       val alpha_lhss = mk_conjl alphas
@@ -307,7 +369,7 @@
   val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall)
   val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs))
   val rel_bns_nos = map (fn (_, i, _) => i) rel_bns;
-  fun filter_fun (a, b) = b mem rel_bns_nos;
+  fun filter_fun (_, b) = b mem rel_bns_nos;
   val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1))
   val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs)))
   val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs)))
@@ -325,38 +387,35 @@
   val (alphas, lthy''') = (Inductive.add_inductive_i
      {quiet_mode = true, verbose = false, alt_name = Binding.empty,
       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
-     (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
-     (add_binds alpha_eqs) [] lthy'')
+     (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names)
+     (alpha_types @ alpha_bn_types)) []
+     (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'')
+  val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
 in
-  ((fvs, alphas), lthy''')
+  ((all_fvs, alphas), lthy''')
 end
 *}
 
 (*
 atom_decl name
-
 datatype lam =
   VAR "name"
 | APP "lam" "lam"
 | LET "bp" "lam"
 and bp =
   BP "name" "lam"
-
 primrec
   bi::"bp \<Rightarrow> atom set"
 where
   "bi (BP x t) = {atom x}"
-
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *}
-
-
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam")
-  [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
+  [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
 print_theorems
 *)
 
-(*
+(*atom_decl name
 datatype rtrm1 =
   rVr1 "name"
 | rAp1 "rtrm1" "rtrm1"
@@ -366,24 +425,38 @@
   BUnit
 | BVr "name"
 | BPr "bp" "bp"
-
-(* to be given by the user *)
-
 primrec
   bv1
 where
   "bv1 (BUnit) = {}"
 | "bv1 (BVr x) = {atom x}"
 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-
-setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *}
-
-local_setup {* define_fv_alpha "Fv.rtrm1"
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
-   [[], [[]], [[], []]]] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *}
+local_setup {*
+  snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1")
+  [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]],
+  [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
 print_theorems
 *)
 
+(*
+atom_decl name
+datatype rtrm5 =
+  rVr5 "name"
+| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
+and rlts =
+  rLnil
+| rLcons "name" "rtrm5" "rlts"
+primrec
+  rbv5
+where
+  "rbv5 rLnil = {}"
+| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *}
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5")
+  [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
+print_theorems
+*)
 
 ML {*
 fun alpha_inj_tac dist_inj intrs elims =

--- a/Nominal/Term5.thy	Wed Mar 10 12:48:38 2010 +0100
+++ b/Nominal/Term5.thy	Wed Mar 10 12:48:55 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