renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
1 (* Title: HOL/Metis.thy
2 Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
3 Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
4 Author: Jasmin Blanchette, TU Muenchen
7 header {* Metis Proof Method *}
11 uses "~~/src/Tools/Metis/metis.ML"
12 ("Tools/Metis/metis_translate.ML")
13 ("Tools/Metis/metis_reconstruct.ML")
14 ("Tools/Metis/metis_tactic.ML")
15 ("Tools/try_methods.ML")
18 subsection {* Literal selection helpers *}
20 definition select :: "'a \<Rightarrow> 'a" where
21 [no_atp]: "select = (\<lambda>x. x)"
23 lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A"
24 by (cut_tac atomize_not [of "\<not> A"]) simp
26 lemma atomize_not_select: "(A \<Longrightarrow> select False) \<equiv> Trueprop (\<not> A)"
27 unfolding select_def by (rule atomize_not)
29 lemma not_atomize_select: "(\<not> A \<Longrightarrow> select False) \<equiv> Trueprop A"
30 unfolding select_def by (rule not_atomize)
32 lemma select_FalseI: "False \<Longrightarrow> select False" by simp
35 subsection {* Metis package *}
37 use "Tools/Metis/metis_translate.ML"
38 use "Tools/Metis/metis_reconstruct.ML"
39 use "Tools/Metis/metis_tactic.ML"
41 setup {* Metis_Tactic.setup *}
43 hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
44 hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
45 fequal_def select_def not_atomize atomize_not_select not_atomize_select
48 subsection {* Try Methods *}
50 use "Tools/try_methods.ML"
52 setup {* Try_Methods.setup *}