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