# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268058505 -3600
# Node ID 2bf82fa871e78a97c26d55d20aa9240d16959ba8
# Parent  5682b7fa5e2466a68b977be20bba67dc14673cbb
Proper recognition of atoms and atom sets.

diff -r 5682b7fa5e24 -r 2bf82fa871e7 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Mon Mar 08 15:06:14 2010 +0100
+++ b/Nominal/Fv.thy	Mon Mar 08 15:28:25 2010 +0100
@@ -61,9 +61,13 @@
 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 thy _ = false;
 *}
 
 
+
 (* Like map2, only if the second list is empty passes empty lists insted of error *)
 ML {*
 fun map2i _ [] [] = []
@@ -127,9 +131,6 @@
     in
       (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)
     end;
-  (* Copy from Term *)
-  fun is_funtype (Type ("fun", [_, _])) = true
-    | is_funtype _ = false;
   (* Similar to one in USyntax *)
   fun mk_pair (fst, snd) =
     let val ty1 = fastype_of fst
@@ -146,6 +147,7 @@
 ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall 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, _) =>
@@ -176,18 +178,20 @@
       val arg_nos = 0 upto (length dts - 1)
       fun fv_bind args (NONE, i, _) =
             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
-            (* TODO we assume that all can be 'atomized' *)
-            if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else
-            mk_single_atom (nth args i)
+            if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else
+            if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else
+            (* TODO we do not know what to do with non-atomizable things *)
+            @{term "{} :: atom set"}
         | fv_bind args (SOME f, i, _) = f $ (nth args i);
       fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
       fun fv_arg ((dt, x), arg_no) =
         let
           val arg =
             if is_rec_type dt then nth fv_frees (body_index dt) $ x else
-            (* TODO: we just assume everything can be 'atomized' *)
-            if (is_funtype o fastype_of) x then mk_atoms x else
-            HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x];
+            if ((is_atom thy) o fastype_of) x then mk_single_atom x else
+            if ((is_atom_set thy) o fastype_of) x then mk_atoms x else
+            (* TODO we do not know what to do with non-atomizable things *)
+            @{term "{} :: atom set"}
           (* If i = j then we generate it only once *)
           val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
           val sub = fv_binds args relevant