| author | blanchet |
| Mon, 30 Jan 2012 17:15:59 +0100 | |
| changeset 46365 | 547d1a1dcaf6 |
| parent 46364 | abab10d1f4a3 |
| child 46366 | 2ded91a6cbd5 |
--- a/src/HOL/IMP/Live_True.thy Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/IMP/Live_True.thy Mon Jan 30 17:15:59 2012 +0100 @@ -146,7 +146,7 @@ lemma while_option_stop2: "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t" apply(simp add: while_option_def split: if_splits) -by (metis (lam_lifting) LeastI_ex) +by (metis (lifting) LeastI_ex) (* move to While_Combinator *) lemma while_option_finite_subset_Some: fixes C :: "'a set" assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
--- a/src/HOL/Library/While_Combinator.thy Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/Library/While_Combinator.thy Mon Jan 30 17:15:59 2012 +0100 @@ -55,7 +55,7 @@ lemma while_option_stop2: "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t" apply(simp add: while_option_def split: if_splits) -by (metis (lam_lifting) LeastI_ex) +by (metis (lifting) LeastI_ex) lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t" by(metis while_option_stop2)
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jan 30 17:15:59 2012 +0100 @@ -19,7 +19,7 @@ val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) fun metis ctxt = - Metis_Tactic.metis_tac [] ATP_Problem_Generate.lam_liftingN ctxt + Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt (thms @ facts) in (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jan 30 17:15:59 2012 +0100 @@ -581,7 +581,7 @@ ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??" ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??" ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags" - ORELSE' Metis_Tactic.metis_tac [] ATP_Problem_Generate.combinatorsN + ORELSE' Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt thms else if !reconstructor = "smt" then SMT_Solver.smt_tac ctxt thms
--- a/src/HOL/TPTP/CASC_Setup.thy Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/TPTP/CASC_Setup.thy Mon Jan 30 17:15:59 2012 +0100 @@ -129,7 +129,7 @@ Sledgehammer_Filter.no_relevance_override)) ORELSE SOLVE_TIMEOUT (max_secs div 10) "metis" - (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Problem_Generate.lam_liftingN ctxt [])) + (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt [])) ORELSE SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) ORELSE
--- a/src/HOL/TPTP/atp_theory_export.ML Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jan 30 17:15:59 2012 +0100 @@ -180,8 +180,8 @@ |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), th |> prop_of |> mono ? monomorphize_term ctxt)) - |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combinatorsN - false true [] @{prop False} + |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false + true [] @{prop False} |> #1 val atp_problem = atp_problem
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jan 30 17:15:59 2012 +0100 @@ -34,9 +34,11 @@ val type_tag_arguments : bool Config.T val no_lamsN : string val hide_lamsN : string + val liftingN : string + val combsN : string + val combs_and_liftingN : string + val combs_or_liftingN : string val lam_liftingN : string - val combinatorsN : string - val hybrid_lamsN : string val keep_lamsN : string val schematic_var_prefix : string val fixed_var_prefix : string @@ -123,10 +125,12 @@ val no_lamsN = "no_lams" (* used internally; undocumented *) val hide_lamsN = "hide_lams" -val lam_liftingN = "lam_lifting" -val combinatorsN = "combinators" -val hybrid_lamsN = "hybrid_lams" +val liftingN = "lifting" +val combsN = "combs" +val combs_and_liftingN = "combs_and_lifting" +val combs_or_liftingN = "combs_or_lifting" val keep_lamsN = "keep_lams" +val lam_liftingN = "lam_lifting" (* legacy *) (* It's still unclear whether all TFF1 implementations will support type signatures such as "!>[A : $tType] : $o", with ghost type variables. *) @@ -1693,11 +1697,15 @@ rpair [] else if lam_trans = hide_lamsN then lift_lams ctxt type_enc ##> K [] - else if lam_trans = lam_liftingN then + else if lam_trans = liftingN orelse lam_trans = lam_liftingN then lift_lams ctxt type_enc - else if lam_trans = combinatorsN then + else if lam_trans = combsN then map (introduce_combinators ctxt) #> rpair [] - else if lam_trans = hybrid_lamsN then + else if lam_trans = combs_and_liftingN then + lift_lams_part_1 ctxt type_enc + ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)]) + #> lift_lams_part_2 + else if lam_trans = combs_or_liftingN then (* ### FIXME: implement *) lift_lams_part_1 ctxt type_enc ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)]) #> lift_lams_part_2
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jan 30 17:15:59 2012 +0100 @@ -121,7 +121,7 @@ fun unalias_type_enc s = AList.lookup (op =) type_enc_aliases s |> the_default [s] -val metis_default_lam_trans = combinatorsN +val metis_default_lam_trans = combsN fun metis_call type_enc lam_trans = let @@ -175,9 +175,12 @@ String.isSubstring ascii_of_lam_fact_prefix s fun lam_trans_from_atp_proof atp_proof default = - if is_axiom_used_in_proof is_combinator_def atp_proof then combinatorsN - else if is_axiom_used_in_proof is_lam_lifted atp_proof then lam_liftingN - else default + case (is_axiom_used_in_proof is_combinator_def atp_proof, + is_axiom_used_in_proof is_lam_lifted atp_proof) of + (false, false) => default + | (false, true) => liftingN + | (true, false) => combsN + | (true, true) => combs_and_liftingN val is_typed_helper_name = String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jan 30 17:15:59 2012 +0100 @@ -245,14 +245,14 @@ let val method = effective_e_weight_method ctxt in (* FUDGE *) if method = e_smartN then - [(0.333, (true, (500, FOF, "mono_tags??", combinatorsN, + [(0.333, (true, (500, FOF, "mono_tags??", combsN, e_fun_weightN))), - (0.334, (true, (50, FOF, "mono_guards??", combinatorsN, + (0.334, (true, (50, FOF, "mono_guards??", combsN, e_fun_weightN))), - (0.333, (true, (1000, FOF, "mono_tags??", combinatorsN, + (0.333, (true, (1000, FOF, "mono_tags??", combsN, e_sym_offset_weightN)))] else - [(1.0, (true, (500, FOF, "mono_tags??", combinatorsN, method)))] + [(1.0, (true, (500, FOF, "mono_tags??", combsN, method)))] end} val e = (eN, e_config) @@ -277,9 +277,9 @@ prem_kind = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", lam_liftingN, + [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", liftingN, sosN))), - (0.333, (true, (50, leo2_thf0, "mono_simple_higher", lam_liftingN, + (0.333, (true, (50, leo2_thf0, "mono_simple_higher", liftingN, no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -335,11 +335,11 @@ prem_kind = Conjecture, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", lam_liftingN, + [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", liftingN, sosN))), - (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", lam_liftingN, + (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", liftingN, sosN))), - (0.334, (false, (50, DFG DFG_Unsorted, "mono_tags??", lam_liftingN, + (0.334, (false, (50, DFG DFG_Unsorted, "mono_tags??", liftingN, no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -357,11 +357,11 @@ prem_kind = #prem_kind spass_config, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", lam_liftingN, + [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", liftingN, sosN))) (*, - (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", lam_liftingN, + (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", liftingN, sosN))), - (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", lam_liftingN, + (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", liftingN, no_sosN)))*)] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -404,15 +404,15 @@ best_slices = fn ctxt => (* FUDGE *) (if is_old_vampire_version () then - [(0.333, (false, (150, FOF, "poly_guards??", hybrid_lamsN, sosN))), - (0.333, (false, (500, FOF, "mono_tags??", hybrid_lamsN, sosN))), - (0.334, (true, (50, FOF, "mono_guards??", hybrid_lamsN, no_sosN)))] + [(0.333, (false, (150, FOF, "poly_guards??", combs_or_liftingN, sosN))), + (0.333, (false, (500, FOF, "mono_tags??", combs_or_liftingN, sosN))), + (0.334, (true, (50, FOF, "mono_guards??", combs_or_liftingN, no_sosN)))] else - [(0.333, (false, (150, vampire_tff0, "poly_guards??", hybrid_lamsN, + [(0.333, (false, (150, vampire_tff0, "poly_guards??", combs_or_liftingN, sosN))), - (0.333, (false, (500, vampire_tff0, "mono_simple", hybrid_lamsN, + (0.333, (false, (500, vampire_tff0, "mono_simple", combs_or_liftingN, sosN))), - (0.334, (true, (50, vampire_tff0, "mono_simple", hybrid_lamsN, + (0.334, (true, (50, vampire_tff0, "mono_simple", combs_or_liftingN, no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -435,10 +435,10 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(0.5, (false, (250, z3_tff0, "mono_simple", combinatorsN, ""))), - (0.25, (false, (125, z3_tff0, "mono_simple", combinatorsN, ""))), - (0.125, (false, (62, z3_tff0, "mono_simple", combinatorsN, ""))), - (0.125, (false, (31, z3_tff0, "mono_simple", combinatorsN, "")))]} + K [(0.5, (false, (250, z3_tff0, "mono_simple", combsN, ""))), + (0.25, (false, (125, z3_tff0, "mono_simple", combsN, ""))), + (0.125, (false, (62, z3_tff0, "mono_simple", combsN, ""))), + (0.125, (false, (31, z3_tff0, "mono_simple", combsN, "")))]} val z3_tptp = (z3_tptpN, z3_tptp_config) @@ -456,7 +456,7 @@ best_slices = K [(1.0, (false, (200, format, type_enc, if is_format_higher_order format then keep_lamsN - else combinatorsN, "")))]} + else combsN, "")))]} val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit) val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple" @@ -537,43 +537,43 @@ val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] - (K (750, FOF, "mono_tags??", combinatorsN) (* FUDGE *)) + (K (750, FOF, "mono_tags??", combsN) (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"] - (K (100, leo2_thf0, "mono_simple_higher", lam_liftingN) (* FUDGE *)) + (K (100, leo2_thf0, "mono_simple_higher", liftingN) (* FUDGE *)) val remote_satallax = remotify_atp satallax "Satallax" ["2.1", "2.0", "2"] (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["1.8"] - (K (250, FOF, "mono_guards??", hybrid_lamsN) (* FUDGE *)) + (K (250, FOF, "mono_guards??", combs_or_liftingN) (* FUDGE *)) val remote_z3_tptp = remotify_atp z3_tptp "Z3" ["3.0"] - (K (250, z3_tff0, "mono_simple", combinatorsN) (* FUDGE *)) + (K (250, z3_tff0, "mono_simple", combsN) (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom - Conjecture (K (500, FOF, "mono_guards??", combinatorsN) (* FUDGE *)) + Conjecture (K (500, FOF, "mono_guards??", combsN) (* FUDGE *)) val remote_iprover = remote_atp iproverN "iProver" [] [] [] Axiom Conjecture - (K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *)) + (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *)) val remote_iprover_eq = remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture - (K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *)) + (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis - (K (100, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *)) + (K (100, explicit_tff0, "mono_simple", liftingN) (* FUDGE *)) val remote_e_tofof = remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom Hypothesis - (K (150, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *)) + (K (150, explicit_tff0, "mono_simple", liftingN) (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] [("#START OF PROOF", "Proved Goals:")] [(OutOfResources, "Too many function symbols"), (Crashed, "Unrecoverable Segmentation Fault")] Hypothesis Hypothesis - (K (50, CNF_UEQ, "mono_tags??", combinatorsN) (* FUDGE *)) + (K (50, CNF_UEQ, "mono_tags??", combsN) (* FUDGE *)) (* Setup *)
--- a/src/HOL/Tools/Metis/metis_generate.ML Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/Tools/Metis/metis_generate.ML Mon Jan 30 17:15:59 2012 +0100 @@ -230,7 +230,8 @@ fold_rev (fn (name, th) => fn (old_skolems, props) => th |> prop_of |> Logic.strip_imp_concl |> conceal_old_skolem_terms (length clauses) old_skolems - ||> lam_trans = lam_liftingN ? eliminate_lam_wrappers + ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN) + ? eliminate_lam_wrappers ||> (fn prop => (name, prop) :: props)) clauses ([], []) (* @@ -238,7 +239,7 @@ tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt o snd) props)) *) - val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans + val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans val (atp_problem, _, _, lifted, sym_tab) = prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans false false [] @{prop False} props
--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Jan 30 17:15:59 2012 +0100 @@ -125,13 +125,15 @@ let val thy = Proof_Context.theory_of ctxt val new_skolemizer = Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) - val do_lams = lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt + val do_lams = + (lam_trans = liftingN orelse lam_trans = lam_liftingN) + ? introduce_lam_wrappers ctxt val th_cls_pairs = map2 (fn j => fn th => (Thm.get_name_hint th, th |> Drule.eta_contraction_rule |> Meson_Clausify.cnf_axiom ctxt new_skolemizer - (lam_trans = combinatorsN) j + (lam_trans = combsN) j ||> map do_lams)) (0 upto length ths0 - 1) ths0 val ths = maps (snd o snd) th_cls_pairs @@ -247,7 +249,7 @@ else (); Meson.MESON (preskolem_tac ctxt) - (maps (neg_clausify ctxt (lam_trans = combinatorsN))) tac ctxt i st0 + (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0 end fun metis_tac [] = generic_metis_tac partial_type_encs @@ -277,7 +279,7 @@ (schem_facts @ ths)) end -val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN] +val metis_lam_transs = [hide_lamsN, liftingN, combsN] fun set_opt _ x NONE = SOME x | set_opt get x (SOME x0) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jan 30 17:15:59 2012 +0100 @@ -134,7 +134,7 @@ val das_tool = "Sledgehammer" val reconstructor_names = [metisN, smtN] -val plain_metis = Metis (hd partial_type_encs, combinatorsN) +val plain_metis = Metis (hd partial_type_encs, combsN) val is_reconstructor = member (op =) reconstructor_names val is_atp = member (op =) o supported_atps @@ -991,8 +991,7 @@ state subgoal SMT (bunch_of_reconstructors false (fn plain => - if plain then metis_default_lam_trans - else lam_liftingN)), + if plain then metis_default_lam_trans else liftingN)), fn preplay => let val one_line_params =
--- a/src/HOL/ex/sledgehammer_tactics.ML Mon Jan 30 17:15:59 2012 +0100 +++ b/src/HOL/ex/sledgehammer_tactics.ML Mon Jan 30 17:15:59 2012 +0100 @@ -71,7 +71,7 @@ fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th = case run_atp override_params relevance_override i i ctxt th of SOME facts => - Metis_Tactic.metis_tac [] ATP_Problem_Generate.combinatorsN ctxt + Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt (maps (thms_of_name ctxt) facts) i th | NONE => Seq.empty