src/HOL/Metis.thy
author blanchet
Tue Dec 07 09:58:56 2010 +0100 (2010-12-07)
changeset 41042 8275f52ac991
parent 39980 f175e482dabe
child 41140 9c68004b8c9d
permissions -rw-r--r--
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
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@41042
    15
     ("Tools/try.ML")
blanchet@39946
    16
begin
blanchet@39946
    17
blanchet@39946
    18
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
blanchet@39946
    19
"fequal X Y \<longleftrightarrow> (X = Y)"
blanchet@39946
    20
blanchet@39946
    21
lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
blanchet@39946
    22
by (simp add: fequal_def)
blanchet@39946
    23
blanchet@39946
    24
lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
blanchet@39946
    25
by (simp add: fequal_def)
blanchet@39946
    26
blanchet@39946
    27
lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
blanchet@39946
    28
by auto
blanchet@39946
    29
blanchet@39946
    30
use "Tools/Metis/metis_translate.ML"
blanchet@39946
    31
use "Tools/Metis/metis_reconstruct.ML"
blanchet@39946
    32
use "Tools/Metis/metis_tactics.ML"
blanchet@39980
    33
blanchet@39980
    34
setup {*
blanchet@39980
    35
  Metis_Reconstruct.setup
blanchet@39980
    36
  #> Metis_Tactics.setup
blanchet@39980
    37
*}
blanchet@39946
    38
blanchet@39953
    39
hide_const (open) fequal
blanchet@39955
    40
hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
blanchet@39953
    41
blanchet@41042
    42
subsection {* Try *}
blanchet@41042
    43
blanchet@41042
    44
use "Tools/try.ML"
blanchet@41042
    45
blanchet@41042
    46
setup {* Try.setup *}
blanchet@41042
    47
blanchet@39946
    48
end