30 fun mono_eq_prover ctxt prop = |
30 fun mono_eq_prover ctxt prop = |
31 let |
31 let |
32 val refl_rules = Lifting_Info.get_reflexivity_rules ctxt |
32 val refl_rules = Lifting_Info.get_reflexivity_rules ctxt |
33 val transfer_rules = Transfer.get_transfer_raw ctxt |
33 val transfer_rules = Transfer.get_transfer_raw ctxt |
34 |
34 |
35 fun main_tac (t, i) = |
35 fun main_tac i = (REPEAT_ALL_NEW (DETERM o resolve_tac refl_rules) THEN_ALL_NEW |
36 case HOLogic.dest_Trueprop t of |
36 (REPEAT_ALL_NEW (DETERM o resolve_tac transfer_rules))) i |
37 Const (@{const_name "less_eq"}, _) $ _ $ _ => REPEAT_ALL_NEW (resolve_tac refl_rules) i |
37 in |
38 | _ => REPEAT_ALL_NEW (resolve_tac transfer_rules) i |
38 SOME (Goal.prove ctxt [] [] prop (K (main_tac 1))) |
39 in |
|
40 SOME (Goal.prove ctxt [] [] prop (K (SUBGOAL main_tac 1))) |
|
41 handle ERROR _ => NONE |
39 handle ERROR _ => NONE |
42 end |
40 end |
43 |
41 |
44 fun try_prove_reflexivity ctxt prop = |
42 fun try_prove_reflexivity ctxt prop = |
45 let |
43 let |
456 in |
454 in |
457 fun mk_readable_rsp_thm_eq tm lthy = |
455 fun mk_readable_rsp_thm_eq tm lthy = |
458 let |
456 let |
459 val ctm = cterm_of (Proof_Context.theory_of lthy) tm |
457 val ctm = cterm_of (Proof_Context.theory_of lthy) tm |
460 |
458 |
461 (* This is not very cheap way of getting the rules but we have only few active |
|
462 liftings in the current setting *) |
|
463 fun get_cr_pcr_eqs ctxt = |
|
464 let |
|
465 fun collect (data : Lifting_Info.quotient) l = |
|
466 if is_some (#pcr_info data) |
|
467 then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l) |
|
468 else l |
|
469 val table = Lifting_Info.get_quotients ctxt |
|
470 in |
|
471 Symtab.fold (fn (_, data) => fn l => collect data l) table [] |
|
472 end |
|
473 |
|
474 fun assms_rewr_conv tactic rule ct = |
459 fun assms_rewr_conv tactic rule ct = |
475 let |
460 let |
476 fun prove_extra_assms thm = |
461 fun prove_extra_assms thm = |
477 let |
462 let |
478 val assms = cprems_of thm |
463 val assms = cprems_of thm |
533 | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm |
518 | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm |
534 end |
519 end |
535 |
520 |
536 val unfold_ret_val_invs = Conv.bottom_conv |
521 val unfold_ret_val_invs = Conv.bottom_conv |
537 (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy |
522 (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy |
538 val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy) |
|
539 val unfold_inv_conv = |
523 val unfold_inv_conv = |
540 Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy |
524 Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy |
541 val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv |
525 val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv) |
542 (cr_to_pcr_conv then_conv simp_arrows_conv)) |
|
543 val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} |
526 val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} |
544 val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy |
527 val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy |
545 val beta_conv = Thm.beta_conversion true |
528 val beta_conv = Thm.beta_conversion true |
546 val eq_thm = |
529 val eq_thm = |
547 (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs |
530 (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs |
564 val new_names = Datatype_Prop.make_tnames (all_typs fixed_def_t) |
547 val new_names = Datatype_Prop.make_tnames (all_typs fixed_def_t) |
565 in |
548 in |
566 rename term new_names |
549 rename term new_names |
567 end |
550 end |
568 |
551 |
|
552 (* This is not very cheap way of getting the rules but we have only few active |
|
553 liftings in the current setting *) |
|
554 fun get_cr_pcr_eqs ctxt = |
|
555 let |
|
556 fun collect (data : Lifting_Info.quotient) l = |
|
557 if is_some (#pcr_info data) |
|
558 then ((Thm.symmetric o safe_mk_meta_eq o #pcr_cr_eq o the o #pcr_info) data :: l) |
|
559 else l |
|
560 val table = Lifting_Info.get_quotients ctxt |
|
561 in |
|
562 Symtab.fold (fn (_, data) => fn l => collect data l) table [] |
|
563 end |
|
564 |
569 (* |
565 (* |
570 |
566 |
571 lifting_definition command. It opens a proof of a corresponding respectfulness |
567 lifting_definition command. It opens a proof of a corresponding respectfulness |
572 theorem in a user-friendly, readable form. Then add_lift_def is called internally. |
568 theorem in a user-friendly, readable form. Then add_lift_def is called internally. |
573 |
569 |
578 val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy |
574 val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy |
579 val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw |
575 val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw |
580 val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty) |
576 val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty) |
581 val rty_forced = (domain_type o fastype_of) rsp_rel; |
577 val rty_forced = (domain_type o fastype_of) rsp_rel; |
582 val forced_rhs = force_rty_type lthy rty_forced rhs; |
578 val forced_rhs = force_rty_type lthy rty_forced rhs; |
583 val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs) |
579 val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv |
584 val opt_proven_rsp_thm = try_prove_reflexivity lthy internal_rsp_tm |
580 (Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy))) |
|
581 val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs) |
|
582 |> cterm_of (Proof_Context.theory_of lthy) |
|
583 |> cr_to_pcr_conv |
|
584 |> ` concl_of |
|
585 |>> Logic.dest_equals |
|
586 |>> snd |
|
587 val to_rsp = rsp_prsp_eq RS Drule.equal_elim_rule2 |
|
588 val opt_proven_rsp_thm = try_prove_reflexivity lthy prsp_tm |
585 val par_thms = Attrib.eval_thms lthy par_xthms |
589 val par_thms = Attrib.eval_thms lthy par_xthms |
586 |
590 |
587 fun after_qed internal_rsp_thm lthy = |
591 fun after_qed internal_rsp_thm lthy = |
588 add_lift_def (binding, mx) qty rhs internal_rsp_thm par_thms lthy |
592 add_lift_def (binding, mx) qty rhs (internal_rsp_thm RS to_rsp) par_thms lthy |
589 |
|
590 in |
593 in |
591 case opt_proven_rsp_thm of |
594 case opt_proven_rsp_thm of |
592 SOME thm => Proof.theorem NONE (K (after_qed thm)) [] lthy |
595 SOME thm => Proof.theorem NONE (K (after_qed thm)) [] lthy |
593 | NONE => |
596 | NONE => |
594 let |
597 let |
595 val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy |
598 val readable_rsp_thm_eq = mk_readable_rsp_thm_eq prsp_tm lthy |
596 val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq) |
599 val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq) |
597 val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm |
600 val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm |
598 |
601 |
599 fun after_qed' thm_list lthy = |
602 fun after_qed' thm_list lthy = |
600 let |
603 let |
601 val internal_rsp_thm = Goal.prove lthy [] [] internal_rsp_tm |
604 val internal_rsp_thm = Goal.prove lthy [] [] prsp_tm |
602 (fn {context = ctxt, ...} => |
605 (fn {context = ctxt, ...} => |
603 rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt (hd thm_list) 1) |
606 rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt (hd thm_list) 1) |
604 in |
607 in |
605 after_qed internal_rsp_thm lthy |
608 after_qed internal_rsp_thm lthy |
606 end |
609 end |