--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/NewAlpha.thy	Thu Apr 29 17:52:19 2010 +0200
@@ -0,0 +1,249 @@
+theory NewAlpha
+imports "NewFv"
+begin
+
+(* Given [fv1, fv2, fv3]
+   produces %(x, y, z). fv1 x u fv2 y u fv3 z *)
+ML {*
+fun mk_compound_fv fvs =
+let
+  val nos = (length fvs - 1) downto 0;
+  val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos);
+  val fvs_union = mk_union fvs_applied;
+  val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs);
+  fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
+in
+  fold fold_fun tys (Abs ("", tyh, fvs_union))
+end;
+*}
+
+(* Given [R1, R2, R3]
+   produces %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
+ML {*
+fun mk_compound_alpha Rs =
+let
+  val nos = (length Rs - 1) downto 0;
+  val nos2 = (2 * length Rs - 1) downto length Rs;
+  val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no)
+    (Rs ~~ (nos2 ~~ nos));
+  val Rs_conj = foldr1 HOLogic.mk_conj Rs_applied;
+  val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs);
+  fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
+  val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))
+in
+  fold fold_fun tys (Abs ("", tyh, abs_rhs))
+end;
+*}
+
+ML {*
+fun mk_pair (fst, snd) =
+let
+  val ty1 = fastype_of fst
+  val ty2 = fastype_of snd
+  val c = HOLogic.pair_const ty1 ty2
+in
+  c $ fst $ snd
+end;
+*}
+
+ML {*
+fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees
+  bn_alphabn alpha_const binds bodys =
+let
+  val thy = ProofContext.theory_of lthy;
+  fun bind_set args (NONE, no) = setify thy (nth args no)
+    | bind_set args (SOME f, no) = f $ (nth args no)
+  fun bind_lst args (NONE, no) = listify thy (nth args no)
+    | bind_lst args (SOME f, no) = f $ (nth args no)
+  fun append (t1, t2) =
+    Const(@{const_name append}, @{typ "atom list \<Rightarrow> atom list \<Rightarrow> atom list"}) $ t1 $ t2;
+  fun binds_fn args nos =
+    if alpha_const = @{const_name alpha_lst}
+    then foldr1 append (map (bind_lst args) nos)
+    else mk_union (map (bind_set args) nos);
+  val lhs_binds = binds_fn args binds;
+  val rhs_binds = binds_fn args2 binds;
+  val lhs_bodys = foldr1 HOLogic.mk_prod (map (nth args) bodys);
+  val rhs_bodys = foldr1 HOLogic.mk_prod (map (nth args2) bodys);
+  val lhs = mk_pair (lhs_binds, lhs_bodys);
+  val rhs = mk_pair (rhs_binds, rhs_bodys);
+  val body_dts = map (nth dts) bodys;
+  fun fv_for_dt dt =
+    if Datatype_Aux.is_rec_type dt
+    then nth fv_frees (Datatype_Aux.body_index dt)
+    else Const (@{const_name supp},
+      Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ "atom set"})
+  val fvs = map fv_for_dt body_dts;
+  val fv = mk_compound_fv fvs;
+  fun alpha_for_dt dt =
+    if Datatype_Aux.is_rec_type dt
+    then nth alpha_frees (Datatype_Aux.body_index dt)
+    else Const (@{const_name "op ="},
+      Datatype_Aux.typ_of_dtyp dt_descr sorts dt -->
+      Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ bool})
+  val alphas = map alpha_for_dt body_dts;
+  val alpha = mk_compound_alpha alphas;
+  val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs
+  val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre)
+  val t = Syntax.check_term lthy alpha_gen_ex
+in
+  case binds of
+    [(SOME bn, i)] => if i mem bodys then [t]
+      else [t, ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)]
+    | _ => [t]
+end
+*}
+
+ML {*
+fun alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn args_in_bn bm =
+case bm of
+  BEmy i =>
+    let
+      val arg = nth args i;
+      val arg2 = nth args2 i;
+      val dt = nth dts i;
+    in
+      case AList.lookup (op=) args_in_bn i of
+        NONE => if Datatype_Aux.is_rec_type dt
+                then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2]
+                else [HOLogic.mk_eq (arg, arg2)]
+      | SOME (SOME (f : term)) => [(the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2]
+      | SOME NONE => []
+    end
+| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+    fv_frees bn_alphabn @{const_name alpha_lst} x y
+| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+    fv_frees bn_alphabn @{const_name alpha_gen} x y
+| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+    fv_frees bn_alphabn @{const_name alpha_res} x y
+*}
+
+
+ML {*
+fun alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess
+  (alphabn, (_, ith_dtyp, args_in_bns)) =
+let
+  fun alpha_bn_constr (cname, dts) (args_in_bn, bclauses) =
+  let
+    val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
+    val names = Datatype_Prop.make_tnames Ts;
+    val names2 = Name.variant_list 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 dt_descr sorts ith_dtyp));
+    val alpha_bn_bm = alpha_bn_bm lthy dt_descr sorts dts args args2 alpha_frees
+      fv_frees bn_alphabn args_in_bn;
+    val rhs = HOLogic.mk_Trueprop
+      (alphabn $ (list_comb (c, args)) $ (list_comb (c, args2)));
+    val lhss = map HOLogic.mk_Trueprop (flat (map alpha_bn_bm bclauses))
+  in
+    Library.foldr Logic.mk_implies (lhss, rhs)
+  end;
+  val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
+in
+  map2 alpha_bn_constr constrs (args_in_bns ~~ bclausess)
+end
+*}
+
+ML {*
+fun alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss =
+let
+  fun mk_alphabn_free (bn, ith, _) =
+    let
+      val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
+      val ty = nth_dtyp dt_descr sorts ith;
+      val alphabn_type = ty --> ty --> @{typ bool};
+      val alphabn_free = Free(alphabn_name, alphabn_type);
+    in
+      (alphabn_name, alphabn_free)
+    end;
+  val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free bn_funs);
+  val bn_alphabn = (map (fn (bn, _, _) => bn) bn_funs) ~~ alphabn_frees
+  val bclausessl = map (fn (_, i, _) => nth bclausesss i) bn_funs;
+  val eqs = map2 (alpha_bn lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausessl
+    (alphabn_frees ~~ bn_funs);
+in
+  (bn_alphabn, alphabn_names, eqs)
+end
+*}
+
+ML {*
+fun alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn bm =
+case bm of
+  BEmy i =>
+    let
+      val arg = nth args i;
+      val arg2 = nth args2 i;
+      val dt = nth dts i;
+    in
+      if Datatype_Aux.is_rec_type dt
+      then [(nth alpha_frees (Datatype_Aux.body_index dt)) $ arg $ arg2]
+      else [HOLogic.mk_eq (arg, arg2)]
+    end
+| BLst (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+    fv_frees bn_alphabn @{const_name alpha_lst} x y
+| BSet (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+    fv_frees bn_alphabn @{const_name alpha_gen} x y
+| BRes (x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees
+    fv_frees bn_alphabn @{const_name alpha_res} x y
+*}
+
+ML {*
+fun alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn bclausess (alpha_free, ith_dtyp) =
+let
+  fun alpha_constr (cname, dts) bclauses =
+  let
+    val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
+    val names = Datatype_Prop.make_tnames Ts;
+    val names2 = Name.variant_list 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 dt_descr sorts ith_dtyp));
+    val alpha_bm = alpha_bm lthy dt_descr sorts dts args args2 alpha_frees fv_frees bn_alphabn
+    val rhs = HOLogic.mk_Trueprop
+      (alpha_free $ (list_comb (c, args)) $ (list_comb (c, args2)));
+    val lhss = map HOLogic.mk_Trueprop (flat (map alpha_bm bclauses))
+  in
+    Library.foldr Logic.mk_implies (lhss, rhs)
+  end;
+  val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
+in
+  map2 alpha_constr constrs bclausess
+end
+*}
+
+ML {*
+fun define_raw_alpha (dt_info : Datatype_Aux.info) bn_funs bclausesss fv_frees lthy =
+let
+  val {descr as dt_descr, sorts, ...} = dt_info;
+
+  val alpha_names = prefix_dt_names dt_descr sorts "alpha_";
+  val alpha_types = map (fn (i, _) =>
+    nth_dtyp dt_descr sorts i --> nth_dtyp dt_descr sorts i --> @{typ bool}) dt_descr;
+  val alpha_frees = map Free (alpha_names ~~ alpha_types);
+
+  val (bn_alphabn, alpha_bn_names, alpha_bn_eqs) =
+    alpha_bns lthy dt_descr sorts alpha_frees fv_frees bn_funs bclausesss
+
+  val alpha_bns = map snd bn_alphabn;
+  val alpha_bn_types = map fastype_of alpha_bns;
+
+  val alpha_nums = 0 upto (length alpha_frees - 1)
+
+  val alpha_eqs = map2 (alpha lthy dt_descr sorts alpha_frees fv_frees bn_alphabn) bclausesss
+    (alpha_frees ~~ alpha_nums);
+
+  val all_alpha_names = map2 (fn s => fn ty => ((Binding.name s, ty), NoSyn))
+    (alpha_names @ alpha_bn_names) (alpha_types @ alpha_bn_types)
+  val all_alpha_eqs = map (pair Attrib.empty_binding) (flat alpha_eqs @ flat alpha_bn_eqs)
+
+  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}
+     all_alpha_names [] all_alpha_eqs [] lthy
+in
+  (alphas, lthy')
+end
+*}
+
+end

--- a/Nominal/NewParser.thy	Thu Apr 29 16:59:33 2010 +0200
+++ b/Nominal/NewParser.thy	Thu Apr 29 17:52:19 2010 +0200
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "NewFv"
+        "Perm" "NewFv" "NewAlpha"
 begin
 
 section{* Interface for nominal_datatype *}
@@ -278,8 +278,9 @@
   val lthy3 = Theory_Target.init NONE thy;
 
   val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val (alpha, lthy5) = define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4;
 in
-  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
+  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5)
 end
 *}
 
@@ -466,6 +467,7 @@
 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
 thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps
+thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros
 
 nominal_datatype exp =
   EVar name
@@ -516,6 +518,7 @@
 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
 thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps
+thm alpha_exp_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb_raw_alpha_lrbs_raw_alpha_pat_raw_alpha_b_lrbs_raw_alpha_b_pat_raw_alpha_b_fnclauses_raw_alpha_b_lrb_raw_alpha_b_fnclause_raw.intros
 
 nominal_datatype ty =
   Var "name"
@@ -524,6 +527,7 @@
 nominal_datatype tys =
   All xs::"name fset" ty::"ty_raw" bind_res xs in ty
 thm fv_tys_raw.simps
+thm alpha_tys_raw.intros
 
 (* some further tests *)