--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ATP_Linkup.thy Wed Nov 08 21:45:15 2006 +0100
@@ -0,0 +1,104 @@
+(* Title: HOL/ATP_Linkup.thy
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Author: Jia Meng, NICTA
+*)
+
+header{* The Isabelle-ATP Linkup *}
+
+theory ATP_Linkup
+imports Hilbert_Choice Map Extraction
+uses
+ "Tools/polyhash.ML"
+ "Tools/ATP/AtpCommunication.ML"
+ "Tools/ATP/watcher.ML"
+ "Tools/ATP/reduce_axiomsN.ML"
+ "Tools/res_clause.ML"
+ ("Tools/res_hol_clause.ML")
+ ("Tools/res_axioms.ML")
+ ("Tools/res_atp.ML")
+ ("Tools/res_atp_provers.ML")
+ ("Tools/res_atp_methods.ML")
+begin
+
+constdefs
+ COMBI :: "'a => 'a"
+ "COMBI P == P"
+
+ COMBK :: "'a => 'b => 'a"
+ "COMBK P Q == P"
+
+ COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
+ "COMBB P Q R == P (Q R)"
+
+ COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
+ "COMBC P Q R == P R Q"
+
+ COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
+ "COMBS P Q R == P R (Q R)"
+
+ COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
+ "COMBB' M P Q R == M (P (Q R))"
+
+ COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
+ "COMBC' M P Q R == M (P R) Q"
+
+ COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
+ "COMBS' M P Q R == M (P R) (Q R)"
+
+ fequal :: "'a => 'a => bool"
+ "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)
+
+lemma K_simp: "COMBK P == (%Q. P)"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBK_def)
+done
+
+lemma I_simp: "COMBI == (%P. P)"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBI_def)
+done
+
+lemma B_simp: "COMBB P Q == %R. P (Q R)"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (simp add: COMBB_def)
+done
+
+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
+
+use "Tools/res_axioms.ML"
+use "Tools/res_hol_clause.ML"
+use "Tools/res_atp.ML"
+
+setup ResAxioms.meson_method_setup
+
+
+subsection {* Setup for Vampire, E prover and SPASS *}
+
+use "Tools/res_atp_provers.ML"
+
+oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
+oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
+oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
+
+use "Tools/res_atp_methods.ML"
+setup ResAtpMethods.ResAtps_setup
+
+end
--- a/src/HOL/IsaMakefile Wed Nov 08 21:45:14 2006 +0100
+++ b/src/HOL/IsaMakefile Wed Nov 08 21:45:15 2006 +0100
@@ -97,7 +97,7 @@
Lattices.thy List.ML List.thy Main.thy Map.thy \
Nat.ML Nat.thy OrderedGroup.ML OrderedGroup.thy \
Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy \
- ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy \
+ ROOT.ML Recdef.thy Record.thy Refute.thy \
Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML \
Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML \
Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML \
@@ -120,7 +120,7 @@
Transitive_Closure.ML Transitive_Closure.thy \
Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy \
arith_data.ML \
- document/root.tex hologic.ML simpdata.ML ResAtpMethods.thy \
+ document/root.tex hologic.ML simpdata.ML ATP_Linkup.thy \
Tools/res_atp_provers.ML Tools/res_atp_methods.ML \
Tools/res_hol_clause.ML \
Tools/function_package/sum_tools.ML \
--- a/src/HOL/Main.thy Wed Nov 08 21:45:14 2006 +0100
+++ b/src/HOL/Main.thy Wed Nov 08 21:45:15 2006 +0100
@@ -5,7 +5,7 @@
header {* Main HOL *}
theory Main
-imports SAT Reconstruction ResAtpMethods
+imports SAT ATP_Linkup
begin
text {*
@@ -14,7 +14,7 @@
*}
text {* \medskip Late clause setup: installs \emph{all} known theorems
- into the clause cache; cf.\ theory @{text Reconstruction}. *}
+ into the clause cache; cf.\ theory @{text ATP_Linkup}. *}
setup ResAxioms.setup
--- a/src/HOL/Reconstruction.thy Wed Nov 08 21:45:14 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-(* Title: HOL/Reconstruction.thy
- ID: $Id$
- Author: Lawrence C Paulson
- Copyright 2004 University of Cambridge
-*)
-
-header{* Reconstructing external resolution proofs *}
-
-theory Reconstruction
-imports Hilbert_Choice Map Extraction
-uses "Tools/polyhash.ML"
- "Tools/ATP/AtpCommunication.ML"
- "Tools/ATP/watcher.ML"
- "Tools/ATP/reduce_axiomsN.ML"
- "Tools/res_clause.ML"
- ("Tools/res_hol_clause.ML")
- ("Tools/res_axioms.ML")
- ("Tools/res_atp.ML")
-
-begin
-
-constdefs
- COMBI :: "'a => 'a"
- "COMBI P == P"
-
- COMBK :: "'a => 'b => 'a"
- "COMBK P Q == P"
-
- COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
- "COMBB P Q R == P (Q R)"
-
- COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
- "COMBC P Q R == P R Q"
-
- COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
- "COMBS P Q R == P R (Q R)"
-
- COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
- "COMBB' M P Q R == M (P (Q R))"
-
- COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
- "COMBC' M P Q R == M (P R) Q"
-
- COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
- "COMBS' M P Q R == M (P R) (Q R)"
-
- fequal :: "'a => 'a => bool"
- "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)
-
-lemma K_simp: "COMBK P == (%Q. P)"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBK_def)
-done
-
-lemma I_simp: "COMBI == (%P. P)"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBI_def)
-done
-
-lemma B_simp: "COMBB P Q == %R. P (Q R)"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (simp add: COMBB_def)
-done
-
-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
-
-use "Tools/res_axioms.ML"
-use "Tools/res_hol_clause.ML"
-use "Tools/res_atp.ML"
-
-setup ResAxioms.meson_method_setup
-
-end
--- a/src/HOL/ResAtpMethods.thy Wed Nov 08 21:45:14 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* ID: $Id$
- Author: Jia Meng, NICTA
-*)
-
-header {* ATP setup (Vampire, E prover and SPASS) *}
-
-theory ResAtpMethods
-imports Reconstruction
-uses
- "Tools/res_atp_provers.ML"
- ("Tools/res_atp_methods.ML")
-
-begin
-
-oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
-oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
-oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
-
-use "Tools/res_atp_methods.ML"
-setup ResAtpMethods.ResAtps_setup
-
-end
--- a/src/HOL/Tools/res_axioms.ML Wed Nov 08 21:45:14 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML Wed Nov 08 21:45:15 2006 +0100
@@ -60,9 +60,9 @@
in Net.insert_term eq_thm (t, th) net end;
val abstraction_cache = ref
- (seed (thm"Reconstruction.I_simp")
- (seed (thm"Reconstruction.B_simp")
- (seed (thm"Reconstruction.K_simp") Net.empty)));
+ (seed (thm"ATP_Linkup.I_simp")
+ (seed (thm"ATP_Linkup.B_simp")
+ (seed (thm"ATP_Linkup.K_simp") Net.empty)));
(**** Transformation of Elimination Rules into First-Order Formulas****)
@@ -137,15 +137,15 @@
(**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
-(*Transfer a theorem into theory Reconstruction.thy if it is not already
+(*Transfer a theorem into theory ATP_Linkup.thy if it is not already
inside that theory -- because it's needed for Skolemization *)
-(*This will refer to the final version of theory Reconstruction.*)
+(*This will refer to the final version of theory ATP_Linkup.*)
val recon_thy_ref = Theory.self_ref (the_context ());
-(*If called while Reconstruction is being created, it will transfer to the
+(*If called while ATP_Linkup is being created, it will transfer to the
current version. If called afterward, it will transfer to the final version.*)
-fun transfer_to_Reconstruction th =
+fun transfer_to_ATP_Linkup th =
transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
fun is_taut th =
@@ -476,7 +476,7 @@
(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
fun to_nnf th =
- th |> transfer_to_Reconstruction
+ th |> transfer_to_ATP_Linkup
|> transform_elim |> zero_var_indexes |> freeze_thm
|> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas ~1;
--- a/src/HOL/Tools/res_clause.ML Wed Nov 08 21:45:14 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML Wed Nov 08 21:45:15 2006 +0100
@@ -125,15 +125,15 @@
("op Un", "union"),
("op Int", "inter"),
("List.op @", "append"),
- ("Reconstruction.fequal", "fequal"),
- ("Reconstruction.COMBI", "COMBI"),
- ("Reconstruction.COMBK", "COMBK"),
- ("Reconstruction.COMBB", "COMBB"),
- ("Reconstruction.COMBC", "COMBC"),
- ("Reconstruction.COMBS", "COMBS"),
- ("Reconstruction.COMBB'", "COMBB_e"),
- ("Reconstruction.COMBC'", "COMBC_e"),
- ("Reconstruction.COMBS'", "COMBS_e")];
+ ("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")];
val type_const_trans_table =
Symtab.make [("*", "prod"),
--- a/src/HOL/Tools/res_hol_clause.ML Wed Nov 08 21:45:14 2006 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML Wed Nov 08 21:45:15 2006 +0100
@@ -11,16 +11,16 @@
(* theorems for combinators and function extensionality *)
val ext = thm "HOL.ext";
-val comb_I = thm "Reconstruction.COMBI_def";
-val comb_K = thm "Reconstruction.COMBK_def";
-val comb_B = thm "Reconstruction.COMBB_def";
-val comb_C = thm "Reconstruction.COMBC_def";
-val comb_S = thm "Reconstruction.COMBS_def";
-val comb_B' = thm "Reconstruction.COMBB'_def";
-val comb_C' = thm "Reconstruction.COMBC'_def";
-val comb_S' = thm "Reconstruction.COMBS'_def";
-val fequal_imp_equal = thm "Reconstruction.fequal_imp_equal";
-val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal";
+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 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";
(*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard
combinators appear to work best.*)
@@ -81,7 +81,7 @@
(*******************************************)
-fun mk_compact_comb (tm as (Const("Reconstruction.COMBB",_)$p) $ (Const("Reconstruction.COMBB",_)$q$r)) Bnds count_comb =
+fun mk_compact_comb (tm as (Const("ATP_Linkup.COMBB",_)$p) $ (Const("ATP_Linkup.COMBB",_)$q$r)) Bnds count_comb =
let val tp_p = Term.type_of1(Bnds,p)
val tp_q = Term.type_of1(Bnds,q)
val tp_r = Term.type_of1(Bnds,r)
@@ -90,9 +90,9 @@
val _ = increB' count_comb
val _ = decreB count_comb 2
in
- Const("Reconstruction.COMBB'",typ_B') $ p $ q $ r
+ Const("ATP_Linkup.COMBB'",typ_B') $ p $ q $ r
end
- | mk_compact_comb (tm as (Const("Reconstruction.COMBC",_) $ (Const("Reconstruction.COMBB",_)$p$q) $ r)) Bnds count_comb =
+ | mk_compact_comb (tm as (Const("ATP_Linkup.COMBC",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) Bnds count_comb =
let val tp_p = Term.type_of1(Bnds,p)
val tp_q = Term.type_of1(Bnds,q)
val tp_r = Term.type_of1(Bnds,r)
@@ -102,9 +102,9 @@
val _ = decreC count_comb 1
val _ = decreB count_comb 1
in
- Const("Reconstruction.COMBC'",typ_C') $ p $ q $ r
+ Const("ATP_Linkup.COMBC'",typ_C') $ p $ q $ r
end
- | mk_compact_comb (tm as (Const("Reconstruction.COMBS",_) $ (Const("Reconstruction.COMBB",_)$p$q) $ r)) Bnds count_comb =
+ | mk_compact_comb (tm as (Const("ATP_Linkup.COMBS",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) Bnds count_comb =
let val tp_p = Term.type_of1(Bnds,p)
val tp_q = Term.type_of1(Bnds,q)
val tp_r = Term.type_of1(Bnds,r)
@@ -114,7 +114,7 @@
val _ = decreS count_comb 1
val _ = decreB count_comb 1
in
- Const("Reconstruction.COMBS'",typ_S') $ p $ q $ r
+ Const("ATP_Linkup.COMBS'",typ_S') $ p $ q $ r
end
| mk_compact_comb tm _ _ = tm;
@@ -124,28 +124,28 @@
fun lam2comb (Abs(x,tp,Bound 0)) _ count_comb =
let val _ = increI count_comb
in
- Const("Reconstruction.COMBI",tp-->tp)
+ Const("ATP_Linkup.COMBI",tp-->tp)
end
| lam2comb (Abs(x,tp,Bound n)) Bnds count_comb =
let val tb = List.nth(Bnds,n-1)
val _ = increK count_comb
in
- Const("Reconstruction.COMBK", [tb,tp] ---> tb) $ (Bound (n-1))
+ Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ (Bound (n-1))
end
| lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb =
let val _ = increK count_comb
in
- Const("Reconstruction.COMBK",[t2,t1] ---> t2) $ Const(c,t2)
+ Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2)
end
| lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb =
let val _ = increK count_comb
in
- Const("Reconstruction.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
+ Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
end
| lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb =
let val _ = increK count_comb
in
- Const("Reconstruction.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
+ Const("ATP_Linkup.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
end
| lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds count_comb =
let val tr = Term.type_of1(t1::Bnds,P)
@@ -159,8 +159,8 @@
val _ = increI count_comb
val _ = increS count_comb
in
- compact_comb (Const("Reconstruction.COMBS",tS) $ P' $
- Const("Reconstruction.COMBI",tI)) Bnds count_comb
+ compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $
+ Const("ATP_Linkup.COMBI",tI)) Bnds count_comb
end
end
| lam2comb (t as (Abs(x,t1,P$Q))) Bnds count_comb =
@@ -174,7 +174,7 @@
val PQ' = incr_boundvars ~1(P $ Q)
val _ = increK count_comb
in
- Const("Reconstruction.COMBK",tK) $ PQ'
+ Const("ATP_Linkup.COMBK",tK) $ PQ'
end
else if nfreeP then
let val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb
@@ -184,7 +184,7 @@
val tB = [tp,tq',t1] ---> tpq
val _ = increB count_comb
in
- compact_comb (Const("Reconstruction.COMBB",tB) $ P' $ Q') Bnds count_comb
+ compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') Bnds count_comb
end
else if nfreeQ then
let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
@@ -194,7 +194,7 @@
val tC = [tp',tq,t1] ---> tpq
val _ = increC count_comb
in
- compact_comb (Const("Reconstruction.COMBC",tC) $ P' $ Q') Bnds count_comb
+ compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') Bnds count_comb
end
else
let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
@@ -204,7 +204,7 @@
val tS = [tp',tq',t1] ---> tpq
val _ = increS count_comb
in
- compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Q') Bnds count_comb
+ compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') Bnds count_comb
end
end
| lam2comb (t as (Abs(x,t1,_))) _ _ = raise ResClause.CLAUSE("HOL CLAUSE",t);
@@ -718,8 +718,8 @@
completeness. Unfortunately, they are very prolific, causing greatly increased runtimes.
They also lead to many unsound proofs. Thus it is well that the "exists too_general_bool"
test deletes them except with the full-typed translation.*)
-val iff_thms = [pretend_cnf "Reconstruction.iff_positive",
- pretend_cnf "Reconstruction.iff_negative"];
+val iff_thms = [pretend_cnf "ATP_Linkup.iff_positive",
+ pretend_cnf "ATP_Linkup.iff_negative"];
fun get_helper_clauses () =
let val IK = if !combI_count > 0 orelse !combK_count > 0
@@ -802,4 +802,4 @@
clnames
end;
-end
\ No newline at end of file
+end