327 val bns = raw_bn_funs ~~ bn_nos; (* Are exported *) |
327 val bns = raw_bn_funs ~~ bn_nos; (* Are exported *) |
328 val alpha_intros_loc = #intrs alpha; |
328 val alpha_intros_loc = #intrs alpha; |
329 val alpha_cases_loc = #elims alpha |
329 val alpha_cases_loc = #elims alpha |
330 val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc |
330 val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc |
331 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
331 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
332 val alpha_inj_loc = build_alpha_inj alpha_intros_loc (inject @ distincts) alpha_cases_loc lthy4 |
332 val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
333 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
|
334 val _ = tracing "Proving equivariance"; |
333 val _ = tracing "Proving equivariance"; |
335 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
334 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
336 val fv_eqvt_tac = |
335 val fv_eqvt_tac = |
337 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
336 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
338 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5 |
337 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5 |
342 fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts) |
341 fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts) |
343 (fv_ts_bn ~~ (map snd bns)) lthy6; |
342 (fv_ts_bn ~~ (map snd bns)) lthy6; |
344 val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts) |
343 val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts) |
345 fun alpha_eqvt_tac' _ = |
344 fun alpha_eqvt_tac' _ = |
346 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
345 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
347 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6a 1 |
346 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 |
348 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
347 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
349 val _ = tracing "Proving equivalence"; |
348 val _ = tracing "Proving equivalence"; |
350 val alpha_equivp = |
349 val alpha_equivp = |
351 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn |
350 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn |
352 else build_equivps alpha_ts induct alpha_induct |
351 else build_equivps alpha_ts induct alpha_induct |
353 inject alpha_inj distincts alpha_cases alpha_eqvt lthy6a; |
352 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a; |
354 val qty_binds = map (fn (_, b, _, _) => b) dts; |
353 val qty_binds = map (fn (_, b, _, _) => b) dts; |
355 val qty_names = map Name.of_binding qty_binds; |
354 val qty_names = map Name.of_binding qty_binds; |
356 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
355 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
357 val lthy7 = define_quotient_type |
356 val lthy7 = define_quotient_type |
358 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn)) |
357 (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn)) |
375 else fvbv_rsp_tac alpha_induct fv_def 1; |
374 else fvbv_rsp_tac alpha_induct fv_def 1; |
376 val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9 |
375 val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9 |
377 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
376 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
378 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
377 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
379 fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
378 fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy |
380 else constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1 |
379 else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1 |
381 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
380 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
382 const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11 |
381 const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11 |
383 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts |
382 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts |
384 val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12; |
383 val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12; |
385 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
384 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
401 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a; |
400 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a; |
402 val q_fv = map (lift_thm lthy15) fv_def; |
401 val q_fv = map (lift_thm lthy15) fv_def; |
403 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
402 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
404 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
403 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
405 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
404 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
406 val _ = tracing "Lifting pseudo-injectivity"; |
405 val _ = tracing "Lifting eq-iff"; |
407 val inj_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_inj |
406 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_eq_iff |
408 val inj_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) inj_unfolded1 |
407 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1 |
409 val q_inj_pre1 = map (lift_thm lthy17) inj_unfolded2; |
408 val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2; |
410 val q_inj_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_inj_pre1 |
409 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1 |
411 val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre2 |
410 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2 |
412 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; |
411 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_eq_iff"), []), q_eq_iff) lthy17; |
413 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
412 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
414 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
413 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
415 val q_dis = map (lift_thm lthy18) rel_dists; |
414 val q_dis = map (lift_thm lthy18) rel_dists; |
416 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; |
415 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; |
417 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; |
416 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; |