191 |
191 |
192 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
192 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
193 val {descr, sorts, ...} = dtinfo |
193 val {descr, sorts, ...} = dtinfo |
194 |
194 |
195 val raw_tys = all_dtyps descr sorts |
195 val raw_tys = all_dtyps descr sorts |
196 val raw_full_ty_names = map (fst o dest_Type) raw_tys |
|
197 val tvs = hd raw_tys |
196 val tvs = hd raw_tys |
198 |> snd o dest_Type |
197 |> snd o dest_Type |
199 |> map dest_TFree |
198 |> map dest_TFree |
200 |
199 |
201 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names |
200 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_dt_names |
202 |
201 |
203 val raw_cns_info = all_dtyp_constrs_types descr sorts |
202 val raw_cns_info = all_dtyp_constrs_types descr sorts |
204 val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info |
203 val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info |
205 |
204 |
206 val raw_inject_thms = flat (map #inject dtinfos) |
205 val raw_inject_thms = flat (map #inject dtinfos) |
213 |> `(fn thms => (length thms) div 2) |
212 |> `(fn thms => (length thms) div 2) |
214 |> uncurry drop |
213 |> uncurry drop |
215 |
214 |
216 val _ = trace_msg (K "Defining raw permutations...") |
215 val _ = trace_msg (K "Defining raw permutations...") |
217 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = |
216 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = |
218 define_raw_perms raw_full_ty_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0 |
217 define_raw_perms raw_dt_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0 |
219 |
218 |
220 (* noting the raw permutations as eqvt theorems *) |
219 (* noting the raw permutations as eqvt theorems *) |
221 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a |
220 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a |
222 |
221 |
223 val _ = trace_msg (K "Defining raw fv- and bn-functions...") |
222 val _ = trace_msg (K "Defining raw fv- and bn-functions...") |
224 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
223 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
225 define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
224 define_raw_bns raw_dt_names raw_dts raw_bn_funs raw_bn_eqs |
226 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
225 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 |
227 |
226 |
228 (* defining the permute_bn functions *) |
227 (* defining the permute_bn functions *) |
229 val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = |
228 val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = |
230 define_raw_bn_perms raw_tys raw_bn_info raw_cns_info |
229 define_raw_bn_perms raw_tys raw_bn_info raw_cns_info |
231 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a |
230 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a |
232 |
231 |
233 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = |
232 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = |
234 define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses |
233 define_raw_fvs raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses |
235 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b |
234 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b |
236 |
235 |
237 val _ = trace_msg (K "Defining alpha relations...") |
236 val _ = trace_msg (K "Defining alpha relations...") |
238 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
237 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
239 define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c |
238 define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c |
240 |
239 |
241 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
240 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
242 |
241 |
243 val _ = trace_msg (K "Proving distinct theorems...") |
242 val _ = trace_msg (K "Proving distinct theorems...") |
244 val alpha_distincts = |
243 val alpha_distincts = |