--- 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")