--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jul 19 14:47:53 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jul 22 13:07:09 2021 +0200
@@ -1325,10 +1325,10 @@
| _ => do_term bs t)
in do_formula [] end
-fun presimplify_term ctxt t =
+fun presimplify_term simp_options ctxt t =
if exists_Const (member (op =) Meson.presimplified_consts o fst) t then
t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
- |> Meson.presimplify ctxt
+ |> Meson.presimplify simp_options ctxt
|> Thm.prop_of
else
t
@@ -1362,7 +1362,7 @@
? map_types (map_type_tvar freeze_tvar)
end
-fun presimp_prop ctxt type_enc t =
+fun presimp_prop simp_options ctxt type_enc t =
let
val t = t |> Envir.beta_eta_contract
|> transform_elim_prop
@@ -1373,7 +1373,7 @@
t |> need_trueprop ? HOLogic.mk_Trueprop
|> (if is_ho then unextensionalize_def
else cong_extensionalize_term ctxt #> abs_extensionalize_term ctxt)
- |> presimplify_term ctxt
+ |> presimplify_term simp_options ctxt
|> HOLogic.dest_Trueprop
end
handle TERM _ => \<^const>\<open>True\<close>
@@ -1958,7 +1958,7 @@
| s_not_prop (\<^const>\<open>Pure.imp\<close> $ t $ \<^prop>\<open>False\<close>) = t
| s_not_prop t = \<^const>\<open>Pure.imp\<close> $ t $ \<^prop>\<open>False\<close>
-fun translate_formulas 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
@@ -1976,7 +1976,7 @@
|> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts)
val ((conjs, facts), lam_facts) =
(conjs, facts)
- |> presimp ? apply2 (map (apsnd (apsnd (presimp_prop ctxt type_enc))))
+ |> presimp ? apply2 (map (apsnd (apsnd (presimp_prop simp_options ctxt type_enc))))
|> (if lam_trans = no_lamsN then
rpair []
else
@@ -2718,8 +2718,9 @@
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 (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
- translate_formulas 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
--- a/src/HOL/Tools/Meson/meson.ML Mon Jul 19 14:47:53 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Thu Jul 22 13:07:09 2021 +0200
@@ -8,6 +8,7 @@
signature MESON =
sig
+ type simp_options = {if_simps : bool}
val trace : bool Config.T
val max_clauses : int Config.T
val first_order_resolve : Proof.context -> thm -> thm -> thm
@@ -16,11 +17,11 @@
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
val finish_cnf: thm list -> thm list
val presimplified_consts : string list
- val presimplify: Proof.context -> thm -> thm
- val make_nnf: Proof.context -> thm -> thm
+ val presimplify: simp_options -> Proof.context -> thm -> thm
+ val make_nnf: simp_options -> Proof.context -> thm -> thm
val choice_theorems : theory -> thm list
- val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
- val skolemize : Proof.context -> thm -> thm
+ val skolemize_with_choice_theorems : simp_options -> Proof.context -> thm list -> thm -> thm
+ val skolemize : simp_options -> Proof.context -> thm -> thm
val cong_extensionalize_thm : Proof.context -> thm -> thm
val abs_extensionalize_conv : Proof.context -> conv
val abs_extensionalize_thm : Proof.context -> thm -> thm
@@ -30,7 +31,7 @@
val best_prolog_tac: Proof.context -> (thm -> int) -> thm list -> tactic
val depth_prolog_tac: Proof.context -> thm list -> tactic
val gocls: thm list -> thm list
- val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic
+ val skolemize_prems_tac : simp_options -> Proof.context -> thm list -> int -> tactic
val MESON:
tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context
-> int -> tactic
@@ -48,6 +49,8 @@
structure Meson : MESON =
struct
+type simp_options = {if_simps : bool}
+
val trace = Attrib.setup_config_bool \<^binding>\<open>meson_trace\<close> (K false)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
@@ -530,13 +533,14 @@
val nnf_simps =
@{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}
+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
"Let_def [abs_def]". *)
-val nnf_ss =
+fun nnf_ss simp_options =
simpset_of (put_simpset HOL_basic_ss \<^context>
- addsimps nnf_extra_simps
+ addsimps (nnf_extra_simps simp_options)
addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>, \<^simproc>\<open>neq\<close>, \<^simproc>\<open>let_simp\<close>])
val presimplified_consts =
@@ -544,14 +548,14 @@
\<^const_name>\<open>Ex1\<close>, \<^const_name>\<open>Ball\<close>, \<^const_name>\<open>Bex\<close>, \<^const_name>\<open>If\<close>,
\<^const_name>\<open>Let\<close>]
-fun presimplify ctxt =
+fun presimplify simp_options ctxt =
rewrite_rule ctxt (map safe_mk_meta_eq nnf_simps)
- #> simplify (put_simpset nnf_ss ctxt)
+ #> simplify (put_simpset (nnf_ss simp_options) ctxt)
#> rewrite_rule ctxt @{thms Let_def [abs_def]}
-fun make_nnf ctxt th =
+fun make_nnf simp_options ctxt th =
(case Thm.prems_of th of
- [] => th |> presimplify ctxt |> make_nnf1 ctxt
+ [] => th |> presimplify simp_options ctxt |> make_nnf1 ctxt
| _ => raise THM ("make_nnf: premises in argument", 0, [th]));
fun choice_theorems thy =
@@ -559,7 +563,7 @@
(* Pull existential quantifiers to front. This accomplishes Skolemization for
clauses that arise from a subgoal. *)
-fun skolemize_with_choice_theorems ctxt choice_ths =
+fun skolemize_with_choice_theorems simp_options ctxt choice_ths =
let
fun aux th =
if not (has_conns [\<^const_name>\<open>Ex\<close>] (Thm.prop_of th)) then
@@ -575,11 +579,11 @@
handle THM ("tryres", _, _) =>
rename_bound_vars_RS th ex_forward
|> forward_res ctxt aux
- in aux o make_nnf ctxt end
+ in aux o make_nnf simp_options ctxt end
-fun skolemize ctxt =
+fun skolemize simp_options ctxt =
let val thy = Proof_Context.theory_of ctxt in
- skolemize_with_choice_theorems ctxt (choice_theorems thy)
+ skolemize_with_choice_theorems simp_options ctxt (choice_theorems thy)
end
exception NO_F_PATTERN of unit
@@ -638,7 +642,7 @@
val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
-fun try_skolemize_etc ctxt th =
+fun try_skolemize_etc simp_options ctxt th =
let
val th = th |> cong_extensionalize_thm ctxt
in
@@ -647,7 +651,7 @@
Sledgehammer does, but also keep an unextensionalized version of "th" for
backward compatibility. *)
|> insert Thm.eq_thm_prop (abs_extensionalize_thm ctxt th)
- |> map_filter (fn th => th |> try (skolemize ctxt)
+ |> map_filter (fn th => th |> try (skolemize simp_options ctxt)
|> tap (fn NONE =>
trace_msg ctxt (fn () =>
"Failed to skolemize " ^
@@ -687,8 +691,9 @@
(*Return all negative clauses, as possible goal clauses*)
fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
-fun skolemize_prems_tac ctxt prems =
- cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o eresolve_tac ctxt [exE]
+fun skolemize_prems_tac simp_options ctxt prems =
+ cut_facts_tac (maps (try_skolemize_etc simp_options ctxt) prems) THEN'
+ REPEAT o eresolve_tac ctxt [exE]
(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
Function mkcl converts theorems to clauses.*)
@@ -698,7 +703,7 @@
resolve_tac ctxt @{thms ccontr} 1,
preskolem_tac,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
- EVERY1 [skolemize_prems_tac ctxt' negs,
+ EVERY1 [skolemize_prems_tac {if_simps = 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*)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Mon Jul 19 14:47:53 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Jul 22 13:07:09 2021 +0200
@@ -15,8 +15,7 @@
val introduce_combinators_in_theorem : Proof.context -> thm -> thm
val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
val ss_only : thm list -> Proof.context -> Proof.context
- val cnf_axiom :
- Proof.context -> bool -> bool -> int -> thm
+ val cnf_axiom : Meson.simp_options -> Proof.context -> bool -> bool -> int -> thm
-> (thm * term) option * thm list
end;
@@ -295,7 +294,7 @@
|> Skip_Proof.make_thm \<^theory>
(* Converts an Isabelle theorem into NNF. *)
-fun nnf_axiom choice_ths new_skolem ax_no th ctxt =
+fun nnf_axiom simp_options choice_ths new_skolem ax_no th ctxt =
let
val thy = Proof_Context.theory_of ctxt
val th =
@@ -306,12 +305,12 @@
val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
|> Meson.cong_extensionalize_thm ctxt
|> Meson.abs_extensionalize_thm ctxt
- |> Meson.make_nnf ctxt
+ |> Meson.make_nnf simp_options ctxt
in
if new_skolem then
let
fun skolemize choice_ths =
- Meson.skolemize_with_choice_theorems ctxt choice_ths
+ Meson.skolemize_with_choice_theorems simp_options ctxt choice_ths
#> simplify (ss_only @{thms all_simps[symmetric]} ctxt)
val no_choice = null choice_ths
val pull_out =
@@ -359,11 +358,11 @@
end
(* Convert a theorem to CNF, with additional premises due to skolemization. *)
-fun cnf_axiom ctxt0 new_skolem combinators ax_no th =
+fun cnf_axiom simp_options ctxt0 new_skolem combinators ax_no th =
let
val choice_ths = Meson.choice_theorems (Proof_Context.theory_of ctxt0)
val (opt, (nnf_th, ctxt1)) =
- nnf_axiom choice_ths new_skolem ax_no th ctxt0
+ nnf_axiom simp_options choice_ths new_skolem ax_no th ctxt0
fun clausify th =
Meson.make_cnf
(if new_skolem orelse null choice_ths then []
--- a/src/HOL/Tools/Meson/meson_tactic.ML Mon Jul 19 14:47:53 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_tactic.ML Thu Jul 22 13:07:09 2021 +0200
@@ -15,7 +15,7 @@
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 ctxt' false true 0) ths) end
+ in Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom {if_simps = true} ctxt' false true 0) ths) end
val _ =
Theory.setup
--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Jul 19 14:47:53 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Jul 22 13:07:09 2021 +0200
@@ -155,7 +155,7 @@
(Thm.get_name_hint th,
th
|> Drule.eta_contraction_rule
- |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j
+ |> Meson_Clausify.cnf_axiom {if_simps = 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
--- a/src/HOL/ex/Meson_Test.thy Mon Jul 19 14:47:53 2021 +0200
+++ b/src/HOL/ex/Meson_Test.thy Thu Jul 22 13:07:09 2021 +0200
@@ -26,8 +26,8 @@
ML_prf \<open>
val ctxt = \<^context>;
val prem25 = Thm.assume \<^cprop>\<open>\<not> ?thesis\<close>;
- val nnf25 = Meson.make_nnf ctxt prem25;
- val xsko25 = Meson.skolemize ctxt nnf25;
+ val nnf25 = Meson.make_nnf {if_simps = true} ctxt prem25;
+ val xsko25 = Meson.skolemize {if_simps = true} ctxt nnf25;
\<close>
apply (tactic \<open>cut_tac xsko25 1 THEN REPEAT (eresolve_tac \<^context> [exE] 1)\<close>)
ML_val \<open>
@@ -50,8 +50,8 @@
ML_prf \<open>
val ctxt = \<^context>;
val prem26 = Thm.assume \<^cprop>\<open>\<not> ?thesis\<close>
- val nnf26 = Meson.make_nnf ctxt prem26;
- val xsko26 = Meson.skolemize ctxt nnf26;
+ val nnf26 = Meson.make_nnf {if_simps = true} ctxt prem26;
+ val xsko26 = Meson.skolemize {if_simps = true} ctxt nnf26;
\<close>
apply (tactic \<open>cut_tac xsko26 1 THEN REPEAT (eresolve_tac \<^context> [exE] 1)\<close>)
ML_val \<open>
@@ -77,8 +77,8 @@
ML_prf \<open>
val ctxt = \<^context>;
val prem43 = Thm.assume \<^cprop>\<open>\<not> ?thesis\<close>;
- val nnf43 = Meson.make_nnf ctxt prem43;
- val xsko43 = Meson.skolemize ctxt nnf43;
+ val nnf43 = Meson.make_nnf {if_simps = true} ctxt prem43;
+ val xsko43 = Meson.skolemize {if_simps = true} ctxt nnf43;
\<close>
apply (tactic \<open>cut_tac xsko43 1 THEN REPEAT (eresolve_tac \<^context> [exE] 1)\<close>)
ML_val \<open>