255 |
255 |
256 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
256 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
257 val raw_dt_names' = map (Long_Name.qualify thy_name) raw_dt_names |
257 val raw_dt_names' = map (Long_Name.qualify thy_name) raw_dt_names |
258 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
258 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
259 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
259 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
260 (*val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs)*) |
|
261 |
260 |
262 val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy |
261 val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy |
263 val (raw_bn_funs2, raw_bn_eqs2, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 |
262 val (raw_bn_funs', raw_bn_eqs', lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 |
264 |
263 |
265 val raw_bn_descr = |
264 val raw_bn_info = |
266 prep_bn_descr lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs2) |
265 prep_bn_info lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs') |
267 in |
266 in |
268 (raw_dt_full_names, raw_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr, lthy2) |
267 (raw_dt_full_names, raw_bclauses, raw_bn_funs', raw_bn_eqs', raw_bn_info, lthy2) |
269 end |
268 end |
270 *} |
269 *} |
271 |
270 |
272 lemma equivp_hack: "equivp x" |
271 lemma equivp_hack: "equivp x" |
273 sorry |
272 sorry |
308 |
307 |
309 ML {* |
308 ML {* |
310 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
309 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
311 let |
310 let |
312 (* definition of the raw datatypes *) |
311 (* definition of the raw datatypes *) |
313 val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_descr, lthy1) = |
312 val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_info, lthy1) = |
314 if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
313 if get_STEPS lthy > 1 |
|
314 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
315 else raise TEST lthy |
315 else raise TEST lthy |
316 |
316 |
317 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) |
317 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) |
318 val {descr, sorts, ...} = dtinfo |
318 val {descr, sorts, ...} = dtinfo |
319 val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr |
319 val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr |
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, fvbn, fv_def, lthy3a) = |
346 val (fv, fv_bn, fv_def, lthy3a) = |
347 if get_STEPS lthy2 > 3 |
347 if get_STEPS lthy2 > 3 |
348 then define_raw_fvs descr sorts raw_bn_funs raw_bn_descr 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 |
351 |
352 (* definition of raw alphas *) |
352 (* definition of raw alphas *) |
353 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
353 val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
354 if get_STEPS lthy > 4 |
354 if get_STEPS lthy > 4 |
355 then define_raw_alpha dtinfo raw_bn_descr raw_bclauses fv lthy3a |
355 then define_raw_alpha descr sorts raw_bn_info raw_bclauses fv lthy3a |
356 else raise TEST lthy3a |
356 else raise TEST lthy3a |
357 |
357 |
358 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
358 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
359 |
359 |
360 val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; |
360 val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr; |
361 val bn_tys = map (domain_type o fastype_of) [] (*raw_bn_funs;*) |
361 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; |
362 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
363 val bns = [] (*raw_bn_funs*) ~~ bn_nos; |
363 val bns = raw_bn_funs ~~ bn_nos; |
364 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
364 val rel_dists = flat (map (distinct_rel lthy4 alpha_cases) |
365 (rel_distinct ~~ alpha_ts_nobn)); |
365 (rel_distinct ~~ alpha_ts_nobn)); |
366 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
366 val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases) |
367 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
367 ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) |
368 |
368 |
369 (* definition of raw_alpha_eq_iff lemmas *) |
369 (* definition of raw_alpha_eq_iff lemmas *) |
370 val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 |
370 val alpha_eq_iff = |
|
371 if get_STEPS lthy > 5 |
|
372 then build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4 |
|
373 else raise TEST lthy4 |
|
374 |
371 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
375 val alpha_eq_iff_simp = map remove_loop alpha_eq_iff; |
372 |
376 |
373 (* proving equivariance lemmas *) |
377 (* proving equivariance lemmas *) |
374 val _ = warning "Proving equivariance"; |
378 val _ = warning "Proving equivariance"; |
375 val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm ((*raw_bn_eqs @*) raw_perm_defs) (map fst bns) lthy4 |
379 val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm ((*raw_bn_eqs @*) raw_perm_defs) (map fst bns) lthy4 |
376 val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5 |
380 val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fv_bn) lthy5 |
377 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; |
381 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; |
378 |
382 |
379 (* proving alpha equivalence *) |
383 (* proving alpha equivalence *) |
380 val _ = warning "Proving equivalence"; |
384 val _ = warning "Proving equivalence"; |
381 val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
385 val fv_alpha_all = combine_fv_alpha_bns (fv, fv_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
382 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; |
386 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; |
383 val alpha_equivp = |
387 val alpha_equivp = |
384 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts |
388 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts |
385 else build_equivps alpha_ts reflps alpha_induct |
389 else build_equivps alpha_ts reflps alpha_induct |
386 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a; |
390 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a; |
405 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
409 fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy |
406 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
410 else fvbv_rsp_tac alpha_induct fv_def lthy8 1; |
407 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
411 val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; |
408 val (fv_rsp_pre, lthy10) = fold_map |
412 val (fv_rsp_pre, lthy10) = fold_map |
409 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
413 (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] |
410 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9; |
414 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fv_bn) lthy9; |
411 val fv_rsp = flat (map snd fv_rsp_pre); |
415 val fv_rsp = flat (map snd fv_rsp_pre); |
412 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
416 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
413 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
417 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
414 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
418 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
415 else |
419 else |
419 fun const_rsp_tac _ = |
423 fun const_rsp_tac _ = |
420 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a |
424 let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a |
421 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
425 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end |
422 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
426 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
423 const_rsp_tac) raw_consts lthy11a |
427 const_rsp_tac) raw_consts lthy11a |
424 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn) |
428 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fv_bn) |
425 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12; |
429 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fv_bn)) lthy12; |
426 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
430 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
427 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
431 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
428 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ [] (*raw_bn_funs*)) lthy12a; |
432 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ [] (*raw_bn_funs*)) lthy12a; |
429 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
433 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn |
430 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = |
434 val (qalpha_ts_bn, qalphabn_defs, lthy12c) = |