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
     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 {*
    34   Metis_Reconstruct.setup
    35   #> Metis_Tactics.setup
    36 *}
    37 
    38 hide_const (open) fequal
    39 hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
    40 
    41 end