
diff -r baa67b07f436 -r 4eaae533efc3 Nominal/Fv.thy
--- 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 =




