# HG changeset patch # User haftmann # Date 1277443161 -7200 # Node ID a92a7f45ca28a3e7567affda0e64f4d66dea0761 # Parent f5a4b7ac635f174f842cd66d8dbcbba49c67d163# Parent d1fa353e1c4a5e6ff16c42e53f974ec906e9c440 merged diff -r d1fa353e1c4a -r a92a7f45ca28 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Jun 24 21:04:35 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Fri Jun 25 07:19:21 2010 +0200 @@ -53,16 +53,6 @@ lemma equal_imp_fequal [no_atp]: "X = Y \ fequal X Y" by (simp add: fequal_def) -text{*These two represent the equivalence between Boolean equality and iff. -They can't be converted to clauses automatically, as the iff would be -expanded...*} - -lemma iff_positive: "P \ Q \ P = Q" -by blast - -lemma iff_negative: "\ P \ \ Q \ P = Q" -by blast - text{*Theorems for translation to combinators*} lemma abs_S [no_atp]: "\x. (f x) (g x) \ COMBS f g" diff -r d1fa353e1c4a -r a92a7f45ca28 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 24 21:04:35 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Jun 25 07:19:21 2010 +0200 @@ -2520,6 +2520,8 @@ let val pred_intro_rule = nth (intros_of ctxt pred) (i - 1) val (in_ts, clause_out_ts) = split_mode mode ts; + val split_ss = HOL_basic_ss' addsimps [@{thm split_eta}, @{thm split_beta}, + @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] fun prove_prems2 out_ts [] = print_tac options "before prove_match2 - last call:" THEN prove_match2 options ctxt out_ts @@ -2530,14 +2532,12 @@ THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1)) THEN (asm_full_simp_tac HOL_basic_ss' 1) THEN SOLVED (print_tac options "state before applying intro rule:" - THEN (rtac pred_intro_rule 1) + THEN (rtac pred_intro_rule (* How to handle equality correctly? *) - THEN (print_tac options "state before assumption matching") - THEN (REPEAT (atac 1 ORELSE - (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps - [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, - @{thm "snd_conv"}, @{thm pair_collapse}]) 1) - THEN print_tac options "state after simp_tac:")))) + THEN_ALL_NEW (K (print_tac options "state before assumption matching") + THEN' (fn i => REPEAT (atac i ORELSE (CHANGED (asm_full_simp_tac split_ss i) + THEN print_tac options "state after pre-simplification:"))) + THEN' (K (print_tac options "state after assumption matching:")))) 1) | prove_prems2 out_ts ((p, deriv) :: ps) = let val mode = head_mode_of deriv diff -r d1fa353e1c4a -r a92a7f45ca28 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Jun 24 21:04:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 25 07:19:21 2010 +0200 @@ -679,8 +679,7 @@ (*The modes FO and FT are sticky. HO can be downgraded to FO.*) fun set_mode FO = FO | set_mode HO = - if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO - else HO + if forall (is_quasi_fol_theorem thy) (cls @ ths) then FO else HO | set_mode FT = FT val mode = set_mode mode0 (*transform isabelle clause to metis clause *) diff -r d1fa353e1c4a -r a92a7f45ca28 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jun 24 21:04:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Jun 25 07:19:21 2010 +0200 @@ -21,7 +21,7 @@ val tvar_classes_of_terms : term list -> string list val tfree_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list - val is_quasi_fol_term : theory -> term -> bool + val is_quasi_fol_theorem : theory -> thm -> bool val relevant_facts : bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list @@ -88,42 +88,70 @@ Symtab.map_default (c, [ctyps]) (fn [] => [] | ctypss => insert (op =) ctyps ctypss) -val fresh_Ex_prefix = "Sledgehammer.Ex." +val fresh_sko_prefix = "Sledgehammer.Skox." + +val flip = Option.map not -fun get_goal_consts_typs thy goals = +(* Including equality in this list might be expected to stop rules like + subset_antisym from being chosen, but for some reason filtering works better + with them listed. The logical signs All, Ex, &, and --> are omitted for CNF + because any remaining occurrences must be within comprehensions. *) +val boring_cnf_consts = + [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, + @{const_name "=="}, @{const_name "op |"}, @{const_name Not}, + @{const_name "op ="}] + +fun get_consts_typs thy pos ts = let - val use_natural_form = !use_natural_form (* Free variables are included, as well as constants, to handle locales. "skolem_id" is included to increase the complexity of theorems containing Skolem functions. In non-CNF form, "Ex" is included but each occurrence is considered fresh, to simulate the effect of Skolemization. *) - fun aux (Const (x as (s, _))) = - (if s = @{const_name Ex} andalso use_natural_form then - (gensym fresh_Ex_prefix, []) - else - (const_with_typ thy x)) - |> add_const_type_to_table - | aux (Free x) = add_const_type_to_table (const_with_typ thy x) - | aux ((t as Const (@{const_name skolem_id}, _)) $ _) = aux t - | aux (t $ u) = aux t #> aux u - | aux (Abs (_, _, t)) = aux t - | aux _ = I - (* Including equality in this list might be expected to stop rules like - subset_antisym from being chosen, but for some reason filtering works better - with them listed. The logical signs All, Ex, &, and --> are omitted for CNF - because any remaining occurrences must be within comprehensions. *) - val standard_consts = - [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, - @{const_name "=="}, @{const_name "op |"}, @{const_name Not}, - @{const_name "op ="}] @ - (if use_natural_form then - [@{const_name All}, @{const_name Ex}, @{const_name "op &"}, - @{const_name "op -->"}] - else - []) + fun do_term t = + case t of + Const x => add_const_type_to_table (const_with_typ thy x) + | Free x => add_const_type_to_table (const_with_typ thy x) + | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t + | t1 $ t2 => do_term t1 #> do_term t2 + | Abs (_, _, t) => do_term t + | _ => I + fun do_quantifier sweet_pos pos body_t = + do_formula pos body_t + #> (if pos = SOME sweet_pos then I + else add_const_type_to_table (gensym fresh_sko_prefix, [])) + and do_equality T t1 t2 = + fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE + else do_term) [t1, t2] + and do_formula pos t = + case t of + Const (@{const_name all}, _) $ Abs (_, _, body_t) => + do_quantifier false pos body_t + | @{const "==>"} $ t1 $ t2 => + do_formula (flip pos) t1 #> do_formula pos t2 + | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => + do_equality T t1 t2 + | @{const Trueprop} $ t1 => do_formula pos t1 + | @{const Not} $ t1 => do_formula (flip pos) t1 + | Const (@{const_name All}, _) $ Abs (_, _, body_t) => + do_quantifier false pos body_t + | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) => + do_quantifier true pos body_t + | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2] + | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2] + | @{const "op -->"} $ t1 $ t2 => + do_formula (flip pos) t1 #> do_formula pos t2 + | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 => + do_equality T t1 t2 + | (t0 as Const (_, @{typ bool})) $ t1 => + do_term t0 #> do_formula pos t1 (* theory constant *) + | _ => do_term t in - Symtab.empty |> fold (Symtab.update o rpair []) standard_consts - |> fold aux goals + Symtab.empty + |> (if !use_natural_form then + fold (do_formula pos) ts + else + fold (Symtab.update o rpair []) boring_cnf_consts + #> fold do_term ts) end (*Inserts a dummy "constant" referring to the theory name, so that relevance @@ -217,7 +245,7 @@ fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys; fun consts_typs_of_term thy t = - Symtab.fold add_expand_pairs (get_goal_consts_typs thy [t]) [] + Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) [] fun pair_consts_typs_axiom theory_relevant thy axiom = (axiom, axiom |> appropriate_prop_of theory_relevant @@ -306,9 +334,11 @@ if weight >= threshold orelse (defs_relevant andalso defines thy (#1 clsthm) rel_const_tab) then - (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ - " passes: " ^ Real.toString weight); - relevant ((ax, weight) :: newrels, rejects) axs) + (trace_msg (fn () => + name ^ " clause " ^ Int.toString n ^ + " passes: " ^ Real.toString weight + (* ^ " consts: " ^ commas (map fst consts_typs) *)); + relevant ((ax, weight) :: newrels, rejects) axs) else relevant (newrels, ax :: rejects) axs end @@ -322,11 +352,15 @@ fun relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override thy (axioms : cnf_thm list) goals = - if relevance_threshold > 0.0 then + if relevance_threshold > 1.0 then + [] + else if relevance_threshold < 0.0 then + axioms + else let val const_tab = fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty - val goal_const_tab = get_goal_consts_typs thy goals + val goal_const_tab = get_consts_typs thy (SOME true) goals val _ = trace_msg (fn () => "Initial constants: " ^ commas (Symtab.keys goal_const_tab)) @@ -340,8 +374,6 @@ trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); relevant end - else - axioms; (***************************************************************) (* Retrieving and filtering lemmas *) @@ -374,6 +406,9 @@ fun subtract_cls ax_clauses = filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of) +val exists_sledgehammer_const = + exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of + fun all_name_thms_pairs respect_no_atp ctxt chained_ths = let val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); @@ -396,7 +431,8 @@ val name1 = Facts.extern facts name; val name2 = Name_Space.extern full_space name; - val ths = filter_out is_theorem_bad_for_atps ths0; + val ths = filter_out (is_theorem_bad_for_atps orf + exists_sledgehammer_const) ths0 in case find_first check_thms [name1, name2, name] of NONE => I @@ -483,13 +519,8 @@ (* ATP invocation methods setup *) (***************************************************************) -fun is_quasi_fol_term thy = - Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] - -(*Ensures that no higher-order theorems "leak out"*) -fun restrict_to_logic thy true cls = - filter (is_quasi_fol_term thy o prop_of o fst) cls - | restrict_to_logic _ false cls = cls +fun is_quasi_fol_theorem thy = + Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****) @@ -539,43 +570,35 @@ (has_typed_var dangerous_types t orelse forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t))) -fun remove_dangerous_clauses full_types add_thms = - filter_out (fn (cnf_th, (_, orig_th)) => - not (member Thm.eq_thm add_thms orig_th) andalso - is_dangerous_term full_types (prop_of cnf_th)) - fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of fun relevant_facts full_types respect_no_atp relevance_threshold relevance_convergence defs_relevant max_new theory_relevant (relevance_override as {add, del, only}) (ctxt, (chained_ths, _)) goal_cls = - if (only andalso null add) orelse relevance_threshold > 1.0 then - [] - else - let - val thy = ProofContext.theory_of ctxt - val has_override = not (null add) orelse not (null del) - val is_FO = is_fol_goal thy goal_cls - val axioms = - checked_name_thm_pairs (respect_no_atp andalso not only) ctxt - (if only then map (name_thms_pair_from_ref ctxt chained_ths) add - else all_name_thms_pairs respect_no_atp ctxt chained_ths) - |> cnf_rules_pairs thy - |> not has_override ? make_unique - |> not only ? restrict_to_logic thy is_FO - |> (if only then - I - else - remove_dangerous_clauses full_types - (maps (ProofContext.get_fact ctxt) add)) - in - relevance_filter ctxt relevance_threshold relevance_convergence - defs_relevant max_new theory_relevant relevance_override - thy axioms (map prop_of goal_cls) - |> has_override ? make_unique - |> sort (prod_ord string_ord int_ord o pairself (fst o snd)) - end + let + val thy = ProofContext.theory_of ctxt + val add_thms = maps (ProofContext.get_fact ctxt) add + val has_override = not (null add) orelse not (null del) + val is_FO = is_fol_goal thy goal_cls + val axioms = + checked_name_thm_pairs (respect_no_atp andalso not only) ctxt + (map (name_thms_pair_from_ref ctxt chained_ths) add @ + (if only then [] + else all_name_thms_pairs respect_no_atp ctxt chained_ths)) + |> cnf_rules_pairs thy + |> not has_override ? make_unique + |> filter (fn (cnf_thm, (_, orig_thm)) => + member Thm.eq_thm add_thms orig_thm orelse + ((not is_FO orelse is_quasi_fol_theorem thy cnf_thm) andalso + not (is_dangerous_term full_types (prop_of cnf_thm)))) + in + relevance_filter ctxt relevance_threshold relevance_convergence + defs_relevant max_new theory_relevant relevance_override + thy axioms (map prop_of goal_cls) + |> has_override ? make_unique + |> sort (prod_ord string_ord int_ord o pairself (fst o snd)) + end (** Helper clauses **) diff -r d1fa353e1c4a -r a92a7f45ca28 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Thu Jun 24 21:04:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 25 07:19:21 2010 +0200 @@ -8,6 +8,8 @@ signature SLEDGEHAMMER_FACT_PREPROCESSOR = sig type cnf_thm = thm * ((string * int) * thm) + + val sledgehammer_prefix: string val chained_prefix: string val trace: bool Unsynchronized.ref val trace_msg: (unit -> string) -> unit @@ -35,13 +37,15 @@ type cnf_thm = thm * ((string * int) * thm) +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator + (* Used to label theorems chained into the goal. *) -val chained_prefix = "Sledgehammer.chained_" +val chained_prefix = sledgehammer_prefix ^ "chained_" val trace = Unsynchronized.ref false; fun trace_msg msg = if !trace then tracing (msg ()) else (); -val skolem_theory_name = "Sledgehammer.Sko" +val skolem_theory_name = sledgehammer_prefix ^ "Sko" val skolem_prefix = "sko_" val skolem_infix = "$" @@ -183,25 +187,14 @@ fun vars_of_thm th = map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); -(*Make a version of fun_cong with a given variable name*) -local - val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*) - val cx = hd (vars_of_thm fun_cong'); - val ty = typ_of (ctyp_of_term cx); - val thy = theory_of_thm fun_cong; - fun mkvar a = cterm_of thy (Var((a,0),ty)); -in -fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong' -end; +val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]} -(*Removes the lambdas from an equation of the form t = (%x. u). A non-negative n, - serves as an upper bound on how many to remove.*) -fun strip_lambdas 0 th = th - | strip_lambdas n th = - case prop_of th of - _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) => - strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x)) - | _ => th; +(* Removes the lambdas from an equation of the form t = (%x. u). *) +fun extensionalize th = + case prop_of th of + _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _])) + $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all) + | _ => th fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true | is_quasi_lambda_free (t1 $ t2) = @@ -339,9 +332,9 @@ fun to_nnf th ctxt0 = let val th1 = th |> transform_elim |> zero_var_indexes val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 - val th3 = th2 - |> Conv.fconv_rule Object_Logic.atomize - |> Meson.make_nnf ctxt |> strip_lambdas ~1 + val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize + |> extensionalize + |> Meson.make_nnf ctxt in (th3, ctxt) end; (*Generate Skolem functions for a theorem supplied in nnf*) diff -r d1fa353e1c4a -r a92a7f45ca28 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Jun 24 21:04:35 2010 +0200 +++ b/src/HOL/Tools/meson.ML Fri Jun 25 07:19:21 2010 +0200 @@ -521,10 +521,9 @@ nnf_ss also includes the one-point simprocs, which are needed to avoid the various one-point theorems from generating junk clauses.*) val nnf_simps = - [@{thm simp_implies_def}, @{thm Ex1_def}, @{thm Ball_def},@{thm Bex_def}, @{thm if_True}, - @{thm if_False}, @{thm if_cancel}, @{thm if_eq_cancel}, @{thm cases_simp}]; -val nnf_extra_simps = - @{thms split_ifs} @ @{thms ex_simps} @ @{thms all_simps} @ @{thms simp_thms}; + @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel + if_eq_cancel cases_simp} +val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms} val nnf_ss = HOL_basic_ss addsimps nnf_extra_simps