275 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
275 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
276 ML {* val cheat_equivp = Unsynchronized.ref false *} |
276 ML {* val cheat_equivp = Unsynchronized.ref false *} |
277 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
277 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
278 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
278 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
279 ML {* val cheat_supp_eq = Unsynchronized.ref false *} |
279 ML {* val cheat_supp_eq = Unsynchronized.ref false *} |
|
280 |
|
281 ML {* |
|
282 fun remove_loop t = |
|
283 let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end |
|
284 handle TERM _ => @{thm eqTrueI} OF [t] |
|
285 *} |
280 |
286 |
281 text {* |
287 text {* |
282 nominal_datatype2 does the following things in order: |
288 nominal_datatype2 does the following things in order: |
283 |
289 |
284 Parser.thy/raw_nominal_decls |
290 Parser.thy/raw_nominal_decls |
397 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
403 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
398 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
404 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
399 |
405 |
400 (* definition of raw_alpha_eq_iff lemmas *) |
406 (* definition of raw_alpha_eq_iff lemmas *) |
401 val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
407 val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
402 val alpha_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) alpha_eq_iff; |
408 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
|
409 val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp); |
403 |
410 |
404 (* proving equivariance lemmas *) |
411 (* proving equivariance lemmas *) |
405 val _ = warning "Proving equivariance"; |
412 val _ = warning "Proving equivariance"; |
406 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
413 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
407 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
414 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
488 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
495 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
489 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
496 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
490 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
497 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
491 val _ = warning "Lifting eq-iff"; |
498 val _ = warning "Lifting eq-iff"; |
492 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
499 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
493 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff |
500 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp |
494 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 |
501 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 |
495 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
502 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
496 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
503 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
497 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |
504 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |
498 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
505 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
499 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
506 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
500 val q_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) q_eq_iff; |
507 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
501 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff_simp) lthy17; |
|
502 val q_dis = map (lift_thm qtys lthy18) rel_dists; |
508 val q_dis = map (lift_thm qtys lthy18) rel_dists; |
503 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
509 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
504 val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); |
510 val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); |
505 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
511 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
506 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
512 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
514 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
520 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
515 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
521 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
516 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
522 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
517 val _ = warning "Support Equations"; |
523 val _ = warning "Support Equations"; |
518 fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else |
524 fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else |
519 supp_eq_tac q_induct q_fv q_perm q_eq_iff_simp lthy22 1; |
525 supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1; |
520 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e => |
526 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e => |
521 let val _ = warning ("Support eqs failed") in [] end; |
527 let val _ = warning ("Support eqs failed") in [] end; |
522 val lthy23 = note_suffix "supp" q_supp lthy22; |
528 val lthy23 = note_suffix "supp" q_supp lthy22; |
523 in |
529 in |
524 (0, lthy23) |
530 (0, lthy23) |