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
     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/lambda_lifting.ML"
    11      "Tools/monomorph.ML"
    12      "Tools/ATP/atp_util.ML"
    13      "Tools/ATP/atp_problem.ML"
    14      "Tools/ATP/atp_proof.ML"
    15      "Tools/ATP/atp_proof_redirect.ML"
    16      ("Tools/ATP/atp_problem_generate.ML")
    17      ("Tools/ATP/atp_proof_reconstruct.ML")
    18      ("Tools/ATP/atp_systems.ML")
    19 begin
    20 
    21 subsection {* Higher-order reasoning helpers *}
    22 
    23 definition fFalse :: bool where [no_atp]:
    24 "fFalse \<longleftrightarrow> False"
    25 
    26 definition fTrue :: bool where [no_atp]:
    27 "fTrue \<longleftrightarrow> True"
    28 
    29 definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
    30 "fNot P \<longleftrightarrow> \<not> P"
    31 
    32 definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    33 "fconj P Q \<longleftrightarrow> P \<and> Q"
    34 
    35 definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    36 "fdisj P Q \<longleftrightarrow> P \<or> Q"
    37 
    38 definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    39 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    40 
    41 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    42 "fequal x y \<longleftrightarrow> (x = y)"
    43 
    44 definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    45 "fAll P \<longleftrightarrow> All P"
    46 
    47 definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    48 "fEx P \<longleftrightarrow> Ex P"
    49 
    50 subsection {* Setup *}
    51 
    52 use "Tools/ATP/atp_problem_generate.ML"
    53 use "Tools/ATP/atp_proof_reconstruct.ML"
    54 use "Tools/ATP/atp_systems.ML"
    55 
    56 setup ATP_Systems.setup
    57 
    58 end