--- a/Nominal/Fv.thy	Mon Mar 01 14:26:14 2010 +0100
+++ b/Nominal/Fv.thy	Mon Mar 01 16:04:03 2010 +0100
@@ -1,5 +1,5 @@
 theory Fv
-imports "Nominal2_Atoms" "Abs"
+imports "Nominal2_Atoms" "Abs" "Perm" (* For testing *)
 begin
 
 (* Bindings are given as a list which has a length being equal
@@ -54,6 +54,7 @@
       in the database.
 *)
 
+(* TODO: should be const_name union *)
 ML {*
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
   (* TODO: It is the same as one in 'nominal_atoms' *)
@@ -64,7 +65,12 @@
     fold (fn a => fn b =>
       if a = noatoms then b else
       if b = noatoms then a else
-      HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms;
+      HOLogic.mk_binop "Set.union" (a, b)) (rev sets) noatoms;
+  fun mk_conjl props =
+    fold (fn a => fn b =>
+      if a = @{term True} then b else
+      if b = @{term True} then a else
+      HOLogic.mk_conj (a, b)) props @{term True};
   fun mk_diff a b =
     if b = noatoms then a else
     if b = a then noatoms else
@@ -90,6 +96,8 @@
 
 *}
 
+ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
+
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy =
@@ -105,58 +113,75 @@
     "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);
-  fun fv_alpha_constr i (cname, dts) bindcs =
+  fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
-      val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
+      val bindslen = length bindcs
+      val pi_strs = replicate bindslen "pi"
+      val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs;
+      val bind_pis = bindcs ~~ pis;
+      val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);
       val args = map Free (names ~~ Ts);
-      val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
+      val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts);
       val args2 = map Free (names2 ~~ Ts);
-      val c = Const (cname, Ts ---> (nth_dtyp i));
-      val fv_c = nth fv_frees i;
-      val alpha = nth alpha_frees i;
-      fun fv_bind args (NONE, i) =
+      val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
+      val fv_c = nth fv_frees ith_dtyp;
+      val alpha = nth alpha_frees ith_dtyp;
+      val arg_nos = 0 upto (length dts - 1)
+      fun fv_bind args (NONE, i, _) =
             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
             (* TODO we assume that all can be 'atomized' *)
             if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else
             mk_single_atom (nth args i)
-        | fv_bind args (SOME f, i) = f $ (nth args i);
-      fun fv_arg ((dt, x), bindxs) =
+        | fv_bind args (SOME f, i, _) = f $ (nth args i);
+      fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
+      fun fv_arg ((dt, x), arg_no) =
         let
           val arg =
             if is_rec_type dt then nth fv_frees (body_index dt) $ x else
             (* TODO: we just assume everything can be 'atomized' *)
             if (is_funtype o fastype_of) x then mk_atoms x else
-            HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]
-          val sub = mk_union (map (fv_bind args) bindxs)
+            HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x];
+          (* If i = j then we generate it only once *)
+          val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
+          val sub = fv_binds args relevant
         in
           mk_diff arg sub
         end;
       val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
-        (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))
+        (fv_c $ list_comb (c, args), mk_union (map fv_arg  (dts ~~ args ~~ arg_nos))))
       val alpha_rhs =
         HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
-      fun alpha_arg ((dt, bindxs), (arg, arg2)) =
-        if bindxs = [] 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 *)
-            val lhs_binds = mk_union (map (fv_bind args) bindxs);
-            val lhs = mk_pair (lhs_binds, arg);
-            val rhs_binds = mk_union (map (fv_bind args2) bindxs);
-            val rhs = mk_pair (rhs_binds, arg2);
-            val alpha = nth alpha_frees (body_index dt);
-            val fv = nth fv_frees (body_index dt);
-            val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs;
-            val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre
-          in
-            HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t)
-          (* TODO Add some test that is makes sense *)
-          end else @{term "True"}
-      val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2))
-      val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs)
+      fun alpha_arg ((dt, arg_no), (arg, arg2)) =
+        let
+          val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) 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 *)
+              val (rbinds, rpis) = split_list relevant
+              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);
+              (* TODO: check that pis have empty intersection *)
+              val pi = foldr1 add_perm rpis;
+              val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
+            in
+              Syntax.check_term lthy alpha_gen_pre
+            (* TODO Add some test that is makes sense *)
+            end else @{term "True"}
+        end
+      val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2))
+      val alpha_lhss = mk_conjl alphas
+      val alpha_lhss_ex =
+        fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss
+      val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs)
     in
       (fv_eq, alpha_eq)
     end;

--- a/Nominal/Term2.thy	Mon Mar 01 14:26:14 2010 +0100
+++ b/Nominal/Term2.thy	Mon Mar 01 16:04:03 2010 +0100
@@ -23,8 +23,11 @@
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *}
 
 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2")
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
-   [[[], []]]] *}
+  [[[],
+    [],
+    [(NONE, 0, 1)],
+    [(SOME @{term rbv2}, 0, 1)]],
+   [[]]] *}
 
 notation
   alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and

--- a/Nominal/Term5.thy	Mon Mar 01 14:26:14 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 01 16:04:03 2010 +0100
@@ -22,8 +22,13 @@
 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)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}
+  [ [],
+    [],
+    [(SOME @{term rbv5}, 0, 1)] ],
+  [ [],
+    []]  ] *}
 print_theorems
 
 (* Alternate version with additional binding of name in rlts in rLcons *)
@@ -57,17 +62,12 @@
   "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)
-  apply (tactic {* 
-    ALLGOALS (
-      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
-      (etac @{thm alpha_gen_compose_eqvt})
-    ) *})
-  apply (simp_all only: eqvts atom_eqvt)
-  done
+sorry
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),
-  (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *}
-thm alpha5_equivp
+lemma alpha5_equivp:
+  "equivp alpha_rtrm5"
+  "equivp alpha_rlts"
+  sorry
 
 quotient_type
   trm5 = rtrm5 / alpha_rtrm5
@@ -92,13 +92,20 @@
   "(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)
-  apply(simp_all add: alpha_gen)
+  apply(simp_all)
+  apply(simp add: alpha_gen)
+  apply(erule conjE)+
+  apply(erule exE)
+  apply(erule conjE)+
+  apply(simp_all)
   done
 
 lemma bv_list_rsp:
   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
   apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2))
   apply(simp_all)
+  apply(clarify)
+  apply simp
   done
 
 lemma [quot_respect]:
@@ -112,8 +119,7 @@
   "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
   "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
   apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
-  apply (clarify) apply (rule conjI)
-  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+  apply (clarify)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
   done
 
@@ -149,49 +155,24 @@
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-apply (subst alpha5_INJ)
-apply (rule conjI)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
+apply (simp add: alpha5_INJ)
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-done
-
-lemma lets_ok2:
-  "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
-   (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (subst alpha5_INJ)
-apply (rule conjI)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="0 :: perm" in exI)
-apply (simp only: alpha_gen)
+apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
 done
 
 lemma lets_ok3:
-  assumes a: "distinct [x, y]"
-  shows "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
-         (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (subst alpha5_INJ)
-apply (rule conjI)
-apply (simp add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="0 :: perm" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
+  "x \<noteq> y \<Longrightarrow>
+   (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+   (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ)
 done
 
+
 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)))"
-apply (simp add: alpha5_INJ(3) alpha_gen)
+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))
 done
 
@@ -214,5 +195,4 @@
 apply (simp add: distinct_helper2)
 done
 
-
 end