author | hoelzl |
Mon, 03 Dec 2012 18:19:08 +0100 | |
changeset 50328 | 25b1e8686ce0 |
parent 48891 | c0eafbd55de3 |
child 52641 | c56b6fa636e8 |
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 |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46641
diff
changeset
|
11 |
keywords "try0" :: diag |
39946 | 12 |
begin |
13 |
||
48891 | 14 |
ML_file "~~/src/Tools/Metis/metis.ML" |
15 |
||
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
16 |
subsection {* Literal selection and lambda-lifting helpers *} |
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
17 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
18 |
definition select :: "'a \<Rightarrow> 'a" where |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
19 |
[no_atp]: "select = (\<lambda>x. x)" |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
20 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
21 |
lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A" |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
22 |
by (cut_tac atomize_not [of "\<not> A"]) simp |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
23 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
24 |
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
|
25 |
unfolding select_def by (rule atomize_not) |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
26 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
27 |
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
|
28 |
unfolding select_def by (rule not_atomize) |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
29 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
30 |
lemma select_FalseI: "False \<Longrightarrow> select False" by simp |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
31 |
|
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
32 |
definition lambda :: "'a \<Rightarrow> 'a" where |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
33 |
[no_atp]: "lambda = (\<lambda>x. x)" |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
34 |
|
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
35 |
lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y" |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
36 |
unfolding lambda_def by assumption |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
37 |
|
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
38 |
|
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
39 |
subsection {* Metis package *} |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
41140
diff
changeset
|
40 |
|
48891 | 41 |
ML_file "Tools/Metis/metis_generate.ML" |
42 |
ML_file "Tools/Metis/metis_reconstruct.ML" |
|
43 |
ML_file "Tools/Metis/metis_tactic.ML" |
|
39980 | 44 |
|
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 |
setup {* Metis_Tactic.setup *} |
39946 | 46 |
|
47946
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
46950
diff
changeset
|
47 |
hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
46950
diff
changeset
|
48 |
lambda |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
46950
diff
changeset
|
49 |
hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
46950
diff
changeset
|
50 |
select_FalseI fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
46950
diff
changeset
|
51 |
fequal_def fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
46950
diff
changeset
|
52 |
fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws |
33afcfad3f8d
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents:
46950
diff
changeset
|
53 |
fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
44651
diff
changeset
|
54 |
|
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39947
diff
changeset
|
55 |
|
46641 | 56 |
subsection {* Try0 *} |
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
57 |
|
48891 | 58 |
ML_file "Tools/try0.ML" |
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 |