incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
authorwenzelm
Wed Nov 08 21:45:15 2006 +0100 (2006-11-08)
changeset 21254d53f76357f41
parent 21253 f1e3967d559a
child 21255 617fdb08abe9
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
src/HOL/ATP_Linkup.thy
src/HOL/IsaMakefile
src/HOL/Main.thy
src/HOL/Reconstruction.thy
src/HOL/ResAtpMethods.thy
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Nov 08 21:45:15 2006 +0100
     1.3 @@ -0,0 +1,104 @@
     1.4 +(*  Title:      HOL/ATP_Linkup.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson
     1.7 +    Author:     Jia Meng, NICTA
     1.8 +*)
     1.9 +
    1.10 +header{* The Isabelle-ATP Linkup *}
    1.11 +
    1.12 +theory ATP_Linkup
    1.13 +imports Hilbert_Choice Map Extraction
    1.14 +uses
    1.15 +  "Tools/polyhash.ML"
    1.16 +  "Tools/ATP/AtpCommunication.ML"
    1.17 +  "Tools/ATP/watcher.ML"
    1.18 +  "Tools/ATP/reduce_axiomsN.ML"
    1.19 +  "Tools/res_clause.ML"
    1.20 +  ("Tools/res_hol_clause.ML")
    1.21 +  ("Tools/res_axioms.ML")
    1.22 +  ("Tools/res_atp.ML")
    1.23 +  ("Tools/res_atp_provers.ML")
    1.24 +  ("Tools/res_atp_methods.ML")
    1.25 +begin
    1.26 +
    1.27 +constdefs
    1.28 +  COMBI :: "'a => 'a"
    1.29 +    "COMBI P == P"
    1.30 +
    1.31 +  COMBK :: "'a => 'b => 'a"
    1.32 +    "COMBK P Q == P"
    1.33 +
    1.34 +  COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
    1.35 +    "COMBB P Q R == P (Q R)"
    1.36 +
    1.37 +  COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
    1.38 +    "COMBC P Q R == P R Q"
    1.39 +
    1.40 +  COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
    1.41 +    "COMBS P Q R == P R (Q R)"
    1.42 +
    1.43 +  COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
    1.44 +    "COMBB' M P Q R == M (P (Q R))"
    1.45 +
    1.46 +  COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
    1.47 +    "COMBC' M P Q R == M (P R) Q"
    1.48 +
    1.49 +  COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
    1.50 +    "COMBS' M P Q R == M (P R) (Q R)"
    1.51 +
    1.52 +  fequal :: "'a => 'a => bool"
    1.53 +    "fequal X Y == (X=Y)"
    1.54 +
    1.55 +lemma fequal_imp_equal: "fequal X Y ==> X=Y"
    1.56 +  by (simp add: fequal_def)
    1.57 +
    1.58 +lemma equal_imp_fequal: "X=Y ==> fequal X Y"
    1.59 +  by (simp add: fequal_def)
    1.60 +
    1.61 +lemma K_simp: "COMBK P == (%Q. P)"
    1.62 +apply (rule eq_reflection)
    1.63 +apply (rule ext)
    1.64 +apply (simp add: COMBK_def)
    1.65 +done
    1.66 +
    1.67 +lemma I_simp: "COMBI == (%P. P)"
    1.68 +apply (rule eq_reflection)
    1.69 +apply (rule ext)
    1.70 +apply (simp add: COMBI_def)
    1.71 +done
    1.72 +
    1.73 +lemma B_simp: "COMBB P Q == %R. P (Q R)"
    1.74 +apply (rule eq_reflection)
    1.75 +apply (rule ext)
    1.76 +apply (simp add: COMBB_def)
    1.77 +done
    1.78 +
    1.79 +text{*These two represent the equivalence between Boolean equality and iff.
    1.80 +They can't be converted to clauses automatically, as the iff would be
    1.81 +expanded...*}
    1.82 +
    1.83 +lemma iff_positive: "P | Q | P=Q"
    1.84 +by blast
    1.85 +
    1.86 +lemma iff_negative: "~P | ~Q | P=Q"
    1.87 +by blast
    1.88 +
    1.89 +use "Tools/res_axioms.ML"
    1.90 +use "Tools/res_hol_clause.ML"
    1.91 +use "Tools/res_atp.ML"
    1.92 +
    1.93 +setup ResAxioms.meson_method_setup
    1.94 +
    1.95 +
    1.96 +subsection {* Setup for Vampire, E prover and SPASS *}
    1.97 +
    1.98 +use "Tools/res_atp_provers.ML"
    1.99 +
   1.100 +oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
   1.101 +oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
   1.102 +oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
   1.103 +
   1.104 +use "Tools/res_atp_methods.ML"
   1.105 +setup ResAtpMethods.ResAtps_setup
   1.106 +
   1.107 +end
     2.1 --- a/src/HOL/IsaMakefile	Wed Nov 08 21:45:14 2006 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Wed Nov 08 21:45:15 2006 +0100
     2.3 @@ -97,7 +97,7 @@
     2.4    Lattices.thy List.ML List.thy Main.thy Map.thy			\
     2.5    Nat.ML Nat.thy OrderedGroup.ML OrderedGroup.thy	\
     2.6    Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
     2.7 -  ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
     2.8 +  ROOT.ML Recdef.thy Record.thy Refute.thy			\
     2.9    Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML		\
    2.10    Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML		\
    2.11    Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML 					\
    2.12 @@ -120,7 +120,7 @@
    2.13    Transitive_Closure.ML Transitive_Closure.thy		\
    2.14    Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
    2.15    arith_data.ML			\
    2.16 -  document/root.tex hologic.ML simpdata.ML ResAtpMethods.thy 			\
    2.17 +  document/root.tex hologic.ML simpdata.ML ATP_Linkup.thy \
    2.18    Tools/res_atp_provers.ML Tools/res_atp_methods.ML	\
    2.19    Tools/res_hol_clause.ML	\
    2.20    Tools/function_package/sum_tools.ML 	\
     3.1 --- a/src/HOL/Main.thy	Wed Nov 08 21:45:14 2006 +0100
     3.2 +++ b/src/HOL/Main.thy	Wed Nov 08 21:45:15 2006 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Main HOL *}
     3.5  
     3.6  theory Main
     3.7 -imports SAT Reconstruction ResAtpMethods
     3.8 +imports SAT ATP_Linkup
     3.9  begin
    3.10  
    3.11  text {*
    3.12 @@ -14,7 +14,7 @@
    3.13  *}
    3.14  
    3.15  text {* \medskip Late clause setup: installs \emph{all} known theorems
    3.16 -  into the clause cache; cf.\ theory @{text Reconstruction}. *}
    3.17 +  into the clause cache; cf.\ theory @{text ATP_Linkup}. *}
    3.18  
    3.19  setup ResAxioms.setup
    3.20  
     4.1 --- a/src/HOL/Reconstruction.thy	Wed Nov 08 21:45:14 2006 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,90 +0,0 @@
     4.4 -(*  Title:      HOL/Reconstruction.thy
     4.5 -    ID:         $Id$
     4.6 -    Author:     Lawrence C Paulson
     4.7 -    Copyright   2004  University of Cambridge
     4.8 -*)
     4.9 -
    4.10 -header{* Reconstructing external resolution proofs *}
    4.11 -
    4.12 -theory Reconstruction
    4.13 -imports Hilbert_Choice Map Extraction
    4.14 -uses 	 "Tools/polyhash.ML"
    4.15 -	 "Tools/ATP/AtpCommunication.ML"
    4.16 -	 "Tools/ATP/watcher.ML"
    4.17 -         "Tools/ATP/reduce_axiomsN.ML"
    4.18 -         "Tools/res_clause.ML"
    4.19 -	 ("Tools/res_hol_clause.ML")
    4.20 -	 ("Tools/res_axioms.ML")
    4.21 -	 ("Tools/res_atp.ML")
    4.22 -
    4.23 -begin
    4.24 -
    4.25 -constdefs
    4.26 -  COMBI :: "'a => 'a"
    4.27 -    "COMBI P == P"
    4.28 -
    4.29 -  COMBK :: "'a => 'b => 'a"
    4.30 -    "COMBK P Q == P"
    4.31 -
    4.32 -  COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
    4.33 -    "COMBB P Q R == P (Q R)"
    4.34 -
    4.35 -  COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
    4.36 -    "COMBC P Q R == P R Q"
    4.37 -
    4.38 -  COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
    4.39 -    "COMBS P Q R == P R (Q R)"
    4.40 -
    4.41 -  COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
    4.42 -    "COMBB' M P Q R == M (P (Q R))"
    4.43 -
    4.44 -  COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
    4.45 -    "COMBC' M P Q R == M (P R) Q"
    4.46 -
    4.47 -  COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
    4.48 -    "COMBS' M P Q R == M (P R) (Q R)"
    4.49 -
    4.50 -  fequal :: "'a => 'a => bool"
    4.51 -    "fequal X Y == (X=Y)"
    4.52 -
    4.53 -lemma fequal_imp_equal: "fequal X Y ==> X=Y"
    4.54 -  by (simp add: fequal_def)
    4.55 -
    4.56 -lemma equal_imp_fequal: "X=Y ==> fequal X Y"
    4.57 -  by (simp add: fequal_def)
    4.58 -
    4.59 -lemma K_simp: "COMBK P == (%Q. P)"
    4.60 -apply (rule eq_reflection) 
    4.61 -apply (rule ext) 
    4.62 -apply (simp add: COMBK_def) 
    4.63 -done
    4.64 -
    4.65 -lemma I_simp: "COMBI == (%P. P)"
    4.66 -apply (rule eq_reflection) 
    4.67 -apply (rule ext) 
    4.68 -apply (simp add: COMBI_def) 
    4.69 -done
    4.70 -
    4.71 -lemma B_simp: "COMBB P Q == %R. P (Q R)"
    4.72 -apply (rule eq_reflection) 
    4.73 -apply (rule ext) 
    4.74 -apply (simp add: COMBB_def) 
    4.75 -done
    4.76 -
    4.77 -text{*These two represent the equivalence between Boolean equality and iff.
    4.78 -They can't be converted to clauses automatically, as the iff would be 
    4.79 -expanded...*}
    4.80 -
    4.81 -lemma iff_positive: "P | Q | P=Q"
    4.82 -by blast
    4.83 -
    4.84 -lemma iff_negative: "~P | ~Q | P=Q"
    4.85 -by blast
    4.86 -
    4.87 -use "Tools/res_axioms.ML"
    4.88 -use "Tools/res_hol_clause.ML"
    4.89 -use "Tools/res_atp.ML"
    4.90 -
    4.91 -setup ResAxioms.meson_method_setup
    4.92 -
    4.93 -end
     5.1 --- a/src/HOL/ResAtpMethods.thy	Wed Nov 08 21:45:14 2006 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,22 +0,0 @@
     5.4 -(* ID: $Id$
     5.5 -   Author: Jia Meng, NICTA
     5.6 -*)
     5.7 -
     5.8 -header {* ATP setup (Vampire, E prover and SPASS) *}
     5.9 -
    5.10 -theory ResAtpMethods
    5.11 -imports Reconstruction
    5.12 -uses
    5.13 -  "Tools/res_atp_provers.ML"
    5.14 -  ("Tools/res_atp_methods.ML")
    5.15 -
    5.16 -begin
    5.17 -
    5.18 -oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
    5.19 -oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
    5.20 -oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
    5.21 -
    5.22 -use "Tools/res_atp_methods.ML"
    5.23 -setup ResAtpMethods.ResAtps_setup
    5.24 -
    5.25 -end
     6.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Nov 08 21:45:14 2006 +0100
     6.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Nov 08 21:45:15 2006 +0100
     6.3 @@ -60,9 +60,9 @@
     6.4    in  Net.insert_term eq_thm (t, th) net end;
     6.5    
     6.6  val abstraction_cache = ref 
     6.7 -      (seed (thm"Reconstruction.I_simp") 
     6.8 -       (seed (thm"Reconstruction.B_simp") 
     6.9 -	(seed (thm"Reconstruction.K_simp") Net.empty)));
    6.10 +      (seed (thm"ATP_Linkup.I_simp") 
    6.11 +       (seed (thm"ATP_Linkup.B_simp") 
    6.12 +	(seed (thm"ATP_Linkup.K_simp") Net.empty)));
    6.13  
    6.14  
    6.15  (**** Transformation of Elimination Rules into First-Order Formulas****)
    6.16 @@ -137,15 +137,15 @@
    6.17  
    6.18  (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
    6.19  
    6.20 -(*Transfer a theorem into theory Reconstruction.thy if it is not already
    6.21 +(*Transfer a theorem into theory ATP_Linkup.thy if it is not already
    6.22    inside that theory -- because it's needed for Skolemization *)
    6.23  
    6.24 -(*This will refer to the final version of theory Reconstruction.*)
    6.25 +(*This will refer to the final version of theory ATP_Linkup.*)
    6.26  val recon_thy_ref = Theory.self_ref (the_context ());
    6.27  
    6.28 -(*If called while Reconstruction is being created, it will transfer to the
    6.29 +(*If called while ATP_Linkup is being created, it will transfer to the
    6.30    current version. If called afterward, it will transfer to the final version.*)
    6.31 -fun transfer_to_Reconstruction th =
    6.32 +fun transfer_to_ATP_Linkup th =
    6.33      transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
    6.34  
    6.35  fun is_taut th =
    6.36 @@ -476,7 +476,7 @@
    6.37  
    6.38  (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
    6.39  fun to_nnf th =
    6.40 -    th |> transfer_to_Reconstruction
    6.41 +    th |> transfer_to_ATP_Linkup
    6.42         |> transform_elim |> zero_var_indexes |> freeze_thm
    6.43         |> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas ~1;
    6.44  
     7.1 --- a/src/HOL/Tools/res_clause.ML	Wed Nov 08 21:45:14 2006 +0100
     7.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Nov 08 21:45:15 2006 +0100
     7.3 @@ -125,15 +125,15 @@
     7.4  		   ("op Un", "union"),
     7.5  		   ("op Int", "inter"),
     7.6  		   ("List.op @", "append"),
     7.7 -		   ("Reconstruction.fequal", "fequal"),
     7.8 -		   ("Reconstruction.COMBI", "COMBI"),
     7.9 -		   ("Reconstruction.COMBK", "COMBK"),
    7.10 -		   ("Reconstruction.COMBB", "COMBB"),
    7.11 -		   ("Reconstruction.COMBC", "COMBC"),
    7.12 -		   ("Reconstruction.COMBS", "COMBS"),
    7.13 -		   ("Reconstruction.COMBB'", "COMBB_e"),
    7.14 -		   ("Reconstruction.COMBC'", "COMBC_e"),
    7.15 -		   ("Reconstruction.COMBS'", "COMBS_e")];
    7.16 +		   ("ATP_Linkup.fequal", "fequal"),
    7.17 +		   ("ATP_Linkup.COMBI", "COMBI"),
    7.18 +		   ("ATP_Linkup.COMBK", "COMBK"),
    7.19 +		   ("ATP_Linkup.COMBB", "COMBB"),
    7.20 +		   ("ATP_Linkup.COMBC", "COMBC"),
    7.21 +		   ("ATP_Linkup.COMBS", "COMBS"),
    7.22 +		   ("ATP_Linkup.COMBB'", "COMBB_e"),
    7.23 +		   ("ATP_Linkup.COMBC'", "COMBC_e"),
    7.24 +		   ("ATP_Linkup.COMBS'", "COMBS_e")];
    7.25  
    7.26  val type_const_trans_table =
    7.27        Symtab.make [("*", "prod"),
     8.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Nov 08 21:45:14 2006 +0100
     8.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Nov 08 21:45:15 2006 +0100
     8.3 @@ -11,16 +11,16 @@
     8.4  
     8.5  (* theorems for combinators and function extensionality *)
     8.6  val ext = thm "HOL.ext";
     8.7 -val comb_I = thm "Reconstruction.COMBI_def";
     8.8 -val comb_K = thm "Reconstruction.COMBK_def";
     8.9 -val comb_B = thm "Reconstruction.COMBB_def";
    8.10 -val comb_C = thm "Reconstruction.COMBC_def";
    8.11 -val comb_S = thm "Reconstruction.COMBS_def";
    8.12 -val comb_B' = thm "Reconstruction.COMBB'_def";
    8.13 -val comb_C' = thm "Reconstruction.COMBC'_def";
    8.14 -val comb_S' = thm "Reconstruction.COMBS'_def";
    8.15 -val fequal_imp_equal = thm "Reconstruction.fequal_imp_equal";
    8.16 -val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal";
    8.17 +val comb_I = thm "ATP_Linkup.COMBI_def";
    8.18 +val comb_K = thm "ATP_Linkup.COMBK_def";
    8.19 +val comb_B = thm "ATP_Linkup.COMBB_def";
    8.20 +val comb_C = thm "ATP_Linkup.COMBC_def";
    8.21 +val comb_S = thm "ATP_Linkup.COMBS_def";
    8.22 +val comb_B' = thm "ATP_Linkup.COMBB'_def";
    8.23 +val comb_C' = thm "ATP_Linkup.COMBC'_def";
    8.24 +val comb_S' = thm "ATP_Linkup.COMBS'_def";
    8.25 +val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
    8.26 +val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
    8.27  
    8.28  (*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard
    8.29    combinators appear to work best.*)
    8.30 @@ -81,7 +81,7 @@
    8.31  
    8.32  
    8.33  (*******************************************)
    8.34 -fun mk_compact_comb (tm as (Const("Reconstruction.COMBB",_)$p) $ (Const("Reconstruction.COMBB",_)$q$r)) Bnds count_comb =
    8.35 +fun mk_compact_comb (tm as (Const("ATP_Linkup.COMBB",_)$p) $ (Const("ATP_Linkup.COMBB",_)$q$r)) Bnds count_comb =
    8.36      let val tp_p = Term.type_of1(Bnds,p)
    8.37  	val tp_q = Term.type_of1(Bnds,q)
    8.38  	val tp_r = Term.type_of1(Bnds,r)
    8.39 @@ -90,9 +90,9 @@
    8.40  	val _ = increB' count_comb
    8.41  	val _ = decreB count_comb 2
    8.42      in
    8.43 -	Const("Reconstruction.COMBB'",typ_B') $ p $ q $ r
    8.44 +	Const("ATP_Linkup.COMBB'",typ_B') $ p $ q $ r
    8.45      end
    8.46 -  | mk_compact_comb (tm as (Const("Reconstruction.COMBC",_) $ (Const("Reconstruction.COMBB",_)$p$q) $ r)) Bnds count_comb =
    8.47 +  | mk_compact_comb (tm as (Const("ATP_Linkup.COMBC",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) Bnds count_comb =
    8.48      let val tp_p = Term.type_of1(Bnds,p)
    8.49  	val tp_q = Term.type_of1(Bnds,q)
    8.50  	val tp_r = Term.type_of1(Bnds,r)
    8.51 @@ -102,9 +102,9 @@
    8.52  	val _ = decreC count_comb 1
    8.53  	val _ = decreB count_comb 1
    8.54      in
    8.55 -	Const("Reconstruction.COMBC'",typ_C') $ p $ q $ r
    8.56 +	Const("ATP_Linkup.COMBC'",typ_C') $ p $ q $ r
    8.57      end
    8.58 -  | mk_compact_comb (tm as (Const("Reconstruction.COMBS",_) $ (Const("Reconstruction.COMBB",_)$p$q) $ r)) Bnds count_comb =
    8.59 +  | mk_compact_comb (tm as (Const("ATP_Linkup.COMBS",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) Bnds count_comb =
    8.60      let val tp_p = Term.type_of1(Bnds,p)
    8.61  	val tp_q = Term.type_of1(Bnds,q)
    8.62  	val tp_r = Term.type_of1(Bnds,r)
    8.63 @@ -114,7 +114,7 @@
    8.64  	val _ = decreS count_comb 1
    8.65  	val _ = decreB count_comb 1
    8.66      in
    8.67 -	Const("Reconstruction.COMBS'",typ_S') $ p $ q $ r
    8.68 +	Const("ATP_Linkup.COMBS'",typ_S') $ p $ q $ r
    8.69      end
    8.70    | mk_compact_comb tm _ _ = tm;
    8.71  
    8.72 @@ -124,28 +124,28 @@
    8.73  fun lam2comb (Abs(x,tp,Bound 0)) _ count_comb = 
    8.74        let val _ = increI count_comb
    8.75        in 
    8.76 -	  Const("Reconstruction.COMBI",tp-->tp) 
    8.77 +	  Const("ATP_Linkup.COMBI",tp-->tp) 
    8.78        end
    8.79    | lam2comb (Abs(x,tp,Bound n)) Bnds count_comb = 
    8.80        let val tb = List.nth(Bnds,n-1)
    8.81  	  val _ = increK count_comb 
    8.82        in
    8.83 -	  Const("Reconstruction.COMBK", [tb,tp] ---> tb) $ (Bound (n-1))
    8.84 +	  Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ (Bound (n-1))
    8.85        end
    8.86    | lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb = 
    8.87        let val _ = increK count_comb 
    8.88        in 
    8.89 -	  Const("Reconstruction.COMBK",[t2,t1] ---> t2) $ Const(c,t2) 
    8.90 +	  Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2) 
    8.91        end
    8.92    | lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb =
    8.93        let val _ = increK count_comb
    8.94        in
    8.95 -	  Const("Reconstruction.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
    8.96 +	  Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
    8.97        end
    8.98    | lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb =
    8.99        let val _ = increK count_comb 
   8.100        in
   8.101 -	  Const("Reconstruction.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
   8.102 +	  Const("ATP_Linkup.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
   8.103        end
   8.104    | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds count_comb =
   8.105        let val tr = Term.type_of1(t1::Bnds,P)
   8.106 @@ -159,8 +159,8 @@
   8.107  	      val _ = increI count_comb
   8.108  	      val _ = increS count_comb
   8.109  	  in
   8.110 -	      compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ 
   8.111 -	                     Const("Reconstruction.COMBI",tI)) Bnds count_comb
   8.112 +	      compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ 
   8.113 +	                     Const("ATP_Linkup.COMBI",tI)) Bnds count_comb
   8.114  	  end
   8.115        end	    
   8.116    | lam2comb (t as (Abs(x,t1,P$Q))) Bnds count_comb =
   8.117 @@ -174,7 +174,7 @@
   8.118  		val PQ' = incr_boundvars ~1(P $ Q)
   8.119  		val _ = increK count_comb
   8.120  	    in 
   8.121 -		Const("Reconstruction.COMBK",tK) $ PQ'
   8.122 +		Const("ATP_Linkup.COMBK",tK) $ PQ'
   8.123  	    end
   8.124  	  else if nfreeP then 
   8.125  	    let val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb
   8.126 @@ -184,7 +184,7 @@
   8.127  		val tB = [tp,tq',t1] ---> tpq
   8.128  		val _ = increB count_comb
   8.129  	    in
   8.130 -		compact_comb (Const("Reconstruction.COMBB",tB) $ P' $ Q') Bnds count_comb 
   8.131 +		compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') Bnds count_comb 
   8.132  	    end
   8.133  	  else if nfreeQ then 
   8.134  	    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   8.135 @@ -194,7 +194,7 @@
   8.136  		val tC = [tp',tq,t1] ---> tpq
   8.137  		val _ = increC count_comb
   8.138  	    in
   8.139 -		compact_comb (Const("Reconstruction.COMBC",tC) $ P' $ Q') Bnds count_comb
   8.140 +		compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') Bnds count_comb
   8.141  	    end
   8.142            else
   8.143  	    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   8.144 @@ -204,7 +204,7 @@
   8.145  		val tS = [tp',tq',t1] ---> tpq
   8.146  		val _ = increS count_comb
   8.147  	    in
   8.148 -		compact_comb (Const("Reconstruction.COMBS",tS) $ P' $ Q') Bnds count_comb
   8.149 +		compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') Bnds count_comb
   8.150  	    end
   8.151        end
   8.152    | lam2comb (t as (Abs(x,t1,_))) _ _ = raise ResClause.CLAUSE("HOL CLAUSE",t);
   8.153 @@ -718,8 +718,8 @@
   8.154    completeness. Unfortunately, they are very prolific, causing greatly increased runtimes.
   8.155    They also lead to many unsound proofs. Thus it is well that the "exists too_general_bool"
   8.156    test deletes them except with the full-typed translation.*)
   8.157 -val iff_thms = [pretend_cnf "Reconstruction.iff_positive", 
   8.158 -                pretend_cnf "Reconstruction.iff_negative"];
   8.159 +val iff_thms = [pretend_cnf "ATP_Linkup.iff_positive", 
   8.160 +                pretend_cnf "ATP_Linkup.iff_negative"];
   8.161  
   8.162  fun get_helper_clauses () =
   8.163      let val IK = if !combI_count > 0 orelse !combK_count > 0 
   8.164 @@ -802,4 +802,4 @@
   8.165  	clnames
   8.166      end;
   8.167  
   8.168 -end
   8.169 \ No newline at end of file
   8.170 +end