273 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
273 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
274 |
274 |
275 val (info, lthy3) = prove_termination (Local_Theory.restore lthy2) |
275 val (info, lthy3) = prove_termination (Local_Theory.restore lthy2) |
276 val {fs, simps, inducts, ...} = info; |
276 val {fs, simps, inducts, ...} = info; |
277 |
277 |
278 val raw_bn_induct = Rule_Cases.strict_mutual_rule lthy3 (the inducts) |
278 val raw_bn_induct = (the inducts) |
279 val raw_bn_eqs = the simps |
279 val raw_bn_eqs = the simps |
280 |
280 |
281 val raw_bn_info = |
281 val raw_bn_info = |
282 prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) |
282 prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) |
283 |
283 |
315 |
315 |
316 fun get_STEPS ctxt = Config.get ctxt STEPS |
316 fun get_STEPS ctxt = Config.get ctxt STEPS |
317 *} |
317 *} |
318 |
318 |
319 setup STEPS_setup |
319 setup STEPS_setup |
320 |
|
321 ML {* |
|
322 fun mk_conjl props = |
|
323 fold (fn a => fn b => |
|
324 if a = @{term True} then b else |
|
325 if b = @{term True} then a else |
|
326 HOLogic.mk_conj (a, b)) (rev props) @{term True}; |
|
327 *} |
|
328 |
|
329 ML {* |
|
330 val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
|
331 *} |
|
332 |
|
333 (* Given function for buildng a goal for an input, prepares a |
|
334 one common goals for all the inputs and proves it by induction |
|
335 together *) |
|
336 ML {* |
|
337 fun prove_by_induct tys build_goal ind utac inputs ctxt = |
|
338 let |
|
339 val names = Datatype_Prop.make_tnames tys; |
|
340 val (names', ctxt') = Variable.variant_fixes names ctxt; |
|
341 val frees = map Free (names' ~~ tys); |
|
342 val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt'; |
|
343 val gls = flat gls_lists; |
|
344 fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls; |
|
345 val trm_gl_lists = map trm_gls_map frees; |
|
346 val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists |
|
347 val trm_gls = map mk_conjl trm_gl_lists; |
|
348 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls); |
|
349 fun tac {context,...} = ( |
|
350 InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind] |
|
351 THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1 |
|
352 val th_loc = Goal.prove ctxt'' [] [] gl tac |
|
353 val ths_loc = HOLogic.conj_elims th_loc |
|
354 val ths = Variable.export ctxt'' ctxt ths_loc |
|
355 in |
|
356 filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths |
|
357 end |
|
358 *} |
|
359 |
|
360 ML {* |
|
361 fun build_eqvt_gl pi frees fnctn ctxt = |
|
362 let |
|
363 val typ = domain_type (fastype_of fnctn); |
|
364 val arg = the (AList.lookup (op=) frees typ); |
|
365 in |
|
366 ([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt) |
|
367 end |
|
368 *} |
|
369 |
|
370 ML {* |
|
371 fun prove_eqvt tys ind simps funs ctxt = |
|
372 let |
|
373 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt; |
|
374 val p = Free (p, @{typ perm}) |
|
375 val simp_set = @{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt' |
|
376 val tac = asm_full_simp_tac (HOL_ss addsimps simp_set) |
|
377 val ths_loc = prove_by_induct tys (build_eqvt_gl p) ind tac funs ctxt' |
|
378 val ths = Variable.export ctxt' ctxt ths_loc |
|
379 val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) |
|
380 val _ = tracing ("eqvt thms\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) ths)) |
|
381 in |
|
382 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
|
383 end |
|
384 *} |
|
385 |
320 |
386 ML {* |
321 ML {* |
387 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
322 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
388 let |
323 let |
389 (* definition of the raw datatypes *) |
324 (* definition of the raw datatypes *) |
409 val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy1) = |
344 val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy1) = |
410 if get_STEPS lthy0 > 1 |
345 if get_STEPS lthy0 > 1 |
411 then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy0 |
346 then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy0 |
412 else raise TEST lthy0 |
347 else raise TEST lthy0 |
413 |
348 |
414 |
|
415 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
349 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
416 val bns = raw_bn_funs ~~ bn_nos; |
350 val bns = raw_bn_funs ~~ bn_nos; |
417 |
351 |
418 (* definitions of raw permutations *) |
352 (* definitions of raw permutations *) |
419 val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = |
353 val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = |
429 val thy_name = Context.theory_name thy |
363 val thy_name = Context.theory_name thy |
430 |
364 |
431 (* definition of raw fv_functions *) |
365 (* definition of raw fv_functions *) |
432 val lthy3 = Theory_Target.init NONE thy; |
366 val lthy3 = Theory_Target.init NONE thy; |
433 |
367 |
434 val (raw_fvs, raw_fv_bns, raw_fv_defs, lthy3a) = |
368 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3a) = |
435 if get_STEPS lthy2 > 3 |
369 if get_STEPS lthy2 > 3 |
436 then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3 |
370 then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3 |
437 else raise TEST lthy3 |
371 else raise TEST lthy3 |
438 |
372 |
439 (* definition of raw alphas *) |
373 (* definition of raw alphas *) |
452 then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases |
386 then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases |
453 else raise TEST lthy4 |
387 else raise TEST lthy4 |
454 |
388 |
455 (* proving equivariance lemmas for bns, fvs and alpha *) |
389 (* proving equivariance lemmas for bns, fvs and alpha *) |
456 val _ = warning "Proving equivariance"; |
390 val _ = warning "Proving equivariance"; |
457 val (bv_eqvt, lthy5) = |
391 val bn_eqvt = |
458 if get_STEPS lthy > 6 |
392 if get_STEPS lthy > 6 |
459 then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) raw_bn_funs lthy4 |
393 then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 |
460 else raise TEST lthy4 |
394 else raise TEST lthy4 |
461 |
395 |
462 val (fv_eqvt, lthy6) = |
396 val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
|
397 val (_, lthy_tmp) = Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4 |
|
398 |
|
399 val fv_eqvt = |
463 if get_STEPS lthy > 7 |
400 if get_STEPS lthy > 7 |
464 then prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5 |
401 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) lthy_tmp |
465 else raise TEST lthy5 |
402 else raise TEST lthy4 |
|
403 |
|
404 val (_, lthy_tmp') = Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp |
466 |
405 |
467 val (alpha_eqvt, lthy6a) = |
406 val (alpha_eqvt, lthy6a) = |
468 if get_STEPS lthy > 8 |
407 if get_STEPS lthy > 8 |
469 then Nominal_Eqvt.equivariance alpha_trms alpha_induct alpha_intros lthy6 |
408 then Nominal_Eqvt.equivariance alpha_trms alpha_induct alpha_intros lthy_tmp' |
470 else raise TEST lthy6 |
409 else raise TEST lthy4 |
471 |
410 |
|
411 val _ = |
|
412 if get_STEPS lthy > 9 |
|
413 then true else raise TEST lthy4 |
472 |
414 |
473 (* proving alpha equivalence *) |
415 (* proving alpha equivalence *) |
474 val _ = warning "Proving equivalence"; |
416 val _ = warning "Proving equivalence"; |
475 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos; |
417 |
|
418 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
|
419 |
476 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy6a; |
420 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy6a; |
477 val alpha_equivp = |
421 val alpha_equivp = |
478 if !cheat_equivp then map (equivp_hack lthy6a) alpha_trms |
422 if !cheat_equivp then map (equivp_hack lthy6a) alpha_trms |
479 else build_equivps alpha_trms reflps alpha_induct |
423 else build_equivps alpha_trms reflps alpha_induct |
480 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy6a; |
424 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy6a; |
557 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 |
501 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 |
558 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 |
502 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 |
559 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
503 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
560 val q_dis = map (lift_thm qtys lthy18) alpha_distincts; |
504 val q_dis = map (lift_thm qtys lthy18) alpha_distincts; |
561 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
505 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
562 val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); |
506 val q_eqvt = map (lift_thm qtys lthy19) (bn_eqvt @ fv_eqvt); |
563 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
507 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
564 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
508 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
565 val _ = warning "Supports"; |
509 val _ = warning "Supports"; |
566 val supports = map (prove_supports lthy20 q_perm) consts; |
510 val supports = map (prove_supports lthy20 q_perm) consts; |
567 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
511 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |