281 |
281 |
282 (* Fixes for these 2 are known *) |
282 (* Fixes for these 2 are known *) |
283 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
283 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
284 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
284 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
285 |
285 |
|
286 |
286 ML {* |
287 ML {* |
287 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
288 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
288 let |
289 let |
289 val thy = ProofContext.theory_of lthy |
290 val thy = ProofContext.theory_of lthy |
290 val thy_name = Context.theory_name thy |
291 val thy_name = Context.theory_name thy |
302 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) |
303 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) |
303 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
304 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
304 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; |
305 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; |
305 val rel_dtinfos = List.take (dtinfos, (length dts)); |
306 val rel_dtinfos = List.take (dtinfos, (length dts)); |
306 val inject = flat (map #inject dtinfos); |
307 val inject = flat (map #inject dtinfos); |
307 val distinct = flat (map #distinct dtinfos); |
308 val distincts = flat (map #distinct dtinfos); |
308 val rel_distinct = map #distinct rel_dtinfos; |
309 val rel_distinct = map #distinct rel_dtinfos; |
309 val induct = #induct dtinfo; |
310 val induct = #induct dtinfo; |
310 val inducts = #inducts dtinfo; |
311 val inducts = #inducts dtinfo; |
311 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
312 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
312 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
313 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
329 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
330 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
330 val bns = raw_bn_funs ~~ bn_nos; |
331 val bns = raw_bn_funs ~~ bn_nos; |
331 val alpha_intros = #intrs alpha; |
332 val alpha_intros = #intrs alpha; |
332 val alpha_cases_loc = #elims alpha |
333 val alpha_cases_loc = #elims alpha |
333 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
334 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
334 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
335 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4 |
335 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
336 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
336 fun alpha_eqvt_tac' _ = |
337 fun alpha_eqvt_tac' _ = |
337 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
338 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
338 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1 |
339 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1 |
339 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4; |
340 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4; |
360 flat (map (fn (i, (_, _, l)) => |
361 flat (map (fn (i, (_, _, l)) => |
361 map (fn (cname, dts) => |
362 map (fn (cname, dts) => |
362 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
363 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
363 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
364 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
364 val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7; |
365 val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7; |
365 val (consts, const_defs) = split_list consts_defs; |
366 val (consts_loc, const_defs) = split_list consts_defs; |
|
367 val morphism_8_7 = ProofContext.export_morphism lthy8 lthy7; |
|
368 val consts = map (Morphism.term morphism_8_7) consts_loc; |
|
369 (* Could be done nicer *) |
|
370 val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); |
366 val (bns_rsp_pre, lthy9) = fold_map ( |
371 val (bns_rsp_pre, lthy9) = fold_map ( |
367 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |
372 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |
368 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8; |
373 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8; |
369 val bns_rsp = flat (map snd bns_rsp_pre); |
374 val bns_rsp = flat (map snd bns_rsp_pre); |
370 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
375 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
404 val q_dis = map (lift_thm lthy18) rel_dists; |
409 val q_dis = map (lift_thm lthy18) rel_dists; |
405 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; |
410 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; |
406 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; |
411 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; |
407 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
412 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
408 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
413 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
409 in |
414 val supports = map (prove_supports lthy20 q_perm) consts |
410 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20) |
415 val _ = map tracing (map PolyML.makestring supports); |
|
416 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys); |
|
417 val thy3 = Local_Theory.exit_global lthy20; |
|
418 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
|
419 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
|
420 val lthy22 = Class.prove_instantiation_instance tac lthy21; |
|
421 in |
|
422 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy22) |
411 end |
423 end |
412 *} |
424 *} |
413 |
425 |
414 |
426 |
415 ML {* |
427 ML {* |