Theory Wellfounded2 (Isabelle repository snapshot 47e4178f9a94 25-Sep-2012)

header {* More on well-founded relations *}

(* author: Andrei Popescu *)

theory Wellfounded2
imports Wellfounded Order_Relation2 "~~/src/HOL/Library/Wfrec"
begin



text {* This section contains some variations of results in the theory 
@{text "Wellfounded.thy"}:
\begin{itemize} 
\item means for slightly more direct definitions by well-founded recursion;
\item variations of well-founded induction; 
\item means for proving a linear order to be a well-order. 
\end{itemize} *}


subsection {* Well-founded recursion via genuine fixpoints *}


(*2*)lemma wfrec_fixpoint:
fixes r :: "('a * 'a) set" and 
      H :: "('a => 'b) => 'a => 'b" 
assumes WF: "wf r" and ADM: "adm_wf r H"
shows "wfrec r H = H (wfrec r H)"
proof(rule ext)
  fix x
  have "wfrec r H x = H (cut (wfrec r H) r x) x" 
  using wfrec[of r H] WF by simp
  also 
  {have "!! y. (y,x) : r ==> (cut (wfrec r H) r x) y = (wfrec r H) y"
   by (auto simp add: cut_apply)
   hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
   using ADM adm_wf_def[of r H] by auto
  }
  finally show "wfrec r H x = H (wfrec r H) x" .
qed
 

(*2*)lemma adm_wf_unique_fixpoint:
fixes r :: "('a * 'a) set" and 
      H :: "('a => 'b) => 'a => 'b" and 
      f :: "'a => 'b" and g :: "'a => 'b"
assumes WF: "wf r" and ADM: "adm_wf r H" and fFP: "f = H f" and gFP: "g = H g"
shows "f = g"
proof-
  {fix x 
   have "f x = g x"
   proof(rule wf_induct[of r "(λx. f x = g x)"], 
         auto simp add: WF)
     fix x assume "∀y. (y, x) ∈ r --> f y = g y"
     hence "H f x = H g x" using ADM adm_wf_def[of r H] by auto
     thus "f x = g x" using fFP and gFP by simp
   qed
  }
  thus ?thesis by (simp add: ext)
qed


(*2*)lemma wfrec_unique_fixpoint:
fixes r :: "('a * 'a) set" and 
      H :: "('a => 'b) => 'a => 'b" and 
      f :: "'a => 'b"
assumes WF: "wf r" and ADM: "adm_wf r H" and 
        fp: "f = H f"
shows "f = wfrec r H"
proof-
  have "H (wfrec r H) = wfrec r H" 
  using assms wfrec_fixpoint[of r H] by simp 
  thus ?thesis 
  using assms adm_wf_unique_fixpoint[of r H "wfrec r H"] by simp
qed



subsection {* Characterizations of well-founded-ness *}


text {* A transitive relation is well-founded iff it is ``locally" well-founded, 
i.e., iff its restriction to the lower bounds of of any element is well-founded.  *}

(*3*)lemma trans_wf_iff:
assumes "trans r" 
shows "wf r = (∀a. wf(r Int (r^-1``{a} × r^-1``{a})))"
proof-
  obtain R where R_def: "R = (λ a. r Int (r^-1``{a} × r^-1``{a}))" by blast
  {assume *: "wf r"
   {fix a 
    have "wf(R a)" 
    using * R_def wf_subset[of r "R a"] by auto
   }
  }
  (*  *)
  moreover 
  {assume *: "∀a. wf(R a)"
   have "wf r" 
   proof(unfold wf_def, clarify)
     fix phi a 
     assume **: "∀a. (∀b. (b,a) ∈ r --> phi b) --> phi a"
     obtain chi where chi_def: "chi = (λb. (b,a) ∈ r --> phi b)" by blast
     with * have "wf (R a)" by auto
     hence "(∀b. (∀c. (c,b) ∈ R a --> chi c) --> chi b) --> (∀b. chi b)"
     unfolding wf_def by blast
     moreover 
     have "∀b. (∀c. (c,b) ∈ R a --> chi c) --> chi b" 
     proof(auto simp add: chi_def R_def)
       fix b 
       assume 1: "(b,a) ∈ r" and 2: "∀c. (c, b) ∈ r ∧ (c, a) ∈ r --> phi c"
       hence "∀c. (c, b) ∈ r --> phi c"
       using assms trans_def[of r] by blast 
       thus "phi b" using ** by blast
     qed
     ultimately have  "∀b. chi b" by (rule mp)    
     with ** chi_def show "phi a" by blast
   qed
  }
  ultimately show ?thesis using R_def by blast
qed


text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded, 
allowing one to assume the set included in the field.  *}

(*2*)lemma wf_eq_minimal2: 
"wf r = (∀A. A <= Field r ∧ A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. ¬ (a',a) ∈ r))"
proof-
  let ?phi = "λ A. A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. ¬ (a',a) ∈ r)"
  have "wf r = (∀A. ?phi A)"
  proof(unfold wf_eq_minimal, auto)
    fix A c assume *: "∀A. (∃c. c ∈ A) --> (∃a∈A. ∀a'. (a', a) ∈ r --> a' ∉ A)" and 
                  **: "∀a∈A. ∃a'∈A. (a', a) ∈ r" and 
                 ***: "c ∈ A"
    obtain a where "a ∈ A ∧ (∀a'. (a', a) ∈ r --> a' ∉ A)" 
    using * *** by auto
    with ** show False by blast
  next
    fix A::"'a set" and c 
    assume *: "∀A. A ≠ {} --> (∃a∈A. ∀a'∈A. (a', a) ∉ r)" and 
           **: "c ∈ A"
    obtain a where "a ∈ A ∧ (∀a'∈A. (a', a) ∉ r)" using * ** by blast
    thus "∃a∈A. ∀a'. (a', a) ∈ r --> a' ∉ A" by blast
  qed  (* Why did this not go directly by blast?  *)
  (*  *)   
  also have "(∀A. ?phi A) = (∀B ≤ Field r. ?phi B)"
  proof
    assume "∀A. ?phi A" 
    thus "∀B ≤ Field r. ?phi B" by simp
  next
    assume *: "∀B ≤ Field r. ?phi B"
    show "∀A. ?phi A"
    proof(clarify)
      fix A::"'a set" assume **: "A ≠ {}"  
      obtain B where B_def: "B = A Int (Field r)" by blast
      show "∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r" 
      proof(cases "B = {}")
        assume Case1: "B = {}"
        obtain a where 1: "a ∈ A ∧ a ∉ Field r" using ** Case1 B_def by auto
        hence "∀a' ∈ A. (a',a) ∉ r" using 1 unfolding Field_def by blast
        thus ?thesis using 1 by auto 
      next
        assume Case2: "B ≠ {}" have 1: "B ≤ Field r" using B_def by auto
        obtain a where 2: "a ∈ B ∧ (∀a' ∈ B. (a',a) ∉ r)" 
        using Case2 1 * by blast
        have "∀a' ∈ A. (a',a) ∉ r"
        proof(clarify)
          fix a' assume "a' ∈ A" and **: "(a',a) ∈ r"
          hence "a' ∈ B" using B_def Field_def by fastforce 
          thus False using 2 ** by auto
        qed
        thus ?thesis using 2 B_def by auto
      qed
    qed
  qed
  finally show ?thesis by blast
qed


text {* The next lemma and its corollary enable one to prove that 
a linear order is a well-order in a way which is more standard than 
via well-founded-ness of the strict version of the relation.  *}

(*3*)lemma Linear_order_wf_diff_Id: 
assumes LI: "Linear_order r"
shows "wf(r - Id) = (∀A ≤ Field r. A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r))"
proof(cases "r ≤ Id")
  assume Case1: "r ≤ Id" 
  hence temp: "r - Id = {}" by blast 
  hence "wf(r - Id)" by (auto simp add: temp)   (* did not work with "using temp"!  *)
  moreover 
  {fix A assume *: "A ≤ Field r" and **: "A ≠ {}"
   obtain a where 1: "r = {} ∨ r = {(a,a)}" using LI 
   unfolding order_on_defs using Case1 rel.Total_subset_Id by blast
   hence "A = {a} ∧ r = {(a,a)}" using * ** unfolding Field_def by blast
   hence "∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r" using 1 by auto
  }
  ultimately show ?thesis by blast
next
  assume Case2: "¬ r ≤ Id"
  hence 1: "Field r = Field(r - Id)" using rel.Total_Id_Field LI 
  unfolding order_on_defs by blast  
  show ?thesis 
  proof
    assume *: "wf(r - Id)"
    show "∀A ≤ Field r. A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r)" 
    proof(clarify)
      fix A assume **: "A ≤ Field r" and ***: "A ≠ {}"
      hence "∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r - Id" 
      using 1 * unfolding wf_eq_minimal2 by auto
      moreover have "∀a ∈ A. ∀a' ∈ A. ((a,a') ∈ r) = ((a',a) ∉ r - Id)"   
      using rel.Linear_order_in_diff_Id[of r] ** LI by blast
      ultimately show "∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r" by blast
    qed
  next 
    assume *: "∀A ≤ Field r. A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r)"
    show "wf(r - Id)"
    proof(unfold wf_eq_minimal2, clarify)
      fix A assume **: "A ≤ Field(r - Id)" and ***: "A ≠ {}"
      hence "∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r" 
      using 1 * by auto
      moreover have "∀a ∈ A. ∀a' ∈ A. ((a,a') ∈ r) = ((a',a) ∉ r - Id)"   
      using rel.Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
      ultimately show "∃a ∈ A. ∀a' ∈ A. (a',a) ∉ r - Id" by blast
    qed
  qed 
qed


(*3*)corollary Linear_order_Well_order_iff: 
assumes LI: "Linear_order r"
shows "Well_order r = (∀A ≤ Field r. A ≠ {} --> (∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r))"
using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by auto


end