Theory well_founded_continued

theory well_founded_continued

(* N. Peltier - http://membres-lig.imag.fr/peltier/ *)

imports Main

begin

subsection ‹Well-Founded Sets›

text ‹Most useful lemmata are already proven in the Well\_Founded theory available in Isabelle. 
We only establish a few convenient results for constructing well-founded sets and relations.›

lemma measure_wf:
  assumes "wf (r :: ('a × 'a) set)"
  assumes "r' = { (x,y). ((m x),(m y)) ∈ r }"
  shows "wf r'"
proof -
  have "(∀Q::'b set. ∀x:: 'b. x∈Q ⟶ (∃z∈Q. ∀y. (y,z)∈ r' --> y∉Q))"
  proof  ((rule allI)+,(rule impI))
    fix Q:: "'b set" fix x:: 'b assume "x∈Q"
    let ?Q' = "(m ` Q)"
    from ‹x ∈ Q› have Q'_not_empty: "m x ∈ ?Q'" by auto
    from assms(1) and Q'_not_empty obtain z' where "z' ∈ ?Q'" and z'min: "∀y. (y,z')∈ r 
      ⟶ y∉?Q'" using wf_eq_minimal [of r] by blast
    from ‹z' ∈ ?Q'› obtain z where "z' = (m z)" and "z ∈ Q" by auto
    have "∀y. (y,z)∈ r' ⟶ y∉Q"
    proof ((rule allI),(rule impI))
      fix y assume "(y,z)∈ r'"
      from assms(2) and this and ‹z' = (m z)› have "((m y),z') ∈ r" by auto
      from this and z'min have "(m y) ∉ ?Q'" by auto
      then show "y∉Q" by auto
    qed
    from this and ‹z ∈ Q› show "(∃z∈Q. ∀y. (y,z)∈ r' --> y∉Q)"  by auto
  qed
  then show ?thesis using wf_eq_minimal by auto
qed

lemma finite_proj_wf:
  assumes "finite E"
  assumes "x ∈ E"
  assumes "acyclic r"
  shows "(∃ y. y ∈ E ∧ (∀ z. (z, y) ∈ r ⟶ z ∉ E))"
proof -
  let ?r = "{ (u,v). (u ∈ E ∧ v ∈ E ∧ (u,v) ∈ r) }"
  from assms(1) have "finite (E × E)" by auto
  have "?r ⊆ (E × E)" by auto
  have "?r ⊆ r" by auto
  from ‹?r ⊆ (E × E)› and ‹finite (E × E)› have "finite ?r" using finite_subset by auto
  from assms(3) and ‹?r ⊆ r› have "acyclic ?r" unfolding acyclic_def using trancl_mono by blast 
  from ‹acyclic ?r› ‹finite ?r› have "wf ?r" using finite_acyclic_wf by auto
  from this assms(2) obtain y where "y ∈ E" and i: "⋀z. (z, y) ∈ ?r ⟹ z ∉ E"  
    using wfE_min [of "?r" x E] by blast
  have "∀z. (z, y) ∈ r ⟶ z ∉ E"
  proof (rule allI,rule impI)
    fix z assume "(z,y) ∈ r"
    show "z ∉ E"
    proof 
      assume "z ∈ E"
      from this and ‹y ∈ E› and ‹(z,y) ∈ r› have "(z,y) ∈ ?r" by auto
      from this and i [of z] and ‹z ∈ E› show False by auto
    qed
  qed
  from this and ‹y ∈ E› show ?thesis by auto
qed

end