264 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) = |
264 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) = |
265 raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
265 raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
266 |
266 |
267 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
267 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
268 val {descr, sorts, ...} = dtinfo; |
268 val {descr, sorts, ...} = dtinfo; |
|
269 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
|
270 val raw_tys = map (fn (i, _) => nth_dtyp i) descr; |
269 |
271 |
270 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
272 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
271 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; |
273 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; |
272 val inject = flat (map #inject dtinfos); |
274 val inject = flat (map #inject dtinfos); |
273 val distincts = flat (map #distinct dtinfos); |
275 val distincts = flat (map #distinct dtinfos); |
281 |
283 |
282 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
284 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
283 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
285 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
284 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
286 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
285 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
287 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
|
288 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
286 val thy = Local_Theory.exit_global lthy2; |
289 val thy = Local_Theory.exit_global lthy2; |
287 val lthy3 = Theory_Target.init NONE thy; |
290 val lthy3 = Theory_Target.init NONE thy; |
|
291 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
288 |
292 |
289 val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
293 val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3; |
290 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
294 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
291 define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a; |
295 define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a; |
292 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
296 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
293 |
297 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
294 in |
298 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
295 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4) |
299 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
|
300 val bns = raw_bn_funs ~~ bn_nos; |
|
301 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
|
302 (rel_distinct ~~ alpha_ts_nobn)); |
|
303 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
|
304 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
|
305 val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
|
306 val _ = tracing "Proving equivariance"; |
|
307 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
|
308 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
|
309 in |
|
310 ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy6) |
296 end |
311 end |
297 *} |
312 *} |
298 |
313 |
299 section {* Preparing and parsing of the specification *} |
314 section {* Preparing and parsing of the specification *} |
300 |
315 |