388 Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => |
392 Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => |
389 prove_eqvt_tac insts ind_thms const_names simps context) |
393 prove_eqvt_tac insts ind_thms const_names simps context) |
390 |> ProofContext.export ctxt'' ctxt |
394 |> ProofContext.export ctxt'' ctxt |
391 end |
395 end |
392 |
396 |
|
397 |
|
398 |
|
399 (*** raw permutation functions ***) |
|
400 |
|
401 (** proves the two pt-type class properties **) |
|
402 |
|
403 fun prove_permute_zero induct perm_defs perm_fns lthy = |
|
404 let |
|
405 val perm_types = map (body_type o fastype_of) perm_fns |
|
406 val perm_indnames = Datatype_Prop.make_tnames perm_types |
|
407 |
|
408 fun single_goal ((perm_fn, T), x) = |
|
409 HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
|
410 |
|
411 val goals = |
|
412 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
413 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
|
414 |
|
415 val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) |
|
416 |
|
417 val tac = (Datatype_Aux.indtac induct perm_indnames |
|
418 THEN_ALL_NEW asm_simp_tac simps) 1 |
|
419 in |
|
420 Goal.prove lthy perm_indnames [] goals (K tac) |
|
421 |> Datatype_Aux.split_conj_thm |
|
422 end |
|
423 |
|
424 |
|
425 fun prove_permute_plus induct perm_defs perm_fns lthy = |
|
426 let |
|
427 val p = Free ("p", @{typ perm}) |
|
428 val q = Free ("q", @{typ perm}) |
|
429 val perm_types = map (body_type o fastype_of) perm_fns |
|
430 val perm_indnames = Datatype_Prop.make_tnames perm_types |
|
431 |
|
432 fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq |
|
433 (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) |
|
434 |
|
435 val goals = |
|
436 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
437 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
|
438 |
|
439 val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) |
|
440 |
|
441 val tac = (Datatype_Aux.indtac induct perm_indnames |
|
442 THEN_ALL_NEW asm_simp_tac simps) 1 |
|
443 in |
|
444 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
|
445 |> Datatype_Aux.split_conj_thm |
|
446 end |
|
447 |
|
448 |
|
449 fun mk_perm_eq ty_perm_assoc cnstr = |
|
450 let |
|
451 fun lookup_perm p (ty, arg) = |
|
452 case (AList.lookup (op=) ty_perm_assoc ty) of |
|
453 SOME perm => perm $ p $ arg |
|
454 | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg |
|
455 |
|
456 val p = Free ("p", @{typ perm}) |
|
457 val (arg_tys, ty) = |
|
458 fastype_of cnstr |
|
459 |> strip_type |
|
460 |
|
461 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
|
462 val args = map Free (arg_names ~~ arg_tys) |
|
463 |
|
464 val lhs = lookup_perm p (ty, list_comb (cnstr, args)) |
|
465 val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) |
|
466 |
|
467 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
468 in |
|
469 (Attrib.empty_binding, eq) |
|
470 end |
|
471 |
|
472 |
|
473 fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy = |
|
474 let |
|
475 val perm_fn_names = full_ty_names |
|
476 |> map Long_Name.base_name |
|
477 |> map (prefix "permute_") |
|
478 |
|
479 val perm_fn_types = map perm_ty tys |
|
480 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
|
481 val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names |
|
482 |
|
483 val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs |
|
484 |
|
485 fun tac _ (_, _, simps) = |
|
486 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
|
487 |
|
488 fun morphism phi (fvs, dfs, simps) = |
|
489 (map (Morphism.term phi) fvs, |
|
490 map (Morphism.thm phi) dfs, |
|
491 map (Morphism.thm phi) simps); |
|
492 |
|
493 val ((perm_funs, perm_eq_thms), lthy') = |
|
494 lthy |
|
495 |> Local_Theory.exit_global |
|
496 |> Class.instantiation (full_ty_names, tvs, @{sort pt}) |
|
497 |> Primrec.add_primrec perm_fn_binds perm_eqs |
|
498 |
|
499 val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' |
|
500 val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' |
|
501 in |
|
502 lthy' |
|
503 |> Class.prove_instantiation_exit_result morphism tac |
|
504 (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) |
|
505 ||> Named_Target.theory_init |
|
506 end |
|
507 |
|
508 |
393 end (* structure *) |
509 end (* structure *) |
394 |
510 |