# HG changeset patch
# User huffman
# Date 1177176752 -7200
# Node ID 116c1d6b4026a8ae3c9696919b82c170426c3c73
# Parent  2a3840aa2ffdaf835bdea482ec0a3fc03be00436
faster proof of wf_eq_minimal

diff -r 2a3840aa2ffd -r 116c1d6b4026 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Sat Apr 21 11:07:45 2007 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Sat Apr 21 19:32:32 2007 +0200
@@ -122,8 +122,18 @@
     by (unfold wf_def, 
         blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"]) 
 next
-  assume "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
-  thus "wf r" by (unfold wf_def, force)
+  assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
+  show "wf r"
+  proof (rule wfUNIVI)
+    fix P :: "'a \<Rightarrow> bool" and x
+    assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x"
+    let ?Q = "{x. \<not> P x}"
+    have "x \<in> ?Q \<longrightarrow> (\<exists>z\<in>?Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> ?Q)"
+      by (rule 1 [THEN spec, THEN spec])
+    hence "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp
+    with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast
+    thus "P x" by simp
+  qed
 qed
 
 lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]