1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:42:09 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:53:55 2010 +0200
1.3 @@ -171,12 +171,12 @@
1.4 AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
1.5
1.6 (* ### FIXME: reintroduce
1.7 -fun make_clause_table xs =
1.8 +fun make_formula_table xs =
1.9 fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
1.10 -(* Remove existing axiom clauses from the conjecture clauses, as this can
1.11 +(* Remove existing axioms from the conjecture, as this can
1.12 dramatically boost an ATP's performance (for some reason). *)
1.13 -fun subtract_cls ax_clauses =
1.14 - filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
1.15 +fun subtract_cls axioms =
1.16 + filter_out (Termtab.defined (make_formula_table axioms) o prop_of)
1.17 *)
1.18
1.19 fun combformula_for_prop thy =
1.20 @@ -277,8 +277,8 @@
1.21 Axiom => HOLogic.true_const
1.22 | Conjecture => HOLogic.false_const
1.23
1.24 -(* making axiom and conjecture clauses *)
1.25 -fun make_clause ctxt (formula_name, kind, t) =
1.26 +(* making axiom and conjecture formulas *)
1.27 +fun make_formula ctxt (formula_name, kind, t) =
1.28 let
1.29 val thy = ProofContext.theory_of ctxt
1.30 (* ### FIXME: perform other transformations previously done by
1.31 @@ -293,13 +293,13 @@
1.32 kind = kind, ctypes_sorts = ctypes_sorts}
1.33 end
1.34
1.35 -fun make_axiom_clause ctxt (name, th) =
1.36 - (name, make_clause ctxt (name, Axiom, prop_of th))
1.37 -fun make_conjecture_clauses ctxt ts =
1.38 - map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
1.39 +fun make_axiom ctxt (name, th) =
1.40 + (name, make_formula ctxt (name, Axiom, prop_of th))
1.41 +fun make_conjectures ctxt ts =
1.42 + map2 (fn j => fn t => make_formula ctxt (Int.toString j, Conjecture, t))
1.43 (0 upto length ts - 1) ts
1.44
1.45 -(** Helper clauses **)
1.46 +(** Helper facts **)
1.47
1.48 fun count_combterm (CombConst ((s, _), _, _)) =
1.49 Symtab.map_entry s (Integer.add 1)
1.50 @@ -324,24 +324,24 @@
1.51 Symtab.make (maps (maps (map (rpair 0) o fst))
1.52 [optional_helpers, optional_typed_helpers])
1.53
1.54 -fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
1.55 +fun get_helper_facts ctxt is_FO full_types conjectures axioms =
1.56 let
1.57 - val ct = fold (fold count_fol_formula) [conjectures, axclauses]
1.58 - init_counters
1.59 + val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
1.60 fun is_needed c = the (Symtab.lookup ct c) > 0
1.61 - val cnfs =
1.62 - (optional_helpers
1.63 - |> full_types ? append optional_typed_helpers
1.64 - |> maps (fn (ss, ths) =>
1.65 - if exists is_needed ss then map (`Thm.get_name_hint) ths
1.66 - else [])) @
1.67 - (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
1.68 - in map (snd o make_axiom_clause ctxt) cnfs end
1.69 + in
1.70 + (optional_helpers
1.71 + |> full_types ? append optional_typed_helpers
1.72 + |> maps (fn (ss, ths) =>
1.73 + if exists is_needed ss then map (`Thm.get_name_hint) ths
1.74 + else [])) @
1.75 + (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
1.76 + |> map (snd o make_axiom ctxt)
1.77 + end
1.78
1.79 fun s_not (@{const Not} $ t) = t
1.80 | s_not t = @{const Not} $ t
1.81
1.82 -fun prepare_clauses ctxt full_types hyp_ts concl_t axcls =
1.83 +fun prepare_formulas ctxt full_types hyp_ts concl_t axcls =
1.84 let
1.85 val thy = ProofContext.theory_of ctxt
1.86 val goal_t = Logic.list_implies (hyp_ts, concl_t)
1.87 @@ -350,19 +350,18 @@
1.88 val subs = tfree_classes_of_terms [goal_t]
1.89 val supers = tvar_classes_of_terms axtms
1.90 val tycons = type_consts_of_terms thy (goal_t :: axtms)
1.91 - (* TFrees in conjecture clauses; TVars in axiom clauses *)
1.92 + (* TFrees in the conjecture; TVars in the axioms *)
1.93 val conjectures =
1.94 map (s_not o HOLogic.dest_Trueprop) hyp_ts @
1.95 - [HOLogic.dest_Trueprop concl_t]
1.96 - |> make_conjecture_clauses ctxt
1.97 - val (clnames, axioms) = ListPair.unzip (map (make_axiom_clause ctxt) axcls)
1.98 - val helper_clauses =
1.99 - get_helper_clauses ctxt is_FO full_types conjectures axioms
1.100 + [HOLogic.dest_Trueprop concl_t]
1.101 + |> make_conjectures ctxt
1.102 + val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt) axcls)
1.103 + val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
1.104 val (supers', arity_clauses) = make_arity_clauses thy tycons supers
1.105 val class_rel_clauses = make_class_rel_clauses thy subs supers'
1.106 in
1.107 (Vector.fromList clnames,
1.108 - (conjectures, axioms, helper_clauses, class_rel_clauses, arity_clauses))
1.109 + (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
1.110 end
1.111
1.112 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
1.113 @@ -585,14 +584,14 @@
1.114 (const_table_for_problem explicit_apply problem) problem
1.115
1.116 fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
1.117 - file (conjectures, axioms, helper_clauses,
1.118 - class_rel_clauses, arity_clauses) =
1.119 + file (conjectures, axioms, helper_facts, class_rel_clauses,
1.120 + arity_clauses) =
1.121 let
1.122 val axiom_lines = map (problem_line_for_axiom full_types) axioms
1.123 val class_rel_lines =
1.124 map problem_line_for_class_rel_clause class_rel_clauses
1.125 val arity_lines = map problem_line_for_arity_clause arity_clauses
1.126 - val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
1.127 + val helper_lines = map (problem_line_for_axiom full_types) helper_facts
1.128 val conjecture_lines =
1.129 map (problem_line_for_conjecture full_types) conjectures
1.130 val tfree_lines = problem_lines_for_free_types conjectures
1.131 @@ -675,7 +674,6 @@
1.132 minimize_command timeout
1.133 ({subgoal, goal, relevance_override, axioms} : problem) =
1.134 let
1.135 - (* get clauses and prepare them for writing *)
1.136 val (ctxt, (_, th)) = goal;
1.137 val thy = ProofContext.theory_of ctxt
1.138 (* ### FIXME: (1) preprocessing for "if" etc. *)
1.139 @@ -688,8 +686,8 @@
1.140 max_new_relevant_facts_per_iter
1.141 (the_default prefers_theory_relevant theory_relevant)
1.142 relevance_override goal hyp_ts concl_t
1.143 - val (internal_thm_names, clauses) =
1.144 - prepare_clauses ctxt full_types hyp_ts concl_t the_axioms
1.145 + val (internal_thm_names, formulas) =
1.146 + prepare_formulas ctxt full_types hyp_ts concl_t the_axioms
1.147
1.148 (* path to unique problem file *)
1.149 val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
1.150 @@ -757,7 +755,7 @@
1.151 val readable_names = debug andalso overlord
1.152 val (pool, conjecture_offset) =
1.153 write_tptp_file thy readable_names explicit_forall full_types
1.154 - explicit_apply probfile clauses
1.155 + explicit_apply probfile formulas
1.156 val conjecture_shape =
1.157 conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
1.158 |> map single
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jul 29 14:42:09 2010 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jul 29 14:53:55 2010 +0200
2.3 @@ -88,18 +88,8 @@
2.4 (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
2.5
2.6 val fresh_prefix = "Sledgehammer.Fresh."
2.7 -
2.8 val flip = Option.map not
2.9 -
2.10 val boring_natural_consts = [@{const_name If}]
2.11 -(* Including equality in this list might be expected to stop rules like
2.12 - subset_antisym from being chosen, but for some reason filtering works better
2.13 - with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
2.14 - because any remaining occurrences must be within comprehensions. *)
2.15 -val boring_cnf_consts =
2.16 - [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
2.17 - @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
2.18 - @{const_name "op ="}]
2.19
2.20 fun get_consts_typs thy pos ts =
2.21 let
2.22 @@ -213,11 +203,8 @@
2.23 (the (Symtab.lookup const_tab c)
2.24 handle Option.Option => raise Fail ("Const: " ^ c)) 0
2.25
2.26 -(*A surprising number of theorems contain only a few significant constants.
2.27 - These include all induction rules, and other general theorems. Filtering
2.28 - theorems in clause form reveals these complexities in the form of Skolem
2.29 - functions. If we were instead to filter theorems in their natural form,
2.30 - some other method of measuring theorem complexity would become necessary.*)
2.31 +(* A surprising number of theorems contain only a few significant constants.
2.32 + These include all induction rules, and other general theorems. *)
2.33
2.34 (* "log" seems best in practice. A constant function of one ignores the constant
2.35 frequencies. *)
2.36 @@ -228,8 +215,8 @@
2.37
2.38 (*Relevant constants are weighted according to frequency,
2.39 but irrelevant constants are simply counted. Otherwise, Skolem functions,
2.40 - which are rare, would harm a clause's chances of being picked.*)
2.41 -fun clause_weight const_tab gctyps consts_typs =
2.42 + which are rare, would harm a formula's chances of being picked.*)
2.43 +fun formula_weight const_tab gctyps consts_typs =
2.44 let val rel = filter (uni_mem gctyps) consts_typs
2.45 val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0
2.46 in
2.47 @@ -270,13 +257,13 @@
2.48 | _ => false
2.49 end;
2.50
2.51 -type annotated_cnf_thm = (string * thm) * (string * const_typ list) list
2.52 +type annotated_thm = (string * thm) * (string * const_typ list) list
2.53
2.54 (*For a reverse sort, putting the largest values first.*)
2.55 fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
2.56
2.57 -(*Limit the number of new clauses, to prevent runaway acceptance.*)
2.58 -fun take_best max_new (newpairs : (annotated_cnf_thm * real) list) =
2.59 +(* Limit the number of new facts, to prevent runaway acceptance. *)
2.60 +fun take_best max_new (newpairs : (annotated_thm * real) list) =
2.61 let val nnew = length newpairs
2.62 in
2.63 if nnew <= max_new then (map #1 newpairs, [])
2.64 @@ -294,8 +281,8 @@
2.65 end
2.66 end;
2.67
2.68 -fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
2.69 - ({add, del, ...} : relevance_override) const_tab =
2.70 +fun relevant_facts ctxt relevance_convergence defs_relevant max_new
2.71 + ({add, del, ...} : relevance_override) const_tab =
2.72 let
2.73 val thy = ProofContext.theory_of ctxt
2.74 val add_thms = maps (ProofContext.get_fact ctxt) add
2.75 @@ -323,7 +310,7 @@
2.76 val weight =
2.77 if member Thm.eq_thm add_thms th then 1.0
2.78 else if member Thm.eq_thm del_thms th then 0.0
2.79 - else clause_weight const_tab rel_const_tab consts_typs
2.80 + else formula_weight const_tab rel_const_tab consts_typs
2.81 in
2.82 if weight >= threshold orelse
2.83 (defs_relevant andalso defines thy th rel_const_tab) then
2.84 @@ -335,7 +322,7 @@
2.85 relevant (newrels, ax :: rejects) axs
2.86 end
2.87 in
2.88 - trace_msg (fn () => "relevant_clauses, current threshold: " ^
2.89 + trace_msg (fn () => "relevant_facts, current threshold: " ^
2.90 Real.toString threshold);
2.91 relevant ([], [])
2.92 end
2.93 @@ -361,11 +348,11 @@
2.94 |> filter (curry (op <>) [] o snd)
2.95 |> map fst))
2.96 val relevant =
2.97 - relevant_clauses ctxt relevance_convergence defs_relevant max_new
2.98 - relevance_override const_tab relevance_threshold
2.99 - goal_const_tab
2.100 - (map (pair_consts_typs_axiom theory_relevant thy)
2.101 - axioms)
2.102 + relevant_facts ctxt relevance_convergence defs_relevant max_new
2.103 + relevance_override const_tab relevance_threshold
2.104 + goal_const_tab
2.105 + (map (pair_consts_typs_axiom theory_relevant thy)
2.106 + axioms)
2.107 in
2.108 trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
2.109 relevant
2.110 @@ -387,11 +374,9 @@
2.111 String.isSuffix "_def" a orelse String.isSuffix "_defs" a
2.112 end;
2.113
2.114 -fun make_clause_table xs =
2.115 +fun make_fact_table xs =
2.116 fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
2.117 -
2.118 -fun make_unique xs =
2.119 - Termtab.fold (cons o snd) (make_clause_table xs) []
2.120 +fun make_unique xs = Termtab.fold (cons o snd) (make_fact_table xs) []
2.121
2.122 (* FIXME: put other record thms here, or declare as "no_atp" *)
2.123 val multi_base_blacklist =
2.124 @@ -427,8 +412,7 @@
2.125 | apply_depth _ = 0
2.126
2.127 fun is_formula_too_complex t =
2.128 - apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
2.129 - formula_has_too_many_lambdas [] t
2.130 + apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
2.131
2.132 val exists_sledgehammer_const =
2.133 exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
2.134 @@ -512,12 +496,13 @@
2.135 (* ATP invocation methods setup *)
2.136 (***************************************************************)
2.137
2.138 -(**** Predicates to detect unwanted clauses (prolific or likely to cause
2.139 +(**** Predicates to detect unwanted facts (prolific or likely to cause
2.140 unsoundness) ****)
2.141
2.142 (** Too general means, positive equality literal with a variable X as one operand,
2.143 when X does not occur properly in the other operand. This rules out clearly
2.144 - inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
2.145 + inconsistent facts such as V = a | V = b, though it by no means guarantees
2.146 + soundness. **)
2.147
2.148 fun var_occurs_in_term ix =
2.149 let
2.150 @@ -532,6 +517,7 @@
2.151 (*Unwanted equalities include
2.152 (1) those between a variable that does not properly occur in the second operand,
2.153 (2) those between a variable and a record, since these seem to be prolific "cases" thms
2.154 + (* FIXME: still a problem? *)
2.155 *)
2.156 fun too_general_eqterms (Var (ix,T), t) =
2.157 not (var_occurs_in_term ix t) orelse is_record_type T
2.158 @@ -544,14 +530,14 @@
2.159 fun has_typed_var tycons = exists_subterm
2.160 (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
2.161
2.162 -(* Clauses are forbidden to contain variables of these types. The typical reason
2.163 +(* Facts are forbidden to contain variables of these types. The typical reason
2.164 is that they lead to unsoundness. Note that "unit" satisfies numerous
2.165 - equations like "?x = ()". The resulting clause will have no type constraint,
2.166 + equations like "?x = ()". The resulting clauses will have no type constraint,
2.167 yielding false proofs. Even "bool" leads to many unsound proofs, though only
2.168 for higher-order problems. *)
2.169 val dangerous_types = [@{type_name unit}, @{type_name bool}];
2.170
2.171 -(* Clauses containing variables of type "unit" or "bool" or of the form
2.172 +(* Facts containing variables of type "unit" or "bool" or of the form
2.173 "?x = A | ?x = B | ?x = C" are likely to lead to unsound proofs if types are
2.174 omitted. *)
2.175 fun is_dangerous_term _ @{prop True} = true
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 14:42:09 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 14:53:55 2010 +0200
3.3 @@ -67,10 +67,10 @@
3.4 fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
3.5
3.6 fun index_in_shape x = find_index (exists (curry (op =) x))
3.7 -fun is_axiom_clause_number thm_names num =
3.8 +fun is_axiom_number thm_names num =
3.9 num > 0 andalso num <= Vector.length thm_names andalso
3.10 Vector.sub (thm_names, num - 1) <> ""
3.11 -fun is_conjecture_clause_number conjecture_shape num =
3.12 +fun is_conjecture_number conjecture_shape num =
3.13 index_in_shape num conjecture_shape >= 0
3.14
3.15 fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
3.16 @@ -281,7 +281,7 @@
3.17 (SOME b, [T]) => (pos, b, T)
3.18 | _ => raise FO_TERM [u]
3.19
3.20 -(** Accumulate type constraints in a clause: negative type literals **)
3.21 +(** Accumulate type constraints in a formula: negative type literals **)
3.22 fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
3.23 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
3.24 | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
3.25 @@ -407,8 +407,8 @@
3.26 | frees as (_, free_T) :: _ =>
3.27 Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t)
3.28
3.29 -(* Interpret a list of syntax trees as a clause, extracting sort constraints
3.30 - as they appear in the formula. *)
3.31 +(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
3.32 + appear in the formula. *)
3.33 fun prop_from_formula thy full_types tfrees phi =
3.34 let
3.35 fun do_formula pos phi =
3.36 @@ -484,13 +484,13 @@
3.37 | replace_deps_in_line p (Inference (num, t, deps)) =
3.38 Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
3.39
3.40 -(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
3.41 - only in type information.*)
3.42 +(* Discard axioms; consolidate adjacent lines that prove the same formula, since
3.43 + they differ only in type information.*)
3.44 fun add_line _ _ (line as Definition _) lines = line :: lines
3.45 | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
3.46 - (* No dependencies: axiom, conjecture clause, or internal axioms or
3.47 - definitions (Vampire). *)
3.48 - if is_axiom_clause_number thm_names num then
3.49 + (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
3.50 + definitions. *)
3.51 + if is_axiom_number thm_names num then
3.52 (* Axioms are not proof lines. *)
3.53 if is_only_type_information t then
3.54 map (replace_deps_in_line (num, [])) lines
3.55 @@ -499,7 +499,7 @@
3.56 (_, []) => lines (*no repetition of proof line*)
3.57 | (pre, Inference (num', _, _) :: post) =>
3.58 pre @ map (replace_deps_in_line (num', [num])) post
3.59 - else if is_conjecture_clause_number conjecture_shape num then
3.60 + else if is_conjecture_number conjecture_shape num then
3.61 Inference (num, t, []) :: lines
3.62 else
3.63 map (replace_deps_in_line (num, [])) lines
3.64 @@ -539,8 +539,8 @@
3.65 | add_desired_line isar_shrink_factor conjecture_shape thm_names frees
3.66 (Inference (num, t, deps)) (j, lines) =
3.67 (j + 1,
3.68 - if is_axiom_clause_number thm_names num orelse
3.69 - is_conjecture_clause_number conjecture_shape num orelse
3.70 + if is_axiom_number thm_names num orelse
3.71 + is_conjecture_number conjecture_shape num orelse
3.72 (not (is_only_type_information t) andalso
3.73 null (Term.add_tvars t []) andalso
3.74 not (exists_subterm (is_bad_free frees) t) andalso
3.75 @@ -562,10 +562,8 @@
3.76 let
3.77 fun axiom_name num =
3.78 let val j = Int.fromString num |> the_default ~1 in
3.79 - if is_axiom_clause_number thm_names j then
3.80 - SOME (Vector.sub (thm_names, j - 1))
3.81 - else
3.82 - NONE
3.83 + if is_axiom_number thm_names j then SOME (Vector.sub (thm_names, j - 1))
3.84 + else NONE
3.85 end
3.86 val tokens_of =
3.87 String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
3.88 @@ -655,7 +653,7 @@
3.89 | smart_case_split proofs facts = CaseSplit (proofs, facts)
3.90
3.91 fun add_fact_from_dep thm_names num =
3.92 - if is_axiom_clause_number thm_names num then
3.93 + if is_axiom_number thm_names num then
3.94 apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
3.95 else
3.96 apfst (insert (op =) (raw_prefix, num))