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 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 = 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 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

  val alpha_ts_loc = #preds alphas;

  val alpha_induct_loc = #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