14 val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> |
14 val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> |
15 term list -> term list -> bn_info -> thm list * thm list |
15 term list -> term list -> bn_info -> thm list * thm list |
16 |
16 |
17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
18 thm list -> (thm list * thm list) |
18 thm list -> (thm list * thm list) |
|
19 |
|
20 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
|
21 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
19 |
22 |
20 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
23 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
21 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
24 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
22 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list |
25 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list |
23 val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list |
26 val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list |
337 in |
340 in |
338 Variable.export ctxt' ctxt thms |
341 Variable.export ctxt' ctxt thms |
339 |> `(map mk_simp_rule) |
342 |> `(map mk_simp_rule) |
340 end |
343 end |
341 |
344 |
|
345 |
|
346 (** proof by induction over the alpha-definitions **) |
|
347 |
|
348 fun is_true @{term "Trueprop True"} = true |
|
349 | is_true _ = false |
|
350 |
|
351 fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt = |
|
352 let |
|
353 val arg_tys = map (domain_type o fastype_of) alphas |
|
354 |
|
355 val ((arg_names1, arg_names2), ctxt') = |
|
356 ctxt |
|
357 |> Variable.variant_fixes (replicate (length alphas) "x") |
|
358 ||>> Variable.variant_fixes (replicate (length alphas) "y") |
|
359 |
|
360 val args1 = map2 (curry Free) arg_names1 arg_tys |
|
361 val args2 = map2 (curry Free) arg_names2 arg_tys |
|
362 |
|
363 val true_trms = replicate (length alphas) (K @{term True}) |
|
364 |
|
365 fun apply_all x fs = map (fn f => f x) fs |
|
366 val goal_rhs = |
|
367 group (props @ (alphas ~~ true_trms)) |
|
368 |> map snd |
|
369 |> map2 apply_all (args1 ~~ args2) |
|
370 |> map fold_conj |
|
371 |
|
372 fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2 |
|
373 val goal_lhs = map2 apply_trm_pair alphas (args1 ~~ args2) |
|
374 |
|
375 val goal = |
|
376 (map2 (curry HOLogic.mk_imp) goal_lhs goal_rhs) |
|
377 |> foldr1 HOLogic.mk_conj |
|
378 |> HOLogic.mk_Trueprop |
|
379 in |
|
380 Goal.prove ctxt' [] [] goal |
|
381 (fn {context, ...} => HEADGOAL |
|
382 (DETERM o (rtac alpha_induct_thm) THEN_ALL_NEW (rtac @{thm TrueI} ORELSE' cases_tac context))) |
|
383 |> singleton (ProofContext.export ctxt' ctxt) |
|
384 |> Datatype_Aux.split_conj_thm |
|
385 |> map Datatype_Aux.split_conj_thm |
|
386 |> flat |
|
387 |> map zero_var_indexes |
|
388 |> map (fn th => th RS mp) |
|
389 |> filter_out (is_true o concl_of) |
|
390 end |
342 |
391 |
343 |
392 |
344 (** reflexivity proof for the alphas **) |
393 (** reflexivity proof for the alphas **) |
345 |
394 |
346 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto} |
395 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto} |
414 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
463 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
415 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, |
464 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, |
416 trans_prem_tac pred_names ctxt ] |
465 trans_prem_tac pred_names ctxt ] |
417 end |
466 end |
418 |
467 |
419 fun prove_sym_tac pred_names intros induct ctxt = |
|
420 let |
|
421 val prem_eq_tac = rtac @{thm sym} THEN' atac |
|
422 val prem_unbound_tac = atac |
|
423 |
|
424 val prem_cases_tacs = FIRST' |
|
425 [prem_eq_tac, prem_unbound_tac, prem_bound_tac pred_names ctxt] |
|
426 in |
|
427 HEADGOAL (rtac induct THEN_ALL_NEW |
|
428 (resolve_tac intros THEN_ALL_NEW prem_cases_tacs)) |
|
429 end |
|
430 |
|
431 fun prep_sym_goal alpha_trm (arg1, arg2) = |
|
432 let |
|
433 val lhs = alpha_trm $ arg1 $ arg2 |
|
434 val rhs = alpha_trm $ arg2 $ arg1 |
|
435 in |
|
436 HOLogic.mk_imp (lhs, rhs) |
|
437 end |
|
438 |
|
439 fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt = |
468 fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt = |
440 let |
469 let |
441 val alpha_names = map (fst o dest_Const) alpha_trms |
470 val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms |
442 val arg_tys = |
471 |
443 alpha_trms |
472 fun tac ctxt = |
444 |> map fastype_of |
473 let |
445 |> map domain_type |
474 val alpha_names = map (fst o dest_Const) alpha_trms |
446 val (arg_names1, (arg_names2, ctxt')) = |
475 in |
447 ctxt |
476 resolve_tac alpha_intros THEN_ALL_NEW |
448 |> Variable.variant_fixes (replicate (length arg_tys) "x") |
477 FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names ctxt] |
449 ||> Variable.variant_fixes (replicate (length arg_tys) "y") |
478 end |
450 val args1 = map Free (arg_names1 ~~ arg_tys) |
479 in |
451 val args2 = map Free (arg_names2 ~~ arg_tys) |
480 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt |
452 val goal = HOLogic.mk_Trueprop |
481 end |
453 (foldr1 HOLogic.mk_conj (map2 prep_sym_goal alpha_trms (args1 ~~ args2))) |
|
454 in |
|
455 Goal.prove ctxt' [] [] goal |
|
456 (fn {context,...} => prove_sym_tac alpha_names alpha_intros alpha_induct context) |
|
457 |> singleton (ProofContext.export ctxt' ctxt) |
|
458 |> Datatype_Aux.split_conj_thm |
|
459 |> map (fn th => zero_var_indexes (th RS mp)) |
|
460 end |
|
461 |
|
462 |
482 |
463 |
483 |
464 (** transitivity proof for alphas **) |
484 (** transitivity proof for alphas **) |
465 |
485 |
466 (* applies cases rules and resolves them with the last premise *) |
486 (* applies cases rules and resolves them with the last premise *) |
498 aatac pred_names ctxt, |
518 aatac pred_names ctxt, |
499 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, |
519 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, |
500 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) |
520 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) |
501 end |
521 end |
502 |
522 |
503 fun prove_trans_tac pred_names raw_dt_thms intros induct cases ctxt = |
523 fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt = |
504 let |
524 let |
505 fun all_cases ctxt = |
525 fun all_cases ctxt = |
506 asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) |
526 asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) |
507 THEN' TRY o non_trivial_cases_tac pred_names intros ctxt |
527 THEN' TRY o non_trivial_cases_tac pred_names intros ctxt |
508 in |
528 in |
509 HEADGOAL (rtac induct THEN_ALL_NEW |
529 EVERY' [ rtac @{thm allI}, rtac @{thm impI}, |
510 EVERY' [ rtac @{thm allI}, rtac @{thm impI}, |
530 ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ] |
511 ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]) |
531 end |
512 end |
532 |
513 |
533 fun prep_trans_goal alpha_trm (arg1, arg2) = |
514 fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) = |
534 let |
515 let |
535 val arg_ty = fastype_of arg1 |
516 val lhs = alpha_trm $ arg1 $ arg2 |
|
517 val mid = alpha_trm $ arg2 $ (Bound 0) |
536 val mid = alpha_trm $ arg2 $ (Bound 0) |
518 val rhs = alpha_trm $ arg1 $ (Bound 0) |
537 val rhs = alpha_trm $ arg1 $ (Bound 0) |
519 in |
538 in |
520 HOLogic.mk_imp (lhs, |
539 HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) |
521 HOLogic.all_const arg_ty $ Abs ("z", arg_ty, |
540 end |
522 HOLogic.mk_imp (mid, rhs))) |
|
523 end |
|
524 |
|
525 val norm = @{lemma "A --> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp} |
|
526 |
541 |
527 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = |
542 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = |
528 let |
543 let |
529 val alpha_names = map (fst o dest_Const) alpha_trms |
544 val alpha_names = map (fst o dest_Const) alpha_trms |
530 val arg_tys = |
545 val props = map prep_trans_goal alpha_trms |
531 alpha_trms |
546 val norm = @{lemma "A ==> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp} |
532 |> map fastype_of |
547 in |
533 |> map domain_type |
548 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct |
534 val (arg_names1, (arg_names2, ctxt')) = |
549 (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt |
535 ctxt |
|
536 |> Variable.variant_fixes (replicate (length arg_tys) "x") |
|
537 ||> Variable.variant_fixes (replicate (length arg_tys) "y") |
|
538 val args1 = map Free (arg_names1 ~~ arg_tys) |
|
539 val args2 = map Free (arg_names2 ~~ arg_tys) |
|
540 val goal = HOLogic.mk_Trueprop |
|
541 (foldr1 HOLogic.mk_conj (map2 prep_trans_goal alpha_trms (args1 ~~ args2 ~~ arg_tys))) |
|
542 in |
|
543 Goal.prove ctxt' [] [] goal |
|
544 (fn {context,...} => |
|
545 prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_induct alpha_cases context) |
|
546 |> singleton (ProofContext.export ctxt' ctxt) |
|
547 |> Datatype_Aux.split_conj_thm |
|
548 |> map (fn th => zero_var_indexes (th RS norm)) |
|
549 end |
550 end |
550 |
551 |
551 (* proves the equivp predicate for all alphas *) |
552 (* proves the equivp predicate for all alphas *) |
552 |
553 |
553 val equivp_intro = |
554 val equivp_intro = |
554 @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y z. R x y --> R y z --> R x z|] ==> equivp R" |
555 @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y. R x y --> (!z. R y z --> R x z)|] ==> equivp R" |
555 by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)} |
556 by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)} |
556 |
557 |
557 fun raw_prove_equivp alphas refl symm trans ctxt = |
558 fun raw_prove_equivp alphas refl symm trans ctxt = |
558 let |
559 let |
559 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars |
560 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars |
568 RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) |
569 RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) |
569 end |
570 end |
570 |
571 |
571 |
572 |
572 (* proves that alpha_raw implies alpha_bn *) |
573 (* proves that alpha_raw implies alpha_bn *) |
573 |
|
574 fun is_true @{term "Trueprop True"} = true |
|
575 | is_true _ = false |
|
576 |
574 |
577 fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = |
575 fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = |
578 SUBPROOF (fn {prems, context, ...} => |
576 SUBPROOF (fn {prems, context, ...} => |
579 let |
577 let |
580 val prems' = flat (map Datatype_Aux.split_conj_thm prems) |
578 val prems' = flat (map Datatype_Aux.split_conj_thm prems) |