# HG changeset patch
# User wenzelm
# Date 1737410824 -3600
# Node ID 7e946a55ab4c3d3c14965cd0216825f8a67cee89
# Parent  cb05f8d3fd0503219d9b72b48e317a6af35058f6
tuned proofs;

diff -r cb05f8d3fd05 -r 7e946a55ab4c src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Mon Jan 20 23:00:17 2025 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Mon Jan 20 23:07:04 2025 +0100
@@ -295,7 +295,7 @@
   "list_all2 (P::'t18495 \<Rightarrow> 't18502 \<Rightarrow> bool) [] (l2::'t18502 list) = (l2 = []) \<and>
   list_all2 P ((h1::'t18495) # (t1::'t18495 list)) l2 =
   (if l2 = [] then False else P h1 (hd l2) \<and> list_all2 P t1 (tl l2))"
-  by simp (induct_tac l2, simp_all)
+  by simp (induct l2, simp_all)
 
 lemma FILTER[import_const FILTER : filter]:
   "filter (P::'t18680 \<Rightarrow> bool) [] = [] \<and>
@@ -308,18 +308,19 @@
   by simp
 
 lemma WF[import_const WF : wfP]:
-  "\<forall>u. wfP u \<longleftrightarrow> (\<forall>P. (\<exists>x :: 'A. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
+  "\<forall>R. wfP R \<longleftrightarrow> (\<forall>P. (\<exists>x :: 'A. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. R y x \<longrightarrow> \<not> P y)))"
 proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
-  fix u :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and x :: "'a" and Q
-  assume a: "x \<in> Q"
-  assume "\<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y))"
-  then have "(\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>x. (\<lambda>x. x \<in> Q) x \<and> (\<forall>y. u y x \<longrightarrow> y \<notin> Q))" by auto
-  with a show "\<exists>x\<in>Q. \<forall>y. u y x \<longrightarrow> y \<notin> Q" by auto
-next
-  fix u P and x :: 'A and z
-  assume "P x" "z \<in> {a. P a}" "\<And>y. u y z \<Longrightarrow> y \<notin> {a. P a}"
-  then show "\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)" by auto
+  fix R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and P :: "'a \<Rightarrow> bool" and x z :: "'a"
+  {
+    fix Q
+    assume a: "x \<in> Q"
+    assume "\<forall>P. (\<exists>x. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. R y x \<longrightarrow> \<not> P y))"
+    then have "(\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>x. (\<lambda>x. x \<in> Q) x \<and> (\<forall>y. R y x \<longrightarrow> y \<notin> Q))" by auto
+    with a show "\<exists>x\<in>Q. \<forall>y. R y x \<longrightarrow> y \<notin> Q" by auto
+  next
+    assume "P x" "z \<in> {a. P a}" "\<And>y. R y z \<Longrightarrow> y \<notin> {a. P a}"
+    then show "\<exists>x. P x \<and> (\<forall>y. R y x \<longrightarrow> \<not> P y)" by auto
+  }
 qed auto
 
 end
-