683 val intros = safeIs @ hazIs |
683 val intros = safeIs @ hazIs |
684 val elims = map Classical.classical_rule (safeEs @ hazEs) |
684 val elims = map Classical.classical_rule (safeEs @ hazEs) |
685 val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd |
685 val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd |
686 in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end |
686 in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end |
687 |
687 |
|
688 fun all_prefixes_of s = |
|
689 map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1) |
|
690 |
|
691 (* This is a terrible hack. Free variables are sometimes code as "M__" when they |
|
692 are displayed as "M" and we want to avoid clashes with these. But sometimes |
|
693 it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all |
|
694 free variables. In the worse case scenario, where the fact won't be resolved |
|
695 correctly, the user can fix it manually, e.g., by naming the fact in |
|
696 question. Ideally we would need nothing of it, but backticks just don't work |
|
697 with schematic variables. *) |
|
698 fun close_form t = |
|
699 (t, [] |> Term.add_free_names t |> maps all_prefixes_of) |
|
700 |> fold (fn ((s, i), T) => fn (t', taken) => |
|
701 let val s' = Name.variant taken s in |
|
702 (Term.all T $ Abs (s', T, abstract_over (Var ((s, i), T), t')), |
|
703 s' :: taken) |
|
704 end) |
|
705 (Term.add_vars t [] |> sort_wrt (fst o fst)) |
|
706 |> fst |
|
707 |
688 fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths = |
708 fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths = |
689 let |
709 let |
690 val thy = ProofContext.theory_of ctxt |
710 val thy = ProofContext.theory_of ctxt |
691 val global_facts = PureThy.facts_of thy |
711 val global_facts = PureThy.facts_of thy |
692 val local_facts = ProofContext.facts_of ctxt |
712 val local_facts = ProofContext.facts_of ctxt |
697 val (intros, elims, simps) = |
717 val (intros, elims, simps) = |
698 if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then |
718 if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then |
699 clasimpset_rules_of ctxt |
719 clasimpset_rules_of ctxt |
700 else |
720 else |
701 (Termtab.empty, Termtab.empty, Termtab.empty) |
721 (Termtab.empty, Termtab.empty, Termtab.empty) |
702 (* Unnamed nonchained formulas with schematic variables are omitted, because |
|
703 they are rejected by the backticks (`...`) parser for some reason. *) |
|
704 fun is_good_unnamed_local th = |
722 fun is_good_unnamed_local th = |
705 not (Thm.has_name_hint th) andalso |
723 not (Thm.has_name_hint th) andalso |
706 (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) andalso |
|
707 forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals |
724 forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals |
708 val unnamed_locals = |
725 val unnamed_locals = |
709 union Thm.eq_thm (Facts.props local_facts) chained_ths |
726 union Thm.eq_thm (Facts.props local_facts) chained_ths |
710 |> filter is_good_unnamed_local |> map (pair "" o single) |
727 |> filter is_good_unnamed_local |> map (pair "" o single) |
711 val full_space = |
728 val full_space = |
721 I |
738 I |
722 else |
739 else |
723 let |
740 let |
724 val multi = length ths > 1 |
741 val multi = length ths > 1 |
725 fun backquotify th = |
742 fun backquotify th = |
726 "`" ^ Print_Mode.setmp [Print_Mode.input] |
743 "`" ^ Print_Mode.setmp (Print_Mode.input :: |
727 (Syntax.string_of_term ctxt) (prop_of th) ^ "`" |
744 filter (curry (op =) Symbol.xsymbolsN) |
|
745 (print_mode_value ())) |
|
746 (Syntax.string_of_term ctxt) (close_form (prop_of th)) ^ "`" |
728 |> String.translate (fn c => if Char.isPrint c then str c else "") |
747 |> String.translate (fn c => if Char.isPrint c then str c else "") |
729 |> simplify_spaces |
748 |> simplify_spaces |
730 fun check_thms a = |
749 fun check_thms a = |
731 case try (ProofContext.get_thms ctxt) a of |
750 case try (ProofContext.get_thms ctxt) a of |
732 NONE => false |
751 NONE => false |