| author | blanchet |
| Mon, 11 Oct 2010 18:03:47 +0700 | |
| changeset 39980 | f175e482dabe |
| parent 39955 | cb9cac7eba29 |
| child 41042 | 8275f52ac991 |
| 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")
|
|
15 |
begin |
|
16 |
||
17 |
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]: |
|
18 |
"fequal X Y \<longleftrightarrow> (X = Y)" |
|
19 |
||
20 |
lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y" |
|
21 |
by (simp add: fequal_def) |
|
22 |
||
23 |
lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y" |
|
24 |
by (simp add: fequal_def) |
|
25 |
||
26 |
lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y" |
|
27 |
by auto |
|
28 |
||
29 |
use "Tools/Metis/metis_translate.ML" |
|
30 |
use "Tools/Metis/metis_reconstruct.ML" |
|
31 |
use "Tools/Metis/metis_tactics.ML" |
|
| 39980 | 32 |
|
33 |
setup {*
|
|
34 |
Metis_Reconstruct.setup |
|
35 |
#> Metis_Tactics.setup |
|
36 |
*} |
|
| 39946 | 37 |
|
|
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39947
diff
changeset
|
38 |
hide_const (open) fequal |
| 39955 | 39 |
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
|
40 |
|
| 39946 | 41 |
end |