diff -r f4da25147389 -r c70e7545b738 Quot/Nominal/atom_decl.ML
--- a/Quot/Nominal/atom_decl.ML	Sat Feb 06 12:58:56 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(*  Title:      atom_decl/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 -> theory -> theory
-end;
-
-structure Atom_Decl :> ATOM_DECL =
-struct
-
-val atomT = @{typ atom};
-val permT = @{typ perm};
-
-val sort_of_const = @{term sort_of};
-fun atom_const T = Const (@{const_name atom}, T --> atomT);
-fun permute_const T = Const (@{const_name permute}, permT --> T --> T);
-
-fun mk_sort_of t = sort_of_const $ t;
-fun mk_atom t = atom_const (fastype_of t) $ t;
-fun mk_permute (p, t) = permute_const (fastype_of t) $ p $ t;
-
-fun atom_decl_set (str : string) : term =
-  let
-    val a = Free ("a", atomT);
-    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", atomT, HOLogic.mk_eq (mk_sort_of a, s))
-  end
-
-fun add_atom_decl (name : binding) (thy : theory) =
-  let
-    val _ = Theory.requires thy "Nominal2_Atoms" "nominal logic";
-    val str = Sign.full_name thy name;
-
-    (* typedef *)
-    val set = atom_decl_set str;
-    val tac = rtac @{thm exists_eq_sort} 1;
-    val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) =
-      Typedef.add_typedef false NONE (name, [], NoSyn) set NONE tac thy;
-
-    (* definition of atom and permute *)
-    val newT = #abs_type info;
-    val RepC = Const (Rep_name, newT --> atomT);
-    val AbsC = Const (Abs_name, atomT --> newT);
-    val a = Free ("a", newT);
-    val p = Free ("p", permT);
-    val atom_eqn =
-      HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a));
-    val permute_eqn =
-      HOLogic.mk_Trueprop (HOLogic.mk_eq
-        (mk_permute (p, a), AbsC $ (mk_permute (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 =
-      Theory_Target.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 (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 = OuterParse and K = OuterKeyword in
-
-val _ =
-  OuterSyntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
-    (P.binding >>
-      (Toplevel.print oo (Toplevel.theory o add_atom_decl)));
-
-end;
-
-end;