# HG changeset patch
# User desharna
# Date 1626952029 -7200
# Node ID bd575b1bd9bf62d02f820557536c7a9844586cc6
# Parent  bed899f14df785566b6e5b279eedf9176da5f8a6
added simp_options to meson

diff -r bed899f14df7 -r bd575b1bd9bf src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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
diff -r bed899f14df7 -r bd575b1bd9bf src/HOL/Tools/Meson/meson.ML
--- 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*)
 
diff -r bed899f14df7 -r bd575b1bd9bf src/HOL/Tools/Meson/meson_clausify.ML
--- 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 []
diff -r bed899f14df7 -r bd575b1bd9bf src/HOL/Tools/Meson/meson_tactic.ML
--- 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
diff -r bed899f14df7 -r bd575b1bd9bf src/HOL/Tools/Metis/metis_tactic.ML
--- 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
diff -r bed899f14df7 -r bd575b1bd9bf src/HOL/ex/Meson_Test.thy
--- 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>