theory NewFv

imports "../Nominal-General/Nominal2_Atoms" 

        "Abs" "Perm" "Rsp" "Nominal2_FSet"

begin

ML {*

datatype bmodes =

   BEmy of int

|  BLst of ((term option * int) list) * (int list)

|  BSet of ((term option * int) list) * (int list)

|  BRes of ((term option * int) list) * (int list)

*}

ML {*

  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);

  (* TODO: It is the same as one in 'nominal_atoms' *)

  fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});

  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];

  val noatoms = @{term "{} :: atom set"};

  fun mk_union sets =

    fold (fn a => fn b =>

      if a = noatoms then b else

      if b = noatoms then a else

      if a = b then a else

      HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;

*}

ML {*

fun is_atom thy typ =

  Sign.of_sort thy (typ, @{sort at})

fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t

  | is_atom_set _ _ = false;

fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t

  | is_atom_fset _ _ = false;

fun mk_atom_set t =

let

  val ty = fastype_of t;

  val atom_ty = HOLogic.dest_setT ty --> @{typ atom};

  val img_ty = atom_ty --> ty --> @{typ "atom set"};

in

  (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)

end;

fun mk_atom_fset t =

let

  val ty = fastype_of t;

  val atom_ty = dest_fsetT ty --> @{typ atom};

  val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};

  val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}

in

  fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t))

end;

fun mk_diff a b =

  if b = noatoms then a else

  if b = a then noatoms else

  HOLogic.mk_binop @{const_name minus} (a, b);

*}

ML {*

fun atoms thy x =

let

  val ty = fastype_of x;

in

  if is_atom thy ty then mk_single_atom x else

  if is_atom_set thy ty then mk_atom_set x else

  if is_atom_fset thy ty then mk_atom_fset x else

  @{term "{} :: atom set"}

end

*}

ML {*

fun setify x =

  if fastype_of x = @{typ "atom list"} then

  Const (@{const_name set}, @{typ "atom list \<Rightarrow> atom set"}) $ x else x

*}

ML {*

fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =

let

  fun fv_body i =

    let

      val x = nth args i;

      val dt = nth dts i;

    in

      if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x

    end

  val fv_bodys = mk_union (map fv_body bodys)

  val bound_vars =

    case binds of

      [(SOME bn, i)] => setify (bn $ nth args i)

    | _ => mk_union (map fv_body (map snd binds));

  val non_rec_vars =

    case binds of

      [(SOME bn, i)] =>

        if i mem bodys

        then ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)

        else noatoms

    | _ => noatoms

in

  mk_union [mk_diff fv_bodys bound_vars, non_rec_vars]

end

*}

ML {*

fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm =

case bm of

  BEmy i =>

    let

      val x = nth args i;

      val dt = nth dts i;

    in

      case AList.lookup (op=) args_in_bn i of

        NONE => if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x

      | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x

      | SOME NONE => noatoms

    end

| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y

| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y

| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y

*}

ML {*

fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees

  bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =

let

  val {descr, sorts, ...} = dt_info;

  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);

  fun fv_bn_constr (cname, dts) (args_in_bn, bml) =

  let

    val Ts = map (typ_of_dtyp descr sorts) dts;

    val names = Datatype_Prop.make_tnames Ts;

    val args = map Free (names ~~ Ts);

    val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));

    val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn

  in

    HOLogic.mk_Trueprop (HOLogic.mk_eq

      (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml)))

  end;

  val (_, (_, _, constrs)) = nth descr ith_dtyp;

in

  map2 fv_bn_constr constrs (args_in_bns ~~ bmll)

end

*}

ML {*

fun fv_bns thy dt_info fv_frees bns bmlll =

let

  fun mk_fvbn_free (bn, ith, _) =

    let

      val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));

    in

      (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))

    end;

  val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bns);

  val bn_fvbn = (map (fn (bn, _, _) => bn) bns) ~~ fvbn_frees

  val bmlls = map (fn (_, i, _) => nth bmlll i) bns;

  val eqs = map2 (fv_bn thy dt_info fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bns);

in

  (bn_fvbn, (fvbn_names, eqs))

end

*}

ML {*

fun fv_bm thy dts args fv_frees bn_fvbn bm =

case bm of

  BEmy i =>

    let

      val x = nth args i;

      val dt = nth dts i;

    in

      if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x

    end

| BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y

| BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y

| BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y

*}

ML {*

fun fv thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn bmll (fv_free, ith_dtyp) =

let

  val {descr, sorts, ...} = dt_info;

  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);

  fun fv_constr (cname, dts) bml =

  let

    val Ts = map (typ_of_dtyp descr sorts) dts;

    val names = Datatype_Prop.make_tnames Ts;

    val args = map Free (names ~~ Ts);

    val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));

    val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn

  in

    HOLogic.mk_Trueprop (HOLogic.mk_eq

      (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml)))

  end;

  val (_, (_, _, constrs)) = nth descr ith_dtyp;

in

  map2 fv_constr constrs bmll

end

*}

ML {*

val by_pat_completeness_auto =

  Proof.global_terminal_proof

    (Method.Basic Pat_Completeness.pat_completeness,

     SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))

fun termination_by method =

  Function.termination_proof NONE

  #> Proof.global_terminal_proof (Method.Basic method, NONE)

*}

ML {*

fun define_fv dt_info bns bmlll lthy =

let

  val thy = ProofContext.theory_of lthy;

  val {descr, sorts, ...} = dt_info;

  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);

  val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>

    "fv_" ^ name_of_typ (nth_dtyp i)) descr);

  val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;

  val fv_frees = map Free (fv_names ~~ fv_types);

  val (bn_fvbn, (fv_bn_names, fv_bn_eqs)) = fv_bns thy dt_info fv_frees bns bmlll;

  val fvbns = map snd bn_fvbn;

  val fv_nums = 0 upto (length fv_frees - 1)

  val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bmlll (fv_frees ~~ fv_nums);

  val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)

  val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs)

  val lthy' =

    lthy

    |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config

    |> by_pat_completeness_auto

    |> Local_Theory.restore

    |> termination_by (Lexicographic_Order.lexicographic_order)

in

  (fv_frees @ fvbns, lthy')

end

*}

end