summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

5 More on well-founded relations (FP).

6 *)

8 header {* More on Well-Founded Relations (FP) *}

10 theory Wellfounded_More_FP

11 imports Wfrec Order_Relation_More_FP

12 begin

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

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

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

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

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. *}

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

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. *}

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

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

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. *}

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

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

194 end