1 (*  Title:      nominal_atoms/ML

     2     Authors:    Brian Huffman, Christian Urban

     3 

     4     Command for defining concrete atom types. 

     5     

     6     At the moment, only single-sorted atom types

     7     are supported. 

     8 *)

     9 

    10 signature ATOM_DECL =

    11 sig

    12   val add_atom_decl: (binding * (binding option)) -> theory -> theory

    13 end;

    14 

    15 structure Atom_Decl :> ATOM_DECL =

    16 struct

    17 

    18 val atomT = @{typ atom};

    19 val permT = @{typ perm};

    20 

    21 val sort_of_const = @{term sort_of};

    22 fun atom_const T = Const (@{const_name atom}, T --> atomT);

    23 fun permute_const T = Const (@{const_name permute}, permT --> T --> T);

    24 

    25 fun mk_sort_of t = sort_of_const $ t;

    26 fun mk_atom t = atom_const (fastype_of t) $ t;

    27 fun mk_permute (p, t) = permute_const (fastype_of t) $ p $ t;

    28 

    29 fun atom_decl_set (str : string) : term =

    30   let

    31     val a = Free ("a", atomT);

    32     val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"})

    33               $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"};

    34   in

    35     HOLogic.mk_Collect ("a", atomT, HOLogic.mk_eq (mk_sort_of a, s))

    36   end

    37 

    38 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =

    39   let

    40     val _ = Theory.requires thy "Nominal2_Atoms" "nominal logic";

    41     val str = Sign.full_name thy name;

    42 

    43     (* typedef *)

    44     val set = atom_decl_set str;

    45     val tac = rtac @{thm exists_eq_simple_sort} 1;

    46     val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) =

    47       Typedef.add_typedef false NONE (name, [], NoSyn) set NONE tac thy;

    48 

    49     (* definition of atom and permute *)

    50     val newT = #abs_type info;

    51     val RepC = Const (Rep_name, newT --> atomT);

    52     val AbsC = Const (Abs_name, atomT --> newT);

    53     val a = Free ("a", newT);

    54     val p = Free ("p", permT);

    55     val atom_eqn =

    56       HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a));

    57     val permute_eqn =

    58       HOLogic.mk_Trueprop (HOLogic.mk_eq

    59         (mk_permute (p, a), AbsC $ (mk_permute (p, RepC $ a))));

    60     val atom_def_name =

    61       Binding.prefix_name "atom_" (Binding.suffix_name "_def" name);

    62     val permute_def_name =

    63       Binding.prefix_name "permute_" (Binding.suffix_name "_def" name);

    64 

    65     (* at class instance *)

    66     val lthy =

    67       Theory_Target.instantiation ([full_tname], [], @{sort at}) thy;

    68     val ((_, (_, permute_ldef)), lthy) =

    69       Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;

    70     val ((_, (_, atom_ldef)), lthy) =

    71       Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy;

    72     val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);

    73     val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef;

    74     val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef;

    75     val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];

    76     val thy = lthy

    77       |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1))

    78       |> Local_Theory.exit_global;

    79   in

    80     thy

    81   end;

    82 

    83 (** outer syntax **)

    84 

    85 local structure P = OuterParse and K = OuterKeyword in

    86 

    87 val _ =

    88   OuterSyntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl

    89     ((P.binding -- Scan.option (Args.parens (P.binding))) >>

    90       (Toplevel.print oo (Toplevel.theory o add_atom_decl)));

    91 

    92 end;

    93 

    94 end;