# HG changeset patch # User wenzelm # Date 1163018715 -3600 # Node ID d53f76357f41c0d71e2fb88adc51f5362fd32568 # Parent f1e3967d559a2d7fb5d32edd36de24d7a148eb2d incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; diff -r f1e3967d559a -r d53f76357f41 src/HOL/ATP_Linkup.thy --- /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 diff -r f1e3967d559a -r d53f76357f41 src/HOL/IsaMakefile --- 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 \ diff -r f1e3967d559a -r d53f76357f41 src/HOL/Main.thy --- 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 diff -r f1e3967d559a -r d53f76357f41 src/HOL/Reconstruction.thy --- 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 diff -r f1e3967d559a -r d53f76357f41 src/HOL/ResAtpMethods.thy --- 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 diff -r f1e3967d559a -r d53f76357f41 src/HOL/Tools/res_axioms.ML --- 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; diff -r f1e3967d559a -r d53f76357f41 src/HOL/Tools/res_clause.ML --- 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"), diff -r f1e3967d559a -r d53f76357f41 src/HOL/Tools/res_hol_clause.ML --- 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