Nominal/NewFv.thy
changeset 1983 4538d63ecc9b
parent 1981 9f9c4965b608
child 1984 92f40c13d581
equal deleted inserted replaced
1982:d1b4c4a28c99 1983:4538d63ecc9b
    62 ML {*
    62 ML {*
    63 fun atoms thy t =
    63 fun atoms thy t =
    64 let
    64 let
    65   val ty = fastype_of t;
    65   val ty = fastype_of t;
    66 in
    66 in
    67   if is_atom thy ty 
    67   if is_atom thy ty
    68     then mk_singleton_atom t 
    68     then mk_singleton_atom t
    69   else if is_atom_set thy ty 
    69   else if is_atom_set thy ty
    70     then mk_atom_set t 
    70     then mk_atom_set t
    71   else if is_atom_fset thy ty 
    71   else if is_atom_fset thy ty
    72     then mk_atom_fset t 
    72     then mk_atom_fset t
    73   else noatoms
    73   else noatoms
    74 end
    74 end
    75 *}
    75 *}
    76 
    76 
    77 ML {*
    77 ML {*
    78 fun mk_supp t =
       
    79   Const (@{const_name supp}, fastype_of t --> @{typ "atom set"}) $ t
       
    80 *}
       
    81 
       
    82 ML {*
       
    83 fun setify x =
    78 fun setify x =
    84   if fastype_of x = @{typ "atom list"} 
    79   if fastype_of x = @{typ "atom list"}
    85   then @{term "set::atom list \<Rightarrow> atom set"} $ x 
    80   then @{term "set::atom list \<Rightarrow> atom set"} $ x
    86   else x
    81   else x
    87 *}
    82 *}
    88 
    83 
    89 ML {*
    84 ML {*
    90 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
    85 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
    91 let
    86 let
    92   fun fv_body i =
    87   fun fv_body supp i =
    93     let
    88     let
    94       val x = nth args i;
    89       val x = nth args i;
    95       val dt = nth dts i;
    90       val dt = nth dts i;
    96     in
    91     in
    97       if Datatype_Aux.is_rec_type dt
    92       if Datatype_Aux.is_rec_type dt
    98       then nth fv_frees (Datatype_Aux.body_index dt) $ x
    93       then nth fv_frees (Datatype_Aux.body_index dt) $ x
    99       else mk_supp x
    94       else (if supp then mk_supp x else atoms thy x)
   100     end
    95     end
   101   val fv_bodys = mk_union (map fv_body bodys)
    96   val fv_bodys = mk_union (map (fv_body true) bodys)
   102   val bound_vars =
    97   val bound_vars =
   103     case binds of
    98     case binds of
   104       [(SOME bn, i)] => setify (bn $ nth args i)
    99       [(SOME bn, i)] => setify (bn $ nth args i)
   105     | _ => mk_union (map fv_body (map snd binds));
   100     | _ => mk_union (map (fv_body false) (map snd binds));
   106   val non_rec_vars =
   101   val non_rec_vars =
   107     case binds of
   102     case binds of
   108       [(SOME bn, i)] =>
   103       [(SOME bn, i)] =>
   109         if i mem bodys
   104         if i mem bodys
   110         then ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
   105         then ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)