347 if get_STEPS lthy2 > 3 |
347 if get_STEPS lthy2 > 3 |
348 then define_raw_fvs descr sorts raw_bn_info raw_bclauses lthy3 |
348 then define_raw_fvs descr sorts raw_bn_info raw_bclauses lthy3 |
349 else raise TEST lthy3 |
349 else raise TEST lthy3 |
350 |
350 |
351 (* definition of raw alphas *) |
351 (* definition of raw alphas *) |
352 val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
352 val (alpha_ts, alpha_bn_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
353 if get_STEPS lthy > 4 |
353 if get_STEPS lthy > 4 |
354 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a |
354 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a |
355 else raise TEST lthy3a |
355 else raise TEST lthy3a |
356 |
356 |
357 val (alpha_ts_nobn, alpha_ts_bn) = chop (length raw_fvs) alpha_ts |
|
358 |
|
359 val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; |
357 val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; |
360 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
358 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
361 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
359 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
|
360 |
362 val bns = raw_bn_funs ~~ bn_nos; |
361 val bns = raw_bn_funs ~~ bn_nos; |
363 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
362 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) (rel_distinct ~~ alpha_ts)); |
364 (rel_distinct ~~ alpha_ts_nobn)); |
|
365 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
363 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
366 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
364 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_bn_ts)) |
367 |
365 |
368 (* definition of raw_alpha_eq_iff lemmas *) |
366 (* definition of raw_alpha_eq_iff lemmas *) |
369 val alpha_eq_iff = |
367 val alpha_eq_iff = |
370 if get_STEPS lthy > 5 |
368 if get_STEPS lthy > 5 |
371 then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 |
369 then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 |
372 else raise TEST lthy4 |
370 else raise TEST lthy4 |
373 |
371 |
374 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
372 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
375 |
373 |
376 (* proving equivariance lemmas *) |
374 (* proving equivariance lemmas for bns, fvs and alpha *) |
377 val _ = warning "Proving equivariance"; |
375 val _ = warning "Proving equivariance"; |
378 val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm ((*raw_bn_eqs @*) raw_perm_defs) (map fst bns) lthy4 |
376 val (bv_eqvt, lthy5) = |
379 val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5 |
377 if get_STEPS lthy > 6 |
380 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; |
378 then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4 |
|
379 else raise TEST lthy4 |
|
380 |
|
381 val (fv_eqvt, lthy6) = |
|
382 if get_STEPS lthy > 7 |
|
383 then prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5 |
|
384 else raise TEST lthy5 |
|
385 |
|
386 val (alpha_eqvt, lthy6a) = |
|
387 if get_STEPS lthy > 8 |
|
388 then Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6 |
|
389 else raise TEST lthy6 |
|
390 |
381 |
391 |
382 (* proving alpha equivalence *) |
392 (* proving alpha equivalence *) |
383 val _ = warning "Proving equivalence"; |
393 val _ = warning "Proving equivalence"; |
384 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
394 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts, alpha_bn_ts) bn_nos; |
385 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; |
395 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; |
386 val alpha_equivp = |
396 val alpha_equivp = |
387 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts |
397 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts |
388 else build_equivps alpha_ts reflps alpha_induct |
398 else build_equivps alpha_ts reflps alpha_induct |
389 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a; |
399 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a; |
390 val qty_binds = map (fn (_, b, _, _) => b) dts; |
400 val qty_binds = map (fn (_, b, _, _) => b) dts; |
391 val qty_names = map Name.of_binding qty_binds; |
401 val qty_names = map Name.of_binding qty_binds; |
392 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
402 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
393 val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts_nobn alpha_equivp lthy6a; |
403 val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts alpha_equivp lthy6a; |
394 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
404 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
395 val raw_consts = |
405 val raw_consts = |
396 flat (map (fn (i, (_, _, l)) => |
406 flat (map (fn (i, (_, _, l)) => |
397 map (fn (cname, dts) => |
407 map (fn (cname, dts) => |
398 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
408 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
399 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
409 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
400 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
410 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; |
401 val _ = warning "Proving respects"; |
411 val _ = warning "Proving respects"; |
402 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct [] (*raw_bn_eqs*) (map fst bns) lthy8; |
412 val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; |
403 val (bns_rsp_pre, lthy9) = fold_map ( |
413 val (bns_rsp_pre, lthy9) = fold_map ( |
404 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
414 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
405 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
415 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
406 val bns_rsp = flat (map snd bns_rsp_pre); |
416 val bns_rsp = flat (map snd bns_rsp_pre); |
407 |
417 |
414 val fv_rsp = flat (map snd fv_rsp_pre); |
424 val fv_rsp = flat (map snd fv_rsp_pre); |
415 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
425 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
416 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
426 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
417 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
427 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
418 else |
428 else |
419 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 exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
429 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 exhaust_thms alpha_bn_ts lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
420 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
430 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
421 alpha_bn_rsp_tac) alpha_ts_bn lthy11 |
431 alpha_bn_rsp_tac) alpha_bn_ts lthy11 |
422 fun const_rsp_tac _ = |
432 fun const_rsp_tac _ = |
423 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a |
433 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_bn_ts lthy11a |
424 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
434 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
425 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
435 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
426 const_rsp_tac) raw_consts lthy11a |
436 const_rsp_tac) raw_consts lthy11a |
427 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
437 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
428 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12; |
438 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12; |
429 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
439 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
430 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
440 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
431 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ [] (*raw_bn_funs*)) lthy12a; |
441 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; |
432 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
442 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_ts |
433 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = |
443 val (qalpha_bn_ts, qalphabn_defs, lthy12c) = |
434 quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
444 quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_ts) lthy12b; |
435 val _ = warning "Lifting permutations"; |
445 val _ = warning "Lifting permutations"; |
436 val thy = Local_Theory.exit_global lthy12c; |
446 val thy = Local_Theory.exit_global lthy12c; |
437 val perm_names = map (fn x => "permute_" ^ x) qty_names |
447 val perm_names = map (fn x => "permute_" ^ x) qty_names |
438 val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) raw_perm_simps thy; |
448 val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) raw_perm_simps thy; |
439 val lthy13 = Theory_Target.init NONE thy'; |
449 val lthy13 = Theory_Target.init NONE thy'; |
477 val thy3 = Local_Theory.exit_global lthy20; |
487 val thy3 = Local_Theory.exit_global lthy20; |
478 val _ = warning "Instantiating FS"; |
488 val _ = warning "Instantiating FS"; |
479 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
489 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
480 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
490 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
481 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
491 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
482 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
492 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts, qalpha_bn_ts) bn_nos; |
483 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
493 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
484 val _ = warning "Support Equations"; |
494 val _ = warning "Support Equations"; |
485 fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else |
495 fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else |
486 supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1; |
496 supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1; |
487 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e => |
497 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e => |