src/HOL/ATP_Linkup.thy
author paulson
Thu Sep 27 17:55:28 2007 +0200 (2007-09-27)
changeset 24742 73b8b42a36b6
parent 24318 2477286fcc7e
child 24819 7d8e0a47392e
permissions -rw-r--r--
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
theorems of Nat.thy are hidden by the Ordering.thy versions
     1 (*  Title:      HOL/ATP_Linkup.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Author:     Jia Meng, NICTA
     5 *)
     6 
     7 header{* The Isabelle-ATP Linkup *}
     8 
     9 theory ATP_Linkup
    10 imports Divides Record Hilbert_Choice Presburger Relation_Power SAT Recdef Extraction 
    11    (*It must be a parent or a child of every other theory, to prevent theory-merge errors.*)
    12 uses
    13   "Tools/polyhash.ML"
    14   "Tools/res_clause.ML"
    15   ("Tools/res_hol_clause.ML")
    16   ("Tools/res_axioms.ML")
    17   ("Tools/res_reconstruct.ML")
    18   ("Tools/watcher.ML")
    19   ("Tools/res_atp.ML")
    20   ("Tools/res_atp_provers.ML")
    21   ("Tools/res_atp_methods.ML")
    22   "~~/src/Tools/Metis/metis.ML"
    23   ("Tools/metis_tools.ML")
    24 begin
    25 
    26 constdefs
    27   COMBI :: "'a => 'a"
    28     "COMBI P == P"
    29 
    30   COMBK :: "'a => 'b => 'a"
    31     "COMBK P Q == P"
    32 
    33   COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
    34     "COMBB P Q R == P (Q R)"
    35 
    36   COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
    37     "COMBC P Q R == P R Q"
    38 
    39   COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
    40     "COMBS P Q R == P R (Q R)"
    41 
    42   COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
    43     "COMBB' M P Q R == M (P (Q R))"
    44 
    45   COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
    46     "COMBC' M P Q R == M (P R) Q"
    47 
    48   COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
    49     "COMBS' M P Q R == M (P R) (Q R)"
    50 
    51   fequal :: "'a => 'a => bool"
    52     "fequal X Y == (X=Y)"
    53 
    54 lemma fequal_imp_equal: "fequal X Y ==> X=Y"
    55   by (simp add: fequal_def)
    56 
    57 lemma equal_imp_fequal: "X=Y ==> fequal X Y"
    58   by (simp add: fequal_def)
    59 
    60 lemma K_simp: "COMBK P == (%Q. P)"
    61 apply (rule eq_reflection)
    62 apply (rule ext)
    63 apply (simp add: COMBK_def)
    64 done
    65 
    66 lemma I_simp: "COMBI == (%P. P)"
    67 apply (rule eq_reflection)
    68 apply (rule ext)
    69 apply (simp add: COMBI_def)
    70 done
    71 
    72 lemma B_simp: "COMBB P Q == %R. P (Q R)"
    73 apply (rule eq_reflection)
    74 apply (rule ext)
    75 apply (simp add: COMBB_def)
    76 done
    77 
    78 text{*These two represent the equivalence between Boolean equality and iff.
    79 They can't be converted to clauses automatically, as the iff would be
    80 expanded...*}
    81 
    82 lemma iff_positive: "P | Q | P=Q"
    83 by blast
    84 
    85 lemma iff_negative: "~P | ~Q | P=Q"
    86 by blast
    87 
    88 use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
    89 use "Tools/res_hol_clause.ML"  --{*requires the combinators*}
    90 use "Tools/res_reconstruct.ML"
    91 use "Tools/watcher.ML"
    92 use "Tools/res_atp.ML"
    93 
    94 setup ResAxioms.meson_method_setup
    95 
    96 
    97 subsection {* Setup for Vampire, E prover and SPASS *}
    98 
    99 use "Tools/res_atp_provers.ML"
   100 
   101 oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
   102 oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
   103 oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
   104 
   105 use "Tools/res_atp_methods.ML"
   106 setup ResAtpMethods.setup
   107 
   108 
   109 subsection {* The Metis prover *}
   110 
   111 use "Tools/metis_tools.ML"
   112 setup MetisTools.setup
   113 
   114 (*Sledgehammer*)
   115 setup ResAxioms.setup
   116 
   117 setup {*
   118   Theory.at_end ResAxioms.clause_cache_endtheory
   119 *}
   120 
   121 end