src/HOL/Sledgehammer.thy
changeset 35827 f552152d7747
parent 35826 1590abc3d42a
child 35865 2f8fb5242799
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Sledgehammer.thy	Wed Mar 17 19:37:44 2010 +0100
     1.3 @@ -0,0 +1,130 @@
     1.4 +(*  Title:      HOL/Sledgehammer.thy
     1.5 +    Author:     Lawrence C Paulson
     1.6 +    Author:     Jia Meng, NICTA
     1.7 +    Author:     Fabian Immler, TUM
     1.8 +*)
     1.9 +
    1.10 +header {* Sledgehammer: Isabelle--ATP Linkup *}
    1.11 +
    1.12 +theory Sledgehammer
    1.13 +imports Plain Hilbert_Choice
    1.14 +uses
    1.15 +  "Tools/polyhash.ML"
    1.16 +  "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    1.17 +  ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
    1.18 +  ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
    1.19 +  ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    1.20 +  ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
    1.21 +  ("Tools/ATP_Manager/atp_manager.ML")
    1.22 +  ("Tools/ATP_Manager/atp_wrapper.ML")
    1.23 +  ("Tools/ATP_Manager/atp_minimal.ML")
    1.24 +  "~~/src/Tools/Metis/metis.ML"
    1.25 +  ("Tools/Sledgehammer/metis_tactics.ML")
    1.26 +begin
    1.27 +
    1.28 +definition COMBI :: "'a => 'a"
    1.29 +  where "COMBI P == P"
    1.30 +
    1.31 +definition COMBK :: "'a => 'b => 'a"
    1.32 +  where "COMBK P Q == P"
    1.33 +
    1.34 +definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
    1.35 +  where "COMBB P Q R == P (Q R)"
    1.36 +
    1.37 +definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
    1.38 +  where "COMBC P Q R == P R Q"
    1.39 +
    1.40 +definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
    1.41 +  where "COMBS P Q R == P R (Q R)"
    1.42 +
    1.43 +definition fequal :: "'a => 'a => bool"
    1.44 +  where "fequal X Y == (X=Y)"
    1.45 +
    1.46 +lemma fequal_imp_equal: "fequal X Y ==> X=Y"
    1.47 +  by (simp add: fequal_def)
    1.48 +
    1.49 +lemma equal_imp_fequal: "X=Y ==> fequal X Y"
    1.50 +  by (simp add: fequal_def)
    1.51 +
    1.52 +text{*These two represent the equivalence between Boolean equality and iff.
    1.53 +They can't be converted to clauses automatically, as the iff would be
    1.54 +expanded...*}
    1.55 +
    1.56 +lemma iff_positive: "P | Q | P=Q"
    1.57 +by blast
    1.58 +
    1.59 +lemma iff_negative: "~P | ~Q | P=Q"
    1.60 +by blast
    1.61 +
    1.62 +text{*Theorems for translation to combinators*}
    1.63 +
    1.64 +lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
    1.65 +apply (rule eq_reflection)
    1.66 +apply (rule ext) 
    1.67 +apply (simp add: COMBS_def) 
    1.68 +done
    1.69 +
    1.70 +lemma abs_I: "(%x. x) == COMBI"
    1.71 +apply (rule eq_reflection)
    1.72 +apply (rule ext) 
    1.73 +apply (simp add: COMBI_def) 
    1.74 +done
    1.75 +
    1.76 +lemma abs_K: "(%x. y) == COMBK y"
    1.77 +apply (rule eq_reflection)
    1.78 +apply (rule ext) 
    1.79 +apply (simp add: COMBK_def) 
    1.80 +done
    1.81 +
    1.82 +lemma abs_B: "(%x. a (g x)) == COMBB a g"
    1.83 +apply (rule eq_reflection)
    1.84 +apply (rule ext) 
    1.85 +apply (simp add: COMBB_def) 
    1.86 +done
    1.87 +
    1.88 +lemma abs_C: "(%x. (f x) b) == COMBC f b"
    1.89 +apply (rule eq_reflection)
    1.90 +apply (rule ext) 
    1.91 +apply (simp add: COMBC_def) 
    1.92 +done
    1.93 +
    1.94 +
    1.95 +subsection {* Setup of external ATPs *}
    1.96 +
    1.97 +use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
    1.98 +setup Sledgehammer_Fact_Preprocessor.setup
    1.99 +use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
   1.100 +use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
   1.101 +setup Sledgehammer_Proof_Reconstruct.setup
   1.102 +use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
   1.103 +
   1.104 +use "Tools/ATP_Manager/atp_wrapper.ML"
   1.105 +setup ATP_Wrapper.setup
   1.106 +use "Tools/ATP_Manager/atp_manager.ML"
   1.107 +use "Tools/ATP_Manager/atp_minimal.ML"
   1.108 +
   1.109 +text {* basic provers *}
   1.110 +setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
   1.111 +setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
   1.112 +setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
   1.113 +
   1.114 +text {* provers with stuctured output *}
   1.115 +setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
   1.116 +setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
   1.117 +
   1.118 +text {* on some problems better results *}
   1.119 +setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
   1.120 +
   1.121 +text {* remote provers via SystemOnTPTP *}
   1.122 +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
   1.123 +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
   1.124 +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
   1.125 +  
   1.126 +
   1.127 +
   1.128 +subsection {* The Metis prover *}
   1.129 +
   1.130 +use "Tools/Sledgehammer/metis_tactics.ML"
   1.131 +setup Metis_Tactics.setup
   1.132 +
   1.133 +end