src/HOL/Wellfounded.thy
 changeset 33216 7c61bc5d7310 parent 33215 6fd85372981e child 33217 ab979f6e99f4
1.1 --- a/src/HOL/Wellfounded.thy	Mon Oct 26 23:26:18 2009 +0100
1.2 +++ b/src/HOL/Wellfounded.thy	Mon Oct 26 23:26:57 2009 +0100
1.3 @@ -84,7 +84,62 @@
1.5  subsection {* Basic Results *}
1.7 -text{*transitive closure of a well-founded relation is well-founded! *}
1.8 +text {* Point-free characterization of well-foundedness *}
1.9 +
1.10 +lemma wfE_pf:
1.11 +  assumes wf: "wf R"
1.12 +  assumes a: "A \<subseteq> R `` A"
1.13 +  shows "A = {}"
1.14 +proof -
1.15 +  { fix x
1.16 +    from wf have "x \<notin> A"
1.17 +    proof induct
1.18 +      fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A"
1.19 +      then have "x \<notin> R `` A" by blast
1.20 +      with a show "x \<notin> A" by blast
1.21 +    qed
1.22 +  } thus ?thesis by auto
1.23 +qed
1.24 +
1.25 +lemma wfI_pf:
1.26 +  assumes a: "\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}"
1.27 +  shows "wf R"
1.28 +proof (rule wfUNIVI)
1.29 +  fix P :: "'a \<Rightarrow> bool" and x
1.30 +  let ?A = "{x. \<not> P x}"
1.31 +  assume "\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x"
1.32 +  then have "?A \<subseteq> R `` ?A" by blast
1.33 +  with a show "P x" by blast
1.34 +qed
1.35 +
1.36 +text{*Minimal-element characterization of well-foundedness*}
1.37 +
1.38 +lemma wfE_min:
1.39 +  assumes wf: "wf R" and Q: "x \<in> Q"
1.40 +  obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
1.41 +  using Q wfE_pf[OF wf, of Q] by blast
1.42 +
1.43 +lemma wfI_min:
1.44 +  assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q"
1.45 +  shows "wf R"
1.46 +proof (rule wfI_pf)
1.47 +  fix A assume b: "A \<subseteq> R `` A"
1.48 +  { fix x assume "x \<in> A"
1.49 +    from a[OF this] b have "False" by blast
1.50 +  }
1.51 +  thus "A = {}" by blast
1.52 +qed
1.53 +
1.54 +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))"
1.55 +apply auto
1.56 +apply (erule wfE_min, assumption, blast)
1.57 +apply (rule wfI_min, auto)
1.58 +done
1.59 +
1.60 +lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
1.61 +
1.62 +text{* Well-foundedness of transitive closure *}
1.63 +
1.64  lemma wf_trancl:
1.65    assumes "wf r"
1.66    shows "wf (r^+)"
1.67 @@ -124,43 +179,8 @@
1.68    apply (erule wf_trancl)
1.69    done
1.71 +text {* Well-foundedness of subsets *}
1.73 -text{*Minimal-element characterization of well-foundedness*}
1.74 -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))"
1.75 -proof (intro iffI strip)
1.76 -  fix Q :: "'a set" and x
1.77 -  assume "wf r" and "x \<in> Q"
1.78 -  then show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
1.79 -    unfolding wf_def
1.80 -    by (blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"])
1.81 -next
1.82 -  assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
1.83 -  show "wf r"
1.84 -  proof (rule wfUNIVI)
1.85 -    fix P :: "'a \<Rightarrow> bool" and x
1.86 -    assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x"
1.87 -    let ?Q = "{x. \<not> P x}"
1.88 -    have "x \<in> ?Q \<longrightarrow> (\<exists>z \<in> ?Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> ?Q)"
1.89 -      by (rule 1 [THEN spec, THEN spec])
1.90 -    then have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp
1.91 -    with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast
1.92 -    then show "P x" by simp
1.93 -  qed
1.94 -qed
1.95 -
1.96 -lemma wfE_min:
1.97 -  assumes "wf R" "x \<in> Q"
1.98 -  obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
1.99 -  using assms unfolding wf_eq_minimal by blast
1.101 -lemma wfI_min:
1.102 -  "(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q)
1.103 -  \<Longrightarrow> wf R"
1.104 -  unfolding wf_eq_minimal by blast
1.106 -lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
1.108 -text {* Well-foundedness of subsets *}
1.109  lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
1.110    apply (simp (no_asm_use) add: wf_eq_minimal)
1.111    apply fast
1.112 @@ -169,7 +189,8 @@
1.113  lemmas wfP_subset = wf_subset [to_pred]
1.115  text {* Well-foundedness of the empty relation *}
1.116 -lemma wf_empty [iff]: "wf({})"
1.118 +lemma wf_empty [iff]: "wf {}"
1.119    by (simp add: wf_def)
1.121  lemma wfP_empty [iff]:
1.122 @@ -189,7 +210,20 @@
1.123    apply (rule Int_lower2)
1.124    done
1.126 -text{*Well-foundedness of insert*}
1.127 +text {* Exponentiation *}
1.129 +lemma wf_exp:
1.130 +  assumes "wf (R ^^ n)"
1.131 +  shows "wf R"
1.132 +proof (rule wfI_pf)
1.133 +  fix A assume "A \<subseteq> R `` A"
1.134 +  then have "A \<subseteq> (R ^^ n) `` A" by (induct n) force+
1.135 +  with `wf (R ^^ n)`
1.136 +  show "A = {}" by (rule wfE_pf)
1.137 +qed
1.139 +text {* Well-foundedness of insert *}
1.141  lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
1.142  apply (rule iffI)
1.143   apply (blast elim: wf_trancl [THEN wf_irrefl]
1.144 @@ -212,6 +246,7 @@
1.145  done
1.147  text{*Well-foundedness of image*}
1.149  lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
1.150  apply (simp only: wf_eq_minimal, clarify)
1.151  apply (case_tac "EX p. f p : Q")