renamed "ATP_Linkup" theory to "Sledgehammer"
authorblanchet
Wed Mar 17 19:37:44 2010 +0100 (2010-03-17)
changeset 35827f552152d7747
parent 35826 1590abc3d42a
child 35828 46cfc4b8112e
renamed "ATP_Linkup" theory to "Sledgehammer"
src/HOL/ATP_Linkup.thy
src/HOL/IsaMakefile
src/HOL/List.thy
src/HOL/Quotient.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Wed Mar 17 19:26:05 2010 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,130 +0,0 @@
     1.4 -(*  Title:      HOL/ATP_Linkup.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 {* The Isabelle-ATP Linkup *}
    1.11 -
    1.12 -theory ATP_Linkup
    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
     2.1 --- a/src/HOL/IsaMakefile	Wed Mar 17 19:26:05 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Wed Mar 17 19:37:44 2010 +0100
     2.3 @@ -246,7 +246,6 @@
     2.4  	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
     2.5  
     2.6  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
     2.7 -  ATP_Linkup.thy \
     2.8    Big_Operators.thy \
     2.9    Code_Evaluation.thy \
    2.10    Code_Numeral.thy \
    2.11 @@ -271,6 +270,7 @@
    2.12    Random_Sequence.thy \
    2.13    Recdef.thy \
    2.14    SetInterval.thy \
    2.15 +  Sledgehammer.thy \
    2.16    String.thy \
    2.17    Typerep.thy \
    2.18    $(SRC)/Provers/Arith/assoc_fold.ML \
     3.1 --- a/src/HOL/List.thy	Wed Mar 17 19:26:05 2010 +0100
     3.2 +++ b/src/HOL/List.thy	Wed Mar 17 19:37:44 2010 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* The datatype of finite lists *}
     3.5  
     3.6  theory List
     3.7 -imports Plain Presburger ATP_Linkup Recdef
     3.8 +imports Plain Presburger Sledgehammer Recdef
     3.9  uses ("Tools/list_code.ML")
    3.10  begin
    3.11  
     4.1 --- a/src/HOL/Quotient.thy	Wed Mar 17 19:26:05 2010 +0100
     4.2 +++ b/src/HOL/Quotient.thy	Wed Mar 17 19:37:44 2010 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Definition of Quotient Types *}
     4.5  
     4.6  theory Quotient
     4.7 -imports Plain ATP_Linkup
     4.8 +imports Plain Sledgehammer
     4.9  uses
    4.10    ("~~/src/HOL/Tools/Quotient/quotient_info.ML")
    4.11    ("~~/src/HOL/Tools/Quotient/quotient_typ.ML")
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Sledgehammer.thy	Wed Mar 17 19:37:44 2010 +0100
     5.3 @@ -0,0 +1,130 @@
     5.4 +(*  Title:      HOL/Sledgehammer.thy
     5.5 +    Author:     Lawrence C Paulson
     5.6 +    Author:     Jia Meng, NICTA
     5.7 +    Author:     Fabian Immler, TUM
     5.8 +*)
     5.9 +
    5.10 +header {* Sledgehammer: Isabelle--ATP Linkup *}
    5.11 +
    5.12 +theory Sledgehammer
    5.13 +imports Plain Hilbert_Choice
    5.14 +uses
    5.15 +  "Tools/polyhash.ML"
    5.16 +  "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    5.17 +  ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
    5.18 +  ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
    5.19 +  ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    5.20 +  ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
    5.21 +  ("Tools/ATP_Manager/atp_manager.ML")
    5.22 +  ("Tools/ATP_Manager/atp_wrapper.ML")
    5.23 +  ("Tools/ATP_Manager/atp_minimal.ML")
    5.24 +  "~~/src/Tools/Metis/metis.ML"
    5.25 +  ("Tools/Sledgehammer/metis_tactics.ML")
    5.26 +begin
    5.27 +
    5.28 +definition COMBI :: "'a => 'a"
    5.29 +  where "COMBI P == P"
    5.30 +
    5.31 +definition COMBK :: "'a => 'b => 'a"
    5.32 +  where "COMBK P Q == P"
    5.33 +
    5.34 +definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
    5.35 +  where "COMBB P Q R == P (Q R)"
    5.36 +
    5.37 +definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
    5.38 +  where "COMBC P Q R == P R Q"
    5.39 +
    5.40 +definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
    5.41 +  where "COMBS P Q R == P R (Q R)"
    5.42 +
    5.43 +definition fequal :: "'a => 'a => bool"
    5.44 +  where "fequal X Y == (X=Y)"
    5.45 +
    5.46 +lemma fequal_imp_equal: "fequal X Y ==> X=Y"
    5.47 +  by (simp add: fequal_def)
    5.48 +
    5.49 +lemma equal_imp_fequal: "X=Y ==> fequal X Y"
    5.50 +  by (simp add: fequal_def)
    5.51 +
    5.52 +text{*These two represent the equivalence between Boolean equality and iff.
    5.53 +They can't be converted to clauses automatically, as the iff would be
    5.54 +expanded...*}
    5.55 +
    5.56 +lemma iff_positive: "P | Q | P=Q"
    5.57 +by blast
    5.58 +
    5.59 +lemma iff_negative: "~P | ~Q | P=Q"
    5.60 +by blast
    5.61 +
    5.62 +text{*Theorems for translation to combinators*}
    5.63 +
    5.64 +lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
    5.65 +apply (rule eq_reflection)
    5.66 +apply (rule ext) 
    5.67 +apply (simp add: COMBS_def) 
    5.68 +done
    5.69 +
    5.70 +lemma abs_I: "(%x. x) == COMBI"
    5.71 +apply (rule eq_reflection)
    5.72 +apply (rule ext) 
    5.73 +apply (simp add: COMBI_def) 
    5.74 +done
    5.75 +
    5.76 +lemma abs_K: "(%x. y) == COMBK y"
    5.77 +apply (rule eq_reflection)
    5.78 +apply (rule ext) 
    5.79 +apply (simp add: COMBK_def) 
    5.80 +done
    5.81 +
    5.82 +lemma abs_B: "(%x. a (g x)) == COMBB a g"
    5.83 +apply (rule eq_reflection)
    5.84 +apply (rule ext) 
    5.85 +apply (simp add: COMBB_def) 
    5.86 +done
    5.87 +
    5.88 +lemma abs_C: "(%x. (f x) b) == COMBC f b"
    5.89 +apply (rule eq_reflection)
    5.90 +apply (rule ext) 
    5.91 +apply (simp add: COMBC_def) 
    5.92 +done
    5.93 +
    5.94 +
    5.95 +subsection {* Setup of external ATPs *}
    5.96 +
    5.97 +use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
    5.98 +setup Sledgehammer_Fact_Preprocessor.setup
    5.99 +use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
   5.100 +use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
   5.101 +setup Sledgehammer_Proof_Reconstruct.setup
   5.102 +use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
   5.103 +
   5.104 +use "Tools/ATP_Manager/atp_wrapper.ML"
   5.105 +setup ATP_Wrapper.setup
   5.106 +use "Tools/ATP_Manager/atp_manager.ML"
   5.107 +use "Tools/ATP_Manager/atp_minimal.ML"
   5.108 +
   5.109 +text {* basic provers *}
   5.110 +setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
   5.111 +setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
   5.112 +setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
   5.113 +
   5.114 +text {* provers with stuctured output *}
   5.115 +setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
   5.116 +setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
   5.117 +
   5.118 +text {* on some problems better results *}
   5.119 +setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
   5.120 +
   5.121 +text {* remote provers via SystemOnTPTP *}
   5.122 +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
   5.123 +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
   5.124 +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
   5.125 +  
   5.126 +
   5.127 +
   5.128 +subsection {* The Metis prover *}
   5.129 +
   5.130 +use "Tools/Sledgehammer/metis_tactics.ML"
   5.131 +setup Metis_Tactics.setup
   5.132 +
   5.133 +end
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Mar 17 19:26:05 2010 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Mar 17 19:37:44 2010 +0100
     6.3 @@ -104,15 +104,15 @@
     6.4                     (@{const_name "op |"}, "or"),
     6.5                     (@{const_name "op -->"}, "implies"),
     6.6                     (@{const_name "op :"}, "in"),
     6.7 -                   ("ATP_Linkup.fequal", "fequal"),
     6.8 -                   ("ATP_Linkup.COMBI", "COMBI"),
     6.9 -                   ("ATP_Linkup.COMBK", "COMBK"),
    6.10 -                   ("ATP_Linkup.COMBB", "COMBB"),
    6.11 -                   ("ATP_Linkup.COMBC", "COMBC"),
    6.12 -                   ("ATP_Linkup.COMBS", "COMBS"),
    6.13 -                   ("ATP_Linkup.COMBB'", "COMBB_e"),
    6.14 -                   ("ATP_Linkup.COMBC'", "COMBC_e"),
    6.15 -                   ("ATP_Linkup.COMBS'", "COMBS_e")];
    6.16 +                   ("Sledgehammer.fequal", "fequal"),
    6.17 +                   ("Sledgehammer.COMBI", "COMBI"),
    6.18 +                   ("Sledgehammer.COMBK", "COMBK"),
    6.19 +                   ("Sledgehammer.COMBB", "COMBB"),
    6.20 +                   ("Sledgehammer.COMBC", "COMBC"),
    6.21 +                   ("Sledgehammer.COMBS", "COMBS"),
    6.22 +                   ("Sledgehammer.COMBB'", "COMBB_e"),
    6.23 +                   ("Sledgehammer.COMBC'", "COMBC_e"),
    6.24 +                   ("Sledgehammer.COMBS'", "COMBS_e")];
    6.25  
    6.26  val type_const_trans_table =
    6.27        Symtab.make [("*", "prod"),
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Mar 17 19:26:05 2010 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Mar 17 19:37:44 2010 +0100
     7.3 @@ -53,13 +53,13 @@
     7.4  
     7.5  (* theorems for combinators and function extensionality *)
     7.6  val ext = thm "HOL.ext";
     7.7 -val comb_I = thm "ATP_Linkup.COMBI_def";
     7.8 -val comb_K = thm "ATP_Linkup.COMBK_def";
     7.9 -val comb_B = thm "ATP_Linkup.COMBB_def";
    7.10 -val comb_C = thm "ATP_Linkup.COMBC_def";
    7.11 -val comb_S = thm "ATP_Linkup.COMBS_def";
    7.12 -val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
    7.13 -val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
    7.14 +val comb_I = thm "Sledgehammer.COMBI_def";
    7.15 +val comb_K = thm "Sledgehammer.COMBK_def";
    7.16 +val comb_B = thm "Sledgehammer.COMBB_def";
    7.17 +val comb_C = thm "Sledgehammer.COMBC_def";
    7.18 +val comb_S = thm "Sledgehammer.COMBS_def";
    7.19 +val fequal_imp_equal = thm "Sledgehammer.fequal_imp_equal";
    7.20 +val equal_imp_fequal = thm "Sledgehammer.equal_imp_fequal";
    7.21  
    7.22  
    7.23  (* Parameter t_full below indicates that full type information is to be