never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
authorblanchet
Thu Jun 24 17:57:36 2010 +0200 (2010-06-24)
changeset 37541a76ace919f1c
parent 37540 48273d1ea331
child 37542 8db1e5d4b93f
never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Jun 24 17:27:18 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Thu Jun 24 17:57:36 2010 +0200
     1.3 @@ -53,16 +53,6 @@
     1.4  lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
     1.5    by (simp add: fequal_def)
     1.6  
     1.7 -text{*These two represent the equivalence between Boolean equality and iff.
     1.8 -They can't be converted to clauses automatically, as the iff would be
     1.9 -expanded...*}
    1.10 -
    1.11 -lemma iff_positive: "P \<or> Q \<or> P = Q"
    1.12 -by blast
    1.13 -
    1.14 -lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
    1.15 -by blast
    1.16 -
    1.17  text{*Theorems for translation to combinators*}
    1.18  
    1.19  lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 17:27:18 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 17:57:36 2010 +0200
     2.3 @@ -35,13 +35,15 @@
     2.4  
     2.5  type cnf_thm = thm * ((string * int) * thm)
     2.6  
     2.7 +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
     2.8 +
     2.9  (* Used to label theorems chained into the goal. *)
    2.10 -val chained_prefix = "Sledgehammer.chained_"
    2.11 +val chained_prefix = sledgehammer_prefix ^ "chained_"
    2.12  
    2.13  val trace = Unsynchronized.ref false;
    2.14  fun trace_msg msg = if !trace then tracing (msg ()) else ();
    2.15  
    2.16 -val skolem_theory_name = "Sledgehammer.Sko"
    2.17 +val skolem_theory_name = sledgehammer_prefix ^ "Sko"
    2.18  val skolem_prefix = "sko_"
    2.19  val skolem_infix = "$"
    2.20  
    2.21 @@ -382,6 +384,8 @@
    2.22  fun is_theorem_bad_for_atps thm =
    2.23    let val t = prop_of thm in
    2.24      is_formula_too_complex t orelse exists_type type_has_topsort t orelse
    2.25 +    exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s
    2.26 +                   | _ => false) t orelse
    2.27      is_strange_thm thm
    2.28    end
    2.29