Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_atoms.ML
changeset 3239 67370521c09c
parent 3233 9ae285ce814e
child 3243 c4f31f1564b7
equal deleted inserted replaced
3238:b2e1a7b83e05 3239:67370521c09c 
    26     HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s))
 
    26     HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s))
 
    27   end
 
    27   end
 
    28 
    28 
    29 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
 
    29 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
 
    30   let
 
    30   let
 
    31     val _ = Theory.requires thy (Context.theory_name @{theory}) "nominal logic";
 
       
    32     val str = Sign.full_name thy name;
 
    31     val str = Sign.full_name thy name;
 
    33 
    32 
    34     (* typedef *)
 
    33     (* typedef *)
 
    35     val set = atom_decl_set str;
 
    34     val set = atom_decl_set str;
 
    36     val tac = rtac @{thm exists_eq_simple_sort} 1;
 
    35     fun tac _ = rtac @{thm exists_eq_simple_sort} 1;
 
    37     val ((full_tname, info  as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
 
    36     val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
 
    38       Typedef.add_typedef_global (name, [], NoSyn) set NONE tac thy;
 
    37       Typedef.add_typedef_global false (name, [], NoSyn) set NONE tac thy;
 
    39 
    38 
    40     (* definition of atom and permute *)
 
    39     (* definition of atom and permute *)
 
    41     val newT = #abs_type (fst info);
 
    40     val newT = #abs_type (fst info);
 
    42     val RepC = Const (Rep_name, newT --> @{typ atom});
 
    41     val RepC = Const (Rep_name, newT --> @{typ atom});
 
    43     val AbsC = Const (Abs_name, @{typ atom} --> newT);
 
    42     val AbsC = Const (Abs_name, @{typ atom} --> newT);
 
    75     thy
 
    74     thy
 
    76   end;
 
    75   end;
 
    77 
    76 
    78 (** outer syntax **)
 
    77 (** outer syntax **)
 
    79 val _ =
 
    78 val _ =
 
    80   Outer_Syntax.command @{command_spec "atom_decl"}
 
    79   Outer_Syntax.command @{command_keyword atom_decl}
 
    81     "declaration of a concrete atom type" 
    80     "declaration of a concrete atom type" 
    82       ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
 
    81       ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
 
    83         (Toplevel.theory o add_atom_decl))
 
    82         (Toplevel.theory o add_atom_decl))
 
    84 
    83 
    85 end;
 
    84 end;
nominal2