src/HOL/Wellfounded.thy

 unfolding wf_def by (blast intro: less_induct)
 
 
 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^+)"
 proof -
   {

 lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)"
   apply (subst trancl_converse [symmetric])
   apply (erule wf_trancl)
   done
 
-
-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
   done
 
 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]:
   "wfP (\<lambda>x y. False)"
 proof -

 lemma wf_Int2: "wf r ==> wf (r' Int r)"
   apply (erule wf_subset)
   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]
               intro: rtrancl_into_trancl1 wf_subset 
                      rtrancl_mono [THEN [2] rev_subsetD])

 txt{*Blast with new substOccur fails*}
 apply (fast intro: converse_rtrancl_into_rtrancl)
 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")
 apply (erule_tac x = "{p. f p : Q}" in allE)
 apply (fast dest: inj_onD, blast)