author | blanchet |
Tue, 05 Oct 2010 12:04:49 +0200 | |
changeset 39955 | cb9cac7eba29 |
parent 39953 | aa54f347e5e2 |
child 39980 | f175e482dabe |
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" |
|
32 |
setup Metis_Tactics.setup |
|
33 |
||
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39947
diff
changeset
|
34 |
hide_const (open) fequal |
39955 | 35 |
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
|
36 |
|
39946 | 37 |
end |