128 (@{const_name Meson.COMBS}, "COMBS"), |
129 (@{const_name Meson.COMBS}, "COMBS"), |
129 (@{const_name If}, "If")] |
130 (@{const_name If}, "If")] |
130 |
131 |
131 (* Invert the table of translations between Isabelle and ATPs. *) |
132 (* Invert the table of translations between Isabelle and ATPs. *) |
132 val const_trans_table_inv = |
133 val const_trans_table_inv = |
133 Symtab.update ("fequal", @{const_name HOL.eq}) |
134 const_trans_table |> Symtab.dest |> map swap |> Symtab.make |
134 (Symtab.make (map swap (Symtab.dest const_trans_table))) |
135 |> fold Symtab.update [("fFalse", @{const_name False}), |
|
136 ("fTrue", @{const_name True}), |
|
137 ("fNot", @{const_name Not}), |
|
138 ("fconj", @{const_name conj}), |
|
139 ("fdisj", @{const_name disj}), |
|
140 ("fimplies", @{const_name implies}), |
|
141 ("fequal", @{const_name HOL.eq})] |
135 |
142 |
136 val invert_const = perhaps (Symtab.lookup const_trans_table_inv) |
143 val invert_const = perhaps (Symtab.lookup const_trans_table_inv) |
137 |
144 |
138 (*Escaping of special characters. |
145 (*Escaping of special characters. |
139 Alphanumeric characters are left unchanged. |
146 Alphanumeric characters are left unchanged. |
658 (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [], |
665 (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [], |
659 old_skolems) |
666 old_skolems) |
660 end |
667 end |
661 end; |
668 end; |
662 |
669 |
663 val helpers = |
670 val metis_helpers = |
664 [("c_COMBI", (false, @{thms Meson.COMBI_def})), |
671 [("c_COMBI", (false, @{thms Meson.COMBI_def})), |
665 ("c_COMBK", (false, @{thms Meson.COMBK_def})), |
672 ("c_COMBK", (false, @{thms Meson.COMBK_def})), |
666 ("c_COMBB", (false, @{thms Meson.COMBB_def})), |
673 ("c_COMBB", (false, @{thms Meson.COMBB_def})), |
667 ("c_COMBC", (false, @{thms Meson.COMBC_def})), |
674 ("c_COMBC", (false, @{thms Meson.COMBC_def})), |
668 ("c_COMBS", (false, @{thms Meson.COMBS_def})), |
675 ("c_COMBS", (false, @{thms Meson.COMBS_def})), |
669 ("c_fequal", |
676 ("c_fequal", |
670 (false, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] |
677 (false, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] |
671 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), |
678 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), |
672 ("c_fFalse", (true, [@{lemma "x = fTrue | x = fFalse" |
679 ("c_fFalse", (true, [@{lemma "x = fTrue | x = fFalse" |
673 by (unfold Metis.fFalse_def Metis.fTrue_def) fast}])), |
680 by (unfold fFalse_def fTrue_def) fast}])), |
674 ("c_fFalse", (false, [@{lemma "~ fFalse" |
681 ("c_fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])), |
675 by (unfold Metis.fFalse_def) fast}])), |
|
676 ("c_fTrue", (true, [@{lemma "x = fTrue | x = fFalse" |
682 ("c_fTrue", (true, [@{lemma "x = fTrue | x = fFalse" |
677 by (unfold Metis.fFalse_def Metis.fTrue_def) fast}])), |
683 by (unfold fFalse_def fTrue_def) fast}])), |
678 ("c_fTrue", (false, [@{lemma "fTrue" |
684 ("c_fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])), |
679 by (unfold Metis.fTrue_def) fast}])), |
|
680 ("c_fNot", |
685 ("c_fNot", |
681 (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] |
686 (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] |
682 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), |
687 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), |
683 ("c_fconj", |
688 ("c_fconj", |
684 (false, @{lemma "~ P | ~ Q | Metis.fconj P Q" |
689 (false, @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" |
685 "~ Metis.fconj P Q | P" |
690 by (unfold fconj_def) fast+})), |
686 "~ Metis.fconj P Q | Q" |
|
687 by (unfold Metis.fconj_def) fast+})), |
|
688 ("c_fdisj", |
691 ("c_fdisj", |
689 (false, @{lemma "~ P | Metis.fdisj P Q" |
692 (false, @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" |
690 "~ Q | Metis.fdisj P Q" |
693 by (unfold fdisj_def) fast+})), |
691 "~ Metis.fdisj P Q | P | Q" |
|
692 by (unfold Metis.fdisj_def) fast+})), |
|
693 ("c_fimplies", |
694 ("c_fimplies", |
694 (false, @{lemma "P | Metis.fimplies P Q" |
695 (false, @{lemma "P | Metis.fimplies P Q" |
695 "~ Q | Metis.fimplies P Q" |
696 "~ Q | Metis.fimplies P Q" |
696 "~ Metis.fimplies P Q | ~ P | Q" |
697 "~ Metis.fimplies P Q | ~ P | Q" |
697 by (unfold Metis.fimplies_def) fast+})), |
698 by (unfold Metis.fimplies_def) fast+})), |
799 val prepare_helper = |
800 val prepare_helper = |
800 zero_var_indexes |
801 zero_var_indexes |
801 #> `(Meson.make_meta_clause |
802 #> `(Meson.make_meta_clause |
802 #> rewrite_rule (map safe_mk_meta_eq fdefs)) |
803 #> rewrite_rule (map safe_mk_meta_eq fdefs)) |
803 val helper_ths = |
804 val helper_ths = |
804 helpers |> filter (is_used o fst) |
805 metis_helpers |
805 |> maps (fn (c, (needs_full_types, thms)) => |
806 |> filter (is_used o fst) |
806 if needs_full_types andalso mode <> FT then [] |
807 |> maps (fn (c, (needs_full_types, thms)) => |
807 else map prepare_helper thms) |
808 if needs_full_types andalso mode <> FT then [] |
|
809 else map prepare_helper thms) |
808 in lmap |> fold (add_thm false) helper_ths end |
810 in lmap |> fold (add_thm false) helper_ths end |
809 in |
811 in |
810 (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap) |
812 (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap) |
811 end |
813 end |
812 |
814 |