blanchet@39946: (* Title: HOL/Metis.thy blanchet@39946: Author: Lawrence C. Paulson, Cambridge University Computer Laboratory blanchet@39946: Author: Jia Meng, Cambridge University Computer Laboratory and NICTA blanchet@39946: Author: Jasmin Blanchette, TU Muenchen blanchet@39946: *) blanchet@39946: blanchet@39946: header {* Metis Proof Method *} blanchet@39946: blanchet@39946: theory Metis blanchet@43085: imports ATP blanchet@39946: begin blanchet@39946: wenzelm@56281: declare [[ML_print_depth = 0]] wenzelm@48891: ML_file "~~/src/Tools/Metis/metis.ML" wenzelm@56281: declare [[ML_print_depth = 10]] wenzelm@48891: blanchet@56946: blanchet@45511: subsection {* Literal selection and lambda-lifting helpers *} blanchet@42349: blanchet@42349: definition select :: "'a \ 'a" where blanchet@54148: "select = (\x. x)" blanchet@42349: blanchet@42349: lemma not_atomize: "(\ A \ False) \ Trueprop A" blanchet@42349: by (cut_tac atomize_not [of "\ A"]) simp blanchet@42349: blanchet@42349: lemma atomize_not_select: "(A \ select False) \ Trueprop (\ A)" blanchet@42349: unfolding select_def by (rule atomize_not) blanchet@42349: blanchet@42349: lemma not_atomize_select: "(\ A \ select False) \ Trueprop A" blanchet@42349: unfolding select_def by (rule not_atomize) blanchet@42349: blanchet@42349: lemma select_FalseI: "False \ select False" by simp blanchet@42349: blanchet@45511: definition lambda :: "'a \ 'a" where blanchet@54148: "lambda = (\x. x)" blanchet@45511: blanchet@45511: lemma eq_lambdaI: "x \ y \ x \ lambda y" blanchet@45511: unfolding lambda_def by assumption blanchet@45511: blanchet@42349: blanchet@42349: subsection {* Metis package *} blanchet@42349: wenzelm@48891: ML_file "Tools/Metis/metis_generate.ML" wenzelm@48891: ML_file "Tools/Metis/metis_reconstruct.ML" wenzelm@48891: ML_file "Tools/Metis/metis_tactic.ML" blanchet@39980: blanchet@44651: setup {* Metis_Tactic.setup *} blanchet@39946: blanchet@56946: hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda blanchet@56946: hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI blanchet@56946: fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def blanchet@56946: fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table fAll_table fEx_table blanchet@56946: fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws fimplies_laws blanchet@56946: fequal_laws fAll_law fEx_law lambda_def eq_lambdaI blanchet@45511: blanchet@39946: end