src/HOL/ATP_Linkup.thy
author wenzelm
Sat Aug 18 13:32:18 2007 +0200 (2007-08-18)
changeset 24318 2477286fcc7e
parent 24288 4016baca4973
child 24742 73b8b42a36b6
permissions -rw-r--r--
renamed ResAtpMethods.setup;
     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
    11 uses
    12   "Tools/polyhash.ML"
    13   "Tools/res_clause.ML"
    14   ("Tools/res_hol_clause.ML")
    15   ("Tools/res_axioms.ML")
    16   ("Tools/res_reconstruct.ML")
    17   ("Tools/watcher.ML")
    18   ("Tools/res_atp.ML")
    19   ("Tools/res_atp_provers.ML")
    20   ("Tools/res_atp_methods.ML")
    21   "~~/src/Tools/Metis/metis.ML"
    22   ("Tools/metis_tools.ML")
    23 begin
    24 
    25 constdefs
    26   COMBI :: "'a => 'a"
    27     "COMBI P == P"
    28 
    29   COMBK :: "'a => 'b => 'a"
    30     "COMBK P Q == P"
    31 
    32   COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
    33     "COMBB P Q R == P (Q R)"
    34 
    35   COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
    36     "COMBC P Q R == P R Q"
    37 
    38   COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
    39     "COMBS P Q R == P R (Q R)"
    40 
    41   COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
    42     "COMBB' M P Q R == M (P (Q R))"
    43 
    44   COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
    45     "COMBC' M P Q R == M (P R) Q"
    46 
    47   COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
    48     "COMBS' M P Q R == M (P R) (Q R)"
    49 
    50   fequal :: "'a => 'a => bool"
    51     "fequal X Y == (X=Y)"
    52 
    53 lemma fequal_imp_equal: "fequal X Y ==> X=Y"
    54   by (simp add: fequal_def)
    55 
    56 lemma equal_imp_fequal: "X=Y ==> fequal X Y"
    57   by (simp add: fequal_def)
    58 
    59 lemma K_simp: "COMBK P == (%Q. P)"
    60 apply (rule eq_reflection)
    61 apply (rule ext)
    62 apply (simp add: COMBK_def)
    63 done
    64 
    65 lemma I_simp: "COMBI == (%P. P)"
    66 apply (rule eq_reflection)
    67 apply (rule ext)
    68 apply (simp add: COMBI_def)
    69 done
    70 
    71 lemma B_simp: "COMBB P Q == %R. P (Q R)"
    72 apply (rule eq_reflection)
    73 apply (rule ext)
    74 apply (simp add: COMBB_def)
    75 done
    76 
    77 text{*These two represent the equivalence between Boolean equality and iff.
    78 They can't be converted to clauses automatically, as the iff would be
    79 expanded...*}
    80 
    81 lemma iff_positive: "P | Q | P=Q"
    82 by blast
    83 
    84 lemma iff_negative: "~P | ~Q | P=Q"
    85 by blast
    86 
    87 use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
    88 use "Tools/res_hol_clause.ML"  --{*requires the combinators*}
    89 use "Tools/res_reconstruct.ML"
    90 use "Tools/watcher.ML"
    91 use "Tools/res_atp.ML"
    92 
    93 setup ResAxioms.meson_method_setup
    94 
    95 
    96 subsection {* Setup for Vampire, E prover and SPASS *}
    97 
    98 use "Tools/res_atp_provers.ML"
    99 
   100 oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
   101 oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
   102 oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
   103 
   104 use "Tools/res_atp_methods.ML"
   105 setup ResAtpMethods.setup
   106 
   107 
   108 subsection {* The Metis prover *}
   109 
   110 use "Tools/metis_tools.ML"
   111 setup MetisTools.setup
   112 
   113 end