bugfixes concerning strange theorems
authorpaulson
Tue Oct 30 15:28:53 2007 +0100 (2007-10-30)
changeset 2524378f8aaa27493
parent 25242 6c3890cbceac
child 25244 42071ca3a14c
bugfixes concerning strange theorems
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Oct 30 15:13:48 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 30 15:28:53 2007 +0100
     1.3 @@ -468,8 +468,8 @@
     1.4          val xname = NameSpace.extern space name;
     1.5        in
     1.6          if blacklisted name then I
     1.7 -        else if is_valid (xname, ths) then cons (xname, ths)
     1.8 -        else if is_valid (name, ths) then cons (name, ths)
     1.9 +        else if is_valid (xname, ths) then cons (xname, filter_out ResAxioms.bad_for_atp ths)
    1.10 +        else if is_valid (name, ths) then cons (name, filter_out ResAxioms.bad_for_atp ths)
    1.11          else I
    1.12        end;
    1.13      val thy = ProofContext.theory_of ctxt;
    1.14 @@ -731,6 +731,8 @@
    1.15          | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
    1.16                                           get_neg_subgoals gls (n+1)
    1.17        val goal_cls = get_neg_subgoals goals 1
    1.18 +                     handle THM ("assume: variables", _, _) => 
    1.19 +                       error "Sledgehammer: Goal contains type variables (TVars)"                       
    1.20        val isFO = case !linkup_logic_mode of
    1.21  			  Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
    1.22  			| Fol => true
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Oct 30 15:13:48 2007 +0100
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Oct 30 15:28:53 2007 +0100
     2.3 @@ -10,6 +10,7 @@
     2.4    val cnf_axiom: thm -> thm list
     2.5    val pairname: thm -> string * thm
     2.6    val multi_base_blacklist: string list 
     2.7 +  val bad_for_atp: thm -> bool
     2.8    val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
     2.9    val cnf_rules_of_ths: thm list -> thm list
    2.10    val neg_clausify: thm list -> thm list
    2.11 @@ -320,6 +321,14 @@
    2.12  fun too_complex t = 
    2.13    Meson.too_many_clauses t orelse excessive_lambdas_fm [] t;
    2.14    
    2.15 +fun is_strange_thm th =
    2.16 +  case head_of (concl_of th) of
    2.17 +      Const (a,_) => (a <> "Trueprop" andalso a <> "==")
    2.18 +    | _ => false;
    2.19 +
    2.20 +fun bad_for_atp th = 
    2.21 +  PureThy.is_internal th orelse too_complex (prop_of th) orelse is_strange_thm th;
    2.22 +
    2.23  val multi_base_blacklist =
    2.24    ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
    2.25  
    2.26 @@ -381,8 +390,7 @@
    2.27  
    2.28  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    2.29  fun skolem_thm (s,th) =
    2.30 -  if (Sign.base_name s) mem_string multi_base_blacklist orelse 
    2.31 -     PureThy.is_internal th orelse too_complex (prop_of th) then []
    2.32 +  if (Sign.base_name s) mem_string multi_base_blacklist orelse bad_for_atp th then []
    2.33    else 
    2.34        let val ctxt0 = Variable.thm_context th
    2.35  	  val (nnfth,ctxt1) = to_nnf th ctxt0
    2.36 @@ -450,8 +458,7 @@
    2.37  val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
    2.38  
    2.39  fun skolem_cache th thy =
    2.40 -  if PureThy.is_internal th orelse too_complex (prop_of th) then thy
    2.41 -  else #2 (skolem_cache_thm th thy);
    2.42 +  if bad_for_atp th then thy else #2 (skolem_cache_thm th thy);
    2.43  
    2.44  fun skolem_cache_list (a,ths) thy =
    2.45    if (Sign.base_name a) mem_string multi_base_blacklist then thy
     3.1 --- a/src/HOL/Tools/res_clause.ML	Tue Oct 30 15:13:48 2007 +0100
     3.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Oct 30 15:28:53 2007 +0100
     3.3 @@ -40,7 +40,6 @@
     3.4    val string_of_fol_type : fol_type -> string
     3.5    datatype type_literal = LTVar of string * string | LTFree of string * string
     3.6    exception CLAUSE of string * term
     3.7 -  val isMeta : string -> bool
     3.8    val add_typs : typ list -> type_literal list
     3.9    val get_tvar_strs: typ list -> string list
    3.10    datatype arLit =
    3.11 @@ -261,11 +260,6 @@
    3.12        let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
    3.13        in (folTyps, union_all ts) end;
    3.14  
    3.15 -
    3.16 -(* Any variables created via the METAHYPS tactical should be treated as
    3.17 -   universal vars, although it is represented as "Free(...)" by Isabelle *)
    3.18 -val isMeta = String.isPrefix "METAHYP1_"
    3.19 -
    3.20  (*Make literals for sorted type variables*)
    3.21  fun sorts_on_typs_aux (_, [])   = []
    3.22    | sorts_on_typs_aux ((x,i),  s::ss) =
     4.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 30 15:13:48 2007 +0100
     4.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Oct 30 15:28:53 2007 +0100
     4.3 @@ -138,8 +138,7 @@
     4.4        in  (c',ts)  end
     4.5    | combterm_of thy (Free(v,t)) =
     4.6        let val (tp,ts) = type_of t
     4.7 -          val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
     4.8 -                   else CombConst(RC.make_fixed_var v, tp, [])
     4.9 +          val v' = CombConst(RC.make_fixed_var v, tp, [])
    4.10        in  (v',ts)  end
    4.11    | combterm_of thy (Var(v,t)) =
    4.12        let val (tp,ts) = type_of t