10 val setup: theory -> theory |
10 val setup: theory -> theory |
11 end; |
11 end; |
12 |
12 |
13 structure Size: SIZE = |
13 structure Size: SIZE = |
14 struct |
14 struct |
15 |
|
16 open Datatype_Aux; |
|
17 |
15 |
18 structure SizeData = Theory_Data |
16 structure SizeData = Theory_Data |
19 ( |
17 ( |
20 type T = (string * thm list) Symtab.table; |
18 type T = (string * thm list) Symtab.table; |
21 val empty = Symtab.empty; |
19 val empty = Symtab.empty; |
54 val SOME (_, _, constrs) = AList.lookup op = descr index |
52 val SOME (_, _, constrs) = AList.lookup op = descr index |
55 in constrs end; |
53 in constrs end; |
56 |
54 |
57 val app = curry (list_comb o swap); |
55 val app = curry (list_comb o swap); |
58 |
56 |
59 fun prove_size_thms (info : info) new_type_names thy = |
57 fun prove_size_thms (info : Datatype.info) new_type_names thy = |
60 let |
58 let |
61 val {descr, sorts, rec_names, rec_rewrites, induct, ...} = info; |
59 val {descr, sorts, rec_names, rec_rewrites, induct, ...} = info; |
62 val l = length new_type_names; |
60 val l = length new_type_names; |
63 val descr' = List.take (descr, l); |
61 val descr' = List.take (descr, l); |
64 val (rec_names1, rec_names2) = chop l rec_names; |
62 val (rec_names1, rec_names2) = chop l rec_names; |
65 val recTs = get_rec_types descr sorts; |
63 val recTs = Datatype_Aux.get_rec_types descr sorts; |
66 val (recTs1, recTs2) = chop l recTs; |
64 val (recTs1, recTs2) = chop l recTs; |
67 val (_, (_, paramdts, _)) :: _ = descr; |
65 val (_, (_, paramdts, _)) :: _ = descr; |
68 val paramTs = map (typ_of_dtyp descr sorts) paramdts; |
66 val paramTs = map (Datatype_Aux.typ_of_dtyp descr sorts) paramdts; |
69 val ((param_size_fs, param_size_fTs), f_names) = paramTs |> |
67 val ((param_size_fs, param_size_fTs), f_names) = paramTs |> |
70 map (fn T as TFree (s, _) => |
68 map (fn T as TFree (s, _) => |
71 let |
69 let |
72 val name = "f" ^ unprefix "'" s; |
70 val name = "f" ^ unprefix "'" s; |
73 val U = T --> HOLogic.natT |
71 val U = T --> HOLogic.natT |
94 val overloaded_size_fns = map HOLogic.size_const recTs1; |
92 val overloaded_size_fns = map HOLogic.size_const recTs1; |
95 |
93 |
96 (* instantiation for primrec combinator *) |
94 (* instantiation for primrec combinator *) |
97 fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) = |
95 fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) = |
98 let |
96 let |
99 val Ts = map (typ_of_dtyp descr sorts) cargs; |
97 val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs; |
100 val k = length (filter is_rec_type cargs); |
98 val k = length (filter Datatype_Aux.is_rec_type cargs); |
101 val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) => |
99 val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) => |
102 if is_rec_type dt then (Bound i :: us, i + 1, j + 1) |
100 if Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1) |
103 else |
101 else |
104 (if b andalso is_poly thy dt' then |
102 (if b andalso is_poly thy dt' then |
105 case size_of_type (K NONE) extra_size size_ofp T of |
103 case size_of_type (K NONE) extra_size size_ofp T of |
106 NONE => us | SOME sz => sz $ Bound j :: us |
104 NONE => us | SOME sz => sz $ Bound j :: us |
107 else us, i, j + 1)) |
105 else us, i, j + 1)) |
159 HOLogic.mk_eq (app fs r $ Free p, |
157 HOLogic.mk_eq (app fs r $ Free p, |
160 the (size_of_type tab extra_size size_ofp T) $ Free p); |
158 the (size_of_type tab extra_size size_ofp T) $ Free p); |
161 |
159 |
162 fun prove_unfolded_size_eqs size_ofp fs = |
160 fun prove_unfolded_size_eqs size_ofp fs = |
163 if null recTs2 then [] |
161 if null recTs2 then [] |
164 else split_conj_thm (Skip_Proof.prove ctxt xs [] |
162 else Datatype_Aux.split_conj_thm (Skip_Proof.prove ctxt xs [] |
165 (HOLogic.mk_Trueprop (mk_conj (replicate l HOLogic.true_const @ |
163 (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l HOLogic.true_const @ |
166 map (mk_unfolded_size_eq (AList.lookup op = |
164 map (mk_unfolded_size_eq (AList.lookup op = |
167 (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) |
165 (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) |
168 (xs ~~ recTs2 ~~ rec_combs2)))) |
166 (xs ~~ recTs2 ~~ rec_combs2)))) |
169 (fn _ => (Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); |
167 (fn _ => (Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); |
170 |
168 |
172 val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs'; |
170 val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs'; |
173 |
171 |
174 (* characteristic equations for size functions *) |
172 (* characteristic equations for size functions *) |
175 fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) = |
173 fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) = |
176 let |
174 let |
177 val Ts = map (typ_of_dtyp descr sorts) cargs; |
175 val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs; |
178 val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts); |
176 val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts); |
179 val ts = map_filter (fn (sT as (s, T), dt) => |
177 val ts = map_filter (fn (sT as (s, T), dt) => |
180 Option.map (fn sz => sz $ Free sT) |
178 Option.map (fn sz => sz $ Free sT) |
181 (if p dt then size_of_type size_of extra_size size_ofp T |
179 (if p dt then size_of_type size_of extra_size size_ofp T |
182 else NONE)) (tnames ~~ Ts ~~ cargs) |
180 else NONE)) (tnames ~~ Ts ~~ cargs) |
200 size_ofp size_const T constr) |
198 size_ofp size_const T constr) |
201 (fn _ => simp_tac simpset 1))) constrs) |
199 (fn _ => simp_tac simpset 1))) constrs) |
202 (descr' ~~ size_fns ~~ recTs1); |
200 (descr' ~~ size_fns ~~ recTs1); |
203 |
201 |
204 val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @ |
202 val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @ |
205 prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3; |
203 prove_size_eqs Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3; |
206 |
204 |
207 val ([size_thms], thy'') = |
205 val ([size_thms], thy'') = |
208 Global_Theory.add_thmss |
206 Global_Theory.add_thmss |
209 [((Binding.name "size", size_eqns), |
207 [((Binding.name "size", size_eqns), |
210 [Simplifier.simp_add, Nitpick_Simps.add, |
208 [Simplifier.simp_add, Nitpick_Simps.add, |
220 let |
218 let |
221 val info as {descr, ...} = Datatype.the_info thy name; |
219 val info as {descr, ...} = Datatype.the_info thy name; |
222 val prefix = |
220 val prefix = |
223 Long_Name.map_base_name (K (space_implode "_" (map Long_Name.base_name new_type_names))) name; |
221 Long_Name.map_base_name (K (space_implode "_" (map Long_Name.base_name new_type_names))) name; |
224 val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt => |
222 val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt => |
225 is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr |
223 Datatype_Aux.is_rec_type dt andalso |
|
224 not (null (fst (Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr |
226 in |
225 in |
227 if no_size then thy |
226 if no_size then thy |
228 else |
227 else |
229 thy |
228 thy |
230 |> Sign.root_path |
229 |> Sign.root_path |