removed dead code
authorpaulson
Wed Oct 10 15:05:42 2007 +0200 (2007-10-10)
changeset 249435f5679e2ec2f
parent 24942 39a23aadc7e1
child 24944 16cb899de153
removed dead code
src/HOL/ATP_Linkup.thy
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Wed Oct 10 15:05:34 2007 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Oct 10 15:05:42 2007 +0200
     1.3 @@ -38,15 +38,6 @@
     1.4  definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
     1.5    where "COMBS P Q R == P R (Q R)"
     1.6  
     1.7 -definition COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
     1.8 -  where "COMBB' M P Q R == M (P (Q R))"
     1.9 -
    1.10 -definition COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
    1.11 -  where "COMBC' M P Q R == M (P R) Q"
    1.12 -
    1.13 -definition COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
    1.14 -  where "COMBS' M P Q R == M (P R) (Q R)"
    1.15 -
    1.16  definition fequal :: "'a => 'a => bool"
    1.17    where "fequal X Y == (X=Y)"
    1.18  
     2.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Oct 10 15:05:34 2007 +0200
     2.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Oct 10 15:05:42 2007 +0200
     2.3 @@ -2,10 +2,6 @@
     2.4     Author: Jia Meng, NICTA
     2.5  
     2.6  FOL clauses translated from HOL formulae.
     2.7 -
     2.8 -The combinator code needs to be deleted after the translation paper has been published.
     2.9 -It cannot be used with proof reconstruction because combinators are not introduced by proof.
    2.10 -The Turner combinators (B', C', S') yield no improvement and should be deleted.
    2.11  *)
    2.12  
    2.13  signature RES_HOL_CLAUSE =
    2.14 @@ -49,9 +45,6 @@
    2.15  val comb_B = thm "ATP_Linkup.COMBB_def";
    2.16  val comb_C = thm "ATP_Linkup.COMBC_def";
    2.17  val comb_S = thm "ATP_Linkup.COMBS_def";
    2.18 -val comb_B' = thm "ATP_Linkup.COMBB'_def";
    2.19 -val comb_C' = thm "ATP_Linkup.COMBC'_def";
    2.20 -val comb_S' = thm "ATP_Linkup.COMBS'_def";
    2.21  val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
    2.22  val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
    2.23  
    2.24 @@ -387,8 +380,7 @@
    2.25  val init_counters =
    2.26      Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
    2.27                   ("c_COMBB", 0), ("c_COMBC", 0),
    2.28 -                 ("c_COMBS", 0), ("c_COMBB_e", 0),
    2.29 -                 ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
    2.30 +                 ("c_COMBS", 0)];
    2.31  
    2.32  fun count_combterm (CombConst(c,tp,_), ct) =
    2.33       (case Symtab.lookup ct c of NONE => ct  (*no counter*)
    2.34 @@ -421,15 +413,9 @@
    2.35          val S = if needed "c_COMBS"
    2.36                  then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
    2.37                  else []
    2.38 -        val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e"
    2.39 -                   then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C'])
    2.40 -                   else []
    2.41 -        val S' = if needed "c_COMBS_e"
    2.42 -                 then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S'])
    2.43 -                 else []
    2.44          val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
    2.45      in
    2.46 -        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S @ B'C' @ S'))
    2.47 +        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S))
    2.48      end;
    2.49  
    2.50  (*Find the minimal arity of each function mentioned in the term. Also, note which uses