src/HOL/Metis.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 41140 9c68004b8c9d
child 42349 721e85fd2db3
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
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@41140
    18
definition fFalse :: bool where [no_atp]:
blanchet@41140
    19
"fFalse \<longleftrightarrow> False"
blanchet@39946
    20
blanchet@41140
    21
definition fTrue :: bool where [no_atp]:
blanchet@41140
    22
"fTrue \<longleftrightarrow> True"
blanchet@41140
    23
blanchet@41140
    24
definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
blanchet@41140
    25
"fNot P \<longleftrightarrow> \<not> P"
blanchet@39946
    26
blanchet@41140
    27
definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
blanchet@41140
    28
"fconj P Q \<longleftrightarrow> P \<and> Q"
blanchet@41140
    29
blanchet@41140
    30
definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
blanchet@41140
    31
"fdisj P Q \<longleftrightarrow> P \<or> Q"
blanchet@39946
    32
blanchet@41140
    33
definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
blanchet@41140
    34
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
blanchet@41140
    35
blanchet@41140
    36
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
blanchet@41140
    37
"fequal x y \<longleftrightarrow> (x = y)"
blanchet@39946
    38
blanchet@39946
    39
use "Tools/Metis/metis_translate.ML"
blanchet@39946
    40
use "Tools/Metis/metis_reconstruct.ML"
blanchet@39946
    41
use "Tools/Metis/metis_tactics.ML"
blanchet@39980
    42
blanchet@39980
    43
setup {*
blanchet@39980
    44
  Metis_Reconstruct.setup
blanchet@39980
    45
  #> Metis_Tactics.setup
blanchet@39980
    46
*}
blanchet@39946
    47
blanchet@41140
    48
hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal
blanchet@41140
    49
hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
blanchet@41140
    50
                 fequal_def
blanchet@39953
    51
blanchet@41042
    52
subsection {* Try *}
blanchet@41042
    53
blanchet@41042
    54
use "Tools/try.ML"
blanchet@41042
    55
blanchet@41042
    56
setup {* Try.setup *}
blanchet@41042
    57
blanchet@39946
    58
end