270 in |
270 in |
271 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
271 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
272 end |
272 end |
273 *} |
273 *} |
274 |
274 |
275 ML {* val cheat_alpha_eqvt = Unsynchronized.ref true *} |
275 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
276 ML {* val cheat_equivp = Unsynchronized.ref true *} |
276 ML {* val cheat_equivp = Unsynchronized.ref false *} |
277 ML {* val cheat_fv_rsp = Unsynchronized.ref true *} |
277 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
|
278 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
|
279 ML {* val cheat_supp_eq = Unsynchronized.ref false *} |
278 |
280 |
279 text {* |
281 text {* |
280 nominal_datatype2 does the following things in order: |
282 nominal_datatype2 does the following things in order: |
281 |
283 |
282 Parser.thy/raw_nominal_decls |
284 Parser.thy/raw_nominal_decls |
441 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
443 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
442 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
444 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
443 val fv_rsp = flat (map snd fv_rsp_pre); |
445 val fv_rsp = flat (map snd fv_rsp_pre); |
444 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
446 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
445 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
447 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
446 (* val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;*) |
448 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
|
449 else |
|
450 let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
447 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
451 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
448 (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11 |
452 alpha_bn_rsp_tac) alpha_ts_bn lthy11 |
449 fun const_rsp_tac _ = |
453 fun const_rsp_tac _ = |
450 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a |
454 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a |
451 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
455 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
452 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
456 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
453 const_rsp_tac) raw_consts lthy11a |
457 const_rsp_tac) raw_consts lthy11a |
491 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
495 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
492 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
496 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
493 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |
497 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |
494 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
498 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
495 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
499 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
496 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
500 val q_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) q_eq_iff; |
|
501 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff_simp) lthy17; |
497 val q_dis = map (lift_thm qtys lthy18) rel_dists; |
502 val q_dis = map (lift_thm qtys lthy18) rel_dists; |
498 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
503 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
499 val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); |
504 val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); |
500 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
505 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
501 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
506 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
508 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
513 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
509 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
514 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
510 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
515 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
511 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
516 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
512 val _ = warning "Support Equations"; |
517 val _ = warning "Support Equations"; |
513 val q_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) q_eq_iff; |
518 fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else |
514 (*supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1*) |
519 supp_eq_tac q_induct q_fv q_perm q_eq_iff_simp lthy22 1; |
515 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => Skip_Proof.cheat_tac thy)) handle _ => []; |
520 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; |
516 val lthy23 = note_suffix "supp" q_supp lthy22; |
522 val lthy23 = note_suffix "supp" q_supp lthy22; |
517 in |
523 in |
518 (0, lthy23) |
524 (0, lthy23) |
519 end |
525 end |
520 *} |
526 *} |