src/HOL/Metis.thy
author blanchet
Mon Oct 04 22:51:53 2010 +0200 (2010-10-04)
changeset 39947 f95834c8bb4d
parent 39946 78faa9b31202
child 39953 aa54f347e5e2
permissions -rw-r--r--
tuning
blanchet@39946
     1
(*  Title:      HOL/Metis.thy
blanchet@39946
     2
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
blanchet@39946
     3
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
blanchet@39946
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@39946
     5
*)
blanchet@39946
     6
blanchet@39946
     7
header {* Metis Proof Method *}
blanchet@39946
     8
blanchet@39946
     9
theory Metis
blanchet@39946
    10
imports Meson
blanchet@39946
    11
uses "~~/src/Tools/Metis/metis.ML"
blanchet@39946
    12
     ("Tools/Metis/metis_translate.ML")
blanchet@39946
    13
     ("Tools/Metis/metis_reconstruct.ML")
blanchet@39946
    14
     ("Tools/Metis/metis_tactics.ML")
blanchet@39946
    15
begin
blanchet@39946
    16
blanchet@39946
    17
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
blanchet@39946
    18
"fequal X Y \<longleftrightarrow> (X = Y)"
blanchet@39946
    19
blanchet@39946
    20
lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
blanchet@39946
    21
by (simp add: fequal_def)
blanchet@39946
    22
blanchet@39946
    23
lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
blanchet@39946
    24
by (simp add: fequal_def)
blanchet@39946
    25
blanchet@39946
    26
lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
blanchet@39946
    27
by auto
blanchet@39946
    28
blanchet@39946
    29
use "Tools/Metis/metis_translate.ML"
blanchet@39946
    30
use "Tools/Metis/metis_reconstruct.ML"
blanchet@39946
    31
use "Tools/Metis/metis_tactics.ML"
blanchet@39946
    32
setup Metis_Tactics.setup
blanchet@39946
    33
blanchet@39946
    34
end