341 val thy_name = Context.theory_name thy |
341 val thy_name = Context.theory_name thy |
342 |
342 |
343 (* definition of raw fv_functions *) |
343 (* definition of raw fv_functions *) |
344 val lthy3 = Theory_Target.init NONE thy; |
344 val lthy3 = Theory_Target.init NONE thy; |
345 |
345 |
346 val (fv, fv_bn, fv_def, lthy3a) = |
346 val (raw_fvs, raw_fv_bns, raw_fv_defs, lthy3a) = |
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 |
|
351 |
350 |
352 (* definition of raw alphas *) |
351 (* definition of raw alphas *) |
353 val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
352 val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
354 if get_STEPS lthy > 4 |
353 if get_STEPS lthy > 4 |
355 then define_raw_alpha descr sorts raw_bn_info raw_bclauses fv lthy3a |
354 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs raw_fv_bns lthy3a |
356 else raise TEST lthy3a |
355 else raise TEST lthy3a |
357 |
356 |
358 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
357 val (alpha_ts_nobn, alpha_ts_bn) = chop (length raw_fvs) alpha_ts |
359 |
358 |
360 val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; |
359 val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; |
361 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
360 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
362 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
361 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
363 val bns = raw_bn_funs ~~ bn_nos; |
362 val bns = raw_bn_funs ~~ bn_nos; |
375 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
374 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
376 |
375 |
377 (* proving equivariance lemmas *) |
376 (* proving equivariance lemmas *) |
378 val _ = warning "Proving equivariance"; |
377 val _ = warning "Proving equivariance"; |
379 val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm ((*raw_bn_eqs @*) raw_perm_defs) (map fst bns) lthy4 |
378 val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm ((*raw_bn_eqs @*) raw_perm_defs) (map fst bns) lthy4 |
380 val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fv_bn) lthy5 |
379 val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5 |
381 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; |
380 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; |
382 |
381 |
383 (* proving alpha equivalence *) |
382 (* proving alpha equivalence *) |
384 val _ = warning "Proving equivalence"; |
383 val _ = warning "Proving equivalence"; |
385 val fv_alpha_all = combine_fv_alpha_bns (fv, fv_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
384 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
386 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; |
385 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; |
387 val alpha_equivp = |
386 val alpha_equivp = |
388 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts |
387 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts |
389 else build_equivps alpha_ts reflps alpha_induct |
388 else build_equivps alpha_ts reflps alpha_induct |
390 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a; |
389 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a; |
405 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
404 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
406 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
405 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
407 val bns_rsp = flat (map snd bns_rsp_pre); |
406 val bns_rsp = flat (map snd bns_rsp_pre); |
408 |
407 |
409 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
408 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
410 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
409 else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1; |
411 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
410 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
412 val (fv_rsp_pre, lthy10) = fold_map |
411 val (fv_rsp_pre, lthy10) = fold_map |
413 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
412 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
414 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fv_bn) lthy9; |
413 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (raw_fvs @ raw_fv_bns) lthy9; |
415 val fv_rsp = flat (map snd fv_rsp_pre); |
414 val fv_rsp = flat (map snd fv_rsp_pre); |
416 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
415 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
417 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
416 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
418 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
417 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
419 else |
418 else |
423 fun const_rsp_tac _ = |
422 fun const_rsp_tac _ = |
424 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a |
423 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a |
425 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
424 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
426 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
425 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
427 const_rsp_tac) raw_consts lthy11a |
426 const_rsp_tac) raw_consts lthy11a |
428 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fv_bn) |
427 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
429 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fv_bn)) lthy12; |
428 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12; |
430 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
429 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
431 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
430 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
432 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ [] (*raw_bn_funs*)) lthy12a; |
431 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ [] (*raw_bn_funs*)) lthy12a; |
433 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
432 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
434 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = |
433 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = |
448 fun note_simp_suffix s th ctxt = |
447 fun note_simp_suffix s th ctxt = |
449 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
448 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
450 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
449 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
451 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), |
450 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), |
452 [Rule_Cases.name constr_names q_induct]) lthy13; |
451 [Rule_Cases.name constr_names q_induct]) lthy13; |
453 val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct |
452 val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct |
454 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
453 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
455 val q_perm = map (lift_thm qtys lthy14) raw_perm_defs; |
454 val q_perm = map (lift_thm qtys lthy14) raw_perm_defs; |
456 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
455 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
457 val q_fv = map (lift_thm qtys lthy15) fv_def; |
456 val q_fv = map (lift_thm qtys lthy15) raw_fv_defs; |
458 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
457 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
459 val q_bn = map (lift_thm qtys lthy16) [] (*raw_bn_eqs;*) |
458 val q_bn = map (lift_thm qtys lthy16) [] (*raw_bn_eqs;*) |
460 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
459 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
461 val _ = warning "Lifting eq-iff"; |
460 val _ = warning "Lifting eq-iff"; |
462 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
461 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |