# HG changeset patch # User fleury # Date 1406721793 -7200 # Node ID 4856a7b8b9c3e2f0844939a19793acef4f46b74b # Parent 9e4d2f7ad0a07c9e9c444f8f7f1c31b5ad76a146 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma. diff -r 9e4d2f7ad0a0 -r 4856a7b8b9c3 src/HOL/ATP.thy --- a/src/HOL/ATP.thy Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/ATP.thy Wed Jul 30 14:03:13 2014 +0200 @@ -6,7 +6,7 @@ header {* Automatic Theorem Provers (ATPs) *} theory ATP -imports Meson Hilbert_Choice +imports Meson begin subsection {* ATP problems and proofs *} diff -r 9e4d2f7ad0a0 -r 4856a7b8b9c3 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 30 14:03:13 2014 +0200 @@ -90,18 +90,17 @@ val skip_term: string list -> string * string list val parse_thf0_formula :string list -> - ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, - 'c) ATP_Problem.atp_formula * - string list - val dummy_atype : string ATP_Problem.atp_type - val role_of_tptp_string: string -> ATP_Problem.atp_formula_role + ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula * + string list + val dummy_atype : string ATP_Problem.atp_type + val role_of_tptp_string: string -> ATP_Problem.atp_formula_role val parse_line: string -> ('a * string ATP_Problem.atp_problem_line list) list -> - string list -> ((string * string list) * ATP_Problem.atp_formula_role * - (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, - 'c) ATP_Problem.atp_formula - * string * (string * 'd list) list) list * string list + string list -> ((string * string list) * ATP_Problem.atp_formula_role * + (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, + 'c) ATP_Problem.atp_formula + * string * (string * 'd list) list) list * string list val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role * - ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list + ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list val vampire_step_name_ord : (string * 'a) * (string * 'a) -> order val core_of_agsyhol_proof : string -> string list option end; @@ -478,8 +477,8 @@ [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal, tptp_app] -fun parse_one_in_list list = - foldl1 (op ||) (map Scan.this_string list) +fun parse_one_in_list xs = + foldl1 (op ||) (map Scan.this_string xs) fun parse_binary_op x = (parse_one_in_list tptp_binary_ops diff -r 9e4d2f7ad0a0 -r 4856a7b8b9c3 src/HOL/Tools/ATP/atp_satallax.ML --- a/src/HOL/Tools/ATP/atp_satallax.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_satallax.ML Wed Jul 30 14:03:13 2014 +0200 @@ -30,7 +30,7 @@ ((Symbol.scan_ascii_id || ($$ "$" |-- Symbol.scan_ascii_id)) -- Scan.option ( $$ "(" |-- Scan.option (Symbol.scan_ascii_id --| $$ ",") -- ((Scan.option (($$ "[" |-- (Scan.option ((scan_general_id - -- Scan.repeat ($$ "," |-- scan_general_id)) >> uncurry cons) --| $$ "]")) + -- Scan.repeat ($$ "," |-- scan_general_id)) >> (op ::)) --| $$ "]")) || (skip_term >> K "") >> (fn x => SOME [x])) >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x @@ -39,12 +39,12 @@ fun parse_prems x = (($$ "[" |-- parse_prem -- Scan.repeat ($$ "," |-- parse_prem) --| $$ "]") - >> uncurry cons) x + >> (op ::)) x fun parse_tstp_satallax_extra_arguments x = ($$ "," |-- scan_general_id -- (($$ "(" |-- Symbol.scan_ascii_id --| $$ "," ) -- ($$ "[" |-- Scan.option ((parse_satallax_tstp_information - -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> uncurry cons) + -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> (op ::)) --| $$ "]") -- (Scan.optional ($$ "," |-- parse_prems) [] -- Scan.optional ($$ "," |-- parse_prems) [] >> (fn (x, []) => x | (_, x) => x)) @@ -58,7 +58,6 @@ || (Scan.this_string "tab_inh" |-- skip_term --| $$ ".") >> K dummy_satallax_step) x - datatype satallax_step = Satallax_Step of { id: string, role: string, @@ -106,19 +105,23 @@ end fun create_grouped_goal_assumption rule new_goals generated_assumptions = - if length new_goals = length generated_assumptions then - new_goals ~~ (map single generated_assumptions) - else if 2 * length new_goals = length generated_assumptions then - let - fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) = - (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions - | group_by_pair [] [] = [] - in - group_by_pair new_goals generated_assumptions - end - else - raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.") - + let + val number_of_new_goals = length new_goals + val number_of_new_assms = length generated_assumptions + in + if number_of_new_goals = number_of_new_assms then + new_goals ~~ (map single generated_assumptions) + else if 2 * number_of_new_goals = number_of_new_assms then + let + fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) = + (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions + | group_by_pair [] [] = [] + in + group_by_pair new_goals generated_assumptions + end + else + raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.") + end fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) = let val (used_assumptions, new_goals, generated_assumptions) = seperate_dependices used_rules @@ -173,9 +176,9 @@ | SOME (_, th) => let val simplified_ths_with_inlined_assumption = - (case List.partition (curry tptp_term_equal th o remove_not_not) ths of - ([], ths) => ATerm ((tptp_not, [dummy_atype]), [th]) :: ths - | (_, _) => []) + (case List.partition (curry tptp_term_equal th o remove_not_not) ths of + ([], ths) => ATerm ((tptp_not, [dummy_atype]), [th]) :: ths + | (_, _) => []) in find_assumptions_to_inline simplified_ths_with_inlined_assumption assms to_inline no_inline end)) @@ -190,7 +193,6 @@ | ATerm (("~", _ ), [ATerm (("$true", _), _)]) => a | _ => ATerm ((tptp_or, [dummy_atype]), [a, b]))) l) - fun get_conclusion (Satallax_Step {theorem = AAtom theorem, ...}) = theorem fun add_assumption new_used_assumptions ((Satallax_Step {id, role, theorem, assumptions, @@ -208,7 +210,7 @@ fun inline_in_step (Linear_Part {node as Satallax_Step {generated_goal_assumptions, used_assumptions, rule, ...}, succs}) = if generated_goal_assumptions = [] then - Linear_Part {node = node, succs = []} + Linear_Part {node = node, succs = []} else let (*one singel goal is created, two hypothesis can be created, for the "and" rule: @@ -230,8 +232,8 @@ fun inline_contradictory_assumptions (Linear_Part {node as Satallax_Step{id, theorem, ...}, succs}) (to_inline, no_inline) = let - val (succs, inliner) = fold_map inline_contradictory_assumptions - succs (to_inline, (id, theorem) :: no_inline) + val (succs, inliner) = fold_map inline_contradictory_assumptions succs + (to_inline, (id, theorem) :: no_inline) in (Linear_Part {node = node, succs = succs}, inliner) end @@ -239,8 +241,8 @@ theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions, used_assumptions, detailed_eigen}, deps}) (to_inline, no_inline) = let - val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions - deps (to_inline, no_inline) + val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions deps + (to_inline, no_inline) val to_inline'' = map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s))) (List.filter (fn s => nth_string s 0 = "h") @@ -292,16 +294,16 @@ end val satallax_known_theorems = ["eq_ind", "eq_trans2", "eq_trans3", "eq_neg_neg_id", "eq_true", - "eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq", - "eq_forall_nexists", "eq_exists_nforall", "eq_leib1", "eq_leib2", "eq_leib3", "eq_leib4", - "eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"] + "eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq", + "eq_forall_nexists", "eq_exists_nforall", "eq_leib1", "eq_leib2", "eq_leib3", "eq_leib4", + "eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"] val is_special_satallax_rule = member (op =) satallax_known_theorems fun terms_to_upper_case var (AAbs (((var', ty), b), ts)) = - let - val bdy = terms_to_upper_case var b - val ts' = map (terms_to_upper_case var) ts - in + let + val bdy = terms_to_upper_case var b + val ts' = map (terms_to_upper_case var) ts + in AAbs (((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), ty), bdy), ts') end @@ -364,7 +366,7 @@ fun remove_unused_dependency steps = let fun find_all_ids [] = [] - | find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps + | find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps fun keep_only_used used_ids steps = let fun remove_unused (((id, ids), role, theorem, rule, deps) :: steps) = @@ -377,26 +379,25 @@ keep_only_used (find_all_ids steps) steps end - fun parse_proof local_name problem = - strip_spaces_except_between_idents - #> raw_explode - #> - (if local_name <> satallaxN then - (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) - (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat))) - #> fst) - else - (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) - (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line)))) - #> fst - #> rev - #> map to_satallax_step - #> seperate_assumptions_and_steps - #> create_satallax_proof_graph - #> add_quantifier_in_tree_part [] [] - #> transform_to_standard_atp_step [] - #> remove_unused_dependency)) + strip_spaces_except_between_idents + #> raw_explode + #> + (if local_name <> satallaxN then + (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) + (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat))) + #> fst) + else + (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) + (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line)))) + #> fst + #> rev + #> map to_satallax_step + #> seperate_assumptions_and_steps + #> create_satallax_proof_graph + #> add_quantifier_in_tree_part [] [] + #> transform_to_standard_atp_step [] + #> remove_unused_dependency)) fun atp_proof_of_tstplike_proof _ _ "" = [] | atp_proof_of_tstplike_proof local_prover problem tstp = diff -r 9e4d2f7ad0a0 -r 4856a7b8b9c3 src/HOL/Tools/SMT2/smt2_systems.ML --- a/src/HOL/Tools/SMT2/smt2_systems.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML Wed Jul 30 14:03:13 2014 +0200 @@ -105,7 +105,7 @@ smt_options = [], default_max_relevant = 120 (* FUDGE *), outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" - "warning : proof_done: status is still open"), + "warning : proof_done: status is still open"), parse_proof = SOME VeriT_Proof_Parse.parse_proof, replay = NONE } diff -r 9e4d2f7ad0a0 -r 4856a7b8b9c3 src/HOL/Tools/SMT2/smtlib2_isar.ML --- a/src/HOL/Tools/SMT2/smtlib2_isar.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML Wed Jul 30 14:03:13 2014 +0200 @@ -59,7 +59,7 @@ and un_term t = map_aterms un_free t in un_term end -(* It is not entirely clear if this is necessary for abstractions variables. *) +(* It is not entirely clear why this should be necessary, especially for abstractions variables. *) val unskolemize_names = Term.map_abs_vars (perhaps (try Name.dest_skolem)) #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T)))) diff -r 9e4d2f7ad0a0 -r 4856a7b8b9c3 src/HOL/Tools/SMT2/verit_isar.ML --- a/src/HOL/Tools/SMT2/verit_isar.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/SMT2/verit_isar.ML Wed Jul 30 14:03:13 2014 +0200 @@ -27,7 +27,6 @@ conjecture_id fact_helper_ids proof = let val thy = Proof_Context.theory_of ctxt - fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) = let val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs @@ -45,6 +44,8 @@ [(name0, role0, concl0, rule, []), ((id, []), Plain, concl', veriT_rewrite_rule, name0 :: normalizing_prems ctxt concl0)] end + else if rule = veriT_tmp_ite_elim_rule then + [standard_step Lemma] else [standard_step Plain] end diff -r 9e4d2f7ad0a0 -r 4856a7b8b9c3 src/HOL/Tools/SMT2/verit_proof.ML --- a/src/HOL/Tools/SMT2/verit_proof.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/SMT2/verit_proof.ML Wed Jul 30 14:03:13 2014 +0200 @@ -22,6 +22,8 @@ val veriT_step_prefix : string val veriT_input_rule: string val veriT_rewrite_rule : string + val veriT_tmp_skolemize_rule : string + val veriT_tmp_ite_elim_rule : string end; structure VeriT_Proof: VERIT_PROOF = @@ -85,6 +87,14 @@ replace_bound_var_by_free_var v free_vars | replace_bound_var_by_free_var u _ = u +fun replace_bound_all_by_ex ((q as Const (_, typ)) $ Abs (var, ty, u)) free_var = + (case List.find (fn v => String.isPrefix v var) free_var of + NONE => q $ Abs (var, ty, replace_bound_all_by_ex u free_var) + | SOME _ => Const (@{const_name "HOL.Ex"}, typ) $ Abs (var, ty, replace_bound_all_by_ex u free_var)) + | replace_bound_all_by_ex (u $ v) free_vars = replace_bound_all_by_ex u free_vars $ + replace_bound_all_by_ex v free_vars + | replace_bound_all_by_ex u _ = u + fun find_type_in_formula (Abs(v, ty, u)) var_name = if String.isPrefix var_name v then SOME ty else find_type_in_formula u var_name | find_type_in_formula (u $ v) var_name = @@ -195,7 +205,7 @@ #> fix_subproof_steps ##> to_node #> (fn (subproof, (step, cx)) => (subproof @ [step], cx)) - #> (fn (steps, cx) => fold_map update_step_and_cx steps cx) + #> uncurry (fold_map update_step_and_cx) end @@ -236,8 +246,8 @@ (*Yes every case is possible: the introduced var is not on a special size of the equality sign.*) fun find_ite_var_in_term (Const ("HOL.If", _) $ _ $ - (Const ("HOL.eq", _) $ Free (var1, _) $ Free (var2, _) ) $ - (Const ("HOL.eq", _) $ Free (var3, _) $ Free (var4, _) )) = + (Const (@{const_name "HOL.eq"}, _) $ Free (var1, _) $ Free (var2, _) ) $ + (Const (@{const_name "HOL.eq"}, _) $ Free (var3, _) $ Free (var4, _) )) = let fun get_number_of_ite_transformed_var var = perhaps (try (unprefix "ite")) var @@ -278,7 +288,7 @@ fun correct_veriT_step steps (st as VeriT_Node {id, rule, prems, concl, bounds}) = - if rule = "tmp_ite_elim" then + if rule = veriT_tmp_ite_elim_rule then if bounds = [] then (*if the introduced var has already been defined, adding the definition as a dependency*) @@ -325,7 +335,7 @@ val smtlib2_lines_without_at = remove_all_at (map SMTLIB2.parse (seperate_into_steps lines)) val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l) - smtlib2_lines_without_at (empty_context ctxt typs funs)) + smtlib2_lines_without_at (empty_context ctxt typs funs)) val t = correct_veriT_steps u fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) = mk_step id rule prems concl bounds diff -r 9e4d2f7ad0a0 -r 4856a7b8b9c3 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:13 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:13 2014 +0200 @@ -66,7 +66,7 @@ zipperposition_cnf_rule] val is_skolemize_rule = member (op =) skolemize_rules -val is_arith_rule = (String.isPrefix z3_th_lemma_rule) orf (member (op =) veriT_arith_rules) +val is_arith_rule = String.isPrefix z3_th_lemma_rule orf member (op =) veriT_arith_rules val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule fun raw_label_of_num num = (num, 0) @@ -84,8 +84,7 @@ line :: lines else if t aconv @{prop True} then map (replace_dependencies_in_line (name, [])) lines - else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule - orelse is_skolemize_rule rule then + else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines else if role = Axiom then lines (* axioms (facts) need no proof lines *)