theory NewAlpha
imports "NewFv"
begin

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
  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' 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
  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 = false, 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