Nominal-General/nominal_atoms.ML
changeset 2568 8193bbaa07fe
parent 2567 41137dc935ff
child 2569 94750b31a97d
equal deleted inserted replaced
2567:41137dc935ff 2568:8193bbaa07fe
     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 fun atom_decl_set (str : string) : term =
       
    19   let
       
    20     val a = Free ("a", @{typ atom});
       
    21     val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"})
       
    22               $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"};
       
    23   in
       
    24     HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s))
       
    25   end
       
    26 
       
    27 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
       
    28   let
       
    29     val _ = Theory.requires thy "Nominal2_Base" "nominal logic";
       
    30     val str = Sign.full_name thy name;
       
    31 
       
    32     (* typedef *)
       
    33     val set = atom_decl_set str;
       
    34     val tac = rtac @{thm exists_eq_simple_sort} 1;
       
    35     val ((full_tname, info  as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
       
    36       Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy;
       
    37 
       
    38     (* definition of atom and permute *)
       
    39     val newT = #abs_type (fst info);
       
    40     val RepC = Const (Rep_name, newT --> @{typ atom});
       
    41     val AbsC = Const (Abs_name, @{typ atom} --> newT);
       
    42     val a = Free ("a", newT);
       
    43     val p = Free ("p", @{typ perm});
       
    44     val atom_eqn =
       
    45       HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a));
       
    46     val permute_eqn =
       
    47       HOLogic.mk_Trueprop (HOLogic.mk_eq
       
    48         (mk_perm p a, AbsC $ (mk_perm p (RepC $ a))));
       
    49     val atom_def_name =
       
    50       Binding.prefix_name "atom_" (Binding.suffix_name "_def" name);
       
    51     val permute_def_name =
       
    52       Binding.prefix_name "permute_" (Binding.suffix_name "_def" name);
       
    53 
       
    54     (* at class instance *)
       
    55     val lthy =
       
    56       Class.instantiation ([full_tname], [], @{sort at}) thy;
       
    57     val ((_, (_, permute_ldef)), lthy) =
       
    58       Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
       
    59     val ((_, (_, atom_ldef)), lthy) =
       
    60       Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy;
       
    61     val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
       
    62     val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef;
       
    63     val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef;
       
    64     val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];
       
    65     val thy = lthy
       
    66       |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1))
       
    67       |> Local_Theory.exit_global;
       
    68   in
       
    69     thy
       
    70   end;
       
    71 
       
    72 (** outer syntax **)
       
    73 
       
    74 local structure P = Parse and K = Keyword in
       
    75 
       
    76 val _ =
       
    77   Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
       
    78     ((P.binding -- Scan.option (Args.parens (P.binding))) >>
       
    79       (Toplevel.print oo (Toplevel.theory o add_atom_decl)));
       
    80 
       
    81 end;
       
    82 
       
    83 end;