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 |
|
|
33 |
setup Metis_Tactics.setup
|
|
34 |
|
|
35 |
end
|