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