54 |
54 |
55 val app = curry (list_comb o swap); |
55 val app = curry (list_comb o swap); |
56 |
56 |
57 fun prove_size_thms (info : Datatype.info) new_type_names thy = |
57 fun prove_size_thms (info : Datatype.info) new_type_names thy = |
58 let |
58 let |
59 val {descr, sorts, rec_names, rec_rewrites, induct, ...} = info; |
59 val {descr, rec_names, rec_rewrites, induct, ...} = info; |
60 val l = length new_type_names; |
60 val l = length new_type_names; |
61 val descr' = List.take (descr, l); |
61 val descr' = List.take (descr, l); |
62 val (rec_names1, rec_names2) = chop l rec_names; |
62 val (rec_names1, rec_names2) = chop l rec_names; |
63 val recTs = Datatype_Aux.get_rec_types descr sorts; |
63 val recTs = Datatype_Aux.get_rec_types descr; |
64 val (recTs1, recTs2) = chop l recTs; |
64 val (recTs1, recTs2) = chop l recTs; |
65 val (_, (_, paramdts, _)) :: _ = descr; |
65 val (_, (_, paramdts, _)) :: _ = descr; |
66 val paramTs = map (Datatype_Aux.typ_of_dtyp descr sorts) paramdts; |
66 val paramTs = map (Datatype_Aux.typ_of_dtyp descr) paramdts; |
67 val ((param_size_fs, param_size_fTs), f_names) = paramTs |> |
67 val ((param_size_fs, param_size_fTs), f_names) = paramTs |> |
68 map (fn T as TFree (s, _) => |
68 map (fn T as TFree (s, _) => |
69 let |
69 let |
70 val name = "f" ^ unprefix "'" s; |
70 val name = "f" ^ unprefix "'" s; |
71 val U = T --> HOLogic.natT |
71 val U = T --> HOLogic.natT |
92 val overloaded_size_fns = map HOLogic.size_const recTs1; |
92 val overloaded_size_fns = map HOLogic.size_const recTs1; |
93 |
93 |
94 (* instantiation for primrec combinator *) |
94 (* instantiation for primrec combinator *) |
95 fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) = |
95 fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) = |
96 let |
96 let |
97 val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs; |
97 val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs; |
98 val k = length (filter Datatype_Aux.is_rec_type cargs); |
98 val k = length (filter Datatype_Aux.is_rec_type cargs); |
99 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) => |
100 if Datatype_Aux.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) |
101 else |
101 else |
102 (if b andalso is_poly thy dt' then |
102 (if b andalso is_poly thy dt' then |
170 val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs'; |
170 val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs'; |
171 |
171 |
172 (* characteristic equations for size functions *) |
172 (* characteristic equations for size functions *) |
173 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) = |
174 let |
174 let |
175 val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs; |
175 val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs; |
176 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); |
177 val ts = map_filter (fn (sT as (s, T), dt) => |
177 val ts = map_filter (fn (sT as (s, T), dt) => |
178 Option.map (fn sz => sz $ Free sT) |
178 Option.map (fn sz => sz $ Free sT) |
179 (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 |
180 else NONE)) (tnames ~~ Ts ~~ cargs) |
180 else NONE)) (tnames ~~ Ts ~~ cargs) |