theory NewAlpha

imports "Abs" "Perm" "Nominal2_FSet"

uses ("nominal_dt_rawperm.ML")

     ("nominal_dt_rawfuns.ML")

begin

use "nominal_dt_rawperm.ML"

use "nominal_dt_rawfuns.ML"

ML {*

open Nominal_Dt_RawPerm

open Nominal_Dt_RawFuns

*}

ML {*

fun mk_binop2 ctxt s (l, r) =

  Syntax.check_term ctxt (Const (s, dummyT) $ l $ r)

*}

ML {*

fun mk_compound_fv' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_fv})

fun mk_compound_alpha' ctxt = foldr1 (mk_binop2 ctxt @{const_name prod_rel})

*}

ML {*

fun alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees fv_frees

  bn_alphabn alpha_const binds bodys =

let

  fun bind_set args (NONE, no) = setify lthy (nth args no)

    | bind_set args (SOME f, no) = f $ (nth args no)

  fun bind_lst args (NONE, no) = listify lthy (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 fold_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 = HOLogic.mk_prod (lhs_binds, lhs_bodys);

  val rhs = HOLogic.mk_prod (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' lthy 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' lthy 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

  fun alpha_bn_bind (SOME bn, i) =

      if member (op =) bodys i then NONE

      else SOME ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)

    | alpha_bn_bind (NONE, _) = NONE

in

  t :: (map_filter alpha_bn_bind binds)

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

  BC (_, [], [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

| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

    fv_frees bn_alphabn @{const_name alpha_lst} x y

| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

    fv_frees bn_alphabn @{const_name alpha_gen} x y

| BC (Res, 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

  BC (_, [], [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

| BC (Lst, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

    fv_frees bn_alphabn @{const_name alpha_lst} x y

| BC (Set, x, y) => alpha_bm_lsts lthy dt_descr sorts dts args args2 alpha_frees

    fv_frees bn_alphabn @{const_name alpha_gen} x y

| BC (Res, 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

  val alpha_ts_loc = #preds alphas;

  val alpha_induct_loc = #raw_induct alphas;

  val alpha_intros_loc = #intrs alphas;

  val alpha_cases_loc = #elims alphas;

  val morphism = ProofContext.export_morphism lthy' lthy;

  val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;

  val alpha_induct = Morphism.thm morphism alpha_induct_loc;

  val alpha_intros = Morphism.fact morphism alpha_intros_loc

  val alpha_cases = Morphism.fact morphism alpha_cases_loc

in

  (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy')

end

*}

end