# HG changeset patch
# User desharna
# Date 1710662744 -3600
# Node ID 91b7695c92cff77b7fa09d080e50f801fcfe74e9
# Parent  65e0682cca6396b111e48b36808abfff6c366411
tuned proofs

diff -r 65e0682cca63 -r 91b7695c92cf src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Mar 17 09:03:18 2024 +0100
+++ b/src/HOL/Wellfounded.thy	Sun Mar 17 09:05:44 2024 +0100
@@ -150,19 +150,8 @@
     by blast
 qed
 
-lemma wfE_pf:
-  assumes wf: "wf R"
-    and a: "A \<subseteq> R `` A"
-  shows "A = {}"
-proof -
-  from wf have "x \<notin> A" for x
-  proof induct
-    fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A"
-    then have "x \<notin> R `` A" by blast
-    with a show "x \<notin> A" by blast
-  qed
-  then show ?thesis by auto
-qed
+lemma wfE_pf: "wf R \<Longrightarrow> A \<subseteq> R `` A \<Longrightarrow> A = {}"
+  using wf_onE_pf[of UNIV, unfolded wf_on_UNIV, simplified] .
 
 lemma wf_onI_pf:
   assumes "\<And>B. B \<subseteq> A \<Longrightarrow> B \<subseteq> R `` B \<Longrightarrow> B = {}"
@@ -180,16 +169,8 @@
     by simp
 qed
 
-lemma wfI_pf:
-  assumes a: "\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}"
-  shows "wf R"
-proof (rule wfUNIVI)
-  fix P :: "'a \<Rightarrow> bool" and x
-  let ?A = "{x. \<not> P x}"
-  assume "\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x"
-  then have "?A \<subseteq> R `` ?A" by blast
-  with a show "P x" by blast
-qed
+lemma wfI_pf: "(\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}) \<Longrightarrow> wf R"
+  using wf_onI_pf[of UNIV, unfolded wf_on_UNIV, simplified] .
 
 
 subsubsection \<open>Minimal-element characterization of well-foundedness\<close>
@@ -244,9 +225,7 @@
 qed
 
 lemma wf_eq_minimal: "wf r \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q))"
-  apply (rule iffI)
-   apply (blast intro:  elim!: wfE_min)
-  by (rule wfI_min) auto
+  unfolding wf_iff_ex_minimal by blast
 
 lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]