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