256 ||>> pair raw_bclauses |
256 ||>> pair raw_bclauses |
257 ||>> pair raw_bns |
257 ||>> pair raw_bns |
258 end |
258 end |
259 *} |
259 *} |
260 |
260 |
|
261 lemma equivp_hack: "equivp x" |
|
262 sorry |
|
263 ML {* |
|
264 fun equivp_hack ctxt rel = |
|
265 let |
|
266 val thy = ProofContext.theory_of ctxt |
|
267 val ty = domain_type (fastype_of rel) |
|
268 val cty = ctyp_of thy ty |
|
269 val ct = cterm_of thy rel |
|
270 in |
|
271 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
|
272 end |
|
273 *} |
|
274 |
|
275 ML {* val cheat_alpha_eqvt = Unsynchronized.ref true *} |
|
276 ML {* val cheat_equivp = Unsynchronized.ref true *} |
|
277 ML {* val cheat_fv_rsp = Unsynchronized.ref true *} |
261 |
278 |
262 text {* |
279 text {* |
263 nominal_datatype2 does the following things in order: |
280 nominal_datatype2 does the following things in order: |
264 |
281 |
265 Parser.thy/raw_nominal_decls |
282 Parser.thy/raw_nominal_decls |
383 |
400 |
384 (* proving equivariance lemmas *) |
401 (* proving equivariance lemmas *) |
385 val _ = warning "Proving equivariance"; |
402 val _ = warning "Proving equivariance"; |
386 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
403 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
387 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
404 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
388 fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy |
405 fun alpha_eqvt_tac' _ = |
|
406 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
|
407 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1 |
389 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
408 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
390 |
409 |
391 (* provind alpha equivalence *) |
410 (* provind alpha equivalence *) |
392 val _ = warning "Proving equivalence"; |
411 val _ = warning "Proving equivalence"; |
393 val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
412 val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
394 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; |
413 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6; |
395 val alpha_equivp = |
414 val alpha_equivp = |
396 build_equivps alpha_ts reflps alpha_induct |
415 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts |
|
416 else build_equivps alpha_ts reflps alpha_induct |
397 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; |
417 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6; |
398 val qty_binds = map (fn (_, b, _, _) => b) dts; |
418 val qty_binds = map (fn (_, b, _, _) => b) dts; |
399 val qty_names = map Name.of_binding qty_binds; |
419 val qty_names = map Name.of_binding qty_binds; |
400 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
420 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
401 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
421 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
410 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
430 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
411 val (bns_rsp_pre, lthy9) = fold_map ( |
431 val (bns_rsp_pre, lthy9) = fold_map ( |
412 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
432 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
413 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
433 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
414 val bns_rsp = flat (map snd bns_rsp_pre); |
434 val bns_rsp = flat (map snd bns_rsp_pre); |
415 (*val _ = map tracing (map PolyML.makestring fv_alpha_all);*) |
435 |
416 fun fv_rsp_tac _ = Skip_Proof.cheat_tac thy |
436 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
|
437 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
417 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
438 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
418 val (fv_rsp_pre, lthy10) = fold_map |
439 val (fv_rsp_pre, lthy10) = fold_map |
419 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
440 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
420 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
441 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
421 val fv_rsp = flat (map snd fv_rsp_pre); |
442 val fv_rsp = flat (map snd fv_rsp_pre); |
422 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
443 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms |
423 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
444 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
|
445 (* val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;*) |
424 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
446 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
425 (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11 |
447 (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11 |
426 fun const_rsp_tac _ = |
448 fun const_rsp_tac _ = |
427 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a |
449 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a |
428 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
450 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
484 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
506 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
485 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
507 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
486 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
508 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
487 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
509 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
488 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
510 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
489 val _ = warning "Support Equations"; |
511 (* val _ = warning "Support Equations"; |
490 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => []; |
512 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => []; |
491 val lthy23 = note_suffix "supp" q_supp lthy22; |
513 val lthy23 = note_suffix "supp" q_supp lthy22;*) |
492 in |
514 in |
493 (0, lthy23) |
515 (0, lthy22) |
494 end |
516 end |
495 *} |
517 *} |
496 |
518 |
497 section {* Preparing and parsing of the specification *} |
519 section {* Preparing and parsing of the specification *} |
498 |
520 |