15 val get_nominal_datatype : theory -> string -> nominal_datatype_info option |
15 val get_nominal_datatype : theory -> string -> nominal_datatype_info option |
16 val mk_perm: typ list -> term -> term -> term |
16 val mk_perm: typ list -> term -> term -> term |
17 val perm_of_pair: term * term -> term |
17 val perm_of_pair: term * term -> term |
18 val mk_not_sym: thm list -> thm list |
18 val mk_not_sym: thm list -> thm list |
19 val perm_simproc: simproc |
19 val perm_simproc: simproc |
20 val setup: theory -> theory |
|
21 end |
20 end |
22 |
21 |
23 structure NominalPackage : NOMINAL_PACKAGE = |
22 structure NominalPackage : NOMINAL_PACKAGE = |
24 struct |
23 struct |
25 |
24 |
66 map (RuleCases.case_names o exhaust_cases descr o #1) |
65 map (RuleCases.case_names o exhaust_cases descr o #1) |
67 (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr); |
66 (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr); |
68 |
67 |
69 end; |
68 end; |
70 |
69 |
71 (* data kind 'HOL/nominal_datatypes' *) |
70 (* theory data *) |
72 |
71 |
73 type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list; |
72 type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list; |
74 |
73 |
75 type nominal_datatype_info = |
74 type nominal_datatype_info = |
76 {index : int, |
75 {index : int, |
81 induction : thm, |
80 induction : thm, |
82 distinct : thm list, |
81 distinct : thm list, |
83 inject : thm list}; |
82 inject : thm list}; |
84 |
83 |
85 structure NominalDatatypesData = TheoryDataFun |
84 structure NominalDatatypesData = TheoryDataFun |
86 (struct |
85 ( |
87 val name = "HOL/nominal_datatypes"; |
|
88 type T = nominal_datatype_info Symtab.table; |
86 type T = nominal_datatype_info Symtab.table; |
89 |
|
90 val empty = Symtab.empty; |
87 val empty = Symtab.empty; |
91 val copy = I; |
88 val copy = I; |
92 val extend = I; |
89 val extend = I; |
93 fun merge _ tabs : T = Symtab.merge (K true) tabs; |
90 fun merge _ tabs : T = Symtab.merge (K true) tabs; |
94 |
91 ); |
95 fun print sg tab = |
|
96 Pretty.writeln (Pretty.strs ("nominal datatypes:" :: |
|
97 map #1 (NameSpace.extern_table (Sign.type_space sg, tab)))); |
|
98 end); |
|
99 |
92 |
100 val get_nominal_datatypes = NominalDatatypesData.get; |
93 val get_nominal_datatypes = NominalDatatypesData.get; |
101 val put_nominal_datatypes = NominalDatatypesData.put; |
94 val put_nominal_datatypes = NominalDatatypesData.put; |
102 val map_nominal_datatypes = NominalDatatypesData.map; |
95 val map_nominal_datatypes = NominalDatatypesData.map; |
103 val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes; |
96 val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes; |
104 val setup = NominalDatatypesData.init; |
97 |
105 |
98 |
106 (**** make datatype info ****) |
99 (**** make datatype info ****) |
107 |
100 |
108 fun make_dt_info descr sorts induct reccomb_names rec_thms |
101 fun make_dt_info descr sorts induct reccomb_names rec_thms |
109 (((i, (_, (tname, _, _))), distinct), inject) = |
102 (((i, (_, (tname, _, _))), distinct), inject) = |