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.4  
     1.5  subsection {* Basic Results *}
     1.6  
     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.70  
    1.71 +text {* Well-foundedness of subsets *}
    1.72  
    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.100 -
   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.105 -
   1.106 -lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
   1.107 -
   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.114  
   1.115  text {* Well-foundedness of the empty relation *}
   1.116 -lemma wf_empty [iff]: "wf({})"
   1.117 +
   1.118 +lemma wf_empty [iff]: "wf {}"
   1.119    by (simp add: wf_def)
   1.120  
   1.121  lemma wfP_empty [iff]:
   1.122 @@ -189,7 +210,20 @@
   1.123    apply (rule Int_lower2)
   1.124    done  
   1.125  
   1.126 -text{*Well-foundedness of insert*}
   1.127 +text {* Exponentiation *}
   1.128 +
   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.138 +
   1.139 +text {* Well-foundedness of insert *}
   1.140 +
   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.146  
   1.147  text{*Well-foundedness of image*}
   1.148 +
   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")