263 in |
263 in |
264 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
264 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
265 end |
265 end |
266 *} |
266 *} |
267 |
267 |
268 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *} |
|
269 ML {* val cheat_equivp = Unsynchronized.ref true *} |
268 ML {* val cheat_equivp = Unsynchronized.ref true *} |
270 |
269 |
271 (* These 3 are not needed any more *) |
270 (* These 4 are not needed any more *) |
272 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
271 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
273 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
272 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
274 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
273 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
|
274 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
275 |
275 |
276 |
276 |
277 ML {* |
277 ML {* |
278 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
278 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
279 let |
279 let |
298 val inject = flat (map #inject dtinfos); |
298 val inject = flat (map #inject dtinfos); |
299 val distincts = flat (map #distinct dtinfos); |
299 val distincts = flat (map #distinct dtinfos); |
300 val rel_distinct = map #distinct rel_dtinfos; |
300 val rel_distinct = map #distinct rel_dtinfos; |
301 val induct = #induct dtinfo; |
301 val induct = #induct dtinfo; |
302 val inducts = #inducts dtinfo; |
302 val inducts = #inducts dtinfo; |
|
303 val exhausts = map #exhaust dtinfos; |
303 val _ = tracing "Defining permutations, fv and alpha"; |
304 val _ = tracing "Defining permutations, fv and alpha"; |
304 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
305 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
305 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
306 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
306 val raw_binds_flat = map (map flat) raw_binds; |
307 val raw_binds_flat = map (map flat) raw_binds; |
307 val ((((fv_ts, ordered_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = |
308 val ((((fv_ts, ordered_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) = |
308 define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; |
309 define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3; |
309 val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts; |
310 val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts; |
310 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
311 val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts |
311 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct |
312 val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct; |
312 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
313 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
313 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
314 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
314 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
315 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
315 val bns = raw_bn_funs ~~ bn_nos; |
316 val bns = raw_bn_funs ~~ bn_nos; |
|
317 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
|
318 (rel_distinct ~~ alpha_ts_nobn)); |
|
319 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
|
320 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
316 val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
321 val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 |
317 val _ = tracing "Proving equivariance"; |
322 val _ = tracing "Proving equivariance"; |
318 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
323 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
319 val fv_eqvt_tac = |
324 val fv_eqvt_tac = |
320 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
325 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
366 val fv_rsp = flat (map snd fv_rsp_pre); |
371 val fv_rsp = flat (map snd fv_rsp_pre); |
367 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
372 val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms |
368 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
373 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
369 val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11; |
374 val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11; |
370 fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 |
375 fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 |
371 fun alpha_bn_rsp_tac x = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else const_rsp_tac x |
|
372 val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
376 val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
373 const_rsp_tac) raw_consts lthy11 |
377 const_rsp_tac) raw_consts lthy11 |
|
378 val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos)) |
374 val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
379 val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] |
375 alpha_bn_rsp_tac) alpha_ts_bn lthy11a |
380 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a |
376 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
381 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts |
377 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
382 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; |
378 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
383 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; |
379 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 |
380 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
385 val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; |
409 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1 |
414 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1 |
410 val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2; |
415 val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2; |
411 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1 |
416 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1 |
412 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2 |
417 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2 |
413 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
418 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
414 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
|
415 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
|
416 val q_dis = map (lift_thm lthy18) rel_dists; |
419 val q_dis = map (lift_thm lthy18) rel_dists; |
417 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
420 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
418 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; |
421 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; |
419 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
422 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
420 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
423 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |