src/HOL/ATP.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 44087 8e491cb8841c
child 45522 3b951bbd2bee
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
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@44087
    10
uses "Tools/lambda_lifting.ML"
blanchet@44087
    11
     "Tools/monomorph.ML"
blanchet@43108
    12
     "Tools/ATP/atp_util.ML"
blanchet@43085
    13
     "Tools/ATP/atp_problem.ML"
blanchet@40178
    14
     "Tools/ATP/atp_proof.ML"
blanchet@40178
    15
     "Tools/ATP/atp_systems.ML"
blanchet@43085
    16
     ("Tools/ATP/atp_translate.ML")
blanchet@43085
    17
     ("Tools/ATP/atp_reconstruct.ML")
blanchet@39951
    18
begin
blanchet@39951
    19
blanchet@43085
    20
subsection {* Higher-order reasoning helpers *}
blanchet@43085
    21
blanchet@43085
    22
definition fFalse :: bool where [no_atp]:
blanchet@43085
    23
"fFalse \<longleftrightarrow> False"
blanchet@43085
    24
blanchet@43085
    25
definition fTrue :: bool where [no_atp]:
blanchet@43085
    26
"fTrue \<longleftrightarrow> True"
blanchet@43085
    27
blanchet@43085
    28
definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
blanchet@43085
    29
"fNot P \<longleftrightarrow> \<not> P"
blanchet@43085
    30
blanchet@43085
    31
definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
blanchet@43085
    32
"fconj P Q \<longleftrightarrow> P \<and> Q"
blanchet@43085
    33
blanchet@43085
    34
definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
blanchet@43085
    35
"fdisj P Q \<longleftrightarrow> P \<or> Q"
blanchet@43085
    36
blanchet@43085
    37
definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
blanchet@43085
    38
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
blanchet@43085
    39
blanchet@43085
    40
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
blanchet@43085
    41
"fequal x y \<longleftrightarrow> (x = y)"
blanchet@43085
    42
nik@43678
    43
definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
nik@43678
    44
"fAll P \<longleftrightarrow> All P"
nik@43678
    45
nik@43678
    46
definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
nik@43678
    47
"fEx P \<longleftrightarrow> Ex P"
blanchet@43085
    48
blanchet@43085
    49
subsection {* Setup *}
blanchet@43085
    50
blanchet@43085
    51
use "Tools/ATP/atp_translate.ML"
blanchet@43085
    52
use "Tools/ATP/atp_reconstruct.ML"
blanchet@43085
    53
blanchet@39951
    54
setup ATP_Systems.setup
blanchet@39951
    55
blanchet@39951
    56
end