14 structure Size: SIZE = |
14 structure Size: SIZE = |
15 struct |
15 struct |
16 |
16 |
17 open DatatypeAux; |
17 open DatatypeAux; |
18 |
18 |
19 structure SizeData = TheoryDataFun( |
19 structure SizeData = TheoryDataFun |
20 struct |
20 ( |
21 type T = thm list Symtab.table; |
21 type T = thm list Symtab.table; |
22 val empty = Symtab.empty; |
22 val empty = Symtab.empty; |
23 val copy = I |
23 val copy = I |
24 val extend = I |
24 val extend = I |
25 fun merge _ = Symtab.merge (K true); |
25 fun merge _ = Symtab.merge (K true); |
26 end); |
26 ); |
27 |
27 |
28 fun specify_consts args thy = |
28 fun specify_consts args thy = |
29 let |
29 let |
30 val specs = map (fn (c, T, mx) => |
30 val specs = map (fn (c, T, mx) => |
31 Const (Sign.full_name thy (Syntax.const_name c mx), T)) args; |
31 Const (Sign.full_name thy (Syntax.const_name c mx), T)) args; |
131 val fs = maps (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr'; |
131 val fs = maps (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr'; |
132 val fTs = map fastype_of fs; |
132 val fTs = map fastype_of fs; |
133 |
133 |
134 val (size_def_thms, thy') = |
134 val (size_def_thms, thy') = |
135 thy |
135 thy |
136 |> Theory.add_consts_i (map (fn (s, T) => |
136 |> Sign.add_consts_i (map (fn (s, T) => |
137 (Sign.base_name s, T --> HOLogic.natT, NoSyn)) |
137 (Sign.base_name s, T --> HOLogic.natT, NoSyn)) |
138 (Library.drop (head_len, size_names ~~ recTs))) |
138 (Library.drop (head_len, size_names ~~ recTs))) |
139 |> fold (fn (_, (name, _, _)) => instance_size_class name) descr' |
139 |> fold (fn (_, (name, _, _)) => instance_size_class name) descr' |
140 |> PureThy.add_defs_i true (map (Thm.no_attributes o (fn (((s, T), def_name), rec_name) => |
140 |> PureThy.add_defs_i true (map (Thm.no_attributes o (fn (((s, T), def_name), rec_name) => |
141 (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT), |
141 (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT), |
188 is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) |
188 is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) |
189 (#descr info) |
189 (#descr info) |
190 in if no_size then thy |
190 in if no_size then thy |
191 else |
191 else |
192 thy |
192 thy |
193 |> Theory.add_path prefix |
193 |> Sign.add_path prefix |
194 |> (if ! quick_and_dirty |
194 |> (if ! quick_and_dirty |
195 then axiomatize_size_thms info head_len |
195 then axiomatize_size_thms info head_len |
196 else prove_size_thms info head_len) |
196 else prove_size_thms info head_len) |
197 ||> Theory.parent_path |
197 ||> Sign.parent_path |
198 |-> (fn thms => PureThy.add_thmss [(("", thms), |
198 |-> (fn thms => PureThy.add_thmss [(("", thms), |
199 [Simplifier.simp_add, Thm.declaration_attribute |
199 [Simplifier.simp_add, Thm.declaration_attribute |
200 (fn thm => Context.mapping (Code.add_default_func thm) I)])]) |
200 (fn thm => Context.mapping (Code.add_default_func thm) I)])]) |
201 |-> (fn thms => SizeData.map (fold (fn typname => Symtab.update_new |
201 |-> (fn thms => SizeData.map (fold (fn typname => Symtab.update_new |
202 (typname, flat thms)) typnames)) |
202 (typname, flat thms)) typnames)) |