# HG changeset patch
# User desharna
# Date 1641487507 -3600
# Node ID 16eaa56f69f70614a333f13997b9eec459ff6a9b
# Parent  afd8da649d75d9ee36580358be9601e4470254fe
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp

diff -r afd8da649d75 -r 16eaa56f69f7 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Jan 05 10:56:41 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Thu Jan 06 17:45:07 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)"