187 let |
187 let |
188 val _ = trace_msg (K "Defining raw datatypes...") |
188 val _ = trace_msg (K "Defining raw datatypes...") |
189 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) = |
189 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) = |
190 define_raw_dts dts bn_funs bn_eqs bclauses lthy |
190 define_raw_dts dts bn_funs bn_eqs bclauses lthy |
191 |
191 |
192 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
192 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_dt_names |
193 val {descr, sorts, ...} = dtinfo |
193 val {descr, sorts, ...} = hd dtinfos |
194 |
194 |
195 val raw_tys = all_dtyps descr sorts |
195 val raw_tys = Datatype_Aux.get_rec_types descr sorts |
196 val tvs = hd raw_tys |
196 val tvs = hd raw_tys |
197 |> snd o dest_Type |
197 |> snd o dest_Type |
198 |> map dest_TFree |
198 |> map dest_TFree |
199 |
199 |
200 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_dt_names |
|
201 |
|
202 val raw_cns_info = all_dtyp_constrs_types descr sorts |
200 val raw_cns_info = all_dtyp_constrs_types descr sorts |
203 val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info |
201 val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info |
204 |
202 |
205 val raw_inject_thms = flat (map #inject dtinfos) |
203 val raw_inject_thms = flat (map #inject dtinfos) |
206 val raw_distinct_thms = flat (map #distinct dtinfos) |
204 val raw_distinct_thms = flat (map #distinct dtinfos) |
207 val raw_induct_thm = #induct dtinfo |
205 val raw_induct_thm = #induct (hd dtinfos) |
208 val raw_induct_thms = #inducts dtinfo |
206 val raw_induct_thms = #inducts (hd dtinfos) |
209 val raw_exhaust_thms = map #exhaust dtinfos |
207 val raw_exhaust_thms = map #exhaust dtinfos |
210 val raw_size_trms = map HOLogic.size_const raw_tys |
208 val raw_size_trms = map HOLogic.size_const raw_tys |
211 val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |
209 val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |
212 |> `(fn thms => (length thms) div 2) |
210 |> `(fn thms => (length thms) div 2) |
213 |> uncurry drop |
211 |> uncurry drop |