theory Parser
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Perm" "Fv" "Rsp" "Lift"
begin

section{* Interface for nominal_datatype *}

text {*

Nominal-Datatype-part:


1nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
               type(s) to be defined             constructors list
               (ty args, name, syn)              (name, typs, syn)

Binder-Function-part:

2rd Arg: (binding * typ option * mixfix) list 
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^    
            binding function(s)           
              to be defined               
            (name, type, syn)             

3th Arg:  term list 
          ^^^^^^^^^
          the equations of the binding functions
          (Trueprop equations)
*}

ML {*

*}

text {*****************************************************}
ML {* 
(* nominal datatype parser *)
local
  structure P = OuterParse

  fun tuple ((x, y, z), u) = (x, y, z, u)
  fun tswap (((x, y), z), u) = (x, y, u, z)
in

val _ = OuterKeyword.keyword "bind"
val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ

(* binding specification *)
(* maybe use and_list *)
val bind_parser = 
  P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name) >> swap)

val constr_parser =
  P.binding -- Scan.repeat anno_typ

(* datatype parser *)
val dt_parser =
  (P.type_args -- P.binding -- P.opt_mixfix >> P.triple1) -- 
    (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> tswap)) >> tuple

(* function equation parser *)
val fun_parser = 
  Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[])

(* main parser *)
val main_parser =
  (P.and_list1 dt_parser) -- fun_parser >> P.triple2

end
*}

(* adds "_raw" to the end of constants and types *)
ML {*
fun add_raw s = s ^ "_raw"
fun add_raws ss = map add_raw ss
fun raw_bind bn = Binding.suffix_name "_raw" bn

fun replace_str ss s = 
  case (AList.lookup (op=) ss s) of 
     SOME s' => s'
   | NONE => s

fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts)
  | replace_typ ty_ss T = T  

fun raw_dts ty_ss dts =
let

  fun raw_dts_aux1 (bind, tys, mx) =
    (raw_bind bind, map (replace_typ ty_ss) tys, mx)

  fun raw_dts_aux2 (ty_args, bind, mx, constrs) =
    (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs)
in
  map raw_dts_aux2 dts
end

fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T)
  | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T)
  | replace_aterm trm_ss trm = trm

fun replace_term trm_ss ty_ss trm =
  trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) 
*}

ML {*
fun get_cnstrs dts =
  map (fn (_, _, _, constrs) => constrs) dts

fun get_typed_cnstrs dts =
  flat (map (fn (_, bn, _, constrs) => 
   (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)

fun get_cnstr_strs dts =
  map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts))

fun get_bn_fun_strs bn_funs =
  map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
*}

ML {*
fun rawify_dts dt_names dts dts_env =
let
  val raw_dts = raw_dts dts_env dts
  val raw_dt_names = add_raws dt_names
in
  (raw_dt_names, raw_dts)
end 
*}

ML {*
fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs =
let
  val bn_funs' = map (fn (bn, ty, mx) => 
    (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs
  
  val bn_eqs' = map (fn (attr, trm) => 
    (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs
in
  (bn_funs', bn_eqs') 
end 
*}

ML {*
fun apfst3 f (a, b, c) = (f a, b, c)
*}

ML {* 
fun rawify_binds dts_env cnstrs_env bn_fun_env binds =
  map (map (map (map (fn (opt_trm, i, j, aty) => 
    (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j, aty))))) binds
*}

ML {*
fun find [] _ = error ("cannot find element")
  | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
*}

ML {*
fun strip_bn_fun t =
  case t of
    Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
  | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
  | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
      (i, NONE) :: strip_bn_fun y
  | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
      (i, NONE) :: strip_bn_fun y
  | Const (@{const_name bot}, _) => []
  | Const (@{const_name Nil}, _) => []
  | (f as Free _) $ Bound i => [(i, SOME f)]
  | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t))
*}

ML {*
fun prep_bn dt_names dts eqs = 
let
  fun aux eq = 
  let
    val (lhs, rhs) = eq
      |> strip_qnt_body "all" 
      |> HOLogic.dest_Trueprop
      |> HOLogic.dest_eq
    val (bn_fun, [cnstr]) = strip_comb lhs
    val (_, ty) = dest_Free bn_fun
    val (ty_name, _) = dest_Type (domain_type ty)
    val dt_index = find_index (fn x => x = ty_name) dt_names
    val (cnstr_head, cnstr_args) = strip_comb cnstr
    val rhs_elements = strip_bn_fun rhs
    val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
  in
    (dt_index, (bn_fun, (cnstr_head, included)))
  end 
  fun order dts i ts = 
  let
    val dt = nth dts i
    val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt)
    val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts
  in
    map (find ts') cts
  end

  val unordered = AList.group (op=) (map aux eqs)
  val unordered' = map (fn (x, y) =>  (x, AList.group (op=) y)) unordered
  val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' 
in
  ordered
end
*}

ML {* 
fun add_primrec_wrapper funs eqs lthy = 
  if null funs then (([], []), lthy)
  else 
   let 
     val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs
     val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs
   in 
     Primrec.add_primrec funs' eqs' lthy
   end
*}

ML {*
fun add_datatype_wrapper dt_names dts =
let
  val conf = Datatype.default_config
in
  Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts)
end
*}

ML {* 
fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
let
  val thy = ProofContext.theory_of lthy
  val thy_name = Context.theory_name thy

  val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
  val dt_full_names = map (Long_Name.qualify thy_name) dt_names 
  val dt_full_names' = add_raws dt_full_names
  val dts_env = dt_full_names ~~ dt_full_names'

  val cnstrs = get_cnstr_strs dts
  val cnstrs_ty = get_typed_cnstrs dts
  val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs
  val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name 
    (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty
  val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names'

  val bn_fun_strs = get_bn_fun_strs bn_funs
  val bn_fun_strs' = add_raws bn_fun_strs
  val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
  val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) 
    (bn_fun_strs ~~ bn_fun_strs')
  
  val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env

  val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs 
  
  val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds 

  val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs)

(*val _ = tracing (cat_lines (map PolyML.makestring raw_bns))*)
in
  lthy 
  |> add_datatype_wrapper raw_dt_names raw_dts 
  ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs
  ||>> pair raw_binds
  ||>> pair raw_bns
end
*}

lemma equivp_hack: "equivp x"
sorry
ML {*
fun equivp_hack ctxt rel =
let
  val thy = ProofContext.theory_of ctxt
  val ty = domain_type (fastype_of rel)
  val cty = ctyp_of thy ty
  val ct = cterm_of thy rel
in
  Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
end
*}

ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
ML {* val cheat_equivp = Unsynchronized.ref false *}
ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
ML {* val cheat_const_rsp = Unsynchronized.ref false *}

(* nominal_datatype2 does the following things in order:
  1) define the raw datatype
  2) define the raw binding functions
  3) define permutations of the raw datatype and show that raw type is in the pt typeclass
  4) define fv and fb_bn
  5) define alpha and alpha_bn
  6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)
  6) prove alpha_eq_iff    (C1 x = C2 y \<leftrightarrow> P x y ...)
     (left-to-right by intro rule, right-to-left by cases; simp)
  7) prove bn_eqvt (common induction on the raw datatype)
  8) prove fv_eqvt (common induction on the raw datatype with help of above)
  9) prove alpha_eqvt and alpha_bn_eqvt
     (common alpha-induction, unfolding alpha_gen, permute of #* and =)
 10) prove that alpha and alpha_bn are equivalence relations
     (common induction and application of 'compose' lemmas)
 11) define quotient types
 12) prove bn respects     (common induction and simp with alpha_gen)
 13) prove fv respects     (common induction and simp with alpha_gen)
 14) prove permute respects    (unfolds to alpha_eqvt)
 15) prove alpha_bn respects
     (alpha_induct then cases then sym and trans of the relations)
 16) show that alpha implies alpha_bn (by unduction, needed in following step)
 17) prove respects for all datatype constructors
     (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
 18) define lifted constructors, fv, bn, alpha_bn, permutations
 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass
 20) lift permutation simplifications
 21) lift induction
 22) lift fv
 23) lift bn
 24) lift eq_iff
 25) lift alpha_distincts
 26) lift fv and bn eqvts
 27) prove that union of arguments supports constructors
 28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
 29) prove supp = fv
*)
ML {*
fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
let
  val _ = tracing "Raw declarations";
  val thy = ProofContext.theory_of lthy
  val thy_name = Context.theory_name thy
  val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) =
    raw_nominal_decls dts bn_funs bn_eqs binds lthy
  val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
  fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
  val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_1)))) raw_bns;
  val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
  val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc
  val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc

  val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
  val {descr, sorts, ...} = dtinfo;
  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
  val raw_tys = map (fn (i, _) => nth_dtyp i) descr;
  val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
  val rel_dtinfos = List.take (dtinfos, (length dts));
  val inject = flat (map #inject dtinfos);
  val distincts = flat (map #distinct dtinfos);
  val rel_distinct = map #distinct rel_dtinfos;
  val induct = #induct dtinfo;
  val exhausts = map #exhaust dtinfos;
  val _ = tracing "Defining permutations, fv and alpha";
  val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
    Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
  val raw_binds_flat = map (map flat) raw_binds;
  val ((((fv_ts, ordered_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) =
    define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;
  val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts;
  val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
  val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct;
  val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
  val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
  val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
  val bns = raw_bn_funs ~~ bn_nos;
  val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
    (rel_distinct ~~ alpha_ts_nobn));
  val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
    ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
  val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
  val _ = tracing "Proving equivariance";
  val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv_ts_nobn @ fv_ts_bn) lthy5
  fun alpha_eqvt_tac' _ =
    if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1
  val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
  val _ = tracing "Proving equivalence";
  val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts;
  val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
  val alpha_equivp =
    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn
    else build_equivps alpha_ts reflps alpha_induct
      inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
  val qty_binds = map (fn (_, b, _, _) => b) dts;
  val qty_names = map Name.of_binding qty_binds;
  val qty_full_names = map (Long_Name.qualify thy_name) qty_names
  val (q_tys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
  val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
  val raw_consts =
    flat (map (fn (i, (_, _, l)) =>
      map (fn (cname, dts) =>
        Const (cname, map (typ_of_dtyp descr sorts) dts --->
          typ_of_dtyp descr sorts (DtRec i))) l) descr);
  val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7;
  val _ = tracing "Proving respects";
  val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
  val _ = map tracing (map PolyML.makestring bns_rsp_pre')
  val (bns_rsp_pre, lthy9) = fold_map (
    fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ =>
       resolve_tac bns_rsp_pre' 1)) bns lthy8;
  val bns_rsp = flat (map snd bns_rsp_pre);
  fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
    else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
  val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
  val (fv_rsp_pre, lthy10) = fold_map
    (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv]
    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9;
  val fv_rsp = flat (map snd fv_rsp_pre);
  val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
  val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;
  val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
        (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11
(*  val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*)
  fun const_rsp_tac _ =
    if !cheat_const_rsp then Skip_Proof.cheat_tac thy
    else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a
      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
    const_rsp_tac) raw_consts lthy11a
  val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts
  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12;
  val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
  val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
  val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
  val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
  val (qalpha_ts_bn, qbn_defs, lthy12c) = quotient_lift_consts_export (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
  val _ = tracing "Lifting permutations";
  val thy = Local_Theory.exit_global lthy12c;
  val perm_names = map (fn x => "permute_" ^ x) qty_names
  val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
  val lthy13 = Theory_Target.init NONE thy';
  val q_name = space_implode "_" qty_names;
  fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
  val _ = tracing "Lifting induction";
  val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
  val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct);
  fun note_suffix s th ctxt =
    snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
  fun note_simp_suffix s th ctxt =
    snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
  val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
    [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13;
  val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
  val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
  val q_perm = map (lift_thm lthy14) raw_perm_def;
  val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
  val q_fv = map (lift_thm lthy15) fv_def;
  val lthy16 = note_simp_suffix "fv" q_fv lthy15;
  val q_bn = map (lift_thm lthy16) raw_bn_eqs;
  val lthy17 = note_simp_suffix "bn" q_bn lthy16;
  val _ = tracing "Lifting eq-iff";
  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff
  val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1
  val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2;
  val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
  val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
  val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
  val q_dis = map (lift_thm lthy18) rel_dists;
  val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
  val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt);
  val (_, lthy20) = Local_Theory.note ((Binding.empty,
    [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
  val _ = tracing "Finite Support";
  val supports = map (prove_supports lthy20 q_perm) consts;
  val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys);
  val thy3 = Local_Theory.exit_global lthy20;
  val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
  fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
  val lthy22 = Class.prove_instantiation_instance tac lthy21
  val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
  val (names, supp_eq_t) = supp_eq fv_alpha_all;
  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
  val lthy23 = note_suffix "supp" q_supp lthy22;
in
  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy23)
end
*}


ML {* 
(* parsing the datatypes and declaring *)
(* constructors in the local theory    *)
fun prepare_dts dt_strs lthy = 
let
  val thy = ProofContext.theory_of lthy
  
  fun mk_type full_tname tvrs =
    Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs)

  fun prep_cnstr lthy full_tname tvs (cname, anno_tys, mx, _) =
  let
    val tys = map (Syntax.read_typ lthy o snd) anno_tys
    val ty = mk_type full_tname tvs
  in
    ((cname, tys ---> ty, mx), (cname, tys, mx))
  end
  
  fun prep_dt lthy (tvs, tname, mx, cnstrs) = 
  let
    val full_tname = Sign.full_name thy tname
    val (cnstrs', cnstrs'') = 
      split_list (map (prep_cnstr lthy full_tname tvs) cnstrs)
  in
    (cnstrs', (tvs, tname, mx, cnstrs''))
  end 

  val (cnstrs, dts) = 
    split_list (map (prep_dt lthy) dt_strs)
in
  lthy
  |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs))
  |> pair dts
end
*}

ML {*
(* parsing the binding function specification and *)
(* declaring the functions in the local theory    *)
fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy =
let
  val ((bn_funs, bn_eqs), _) = 
    Specification.read_spec bn_fun_strs bn_eq_strs lthy

  fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) 
  val bn_funs' = map prep_bn_fun bn_funs
in
  lthy
  |> Local_Theory.theory (Sign.add_consts_i bn_funs')
  |> pair (bn_funs', bn_eqs) 
end 
*}

ML {*
fun find_all eq xs (k',i) = 
  maps (fn (k, (v1, v2)) => if eq (k, k') then [(v1, v2, i)] else []) xs
*}

ML {*
(* associates every SOME with the index in the list; drops NONEs *)
fun mk_env xs =
  let
    fun mapp (_: int) [] = []
      | mapp i (a :: xs) = 
         case a of
           NONE => mapp (i + 1) xs
         | SOME x => (x, i) :: mapp (i + 1) xs
  in mapp 0 xs end
*}

ML {*
fun env_lookup xs x =
  case AList.lookup (op =) xs x of
    SOME x => x
  | NONE => error ("cannot find " ^ x ^ " in the binding specification.");
*}

ML {*
val recursive = Unsynchronized.ref false
val alpha_type = Unsynchronized.ref AlphaGen
*}

ML {*
fun prepare_binds dt_strs lthy = 
let
  fun extract_annos_binds dt_strs =
    map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs

  fun prep_bn env bn_str =
    case (Syntax.read_term lthy bn_str) of
       Free (x, _) => (NONE, env_lookup env x)
     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), !recursive), env_lookup env x)
     | _ => error (bn_str ^ " not allowed as binding specification.");  
 
  fun prep_typ env (i, opt_name) = 
    case opt_name of
      NONE => []
    | SOME x => find_all (op=) env (x,i);
        
  (* annos - list of annotation for each type (either NONE or SOME fo a type *)
  
  fun prep_binds (annos, bind_strs) = 
  let
    val env = mk_env annos (* for every label the index *)
    val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs  
  in
    map_index (prep_typ binds) annos
  end

in
  map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type)))))
  (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
end
*}

ML {*
fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
let
  fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx)

  val lthy0 = 
    Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy
  val (dts, lthy1) = 
    prepare_dts dt_strs lthy0
  val ((bn_funs, bn_eqs), lthy2) = 
    prepare_bn_funs bn_fun_strs bn_eq_strs lthy1
  val binds = prepare_binds dt_strs lthy2
in
  nominal_datatype2 dts bn_funs bn_eqs binds lthy |> snd
end
*}


(* Command Keyword *)

ML {*
let
   val kind = OuterKeyword.thy_decl
in
   OuterSyntax.local_theory "nominal_datatype" "test" kind 
     (main_parser >> nominal_datatype2_cmd)
end
*}


end