# HG changeset patch # User blanchet # Date 1406928590 -7200 # Node ID a63f14f1214c4b2685b4c2e74bc01295ded66f02 # Parent 5bc204ca27cecda408554582b06781eafe37494c fine-tuned Isar reconstruction, esp. boolean simplifications diff -r 5bc204ca27ce -r a63f14f1214c src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Aug 01 23:29:49 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Aug 01 23:29:50 2014 +0200 @@ -107,13 +107,20 @@ let val t' = simplify_bool t in if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t' end - | simplify_bool (@{const Not} $ t) = s_not (simplify_bool t) - | simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u) - | simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u) - | simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u) - | simplify_bool (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_bool t, simplify_bool u) - | simplify_bool (t as Const (@{const_name HOL.eq}, _) $ u $ v) = - if u aconv v then @{const True} else t + | simplify_bool (Const (@{const_name Not}, _) $ t) = s_not (simplify_bool t) + | simplify_bool (Const (@{const_name conj}, _) $ t $ u) = + s_conj (simplify_bool t, simplify_bool u) + | simplify_bool (Const (@{const_name disj}, _) $ t $ u) = + s_disj (simplify_bool t, simplify_bool u) + | simplify_bool (Const (@{const_name implies}, _) $ t $ u) = + s_imp (simplify_bool t, simplify_bool u) + | simplify_bool ((t as Const (@{const_name HOL.eq}, _)) $ u $ v) = + (case (u, v) of + (Const (@{const_name True}, _), _) => v + | (u, Const (@{const_name True}, _)) => u + | (Const (@{const_name False}, _), v) => s_not v + | (u, Const (@{const_name False}, _)) => s_not u + | _ => if u aconv v then @{const True} else t $ simplify_bool u $ simplify_bool v) | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t) | simplify_bool t = t @@ -246,47 +253,27 @@ (* Higher-order translation. Variables are typed (although we don't use that information). Lambdas - are typed. - - The code is similar to term_of_atp_fo. *) -fun term_of_atp_ho ctxt textual sym_tab = + are typed. The code is similar to "term_of_atp_fo". *) +fun term_of_atp_ho ctxt sym_tab = let val thy = Proof_Context.theory_of ctxt - val var_index = var_index_of_textual textual + val var_index = var_index_of_textual true fun do_term opt_T u = (case u of AAbs(((var, ty), term), []) => let val typ = typ_of_atp_type ctxt ty - val var_name = repair_var_name textual var + val var_name = repair_var_name true var val tm = do_term NONE term - in quantify_over_var textual lambda' var_name typ tm end + in quantify_over_var true lambda' var_name typ tm end | ATerm ((s, tys), us) => if s = "" then error "Isar proof reconstruction failed because the ATP proof \ \contains unparsable material." else if s = tptp_equal then - let - val ts = map (do_term NONE) us - fun equal_term ts = - list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts) - in - if textual then - (case ts of - [t1, t2] => - if loose_aconv (t1, t2) then - @{const True} - else if Term.aconv_untyped (t2, @{const True}) then - t1 - else if Term.aconv_untyped (t1, @{const True}) then - t2 - else - equal_term ts - | _ => equal_term ts) - else - equal_term ts - end + list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), + map (do_term NONE) us) else if not (null us) then let val args = List.map (do_term NONE) us @@ -297,10 +284,10 @@ else if s = tptp_and then HOLogic.conj else if s = tptp_implies then HOLogic.imp else if s = tptp_iff orelse s = tptp_equal then HOLogic.eq_const dummyT - else if s = tptp_not_iff orelse s = tptp_not_equal then @{term "% P Q. Q ~= P"} - else if s = tptp_if then @{term "% P Q. Q --> P"} - else if s = tptp_not_and then @{term "% P Q. ~ (P & Q)"} - else if s = tptp_not_or then @{term "% P Q. ~ (P | Q)"} + else if s = tptp_not_iff orelse s = tptp_not_equal then @{term "%P Q. Q ~= P"} + else if s = tptp_if then @{term "%P Q. Q --> P"} + else if s = tptp_not_and then @{term "%P Q. ~ (P & Q)"} + else if s = tptp_not_or then @{term "%P Q. ~ (P | Q)"} else if s = tptp_not then HOLogic.Not else if s = tptp_ho_forall then HOLogic.all_const dummyT else if s = tptp_ho_exists then HOLogic.exists_const dummyT @@ -317,7 +304,7 @@ val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us val T = (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then - if textual then try (Sign.const_instance thy) (s', Ts) else NONE + try (Sign.const_instance thy) (s', Ts) else NONE) |> (fn SOME T => T @@ -343,10 +330,8 @@ (case unprefix_and_unascii fixed_var_prefix s of SOME s => Free (s, T) | NONE => - if textual andalso not (is_tptp_variable s) then - Free (s |> textual ? (repair_var_name_raw #> fresh_up), T) - else - Var ((repair_var_name textual s, var_index), T)) + if not (is_tptp_variable s) then Free (s |> repair_var_name_raw |> fresh_up, T) + else Var ((repair_var_name true s, var_index), T)) in list_comb (t, ts) end)) in do_term end @@ -369,12 +354,8 @@ else if String.isPrefix native_type_prefix s then @{const True} (* ignore TPTP type information *) else if s = tptp_equal then - let val ts = map (do_term [] NONE) us in - if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then - @{const True} - else - list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts) - end + list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), + map (do_term [] NONE) us) else (case unprefix_and_unascii const_prefix s of SOME s' => @@ -452,12 +433,10 @@ in do_term [] end fun term_of_atp ctxt (ATP_Problem.THF _) type_enc = - if ATP_Problem_Generate.is_type_enc_higher_order type_enc - then term_of_atp_ho ctxt + if ATP_Problem_Generate.is_type_enc_higher_order type_enc then K (term_of_atp_ho ctxt) else error "Unsupported Isar reconstruction." | term_of_atp ctxt _ type_enc = - if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc) - then term_of_atp_fo ctxt + if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc) then term_of_atp_fo ctxt else error "Unsupported Isar reconstruction." fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) = @@ -633,6 +612,7 @@ |> prop_of_atp ctxt format type_enc true sym_tab |> unlift_term lifted |> uncombine_term thy + |> simplify_bool in SOME (name, role, t, rule, deps) end diff -r 5bc204ca27ce -r a63f14f1214c src/HOL/Tools/SMT2/smtlib2_isar.ML --- a/src/HOL/Tools/SMT2/smtlib2_isar.ML Fri Aug 01 23:29:49 2014 +0200 +++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML Fri Aug 01 23:29:50 2014 +0200 @@ -11,15 +11,16 @@ val postprocess_step_conclusion: theory -> thm list -> term list -> term -> term val normalizing_prems : Proof.context -> term -> (string * string list) list val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list -> - (''a * 'c) list -> 'c list -> 'c -> 'c -> (ATP_Problem.atp_formula_role * 'c) option + (''a * 'c) list -> 'c list -> 'c -> (ATP_Problem.atp_formula_role * 'c) option val unskolemize_names: term -> term end; structure SMTLIB2_Isar: SMTLIB2_ISAR = struct +open ATP_Util open ATP_Problem -open ATP_Util +open ATP_Proof_Reconstruct fun unlift_term ll_defs = let @@ -42,6 +43,7 @@ Raw_Simplifier.rewrite_term thy rewrite_rules [] #> Object_Logic.atomize_term thy #> not (null ll_defs) ? unlift_term ll_defs + #> simplify_bool #> unskolemize_names #> HOLogic.mk_Trueprop @@ -54,8 +56,8 @@ else NONE) -fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts concl_t - t = +fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts + concl_t = (case ss of [s] => SOME (Axiom, the (AList.lookup (op =) fact_helper_ts s)) | _ => diff -r 5bc204ca27ce -r a63f14f1214c src/HOL/Tools/SMT2/verit_isar.ML --- a/src/HOL/Tools/SMT2/verit_isar.ML Fri Aug 01 23:29:49 2014 +0200 +++ b/src/HOL/Tools/SMT2/verit_isar.ML Fri Aug 01 23:29:50 2014 +0200 @@ -35,7 +35,7 @@ if rule = veriT_input_rule then let val ss = the_list (AList.lookup (op =) fact_helper_ids (the (Int.fromString id))) in (case distinguish_conjecture_and_hypothesis ss (the (Int.fromString id)) - conjecture_id prem_ids fact_helper_ts hyp_ts concl_t concl of + conjecture_id prem_ids fact_helper_ts hyp_ts concl_t of NONE => [] | SOME (role0, concl00) => let diff -r 5bc204ca27ce -r a63f14f1214c src/HOL/Tools/SMT2/z3_new_isar.ML --- a/src/HOL/Tools/SMT2/z3_new_isar.ML Fri Aug 01 23:29:49 2014 +0200 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Fri Aug 01 23:29:50 2014 +0200 @@ -94,7 +94,7 @@ Z3_New_Proof.Asserted => let val ss = the_list (AList.lookup (op =) fact_helper_ids id) in (case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts - hyp_ts concl_t concl of + hyp_ts concl_t of NONE => [] | SOME (role0, concl00) => let diff -r 5bc204ca27ce -r a63f14f1214c src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 23:29:49 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 23:29:50 2014 +0200 @@ -89,7 +89,8 @@ line :: lines else if role = Axiom then lines (* axioms (facts) need no proof lines *) - else map (replace_dependencies_in_line (name, [])) lines + else + map (replace_dependencies_in_line (name, [])) lines | add_line_pass1 line lines = line :: lines fun add_lines_pass2 res _ [] = rev res @@ -210,7 +211,7 @@ val rule_of_clause_id = fst o the o Symtab.lookup steps o fst - val finish_off = simplify_bool #> close_form #> rename_bound_vars + val finish_off = close_form #> rename_bound_vars fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off | prop_of_clause names = diff -r 5bc204ca27ce -r a63f14f1214c src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Aug 01 23:29:49 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Aug 01 23:29:50 2014 +0200 @@ -98,7 +98,7 @@ subproofs1 @ subproofs2, (lfs, gfs), meths, comment1 ^ comment2), hopeless) end -val merge_slack_time = seconds 0.005 +val merge_slack_time = seconds 0.01 val merge_slack_factor = 1.5 fun adjust_merge_timeout max time = @@ -117,7 +117,7 @@ val (compress_further, decrement_step_count) = let val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0 - val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress) + val target_number_of_steps = Real.ceil (Real.fromInt number_of_steps / compress) val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps) in (fn () => !delta > 0, fn () => delta := !delta - 1) @@ -273,8 +273,9 @@ if compress_further () then Proof (xs, assms, compress_steps steps) else proof and compress_steps steps = (* bottom-up: compress innermost proofs first *) - steps |> map (fn step => step |> compress_further () ? compress_sub_levels) - |> compress_further () ? compress_top_level + steps + |> map (fn step => step |> compress_further () ? compress_sub_levels) + |> compress_further () ? compress_top_level and compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) = (* compress subproofs *) Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment)