--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_atoms.ML	Sun Nov 14 16:34:47 2010 +0000
@@ -0,0 +1,83 @@
+(*  Title:      nominal_atoms/ML
+    Authors:    Brian Huffman, Christian Urban
+
+    Command for defining concrete atom types. 
+    
+    At the moment, only single-sorted atom types
+    are supported. 
+*)
+
+signature ATOM_DECL =
+sig
+  val add_atom_decl: (binding * (binding option)) -> theory -> theory
+end;
+
+structure Atom_Decl :> ATOM_DECL =
+struct
+
+fun atom_decl_set (str : string) : term =
+  let
+    val a = Free ("a", @{typ atom});
+    val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"})
+              $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"};
+  in
+    HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s))
+  end
+
+fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
+  let
+    val _ = Theory.requires thy "Nominal2_Base" "nominal logic";
+    val str = Sign.full_name thy name;
+
+    (* typedef *)
+    val set = atom_decl_set str;
+    val tac = rtac @{thm exists_eq_simple_sort} 1;
+    val ((full_tname, info  as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
+      Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy;
+
+    (* definition of atom and permute *)
+    val newT = #abs_type (fst info);
+    val RepC = Const (Rep_name, newT --> @{typ atom});
+    val AbsC = Const (Abs_name, @{typ atom} --> newT);
+    val a = Free ("a", newT);
+    val p = Free ("p", @{typ perm});
+    val atom_eqn =
+      HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a));
+    val permute_eqn =
+      HOLogic.mk_Trueprop (HOLogic.mk_eq
+        (mk_perm p a, AbsC $ (mk_perm p (RepC $ a))));
+    val atom_def_name =
+      Binding.prefix_name "atom_" (Binding.suffix_name "_def" name);
+    val permute_def_name =
+      Binding.prefix_name "permute_" (Binding.suffix_name "_def" name);
+
+    (* at class instance *)
+    val lthy =
+      Class.instantiation ([full_tname], [], @{sort at}) thy;
+    val ((_, (_, permute_ldef)), lthy) =
+      Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
+    val ((_, (_, atom_ldef)), lthy) =
+      Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy;
+    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
+    val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef;
+    val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef;
+    val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];
+    val thy = lthy
+      |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1))
+      |> Local_Theory.exit_global;
+  in
+    thy
+  end;
+
+(** outer syntax **)
+
+local structure P = Parse and K = Keyword in
+
+val _ =
+  Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
+    ((P.binding -- Scan.option (Args.parens (P.binding))) >>
+      (Toplevel.print oo (Toplevel.theory o add_atom_decl)));
+
+end;
+
+end;