src/HOL/Sledgehammer.thy
changeset 35865 2f8fb5242799
parent 35827 f552152d7747
child 35866 513074557e06
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Mar 19 06:14:37 2010 +0100
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Mar 19 13:02:18 2010 +0100
     1.3 @@ -1,7 +1,8 @@
     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 +    Author:     Fabian Immler, TU Muenchen
     1.9 +    Author:     Jasmin Blanchette, TU Muenchen
    1.10  *)
    1.11  
    1.12  header {* Sledgehammer: Isabelle--ATP Linkup *}
    1.13 @@ -10,7 +11,8 @@
    1.14  imports Plain Hilbert_Choice
    1.15  uses
    1.16    "Tools/polyhash.ML"
    1.17 -  "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    1.18 +  "~~/src/Tools/Metis/metis.ML"
    1.19 +  ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
    1.20    ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
    1.21    ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
    1.22    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    1.23 @@ -18,79 +20,79 @@
    1.24    ("Tools/ATP_Manager/atp_manager.ML")
    1.25    ("Tools/ATP_Manager/atp_wrapper.ML")
    1.26    ("Tools/ATP_Manager/atp_minimal.ML")
    1.27 -  "~~/src/Tools/Metis/metis.ML"
    1.28 +  ("Tools/Sledgehammer/meson_tactic.ML")
    1.29    ("Tools/Sledgehammer/metis_tactics.ML")
    1.30  begin
    1.31  
    1.32 -definition COMBI :: "'a => 'a"
    1.33 -  where "COMBI P == P"
    1.34 +definition COMBI :: "'a \<Rightarrow> 'a"
    1.35 +  where "COMBI P \<equiv> P"
    1.36  
    1.37 -definition COMBK :: "'a => 'b => 'a"
    1.38 -  where "COMBK P Q == P"
    1.39 +definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
    1.40 +  where "COMBK P Q \<equiv> P"
    1.41  
    1.42 -definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
    1.43 -  where "COMBB P Q R == P (Q R)"
    1.44 +definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.45 +  where "COMBB P Q R \<equiv> P (Q R)"
    1.46  
    1.47 -definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
    1.48 -  where "COMBC P Q R == P R Q"
    1.49 +definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
    1.50 +  where "COMBC P Q R \<equiv> P R Q"
    1.51  
    1.52 -definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
    1.53 -  where "COMBS P Q R == P R (Q R)"
    1.54 +definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.55 +  where "COMBS P Q R \<equiv> P R (Q R)"
    1.56  
    1.57 -definition fequal :: "'a => 'a => bool"
    1.58 -  where "fequal X Y == (X=Y)"
    1.59 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.60 +  where "fequal X Y \<equiv> (X = Y)"
    1.61  
    1.62 -lemma fequal_imp_equal: "fequal X Y ==> X=Y"
    1.63 +lemma fequal_imp_equal: "fequal X Y \<Longrightarrow> X = Y"
    1.64    by (simp add: fequal_def)
    1.65  
    1.66 -lemma equal_imp_fequal: "X=Y ==> fequal X Y"
    1.67 +lemma equal_imp_fequal: "X = Y \<Longrightarrow> fequal X Y"
    1.68    by (simp add: fequal_def)
    1.69  
    1.70  text{*These two represent the equivalence between Boolean equality and iff.
    1.71  They can't be converted to clauses automatically, as the iff would be
    1.72  expanded...*}
    1.73  
    1.74 -lemma iff_positive: "P | Q | P=Q"
    1.75 +lemma iff_positive: "P \<or> Q \<or> P = Q"
    1.76  by blast
    1.77  
    1.78 -lemma iff_negative: "~P | ~Q | P=Q"
    1.79 +lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
    1.80  by blast
    1.81  
    1.82  text{*Theorems for translation to combinators*}
    1.83  
    1.84 -lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
    1.85 +lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
    1.86  apply (rule eq_reflection)
    1.87  apply (rule ext) 
    1.88  apply (simp add: COMBS_def) 
    1.89  done
    1.90  
    1.91 -lemma abs_I: "(%x. x) == COMBI"
    1.92 +lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
    1.93  apply (rule eq_reflection)
    1.94  apply (rule ext) 
    1.95  apply (simp add: COMBI_def) 
    1.96  done
    1.97  
    1.98 -lemma abs_K: "(%x. y) == COMBK y"
    1.99 +lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
   1.100  apply (rule eq_reflection)
   1.101  apply (rule ext) 
   1.102  apply (simp add: COMBK_def) 
   1.103  done
   1.104  
   1.105 -lemma abs_B: "(%x. a (g x)) == COMBB a g"
   1.106 +lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
   1.107  apply (rule eq_reflection)
   1.108  apply (rule ext) 
   1.109  apply (simp add: COMBB_def) 
   1.110  done
   1.111  
   1.112 -lemma abs_C: "(%x. (f x) b) == COMBC f b"
   1.113 +lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
   1.114  apply (rule eq_reflection)
   1.115  apply (rule ext) 
   1.116  apply (simp add: COMBC_def) 
   1.117  done
   1.118  
   1.119 -
   1.120  subsection {* Setup of external ATPs *}
   1.121  
   1.122 +use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
   1.123  use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
   1.124  setup Sledgehammer_Fact_Preprocessor.setup
   1.125  use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
   1.126 @@ -119,7 +121,12 @@
   1.127  setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
   1.128  setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
   1.129  setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
   1.130 -  
   1.131 +
   1.132 +
   1.133 +subsection {* The MESON prover *}
   1.134 +
   1.135 +use "Tools/Sledgehammer/meson_tactic.ML"
   1.136 +setup Meson_Tactic.setup
   1.137  
   1.138  
   1.139  subsection {* The Metis prover *}