src/HOL/ATP.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 46320 0b8b73b49848
child 47946 33afcfad3f8d
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
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@46320
    15
     "Tools/ATP/atp_proof_redirect.ML"
blanchet@46320
    16
     ("Tools/ATP/atp_problem_generate.ML")
blanchet@46320
    17
     ("Tools/ATP/atp_proof_reconstruct.ML")
blanchet@45522
    18
     ("Tools/ATP/atp_systems.ML")
blanchet@39951
    19
begin
blanchet@39951
    20
blanchet@43085
    21
subsection {* Higher-order reasoning helpers *}
blanchet@43085
    22
blanchet@43085
    23
definition fFalse :: bool where [no_atp]:
blanchet@43085
    24
"fFalse \<longleftrightarrow> False"
blanchet@43085
    25
blanchet@43085
    26
definition fTrue :: bool where [no_atp]:
blanchet@43085
    27
"fTrue \<longleftrightarrow> True"
blanchet@43085
    28
blanchet@43085
    29
definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
blanchet@43085
    30
"fNot P \<longleftrightarrow> \<not> P"
blanchet@43085
    31
blanchet@43085
    32
definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
blanchet@43085
    33
"fconj P Q \<longleftrightarrow> P \<and> Q"
blanchet@43085
    34
blanchet@43085
    35
definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
blanchet@43085
    36
"fdisj P Q \<longleftrightarrow> P \<or> Q"
blanchet@43085
    37
blanchet@43085
    38
definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
blanchet@43085
    39
"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
blanchet@43085
    40
blanchet@43085
    41
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
blanchet@43085
    42
"fequal x y \<longleftrightarrow> (x = y)"
blanchet@43085
    43
nik@43678
    44
definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
nik@43678
    45
"fAll P \<longleftrightarrow> All P"
nik@43678
    46
nik@43678
    47
definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
nik@43678
    48
"fEx P \<longleftrightarrow> Ex P"
blanchet@43085
    49
blanchet@43085
    50
subsection {* Setup *}
blanchet@43085
    51
blanchet@46320
    52
use "Tools/ATP/atp_problem_generate.ML"
blanchet@46320
    53
use "Tools/ATP/atp_proof_reconstruct.ML"
blanchet@45522
    54
use "Tools/ATP/atp_systems.ML"
blanchet@43085
    55
blanchet@39951
    56
setup ATP_Systems.setup
blanchet@39951
    57
blanchet@39951
    58
end