9 sig |
9 sig |
10 val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term |
10 val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term |
11 |
11 |
12 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> |
12 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> |
13 bclause list list list -> term list -> Proof.context -> |
13 bclause list list list -> term list -> Proof.context -> |
14 term list * term list * thm list * thm list * thm * local_theory |
14 term list * term list * thm list * thm list * thm * alpha_result * local_theory |
15 |
15 |
16 val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> |
16 val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> |
17 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
17 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
18 |
18 |
19 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
19 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
20 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
20 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
21 |
21 |
22 val raw_prove_alpha_distincts: Proof.context -> thm list -> thm list -> |
22 val raw_prove_alpha_distincts: Proof.context -> alpha_result -> thm list -> string list -> thm list |
23 term list -> string list -> thm list |
23 val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> thm list -> thm list -> thm list |
24 |
24 val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list |
25 val raw_prove_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
25 val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list |
26 thm list -> thm list |
26 val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list |
27 |
27 val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> |
28 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
28 thm list * thm list |
29 val raw_prove_sym: term list -> thm list -> thm -> thm list -> Proof.context -> thm list |
|
30 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> thm list -> |
|
31 Proof.context -> thm list |
|
32 val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> |
|
33 Proof.context -> thm list * thm list |
|
34 |
|
35 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
29 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
36 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
30 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
37 term list -> thm -> thm list -> Proof.context -> thm list |
31 term list -> thm -> thm list -> Proof.context -> thm list |
38 val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list |
32 val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list |
39 val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list |
33 val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list |
251 |
246 |
252 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
247 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
253 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
248 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
254 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
249 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
255 |
250 |
256 val (alphas, lthy') = Inductive.add_inductive_i |
251 val (alpha_info, lthy') = Inductive.add_inductive_i |
257 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
252 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
258 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
253 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
259 all_alpha_names [] all_alpha_intros [] lthy |
254 all_alpha_names [] all_alpha_intros [] lthy |
260 |
255 |
261 val all_alpha_trms_loc = #preds alphas; |
256 val all_alpha_trms_loc = #preds alpha_info; |
262 val alpha_induct_loc = #raw_induct alphas; |
257 val alpha_raw_induct_loc = #raw_induct alpha_info; |
263 val alpha_intros_loc = #intrs alphas; |
258 val alpha_intros_loc = #intrs alpha_info; |
264 val alpha_cases_loc = #elims alphas; |
259 val alpha_cases_loc = #elims alpha_info; |
265 val phi = ProofContext.export_morphism lthy' lthy; |
260 val phi = ProofContext.export_morphism lthy' lthy; |
266 |
261 |
267 val all_alpha_trms = all_alpha_trms_loc |
262 val all_alpha_trms = all_alpha_trms_loc |
268 |> map (Morphism.term phi) |
263 |> map (Morphism.term phi) |
269 |> map Type.legacy_freeze |
264 |> map Type.legacy_freeze |
270 val alpha_induct = Morphism.thm phi alpha_induct_loc |
265 val alpha_raw_induct = Morphism.thm phi alpha_raw_induct_loc |
271 val alpha_intros = map (Morphism.thm phi) alpha_intros_loc |
266 val alpha_intros = map (Morphism.thm phi) alpha_intros_loc |
272 val alpha_cases = map (Morphism.thm phi) alpha_cases_loc |
267 val alpha_cases = map (Morphism.thm phi) alpha_cases_loc |
273 |
268 |
274 val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms |
269 val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms |
275 in |
270 val alpha_tys = |
276 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
271 alpha_trms |
|
272 |> map fastype_of |
|
273 |> map domain_type |
|
274 |
|
275 val alpha_bn_tys = |
|
276 alpha_bn_trms |
|
277 |> map fastype_of |
|
278 |> map domain_type |
|
279 |
|
280 val alpha_names = map (fst o dest_Const) alpha_trms |
|
281 val alpha_bn_names = map (fst o dest_Const) alpha_bn_trms |
|
282 |
|
283 val alpha_result = AlphaResult |
|
284 {alpha_names = alpha_names, |
|
285 alpha_trms = alpha_trms, |
|
286 alpha_tys = alpha_tys, |
|
287 alpha_bn_names = alpha_bn_names, |
|
288 alpha_bn_trms = alpha_bn_trms, |
|
289 alpha_bn_tys = alpha_bn_tys, |
|
290 alpha_intros = alpha_intros, |
|
291 alpha_cases = alpha_cases, |
|
292 alpha_raw_induct = alpha_raw_induct} |
|
293 in |
|
294 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_raw_induct, alpha_result, lthy') |
277 end |
295 end |
278 |
296 |
279 |
297 |
280 (** induction proofs **) |
298 (** induction proofs **) |
281 |
299 |
383 |
401 |
384 fun distinct_tac cases_thms distinct_thms = |
402 fun distinct_tac cases_thms distinct_thms = |
385 rtac notI THEN' eresolve_tac cases_thms |
403 rtac notI THEN' eresolve_tac cases_thms |
386 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
404 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
387 |
405 |
388 fun raw_prove_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str = |
406 fun raw_prove_alpha_distincts ctxt alpha_result raw_distinct_thms raw_dt_names = |
389 let |
407 let |
390 val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms) |
408 val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result |
391 |
409 |
392 fun mk_alpha_distinct distinct_trm = |
410 val ty_trm_assoc = raw_dt_names ~~ alpha_names |
|
411 |
|
412 fun mk_alpha_distinct raw_distinct_trm = |
393 let |
413 let |
394 val goal = mk_distinct_goal ty_trm_assoc distinct_trm |
414 val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm |
395 in |
415 in |
396 Goal.prove ctxt [] [] goal |
416 Goal.prove ctxt [] [] goal |
397 (K (distinct_tac cases_thms distinct_thms 1)) |
417 (K (distinct_tac alpha_cases raw_distinct_thms 1)) |
398 end |
418 end |
399 in |
419 in |
400 map (mk_alpha_distinct o prop_of) distinct_thms |
420 map (mk_alpha_distinct o prop_of) raw_distinct_thms |
401 end |
421 end |
402 |
422 |
403 |
423 |
404 |
424 |
405 (** produces the alpha_eq_iff simplification rules **) |
425 (** produces the alpha_eq_iff simplification rules **) |
427 in |
447 in |
428 if hyps = [] then HOLogic.mk_Trueprop concl |
448 if hyps = [] then HOLogic.mk_Trueprop concl |
429 else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) |
449 else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) |
430 end; |
450 end; |
431 |
451 |
432 fun raw_prove_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims = |
452 fun raw_prove_alpha_eq_iff ctxt alpha_result raw_distinct_thms raw_inject_thms = |
433 let |
453 let |
|
454 val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result |
|
455 |
434 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
456 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
435 val goals = map mk_alpha_eq_iff_goal thms_imp; |
457 val goals = map mk_alpha_eq_iff_goal thms_imp; |
436 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
458 val tac = alpha_eq_iff_tac (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; |
437 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
459 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
438 in |
460 in |
439 Variable.export ctxt' ctxt thms |
461 Variable.export ctxt' ctxt thms |
440 |> map mk_simp_rule |
462 |> map mk_simp_rule |
441 end |
463 end |
457 asm_full_simp_tac (HOL_ss addsimps prod_simps) ] |
479 asm_full_simp_tac (HOL_ss addsimps prod_simps) ] |
458 in |
480 in |
459 resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac] |
481 resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac] |
460 end |
482 end |
461 |
483 |
462 fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt = |
484 fun raw_prove_refl ctxt alpha_result raw_dt_induct = |
463 let |
485 let |
464 val arg_tys = |
486 val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} = |
465 alpha_trms |
487 alpha_result |
466 |> map fastype_of |
|
467 |> map domain_type |
|
468 |
|
469 val arg_bn_tys = |
|
470 alpha_bns |
|
471 |> map fastype_of |
|
472 |> map domain_type |
|
473 |
488 |
474 val props = |
489 val props = |
475 map (fn (ty, c) => (ty, fn x => c $ x $ x)) |
490 map (fn (ty, c) => (ty, fn x => c $ x $ x)) |
476 ((arg_tys ~~ alpha_trms) @ (arg_bn_tys ~~ alpha_bns)) |
491 ((alpha_tys ~~ alpha_trms) @ (alpha_bn_tys ~~ alpha_bn_trms)) |
477 in |
492 in |
478 induct_prove arg_tys props raw_dt_induct (cases_tac alpha_intros) ctxt |
493 induct_prove alpha_tys props raw_dt_induct (cases_tac alpha_intros) ctxt |
479 end |
494 end |
480 |
495 |
481 |
496 |
482 |
497 |
483 (** symmetry proof for the alphas **) |
498 (** symmetry proof for the alphas **) |
503 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
518 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
504 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
519 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
505 trans_prem_tac pred_names ctxt] |
520 trans_prem_tac pred_names ctxt] |
506 end |
521 end |
507 |
522 |
508 fun raw_prove_sym alpha_trms alpha_intros alpha_induct alpha_eqvt ctxt = |
523 fun raw_prove_sym ctxt alpha_result alpha_eqvt = |
509 let |
524 let |
|
525 val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms, |
|
526 alpha_intros, alpha_raw_induct, ...} = alpha_result |
|
527 |
|
528 val alpha_trms = alpha_trms @ alpha_bn_trms |
|
529 val alpha_names = alpha_names @ alpha_bn_names |
|
530 |
510 val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms |
531 val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms |
511 |
532 |
512 fun tac ctxt = |
533 fun tac ctxt = |
513 let |
534 resolve_tac alpha_intros THEN_ALL_NEW |
514 val alpha_names = map (fst o dest_Const) alpha_trms |
535 FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt] |
515 in |
536 in |
516 resolve_tac alpha_intros THEN_ALL_NEW |
537 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt |
517 FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt] |
|
518 end |
|
519 in |
|
520 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt |
|
521 end |
538 end |
522 |
539 |
523 |
540 |
524 (** transitivity proof for alphas **) |
541 (** transitivity proof for alphas **) |
525 |
542 |
558 aatac pred_names ctxt, |
575 aatac pred_names ctxt, |
559 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
576 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
560 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) |
577 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) |
561 end |
578 end |
562 |
579 |
563 fun prove_trans_tac pred_names raw_dt_thms intros cases alpha_eqvt ctxt = |
580 fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = |
564 let |
581 let |
|
582 val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result |
|
583 val alpha_names = alpha_names @ alpha_bn_names |
|
584 |
565 fun all_cases ctxt = |
585 fun all_cases ctxt = |
566 asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) |
586 asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) |
567 THEN' TRY o non_trivial_cases_tac pred_names intros alpha_eqvt ctxt |
587 THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt |
568 in |
588 in |
569 EVERY' [ rtac @{thm allI}, rtac @{thm impI}, |
589 EVERY' [ rtac @{thm allI}, rtac @{thm impI}, |
570 ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ] |
590 ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ] |
571 end |
591 end |
572 |
592 |
573 fun prep_trans_goal alpha_trm (arg1, arg2) = |
593 fun prep_trans_goal alpha_trm (arg1, arg2) = |
574 let |
594 let |
575 val arg_ty = fastype_of arg1 |
595 val arg_ty = fastype_of arg1 |
577 val rhs = alpha_trm $ arg1 $ (Bound 0) |
597 val rhs = alpha_trm $ arg1 $ (Bound 0) |
578 in |
598 in |
579 HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) |
599 HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) |
580 end |
600 end |
581 |
601 |
582 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases alpha_eqvt ctxt = |
602 fun raw_prove_trans ctxt alpha_result raw_dt_thms alpha_eqvt = |
583 let |
603 let |
584 val alpha_names = map (fst o dest_Const) alpha_trms |
604 val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms, |
|
605 alpha_raw_induct, ...} = alpha_result |
|
606 |
|
607 val alpha_trms = alpha_trms @ alpha_bn_trms |
|
608 |
585 val props = map prep_trans_goal alpha_trms |
609 val props = map prep_trans_goal alpha_trms |
586 in |
610 in |
587 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct |
611 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct |
588 (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases alpha_eqvt) ctxt |
612 (prove_trans_tac alpha_result raw_dt_thms alpha_eqvt) ctxt |
589 end |
613 end |
590 |
614 |
591 |
615 |
592 (** proves the equivp predicate for all alphas **) |
616 (** proves the equivp predicate for all alphas **) |
593 |
617 |
599 |
623 |
600 val transp_def' = |
624 val transp_def' = |
601 @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" |
625 @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" |
602 by (rule eq_reflection, auto simp add: trans_def transp_def)} |
626 by (rule eq_reflection, auto simp add: trans_def transp_def)} |
603 |
627 |
604 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = |
628 fun raw_prove_equivp ctxt alpha_result refl symm trans = |
605 let |
629 let |
|
630 val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result |
|
631 |
606 val refl' = map (fold_rule [reflp_def'] o atomize) refl |
632 val refl' = map (fold_rule [reflp_def'] o atomize) refl |
607 val symm' = map (fold_rule [symp_def'] o atomize) symm |
633 val symm' = map (fold_rule [symp_def'] o atomize) symm |
608 val trans' = map (fold_rule [transp_def'] o atomize) trans |
634 val trans' = map (fold_rule [transp_def'] o atomize) trans |
609 |
635 |
610 fun prep_goal t = |
636 fun prep_goal t = |
611 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
637 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
612 in |
638 in |
613 Goal.prove_multi ctxt [] [] (map prep_goal (alphas @ alpha_bns)) |
639 Goal.prove_multi ctxt [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) |
614 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' |
640 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' |
615 RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) |
641 RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) |
616 |> chop (length alphas) |
642 |> chop (length alpha_trms) |
617 end |
643 end |
618 |
644 |
619 |
645 |
620 (* proves that alpha_raw implies alpha_bn *) |
646 (* proves that alpha_raw implies alpha_bn *) |
621 |
647 |