# HG changeset patch # User desharna # Date 1627374982 -7200 # Node ID a5bab59d580b7ccd4dee18453c6fa92b99c69c5e # Parent 2af4e088c01c4c90fcb6297a859d248c77e3bf29 added support for TFX $let to Sledgehammer's TPTP output diff -r 2af4e088c01c -r a5bab59d580b src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jul 27 20:28:23 2021 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jul 27 10:36:22 2021 +0200 @@ -89,6 +89,7 @@ val tptp_iff : string val tptp_not_iff : string val tptp_ite : string + val tptp_let : string val tptp_app : string val tptp_not_infix : string val tptp_equal : string @@ -249,6 +250,7 @@ val tptp_iff = "<=>" val tptp_not_iff = "<~>" val tptp_ite = "$ite" +val tptp_let = "$let" val tptp_app = "@" val tptp_hilbert_choice = "@+" val tptp_hilbert_the = "@-" @@ -488,6 +490,17 @@ (AQuant (if s = tptp_ho_forall then AForall else AExists, [(s', SOME ty)], AAtom tm)) | _ => app ()) + else if s = tptp_let then + (case ts of + [t1, AAbs (((s', ty), tm), [])] => + let + val declaration = s' ^ " : " ^ of_type ty + val definition = s' ^ " := " ^ of_term t1 + val usage = of_term tm + in + s ^ "(" ^ declaration ^ ", " ^ definition ^ ", " ^ usage ^ ")" + end + | _ => app ()) else if s = tptp_choice then (case ts of [AAbs (((s', ty), tm), args)] => diff -r 2af4e088c01c -r a5bab59d580b src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jul 27 20:28:23 2021 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jul 27 10:36:22 2021 +0200 @@ -342,6 +342,7 @@ (\<^const_name>\Ex\, "Ex"), (\<^const_name>\If\, "If"), (\<^const_name>\Set.member\, "member"), + (\<^const_name>\HOL.Let\, "Let"), (\<^const_name>\Meson.COMBI\, combinator_prefix ^ "I"), (\<^const_name>\Meson.COMBK\, combinator_prefix ^ "K"), (\<^const_name>\Meson.COMBB\, combinator_prefix ^ "B"), @@ -774,12 +775,18 @@ fun trans_fool Ts t = (case t of - (t0 as Const (\<^const_name>\All\, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, trans_fool (T :: Ts) t') - | (t0 as Const (\<^const_name>\All\, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1) - | (t0 as Const (\<^const_name>\Ex\, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, trans_fool (T :: Ts) t') - | (t0 as Const (\<^const_name>\Ex\, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1) + (t1 as Const (\<^const_name>\Let\, _)) $ t2 $ t3 => + (case t3 of + Abs (s3, T, t') => t1 $ trans_fool Ts t2 $ Abs (s3, T, trans_fool (T :: Ts) t') + | _ => trans_fool Ts (t1 $ trans_fool Ts t2 $ eta_expand Ts t3 1)) + | (t0 as Const (\<^const_name>\All\, _)) $ t1 => + (case t1 of + Abs (s, T, t') => t0 $ Abs (s, T, trans_fool (T :: Ts) t') + | _ => trans_fool Ts (t0 $ eta_expand Ts t1 1)) + | (t0 as Const (\<^const_name>\Ex\, _)) $ t1 => + (case t1 of + Abs (s, T, t') => t0 $ Abs (s, T, trans_fool (T :: Ts) t') + | _ => trans_fool Ts (t0 $ eta_expand Ts t1 1)) | t1 $ t2 => trans_fool Ts t1 $ trans_fool Ts t2 | Abs _ => t |> Envir.eta_contract |> do_lambdas ctxt Ts | _ => t) @@ -1179,7 +1186,12 @@ val tm2' = intro false [] tm2 val tm2'' = (case tm1' of - IConst ((s, _), _, _) => + IApp (IConst ((s, _), _, _), _) => + if s = tptp_let then + eta_expand_quantifier_body tm2' + else + tm2' + | IConst ((s, _), _, _) => if s = tptp_ho_forall orelse s = tptp_ho_exists then eta_expand_quantifier_body tm2' else @@ -1189,61 +1201,64 @@ IApp (tm1', tm2'') end | intro top_level args (IConst (name as (s, _), T, T_args)) = - if is_fool andalso s = "c_If" andalso - (length args = 3 orelse is_type_enc_higher_order type_enc) then - IConst (`I tptp_ite, T, []) - else - (case proxify_const s of - SOME proxy_base => - let - val argc = length args - fun plain_const () = IConst (name, T, []) - fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args) - fun handle_fool card x = if card = argc then x else proxy_const () - in - if top_level then - (case s of - "c_False" => IConst (`I tptp_false, T, []) - | "c_True" => IConst (`I tptp_true, T, []) - | _ => plain_const ()) - else if is_type_enc_full_higher_order type_enc then - (case s of - "c_False" => IConst (`I tptp_false, T, []) - | "c_True" => IConst (`I tptp_true, T, []) - | "c_Not" => IConst (`I tptp_not, T, []) - | "c_conj" => IConst (`I tptp_and, T, []) - | "c_disj" => IConst (`I tptp_or, T, []) - | "c_implies" => IConst (`I tptp_implies, T, []) - | "c_All" => tweak_ho_quant tptp_ho_forall T args - | "c_Ex" => tweak_ho_quant tptp_ho_exists T args - | s => - if is_tptp_equal s then - tweak_ho_equal T argc - else - plain_const ()) - else if is_fool then - (case s of - "c_False" => IConst (`I tptp_false, T, []) - | "c_True" => IConst (`I tptp_true, T, []) - | "c_Not" => handle_fool 1 (IConst (`I tptp_not, T, [])) - | "c_conj" => handle_fool 2 (IConst (`I tptp_and, T, [])) - | "c_disj" => handle_fool 2 (IConst (`I tptp_or, T, [])) - | "c_implies" => handle_fool 2 (IConst (`I tptp_implies, T, [])) - | "c_All" => handle_fool 1 (tweak_ho_quant tptp_ho_forall T args) - | "c_Ex" => handle_fool 1 (tweak_ho_quant tptp_ho_exists T args) - | s => - if is_tptp_equal s then - handle_fool 2 (IConst (`I tptp_equal, T, [])) - else - plain_const ()) - else - proxy_const () - end - | NONE => - if s = tptp_choice then - tweak_ho_quant tptp_choice T args - else - IConst (name, T, T_args)) + let val argc = length args in + if is_fool andalso s = "c_If" andalso + (argc = 3 orelse is_type_enc_higher_order type_enc) then + IConst (`I tptp_ite, T, []) + else if is_fool andalso s = "c_Let" andalso argc = 2 then + IConst (`I tptp_let, T, []) + else + (case proxify_const s of + SOME proxy_base => + let + fun plain_const () = IConst (name, T, []) + fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args) + fun handle_fool card x = if card = argc then x else proxy_const () + in + if top_level then + (case s of + "c_False" => IConst (`I tptp_false, T, []) + | "c_True" => IConst (`I tptp_true, T, []) + | _ => plain_const ()) + else if is_type_enc_full_higher_order type_enc then + (case s of + "c_False" => IConst (`I tptp_false, T, []) + | "c_True" => IConst (`I tptp_true, T, []) + | "c_Not" => IConst (`I tptp_not, T, []) + | "c_conj" => IConst (`I tptp_and, T, []) + | "c_disj" => IConst (`I tptp_or, T, []) + | "c_implies" => IConst (`I tptp_implies, T, []) + | "c_All" => tweak_ho_quant tptp_ho_forall T args + | "c_Ex" => tweak_ho_quant tptp_ho_exists T args + | s => + if is_tptp_equal s then + tweak_ho_equal T argc + else + plain_const ()) + else if is_fool then + (case s of + "c_False" => IConst (`I tptp_false, T, []) + | "c_True" => IConst (`I tptp_true, T, []) + | "c_Not" => handle_fool 1 (IConst (`I tptp_not, T, [])) + | "c_conj" => handle_fool 2 (IConst (`I tptp_and, T, [])) + | "c_disj" => handle_fool 2 (IConst (`I tptp_or, T, [])) + | "c_implies" => handle_fool 2 (IConst (`I tptp_implies, T, [])) + | "c_All" => handle_fool 1 (tweak_ho_quant tptp_ho_forall T args) + | "c_Ex" => handle_fool 1 (tweak_ho_quant tptp_ho_exists T args) + | s => + if is_tptp_equal s then + handle_fool 2 (IConst (`I tptp_equal, T, [])) + else + plain_const ()) + else + proxy_const () + end + | NONE => + if s = tptp_choice then + tweak_ho_quant tptp_choice T args + else + IConst (name, T, T_args)) + end | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) | intro _ _ tm = tm in intro true [] end @@ -1958,7 +1973,8 @@ | s_not_prop (\<^const>\Pure.imp\ $ t $ \<^prop>\False\) = t | s_not_prop t = \<^const>\Pure.imp\ $ t $ \<^prop>\False\ -fun translate_formulas simp_options ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts = +fun translate_formulas simp_options ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t + facts = let val thy = Proof_Context.theory_of ctxt val trans_lams = trans_lams_of_string ctxt type_enc lam_trans @@ -2718,9 +2734,13 @@ val lam_trans = if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN else lam_trans - val simp_options = {if_simps = not (is_type_enc_fool type_enc)} + val simp_options = + let val simp = not (is_type_enc_fool type_enc) in + {if_simps = simp, let_simps = simp} + end val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) = - translate_formulas simp_options ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts + translate_formulas simp_options ctxt prem_role format type_enc lam_trans presimp hyp_ts + concl_t facts val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish val ctrss = all_ctrss_of_datatypes ctxt diff -r 2af4e088c01c -r a5bab59d580b src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Tue Jul 27 20:28:23 2021 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Tue Jul 27 10:36:22 2021 +0200 @@ -8,7 +8,8 @@ signature MESON = sig - type simp_options = {if_simps : bool} + type simp_options = {if_simps : bool, let_simps : bool} + val simp_options_all_true : simp_options val trace : bool Config.T val max_clauses : int Config.T val first_order_resolve : Proof.context -> thm -> thm -> thm @@ -49,7 +50,8 @@ structure Meson : MESON = struct -type simp_options = {if_simps : bool} +type simp_options = {if_simps : bool, let_simps : bool} +val simp_options_all_true = {if_simps = true, let_simps = true} val trace = Attrib.setup_config_bool \<^binding>\meson_trace\ (K false) @@ -533,7 +535,7 @@ val nnf_simps = @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel if_eq_cancel cases_simp} -fun nnf_extra_simps ({if_simps} : simp_options) = +fun nnf_extra_simps ({if_simps, ...} : simp_options) = (if if_simps then @{thms split_ifs} else []) @ @{thms ex_simps all_simps simp_thms} (* FIXME: "let_simp" is probably redundant now that we also rewrite with @@ -548,10 +550,10 @@ \<^const_name>\Ex1\, \<^const_name>\Ball\, \<^const_name>\Bex\, \<^const_name>\If\, \<^const_name>\Let\] -fun presimplify simp_options ctxt = +fun presimplify (simp_options as {let_simps, ...} : simp_options) ctxt = rewrite_rule ctxt (map safe_mk_meta_eq nnf_simps) #> simplify (put_simpset (nnf_ss simp_options) ctxt) - #> rewrite_rule ctxt @{thms Let_def [abs_def]} + #> let_simps ? rewrite_rule ctxt @{thms Let_def [abs_def]} fun make_nnf simp_options ctxt th = (case Thm.prems_of th of @@ -703,7 +705,7 @@ resolve_tac ctxt @{thms ccontr} 1, preskolem_tac, Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} => - EVERY1 [skolemize_prems_tac {if_simps = true} ctxt' negs, + EVERY1 [skolemize_prems_tac simp_options_all_true ctxt' negs, Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) diff -r 2af4e088c01c -r a5bab59d580b src/HOL/Tools/Meson/meson_tactic.ML --- a/src/HOL/Tools/Meson/meson_tactic.ML Tue Jul 27 20:28:23 2021 +0200 +++ b/src/HOL/Tools/Meson/meson_tactic.ML Tue Jul 27 10:36:22 2021 +0200 @@ -15,7 +15,10 @@ fun meson_general_tac ctxt ths = let val ctxt' = put_claset HOL_cs ctxt - in Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom {if_simps = true} ctxt' false true 0) ths) end + in + Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt' + false true 0) ths) + end val _ = Theory.setup diff -r 2af4e088c01c -r a5bab59d580b src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Jul 27 20:28:23 2021 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Jul 27 10:36:22 2021 +0200 @@ -155,7 +155,8 @@ (Thm.get_name_hint th, th |> Drule.eta_contraction_rule - |> Meson_Clausify.cnf_axiom {if_simps = true} ctxt new_skolem (lam_trans = combsN) j + |> Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt new_skolem + (lam_trans = combsN) j ||> map do_lams)) (0 upto length ths0 - 1) ths0 val ths = maps (snd o snd) th_cls_pairs