src/HOL/Metis.thy
author haftmann
Mon Nov 29 13:44:54 2010 +0100 (2010-11-29)
changeset 40815 6e2d17cc0d1d
parent 39980 f175e482dabe
child 41042 8275f52ac991
permissions -rw-r--r--
equivI has replaced equiv.intro
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@39980
    32
blanchet@39980
    33
setup {*
blanchet@39980
    34
  Metis_Reconstruct.setup
blanchet@39980
    35
  #> Metis_Tactics.setup
blanchet@39980
    36
*}
blanchet@39946
    37
blanchet@39953
    38
hide_const (open) fequal
blanchet@39955
    39
hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
blanchet@39953
    40
blanchet@39946
    41
end