merged
authorblanchet
Fri Jun 25 12:15:49 2010 +0200 (2010-06-25 ago)
changeset 3755308fc6b026b01
parent 37547 a92a7f45ca28
parent 37552 6034aac65143
child 37554 6c7399bc0d10
child 37566 9ca40dff25bd
merged
     1.1 --- a/src/HOL/Predicate.thy	Fri Jun 25 07:19:21 2010 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Fri Jun 25 12:15:49 2010 +0200
     1.3 @@ -645,7 +645,7 @@
     1.4  lemma "f () = False \<or> f () = True"
     1.5  by simp
     1.6  
     1.7 -lemma closure_of_bool_cases:
     1.8 +lemma closure_of_bool_cases [no_atp]:
     1.9  assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
    1.10  assumes "f = (%u. True) \<Longrightarrow> P f"
    1.11  shows "P f"
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 07:19:21 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 12:15:49 2010 +0200
     2.3 @@ -223,7 +223,7 @@
     2.4            val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
     2.5            val result =
     2.6              do_run false
     2.7 -            |> (fn (_, msecs0, _, SOME IncompleteUnprovable) =>
     2.8 +            |> (fn (_, msecs0, _, SOME _) =>
     2.9                     do_run true
    2.10                     |> (fn (output, msecs, proof, outcome) =>
    2.11                            (output, msecs0 + msecs, proof, outcome))
    2.12 @@ -298,9 +298,11 @@
    2.13  val spass_config : prover_config =
    2.14    {home_var = "SPASS_HOME",
    2.15     executable = "SPASS",
    2.16 +   (* "div 2" accounts for the fact that SPASS is often run twice. *)
    2.17     arguments = fn complete => fn timeout =>
    2.18       ("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    2.19 -      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
    2.20 +      \-VarWeight=3 -TimeLimit=" ^
    2.21 +      string_of_int (to_generous_secs timeout div 2))
    2.22       |> not complete ? prefix "-SOS=1 ",
    2.23     proof_delims = [("Here is a proof", "Formulae used in the proof")],
    2.24     known_failures =
     3.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 07:19:21 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 12:15:49 2010 +0200
     3.3 @@ -446,13 +446,15 @@
     3.4    of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
     3.5    could then fail. See comment on mk_var.*)
     3.6  fun resolve_inc_tyvars(tha,i,thb) =
     3.7 -  let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
     3.8 +  let
     3.9 +      val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
    3.10        val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
    3.11    in
    3.12        case distinct Thm.eq_thm ths of
    3.13          [th] => th
    3.14        | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
    3.15 -  end;
    3.16 +  end
    3.17 +  handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg)
    3.18  
    3.19  fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
    3.20    let
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 07:19:21 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 12:15:49 2010 +0200
     4.3 @@ -88,10 +88,11 @@
     4.4    Symtab.map_default (c, [ctyps])
     4.5                       (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
     4.6  
     4.7 -val fresh_sko_prefix = "Sledgehammer.Skox."
     4.8 +val fresh_prefix = "Sledgehammer.Fresh."
     4.9  
    4.10  val flip = Option.map not
    4.11  
    4.12 +val boring_natural_consts = [@{const_name If}]
    4.13  (* Including equality in this list might be expected to stop rules like
    4.14     subset_antisym from being chosen, but for some reason filtering works better
    4.15     with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
    4.16 @@ -113,12 +114,15 @@
    4.17        | Free x => add_const_type_to_table (const_with_typ thy x)
    4.18        | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
    4.19        | t1 $ t2 => do_term t1 #> do_term t2
    4.20 -      | Abs (_, _, t) => do_term t
    4.21 +      | Abs (_, _, t) =>
    4.22 +        (* Abstractions lead to combinators, so we add a penalty for them. *)
    4.23 +        add_const_type_to_table (gensym fresh_prefix, [])
    4.24 +        #> do_term t
    4.25        | _ => I
    4.26      fun do_quantifier sweet_pos pos body_t =
    4.27        do_formula pos body_t
    4.28        #> (if pos = SOME sweet_pos then I
    4.29 -          else add_const_type_to_table (gensym fresh_sko_prefix, []))
    4.30 +          else add_const_type_to_table (gensym fresh_prefix, []))
    4.31      and do_equality T t1 t2 =
    4.32        fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
    4.33              else do_term) [t1, t2]
    4.34 @@ -148,7 +152,8 @@
    4.35    in
    4.36      Symtab.empty
    4.37      |> (if !use_natural_form then
    4.38 -          fold (do_formula pos) ts
    4.39 +          fold (Symtab.update o rpair []) boring_natural_consts
    4.40 +          #> fold (do_formula pos) ts
    4.41          else
    4.42            fold (Symtab.update o rpair []) boring_cnf_consts
    4.43            #> fold do_term ts)
    4.44 @@ -361,9 +366,15 @@
    4.45        val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
    4.46                             Symtab.empty
    4.47        val goal_const_tab = get_consts_typs thy (SOME true) goals
    4.48 +      val relevance_threshold =
    4.49 +        if !use_natural_form then 0.9 * relevance_threshold (* experimental *)
    4.50 +        else relevance_threshold
    4.51        val _ =
    4.52          trace_msg (fn () => "Initial constants: " ^
    4.53 -                            commas (Symtab.keys goal_const_tab))
    4.54 +                            commas (goal_const_tab
    4.55 +                                    |> Symtab.dest
    4.56 +                                    |> filter (curry (op <>) [] o snd)
    4.57 +                                    |> map fst))
    4.58        val relevant =
    4.59          relevant_clauses ctxt relevance_convergence defs_relevant max_new
    4.60                           relevance_override const_tab relevance_threshold
    4.61 @@ -609,7 +620,7 @@
    4.62  fun count_literal (Literal (_, t)) = count_combterm t
    4.63  fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
    4.64  
    4.65 -val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
    4.66 +fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
    4.67  fun cnf_helper_thms thy raw =
    4.68    map (`Thm.get_name_hint)
    4.69    #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)