src/HOL/Cardinals/Wellfounded_More_FP.thy
author blanchet
Thu Jan 16 16:20:17 2014 +0100 (2014-01-16)
changeset 55017 2df6ad1dbd66
parent 54481 5c9819d7713b
child 55023 38db7814481d
permissions -rw-r--r--
adapted to move of Wfrec
     1 (*  Title:      HOL/Cardinals/Wellfounded_More_FP.thy
     2     Author:     Andrei Popescu, TU Muenchen
     3     Copyright   2012
     4 
     5 More on well-founded relations (FP).
     6 *)
     7 
     8 header {* More on Well-Founded Relations (FP) *}
     9 
    10 theory Wellfounded_More_FP
    11 imports Wfrec Order_Relation_More_FP
    12 begin
    13 
    14 
    15 text {* This section contains some variations of results in the theory
    16 @{text "Wellfounded.thy"}:
    17 \begin{itemize}
    18 \item means for slightly more direct definitions by well-founded recursion;
    19 \item variations of well-founded induction;
    20 \item means for proving a linear order to be a well-order.
    21 \end{itemize} *}
    22 
    23 
    24 subsection {* Well-founded recursion via genuine fixpoints *}
    25 
    26 
    27 (*2*)lemma wfrec_fixpoint:
    28 fixes r :: "('a * 'a) set" and
    29       H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    30 assumes WF: "wf r" and ADM: "adm_wf r H"
    31 shows "wfrec r H = H (wfrec r H)"
    32 proof(rule ext)
    33   fix x
    34   have "wfrec r H x = H (cut (wfrec r H) r x) x"
    35   using wfrec[of r H] WF by simp
    36   also
    37   {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y"
    38    by (auto simp add: cut_apply)
    39    hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
    40    using ADM adm_wf_def[of r H] by auto
    41   }
    42   finally show "wfrec r H x = H (wfrec r H) x" .
    43 qed
    44 
    45 
    46 
    47 subsection {* Characterizations of well-founded-ness *}
    48 
    49 
    50 text {* A transitive relation is well-founded iff it is ``locally" well-founded,
    51 i.e., iff its restriction to the lower bounds of of any element is well-founded.  *}
    52 
    53 (*3*)lemma trans_wf_iff:
    54 assumes "trans r"
    55 shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
    56 proof-
    57   obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
    58   {assume *: "wf r"
    59    {fix a
    60     have "wf(R a)"
    61     using * R_def wf_subset[of r "R a"] by auto
    62    }
    63   }
    64   (*  *)
    65   moreover
    66   {assume *: "\<forall>a. wf(R a)"
    67    have "wf r"
    68    proof(unfold wf_def, clarify)
    69      fix phi a
    70      assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
    71      obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
    72      with * have "wf (R a)" by auto
    73      hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
    74      unfolding wf_def by blast
    75      moreover
    76      have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
    77      proof(auto simp add: chi_def R_def)
    78        fix b
    79        assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
    80        hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
    81        using assms trans_def[of r] by blast
    82        thus "phi b" using ** by blast
    83      qed
    84      ultimately have  "\<forall>b. chi b" by (rule mp)
    85      with ** chi_def show "phi a" by blast
    86    qed
    87   }
    88   ultimately show ?thesis using R_def by blast
    89 qed
    90 
    91 
    92 text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,
    93 allowing one to assume the set included in the field.  *}
    94 
    95 (*2*)lemma wf_eq_minimal2:
    96 "wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))"
    97 proof-
    98   let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
    99   have "wf r = (\<forall>A. ?phi A)"
   100   by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
   101      (rule wfI_min, fast)
   102   (*  *)
   103   also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
   104   proof
   105     assume "\<forall>A. ?phi A"
   106     thus "\<forall>B \<le> Field r. ?phi B" by simp
   107   next
   108     assume *: "\<forall>B \<le> Field r. ?phi B"
   109     show "\<forall>A. ?phi A"
   110     proof(clarify)
   111       fix A::"'a set" assume **: "A \<noteq> {}"
   112       obtain B where B_def: "B = A Int (Field r)" by blast
   113       show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
   114       proof(cases "B = {}")
   115         assume Case1: "B = {}"
   116         obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
   117         using ** Case1 unfolding B_def by blast
   118         hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
   119         thus ?thesis using 1 by blast
   120       next
   121         assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
   122         obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
   123         using Case2 1 * by blast
   124         have "\<forall>a' \<in> A. (a',a) \<notin> r"
   125         proof(clarify)
   126           fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
   127           hence "a' \<in> B" unfolding B_def Field_def by blast
   128           thus False using 2 ** by blast
   129         qed
   130         thus ?thesis using 2 unfolding B_def by blast
   131       qed
   132     qed
   133   qed
   134   finally show ?thesis by blast
   135 qed
   136 
   137 subsection {* Characterizations of well-founded-ness *}
   138 
   139 text {* The next lemma and its corollary enable one to prove that
   140 a linear order is a well-order in a way which is more standard than
   141 via well-founded-ness of the strict version of the relation.  *}
   142 
   143 (*3*)
   144 lemma Linear_order_wf_diff_Id:
   145 assumes LI: "Linear_order r"
   146 shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
   147 proof(cases "r \<le> Id")
   148   assume Case1: "r \<le> Id"
   149   hence temp: "r - Id = {}" by blast
   150   hence "wf(r - Id)" by (simp add: temp)
   151   moreover
   152   {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
   153    obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
   154    unfolding order_on_defs using Case1 rel.Total_subset_Id by auto
   155    hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
   156    hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
   157   }
   158   ultimately show ?thesis by blast
   159 next
   160   assume Case2: "\<not> r \<le> Id"
   161   hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
   162   unfolding order_on_defs by blast
   163   show ?thesis
   164   proof
   165     assume *: "wf(r - Id)"
   166     show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   167     proof(clarify)
   168       fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
   169       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   170       using 1 * unfolding wf_eq_minimal2 by simp
   171       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   172       using rel.Linear_order_in_diff_Id[of r] ** LI by blast
   173       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
   174     qed
   175   next
   176     assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   177     show "wf(r - Id)"
   178     proof(unfold wf_eq_minimal2, clarify)
   179       fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
   180       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
   181       using 1 * by simp
   182       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   183       using rel.Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
   184       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
   185     qed
   186   qed
   187 qed
   188 
   189 (*3*)corollary Linear_order_Well_order_iff:
   190 assumes "Linear_order r"
   191 shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
   192 using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
   193 
   194 end