src/HOL/ATP.thy
author blanchet
Tue May 31 16:38:36 2011 +0200 (2011-05-31)
changeset 43108 eb1e31eb7449
parent 43085 0a2f5b86bdd7
child 43678 56d352659500
permissions -rw-r--r--
use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
     1 (*  Title:      HOL/ATP.thy
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 *)
     5 
     6 header {* Automatic Theorem Provers (ATPs) *}
     7 
     8 theory ATP
     9 imports Meson
    10 uses "Tools/monomorph.ML"
    11      "Tools/ATP/atp_util.ML"
    12      "Tools/ATP/atp_problem.ML"
    13      "Tools/ATP/atp_proof.ML"
    14      "Tools/ATP/atp_systems.ML"
    15      ("Tools/ATP/atp_translate.ML")
    16      ("Tools/ATP/atp_reconstruct.ML")
    17 begin
    18 
    19 subsection {* Higher-order reasoning helpers *}
    20 
    21 definition fFalse :: bool where [no_atp]:
    22 "fFalse \<longleftrightarrow> False"
    23 
    24 definition fTrue :: bool where [no_atp]:
    25 "fTrue \<longleftrightarrow> True"
    26 
    27 definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
    28 "fNot P \<longleftrightarrow> \<not> P"
    29 
    30 definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    31 "fconj P Q \<longleftrightarrow> P \<and> Q"
    32 
    33 definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    34 "fdisj P Q \<longleftrightarrow> P \<or> Q"
    35 
    36 definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    37 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    38 
    39 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    40 "fequal x y \<longleftrightarrow> (x = y)"
    41 
    42 
    43 subsection {* Setup *}
    44 
    45 use "Tools/ATP/atp_translate.ML"
    46 use "Tools/ATP/atp_reconstruct.ML"
    47 
    48 setup ATP_Systems.setup
    49 
    50 end