--- a/src/HOL/ATP_Linkup.thy Wed Mar 17 19:26:05 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-(* Title: HOL/ATP_Linkup.thy
- Author: Lawrence C Paulson
- Author: Jia Meng, NICTA
- Author: Fabian Immler, TUM
-*)
-
-header {* The Isabelle-ATP Linkup *}
-
-theory ATP_Linkup
-imports Plain Hilbert_Choice
-uses
- "Tools/polyhash.ML"
- "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
- ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
- ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
- ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
- ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
- ("Tools/ATP_Manager/atp_manager.ML")
- ("Tools/ATP_Manager/atp_wrapper.ML")
- ("Tools/ATP_Manager/atp_minimal.ML")
- "~~/src/Tools/Metis/metis.ML"
- ("Tools/Sledgehammer/metis_tactics.ML")
-begin
-
-definition COMBI :: "'a => 'a"
- where "COMBI P == P"
-
-definition COMBK :: "'a => 'b => 'a"
- where "COMBK P Q == P"
-
-definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
- where "COMBB P Q R == P (Q R)"
-
-definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
- where "COMBC P Q R == P R Q"
-
-definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
- where "COMBS P Q R == P R (Q R)"
-
-definition fequal :: "'a => 'a => bool"
- where "fequal X Y == (X=Y)"
-
-lemma fequal_imp_equal: "fequal X Y ==> X=Y"
- by (simp add: fequal_def)
-
-lemma equal_imp_fequal: "X=Y ==> fequal X Y"
- by (simp add: fequal_def)
-
-text{*These two represent the equivalence between Boolean equality and iff.
-They can't be converted to clauses automatically, as the iff would be
-expanded...*}
-
-lemma iff_positive: "P | Q | P=Q"
-by blast
-
-lemma iff_negative: "~P | ~Q | P=Q"
-by blast
-
-text{*Theorems for translation to combinators*}
-
-lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBS_def)
-done
-
-lemma abs_I: "(%x. x) == COMBI"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBI_def)
-done
-
-lemma abs_K: "(%x. y) == COMBK y"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBK_def)
-done
-
-lemma abs_B: "(%x. a (g x)) == COMBB a g"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBB_def)
-done
-
-lemma abs_C: "(%x. (f x) b) == COMBC f b"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBC_def)
-done
-
-
-subsection {* Setup of external ATPs *}
-
-use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
-setup Sledgehammer_Fact_Preprocessor.setup
-use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
-use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
-setup Sledgehammer_Proof_Reconstruct.setup
-use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
-
-use "Tools/ATP_Manager/atp_wrapper.ML"
-setup ATP_Wrapper.setup
-use "Tools/ATP_Manager/atp_manager.ML"
-use "Tools/ATP_Manager/atp_minimal.ML"
-
-text {* basic provers *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
-
-text {* provers with stuctured output *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
-
-text {* on some problems better results *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
-
-text {* remote provers via SystemOnTPTP *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
-
-
-
-subsection {* The Metis prover *}
-
-use "Tools/Sledgehammer/metis_tactics.ML"
-setup Metis_Tactics.setup
-
-end
--- a/src/HOL/IsaMakefile Wed Mar 17 19:26:05 2010 +0100
+++ b/src/HOL/IsaMakefile Wed Mar 17 19:37:44 2010 +0100
@@ -246,7 +246,6 @@
@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
- ATP_Linkup.thy \
Big_Operators.thy \
Code_Evaluation.thy \
Code_Numeral.thy \
@@ -271,6 +270,7 @@
Random_Sequence.thy \
Recdef.thy \
SetInterval.thy \
+ Sledgehammer.thy \
String.thy \
Typerep.thy \
$(SRC)/Provers/Arith/assoc_fold.ML \
--- a/src/HOL/List.thy Wed Mar 17 19:26:05 2010 +0100
+++ b/src/HOL/List.thy Wed Mar 17 19:37:44 2010 +0100
@@ -5,7 +5,7 @@
header {* The datatype of finite lists *}
theory List
-imports Plain Presburger ATP_Linkup Recdef
+imports Plain Presburger Sledgehammer Recdef
uses ("Tools/list_code.ML")
begin
--- a/src/HOL/Quotient.thy Wed Mar 17 19:26:05 2010 +0100
+++ b/src/HOL/Quotient.thy Wed Mar 17 19:37:44 2010 +0100
@@ -5,7 +5,7 @@
header {* Definition of Quotient Types *}
theory Quotient
-imports Plain ATP_Linkup
+imports Plain Sledgehammer
uses
("~~/src/HOL/Tools/Quotient/quotient_info.ML")
("~~/src/HOL/Tools/Quotient/quotient_typ.ML")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Sledgehammer.thy Wed Mar 17 19:37:44 2010 +0100
@@ -0,0 +1,130 @@
+(* Title: HOL/Sledgehammer.thy
+ Author: Lawrence C Paulson
+ Author: Jia Meng, NICTA
+ Author: Fabian Immler, TUM
+*)
+
+header {* Sledgehammer: Isabelle--ATP Linkup *}
+
+theory Sledgehammer
+imports Plain Hilbert_Choice
+uses
+ "Tools/polyhash.ML"
+ "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
+ ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
+ ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
+ ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
+ ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
+ ("Tools/ATP_Manager/atp_manager.ML")
+ ("Tools/ATP_Manager/atp_wrapper.ML")
+ ("Tools/ATP_Manager/atp_minimal.ML")
+ "~~/src/Tools/Metis/metis.ML"
+ ("Tools/Sledgehammer/metis_tactics.ML")
+begin
+
+definition COMBI :: "'a => 'a"
+ where "COMBI P == P"
+
+definition COMBK :: "'a => 'b => 'a"
+ where "COMBK P Q == P"
+
+definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
+ where "COMBB P Q R == P (Q R)"
+
+definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
+ where "COMBC P Q R == P R Q"
+
+definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
+ where "COMBS P Q R == P R (Q R)"
+
+definition fequal :: "'a => 'a => bool"
+ where "fequal X Y == (X=Y)"
+
+lemma fequal_imp_equal: "fequal X Y ==> X=Y"
+ by (simp add: fequal_def)
+
+lemma equal_imp_fequal: "X=Y ==> fequal X Y"
+ by (simp add: fequal_def)
+
+text{*These two represent the equivalence between Boolean equality and iff.
+They can't be converted to clauses automatically, as the iff would be
+expanded...*}
+
+lemma iff_positive: "P | Q | P=Q"
+by blast
+
+lemma iff_negative: "~P | ~Q | P=Q"
+by blast
+
+text{*Theorems for translation to combinators*}
+
+lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBS_def)
+done
+
+lemma abs_I: "(%x. x) == COMBI"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBI_def)
+done
+
+lemma abs_K: "(%x. y) == COMBK y"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBK_def)
+done
+
+lemma abs_B: "(%x. a (g x)) == COMBB a g"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBB_def)
+done
+
+lemma abs_C: "(%x. (f x) b) == COMBC f b"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBC_def)
+done
+
+
+subsection {* Setup of external ATPs *}
+
+use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
+setup Sledgehammer_Fact_Preprocessor.setup
+use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
+use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
+setup Sledgehammer_Proof_Reconstruct.setup
+use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
+
+use "Tools/ATP_Manager/atp_wrapper.ML"
+setup ATP_Wrapper.setup
+use "Tools/ATP_Manager/atp_manager.ML"
+use "Tools/ATP_Manager/atp_minimal.ML"
+
+text {* basic provers *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
+
+text {* provers with stuctured output *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
+
+text {* on some problems better results *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
+
+text {* remote provers via SystemOnTPTP *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
+setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
+
+
+
+subsection {* The Metis prover *}
+
+use "Tools/Sledgehammer/metis_tactics.ML"
+setup Metis_Tactics.setup
+
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Mar 17 19:26:05 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Mar 17 19:37:44 2010 +0100
@@ -104,15 +104,15 @@
(@{const_name "op |"}, "or"),
(@{const_name "op -->"}, "implies"),
(@{const_name "op :"}, "in"),
- ("ATP_Linkup.fequal", "fequal"),
- ("ATP_Linkup.COMBI", "COMBI"),
- ("ATP_Linkup.COMBK", "COMBK"),
- ("ATP_Linkup.COMBB", "COMBB"),
- ("ATP_Linkup.COMBC", "COMBC"),
- ("ATP_Linkup.COMBS", "COMBS"),
- ("ATP_Linkup.COMBB'", "COMBB_e"),
- ("ATP_Linkup.COMBC'", "COMBC_e"),
- ("ATP_Linkup.COMBS'", "COMBS_e")];
+ ("Sledgehammer.fequal", "fequal"),
+ ("Sledgehammer.COMBI", "COMBI"),
+ ("Sledgehammer.COMBK", "COMBK"),
+ ("Sledgehammer.COMBB", "COMBB"),
+ ("Sledgehammer.COMBC", "COMBC"),
+ ("Sledgehammer.COMBS", "COMBS"),
+ ("Sledgehammer.COMBB'", "COMBB_e"),
+ ("Sledgehammer.COMBC'", "COMBC_e"),
+ ("Sledgehammer.COMBS'", "COMBS_e")];
val type_const_trans_table =
Symtab.make [("*", "prod"),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Mar 17 19:26:05 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Mar 17 19:37:44 2010 +0100
@@ -53,13 +53,13 @@
(* theorems for combinators and function extensionality *)
val ext = thm "HOL.ext";
-val comb_I = thm "ATP_Linkup.COMBI_def";
-val comb_K = thm "ATP_Linkup.COMBK_def";
-val comb_B = thm "ATP_Linkup.COMBB_def";
-val comb_C = thm "ATP_Linkup.COMBC_def";
-val comb_S = thm "ATP_Linkup.COMBS_def";
-val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
-val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
+val comb_I = thm "Sledgehammer.COMBI_def";
+val comb_K = thm "Sledgehammer.COMBK_def";
+val comb_B = thm "Sledgehammer.COMBB_def";
+val comb_C = thm "Sledgehammer.COMBC_def";
+val comb_S = thm "Sledgehammer.COMBS_def";
+val fequal_imp_equal = thm "Sledgehammer.fequal_imp_equal";
+val equal_imp_fequal = thm "Sledgehammer.equal_imp_fequal";
(* Parameter t_full below indicates that full type information is to be