author | haftmann |
Sun, 26 Feb 2012 15:28:48 +0100 | |
changeset 46689 | f559866a7aa2 |
parent 46641 | 8801a24f9e9a |
child 46950 | d0181abdbdac |
permissions | -rw-r--r-- |
39946 | 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 |
|
5 |
*) |
|
6 |
||
7 |
header {* Metis Proof Method *} |
|
8 |
||
9 |
theory Metis |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43016
diff
changeset
|
10 |
imports ATP |
39946 | 11 |
uses "~~/src/Tools/Metis/metis.ML" |
46320 | 12 |
("Tools/Metis/metis_generate.ML") |
39946 | 13 |
("Tools/Metis/metis_reconstruct.ML") |
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
43085
diff
changeset
|
14 |
("Tools/Metis/metis_tactic.ML") |
46641 | 15 |
("Tools/try0.ML") |
39946 | 16 |
begin |
17 |
||
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
18 |
subsection {* Literal selection and lambda-lifting helpers *} |
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
19 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
20 |
definition select :: "'a \<Rightarrow> 'a" where |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
21 |
[no_atp]: "select = (\<lambda>x. x)" |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
22 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
23 |
lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A" |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
24 |
by (cut_tac atomize_not [of "\<not> A"]) simp |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
25 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
26 |
lemma atomize_not_select: "(A \<Longrightarrow> select False) \<equiv> Trueprop (\<not> A)" |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
27 |
unfolding select_def by (rule atomize_not) |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
28 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
29 |
lemma not_atomize_select: "(\<not> A \<Longrightarrow> select False) \<equiv> Trueprop A" |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
30 |
unfolding select_def by (rule not_atomize) |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
31 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
32 |
lemma select_FalseI: "False \<Longrightarrow> select False" by simp |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
33 |
|
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
34 |
definition lambda :: "'a \<Rightarrow> 'a" where |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
35 |
[no_atp]: "lambda = (\<lambda>x. x)" |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
36 |
|
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
37 |
lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y" |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
38 |
unfolding lambda_def by assumption |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
39 |
|
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
40 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
41 |
subsection {* Metis package *} |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
42 |
|
46320 | 43 |
use "Tools/Metis/metis_generate.ML" |
39946 | 44 |
use "Tools/Metis/metis_reconstruct.ML" |
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
43085
diff
changeset
|
45 |
use "Tools/Metis/metis_tactic.ML" |
39980 | 46 |
|
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
43085
diff
changeset
|
47 |
setup {* Metis_Tactic.setup *} |
39946 | 48 |
|
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
49 |
hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select lambda |
41140
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41042
diff
changeset
|
50 |
hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def |
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
51 |
fequal_def select_def not_atomize atomize_not_select not_atomize_select |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
52 |
select_FalseI lambda_def eq_lambdaI |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
53 |
|
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39947
diff
changeset
|
54 |
|
46641 | 55 |
subsection {* Try0 *} |
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
56 |
|
46641 | 57 |
use "Tools/try0.ML" |
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
58 |
|
46641 | 59 |
setup {* Try0.setup *} |
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
60 |
|
39946 | 61 |
end |