# HG changeset patch
# User blanchet
# Date 1268851064 -3600
# Node ID f552152d77473996c8c92207f45a1bd7492d47c5
# Parent  1590abc3d42a6ea3fad5aa2f1d4c094e90a5dc8d
renamed "ATP_Linkup" theory to "Sledgehammer"

diff -r 1590abc3d42a -r f552152d7747 src/HOL/ATP_Linkup.thy
--- 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
diff -r 1590abc3d42a -r f552152d7747 src/HOL/IsaMakefile
--- 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 \
diff -r 1590abc3d42a -r f552152d7747 src/HOL/List.thy
--- 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
 
diff -r 1590abc3d42a -r f552152d7747 src/HOL/Quotient.thy
--- 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")
diff -r 1590abc3d42a -r f552152d7747 src/HOL/Sledgehammer.thy
--- /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
diff -r 1590abc3d42a -r f552152d7747 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
--- 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"),
diff -r 1590abc3d42a -r f552152d7747 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- 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