
diff -r 8557af71724e -r 0203cd5cfd6c Nominal/Fv.thy
--- 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;




