1 theory NewFv

     2 imports "../Nominal-General/Nominal2_Atoms" 

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

     4 begin

     5 

     6 ML {*

     7 datatype bmodes =

     8    BEmy of int

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

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

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

    12 *}

    13 

    14 ML {*

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

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

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

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

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

    20   fun mk_union sets =

    21     fold (fn a => fn b =>

    22       if a = noatoms then b else

    23       if b = noatoms then a else

    24       if a = b then a else

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

    26 *}

    27 

    28 ML {*

    29 fun is_atom thy typ =

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

    31 

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

    33   | is_atom_set _ _ = false;

    34 

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

    36   | is_atom_fset _ _ = false;

    37 

    38 fun mk_atom_set t =

    39 let

    40   val ty = fastype_of t;

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

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

    43 in

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

    45 end;

    46 

    47 fun mk_atom_fset t =

    48 let

    49   val ty = fastype_of t;

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

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

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

    53 in

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

    55 end;

    56 

    57 fun mk_diff a b =

    58   if b = noatoms then a else

    59   if b = a then noatoms else

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

    61 *}

    62 

    63 ML {*

    64 fun atoms thy x =

    65 let

    66   val ty = fastype_of x;

    67 in

    68   if is_atom thy ty then mk_single_atom x else

    69   if is_atom_set thy ty then mk_atom_set x else

    70   if is_atom_fset thy ty then mk_atom_fset x else

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

    72 end

    73 *}

    74 

    75 ML {*

    76 fun setify x =

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

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

    79 *}

    80 

    81 ML {*

    82 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =

    83 let

    84   fun fv_body i =

    85     let

    86       val x = nth args i;

    87       val dt = nth dts i;

    88     in

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

    90     end

    91   val fv_bodys = mk_union (map fv_body bodys)

    92   val bound_vars =

    93     case binds of

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

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

    96   val non_rec_vars =

    97     case binds of

    98       [(SOME bn, i)] =>

    99         if i mem bodys

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

   101         else noatoms

   102     | _ => noatoms

   103 in

   104   mk_union [mk_diff fv_bodys bound_vars, non_rec_vars]

   105 end

   106 *}

   107 

   108 ML {*

   109 fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm =

   110 case bm of

   111   BEmy i =>

   112     let

   113       val x = nth args i;

   114       val dt = nth dts i;

   115     in

   116       case AList.lookup (op=) args_in_bn i of

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

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

   119       | SOME NONE => noatoms

   120     end

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

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

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

   124 *}

   125 

   126 ML {*

   127 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees

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

   129 let

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

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

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

   133   let

   134     val Ts = map (typ_of_dtyp descr sorts) dts;

   135     val names = Datatype_Prop.make_tnames Ts;

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

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

   138     val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn

   139   in

   140     HOLogic.mk_Trueprop (HOLogic.mk_eq

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

   142   end;

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

   144 in

   145   map2 fv_bn_constr constrs (args_in_bns ~~ bmll)

   146 end

   147 *}

   148 

   149 ML {*

   150 fun fv_bns thy dt_info fv_frees bns bmlll =

   151 let

   152   fun mk_fvbn_free (bn, ith, _) =

   153     let

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

   155     in

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

   157     end;

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

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

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

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

   162 in

   163   (bn_fvbn, (fvbn_names, eqs))

   164 end

   165 *}

   166 

   167 ML {*

   168 fun fv_bm thy dts args fv_frees bn_fvbn bm =

   169 case bm of

   170   BEmy i =>

   171     let

   172       val x = nth args i;

   173       val dt = nth dts i;

   174     in

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

   176     end

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

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

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

   180 *}

   181 

   182 ML {*

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

   184 let

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

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

   187   fun fv_constr (cname, dts) bml =

   188   let

   189     val Ts = map (typ_of_dtyp descr sorts) dts;

   190     val names = Datatype_Prop.make_tnames Ts;

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

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

   193     val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn

   194   in

   195     HOLogic.mk_Trueprop (HOLogic.mk_eq

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

   197   end;

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

   199 in

   200   map2 fv_constr constrs bmll

   201 end

   202 *}

   203 ML {*

   204 val by_pat_completeness_auto =

   205   Proof.global_terminal_proof

   206     (Method.Basic Pat_Completeness.pat_completeness,

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

   208 

   209 fun termination_by method =

   210   Function.termination_proof NONE

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

   212 *}

   213 

   214 

   215 

   216 ML {*

   217 fun define_fv dt_info bns bmlll lthy =

   218 let

   219   val thy = ProofContext.theory_of lthy;

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

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

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

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

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

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

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

   227   val fvbns = map snd bn_fvbn;

   228   val fv_nums = 0 upto (length fv_frees - 1)

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

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

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

   232   val lthy' =

   233     lthy

   234     |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config

   235     |> by_pat_completeness_auto

   236     |> Local_Theory.restore

   237     |> termination_by (Lexicographic_Order.lexicographic_order)

   238 in

   239   (fv_frees @ fvbns, lthy')

   240 end

   241 *}

   242 

   243 end