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