# HG changeset patch
# User desharna
# Date 1665578223 -7200
# Node ID 5ea1f8bfb795aea0291f1bb2d15d4f2cbe46f46d
# Parent  0b2fcf0c61dba37c641deb4764e7205b8562b2a7
added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat

diff -r 0b2fcf0c61db -r 5ea1f8bfb795 NEWS
--- a/NEWS	Wed Oct 12 14:33:04 2022 +0200
+++ b/NEWS	Wed Oct 12 14:37:03 2022 +0200
@@ -24,6 +24,12 @@
       reflp_le[simp]
       totalp_on_singleton[simp]
 
+* Theory "HOL.Wellfounded":
+  - Added lemmas.
+      wfP_if_convertible_to_nat
+      wfP_if_convertible_to_wfP
+      wf_if_convertible_to_wf
+
 
 New in Isabelle2022 (October 2022)
 ----------------------------------
diff -r 0b2fcf0c61db -r 5ea1f8bfb795 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Oct 12 14:33:04 2022 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Oct 12 14:37:03 2022 +0200
@@ -772,7 +772,35 @@
     by (clarsimp simp: inv_image_def wf_eq_minimal)
 qed
 
-text \<open>Measure functions into \<^typ>\<open>nat\<close>\<close>
+
+subsubsection \<open>Conversion to a known well-founded relation\<close>
+
+lemma wf_if_convertible_to_wf:
+  fixes r :: "'a rel" and s :: "'b rel" and f :: "'a \<Rightarrow> 'b"
+  assumes "wf s" and convertible: "\<And>x y. (x, y) \<in> r \<Longrightarrow> (f x, f y) \<in> s"
+  shows "wf r"
+proof (rule wfI_min[of r])
+  fix x :: 'a and Q :: "'a set"
+  assume "x \<in> Q"
+  then obtain y where "y \<in> Q" and "\<And>z. (f z, f y) \<in> s \<Longrightarrow> z \<notin> Q"
+    by (auto elim: wfE_min[OF wf_inv_image[of s f, OF \<open>wf s\<close>], unfolded in_inv_image])
+  thus "\<exists>z \<in> Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
+    by (auto intro: convertible)
+qed
+
+lemma wfP_if_convertible_to_wfP: "wfP S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfP R"
+  using wf_if_convertible_to_wf[to_pred, of S R f] by simp
+
+text \<open>Converting to @{typ nat} is a very common special case that might be found more easily by
+  Sledgehammer.\<close>
+
+lemma wfP_if_convertible_to_nat:
+  fixes f :: "_ \<Rightarrow> nat"
+  shows "(\<And>x y. R x y \<Longrightarrow> f x < f y) \<Longrightarrow> wfP R"
+  by (rule wfP_if_convertible_to_wfP[of "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool", simplified])
+
+
+subsubsection \<open>Measure functions into \<^typ>\<open>nat\<close>\<close>
 
 definition measure :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set"
   where "measure = inv_image less_than"