merged
authordesharna
Fri, 07 Jan 2022 08:50:12 +0100
changeset 74972 e578640c787a
parent 74971 16eaa56f69f7 (diff)
parent 74969 fa0020b47868 (current diff)
child 74973 a565a2889b49
merged
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Jan 05 15:35:23 2022 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Jan 07 08:50:12 2022 +0100
@@ -302,7 +302,7 @@
          if string_ord (getenv "E_VERSION", "2.7") <> LESS then
            (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
          else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
-           (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
+           (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
          else
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN)
      in
--- a/src/HOL/Wellfounded.thy	Wed Jan 05 15:35:23 2022 +0000
+++ b/src/HOL/Wellfounded.thy	Fri Jan 07 08:50:12 2022 +0100
@@ -56,6 +56,12 @@
   obtains "(x, a) \<notin> r"
   by (drule wf_not_sym[OF assms])
 
+lemma wf_imp_asym: "wf r \<Longrightarrow> asym r"
+  by (auto intro: asymI elim: wf_asym)
+
+lemma wfP_imp_asymp: "wfP r \<Longrightarrow> asymp r"
+  by (rule wf_imp_asym[to_pred])
+
 lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r"
   by (blast elim: wf_asym)
 
@@ -68,6 +74,9 @@
   assumes "wf r" shows "irrefl r" 
   using wf_irrefl [OF assms] by (auto simp add: irrefl_def)
 
+lemma wfP_imp_irreflp: "wfP r \<Longrightarrow> irreflp r"
+  by (rule wf_imp_irrefl[to_pred])
+
 lemma wf_wellorderI:
   assumes wf: "wf {(x::'a::ord, y). x < y}"
     and lin: "OFCLASS('a::ord, linorder_class)"