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