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--
     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