# HG changeset patch
# User krauss
# Date 1256596017 -3600
# Node ID 7c61bc5d731039b265c6de4b498b23f21330428b
# Parent  6fd85372981e2d3b52d756ec031e723da2650ca7
point-free characterization of well-foundedness

diff -r 6fd85372981e -r 7c61bc5d7310 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Oct 26 23:26:18 2009 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Oct 26 23:26:57 2009 +0100
@@ -84,7 +84,62 @@
 
 subsection {* Basic Results *}
 
-text{*transitive closure of a well-founded relation is well-founded! *}
+text {* Point-free characterization of well-foundedness *}
+
+lemma wfE_pf:
+  assumes wf: "wf R"
+  assumes a: "A \<subseteq> R `` A"
+  shows "A = {}"
+proof -
+  { fix x
+    from wf have "x \<notin> A"
+    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
+  } thus ?thesis by auto
+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
+
+text{*Minimal-element characterization of well-foundedness*}
+
+lemma wfE_min:
+  assumes wf: "wf R" and Q: "x \<in> Q"
+  obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
+  using Q wfE_pf[OF wf, of Q] by blast
+
+lemma wfI_min:
+  assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q"
+  shows "wf R"
+proof (rule wfI_pf)
+  fix A assume b: "A \<subseteq> R `` A"
+  { fix x assume "x \<in> A"
+    from a[OF this] b have "False" by blast
+  }
+  thus "A = {}" by blast
+qed
+
+lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
+apply auto
+apply (erule wfE_min, assumption, blast)
+apply (rule wfI_min, auto)
+done
+
+lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
+
+text{* Well-foundedness of transitive closure *}
+
 lemma wf_trancl:
   assumes "wf r"
   shows "wf (r^+)"
@@ -124,43 +179,8 @@
   apply (erule wf_trancl)
   done
 
+text {* Well-foundedness of subsets *}
 
-text{*Minimal-element characterization of well-foundedness*}
-lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
-proof (intro iffI strip)
-  fix Q :: "'a set" and x
-  assume "wf r" and "x \<in> Q"
-  then show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
-    unfolding wf_def
-    by (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 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])
-    then have "\<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
-    then show "P x" by simp
-  qed
-qed
-
-lemma wfE_min: 
-  assumes "wf R" "x \<in> Q"
-  obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
-  using assms unfolding wf_eq_minimal by blast
-
-lemma wfI_min:
-  "(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q)
-  \<Longrightarrow> wf R"
-  unfolding wf_eq_minimal by blast
-
-lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
-
-text {* Well-foundedness of subsets *}
 lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
   apply (simp (no_asm_use) add: wf_eq_minimal)
   apply fast
@@ -169,7 +189,8 @@
 lemmas wfP_subset = wf_subset [to_pred]
 
 text {* Well-foundedness of the empty relation *}
-lemma wf_empty [iff]: "wf({})"
+
+lemma wf_empty [iff]: "wf {}"
   by (simp add: wf_def)
 
 lemma wfP_empty [iff]:
@@ -189,7 +210,20 @@
   apply (rule Int_lower2)
   done  
 
-text{*Well-foundedness of insert*}
+text {* Exponentiation *}
+
+lemma wf_exp:
+  assumes "wf (R ^^ n)"
+  shows "wf R"
+proof (rule wfI_pf)
+  fix A assume "A \<subseteq> R `` A"
+  then have "A \<subseteq> (R ^^ n) `` A" by (induct n) force+
+  with `wf (R ^^ n)`
+  show "A = {}" by (rule wfE_pf)
+qed
+
+text {* Well-foundedness of insert *}
+
 lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
 apply (rule iffI)
  apply (blast elim: wf_trancl [THEN wf_irrefl]
@@ -212,6 +246,7 @@
 done
 
 text{*Well-foundedness of image*}
+
 lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
 apply (simp only: wf_eq_minimal, clarify)
 apply (case_tac "EX p. f p : Q")