author | blanchet |
Tue, 07 Dec 2010 09:58:56 +0100 | |
changeset 41042 | 8275f52ac991 |
parent 39980 | f175e482dabe |
child 41140 | 9c68004b8c9d |
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 |
|
10 |
imports Meson |
|
11 |
uses "~~/src/Tools/Metis/metis.ML" |
|
12 |
("Tools/Metis/metis_translate.ML") |
|
13 |
("Tools/Metis/metis_reconstruct.ML") |
|
14 |
("Tools/Metis/metis_tactics.ML") |
|
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
15 |
("Tools/try.ML") |
39946 | 16 |
begin |
17 |
||
18 |
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]: |
|
19 |
"fequal X Y \<longleftrightarrow> (X = Y)" |
|
20 |
||
21 |
lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y" |
|
22 |
by (simp add: fequal_def) |
|
23 |
||
24 |
lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y" |
|
25 |
by (simp add: fequal_def) |
|
26 |
||
27 |
lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y" |
|
28 |
by auto |
|
29 |
||
30 |
use "Tools/Metis/metis_translate.ML" |
|
31 |
use "Tools/Metis/metis_reconstruct.ML" |
|
32 |
use "Tools/Metis/metis_tactics.ML" |
|
39980 | 33 |
|
34 |
setup {* |
|
35 |
Metis_Reconstruct.setup |
|
36 |
#> Metis_Tactics.setup |
|
37 |
*} |
|
39946 | 38 |
|
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39947
diff
changeset
|
39 |
hide_const (open) fequal |
39955 | 40 |
hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal |
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39947
diff
changeset
|
41 |
|
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
42 |
subsection {* Try *} |
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
43 |
|
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
44 |
use "Tools/try.ML" |
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
45 |
|
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
46 |
setup {* Try.setup *} |
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
39980
diff
changeset
|
47 |
|
39946 | 48 |
end |