author  haftmann 
Tue, 04 May 2010 08:55:43 +0200  
changeset 36635  080b755377c0 
parent 35828  46cfc4b8112e 
child 36664  6302f9ad7047 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

1 
(* Title: HOL/Wellfounded.thy 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

2 
Author: Tobias Nipkow 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

3 
Author: Lawrence C Paulson 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

4 
Author: Konrad Slind 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

5 
Author: Alexander Krauss 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

6 
*) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

7 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

8 
header {*Wellfounded Recursion*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

9 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

10 
theory Wellfounded 
35727  11 
imports Transitive_Closure 
31775  12 
uses ("Tools/Function/size.ML") 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

13 
begin 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

14 

26976  15 
subsection {* Basic Definitions *} 
16 

33217  17 
definition wf :: "('a * 'a) set => bool" where 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

18 
"wf(r) == (!P. (!x. (!y. (y,x):r > P(y)) > P(x)) > (!x. P(x)))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

19 

33217  20 
definition wfP :: "('a => 'a => bool) => bool" where 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

21 
"wfP r == wf {(x, y). r x y}" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

22 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

23 
lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

24 
by (simp add: wfP_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

25 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

26 
lemma wfUNIVI: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

27 
"(!!P x. (ALL x. (ALL y. (y,x) : r > P(y)) > P(x)) ==> P(x)) ==> wf(r)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

28 
unfolding wf_def by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

29 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

30 
lemmas wfPUNIVI = wfUNIVI [to_pred] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

31 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

32 
text{*Restriction to domain @{term A} and range @{term B}. If @{term r} is 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

33 
wellfounded over their intersection, then @{term "wf r"}*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

34 
lemma wfI: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

35 
"[ r \<subseteq> A <*> B; 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

36 
!!x P. [\<forall>x. (\<forall>y. (y,x) : r > P y) > P x; x : A; x : B ] ==> P x ] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

37 
==> wf r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

38 
unfolding wf_def by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

39 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

40 
lemma wf_induct: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

41 
"[ wf(r); 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

42 
!!x.[ ALL y. (y,x): r > P(y) ] ==> P(x) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

43 
] ==> P(a)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

44 
unfolding wf_def by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

45 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

46 
lemmas wfP_induct = wf_induct [to_pred] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

47 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

48 
lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

49 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

50 
lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

51 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

52 
lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

53 
by (induct a arbitrary: x set: wf) blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

54 

33215
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset

55 
lemma wf_asym: 
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset

56 
assumes "wf r" "(a, x) \<in> r" 
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset

57 
obtains "(x, a) \<notin> r" 
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset

58 
by (drule wf_not_sym[OF assms]) 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

59 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

60 
lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

61 
by (blast elim: wf_asym) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

62 

33215
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset

63 
lemma wf_irrefl: assumes "wf r" obtains "(a, a) \<notin> r" 
6fd85372981e
replaced (outdated) comments by explicit statements
krauss
parents:
32960
diff
changeset

64 
by (drule wf_not_refl[OF assms]) 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

65 

27823  66 
lemma wf_wellorderI: 
67 
assumes wf: "wf {(x::'a::ord, y). x < y}" 

68 
assumes lin: "OFCLASS('a::ord, linorder_class)" 

69 
shows "OFCLASS('a::ord, wellorder_class)" 

70 
using lin by (rule wellorder_class.intro) 

36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
35828
diff
changeset

71 
(blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf]) 
27823  72 

73 
lemma (in wellorder) wf: 

74 
"wf {(x, y). x < y}" 

75 
unfolding wf_def by (blast intro: less_induct) 

76 

77 

26976  78 
subsection {* Basic Results *} 
79 

33216  80 
text {* Pointfree characterization of wellfoundedness *} 
81 

82 
lemma wfE_pf: 

83 
assumes wf: "wf R" 

84 
assumes a: "A \<subseteq> R `` A" 

85 
shows "A = {}" 

86 
proof  

87 
{ fix x 

88 
from wf have "x \<notin> A" 

89 
proof induct 

90 
fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A" 

91 
then have "x \<notin> R `` A" by blast 

92 
with a show "x \<notin> A" by blast 

93 
qed 

94 
} thus ?thesis by auto 

95 
qed 

96 

97 
lemma wfI_pf: 

98 
assumes a: "\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}" 

99 
shows "wf R" 

100 
proof (rule wfUNIVI) 

101 
fix P :: "'a \<Rightarrow> bool" and x 

102 
let ?A = "{x. \<not> P x}" 

103 
assume "\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x" 

104 
then have "?A \<subseteq> R `` ?A" by blast 

105 
with a show "P x" by blast 

106 
qed 

107 

108 
text{*Minimalelement characterization of wellfoundedness*} 

109 

110 
lemma wfE_min: 

111 
assumes wf: "wf R" and Q: "x \<in> Q" 

112 
obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q" 

113 
using Q wfE_pf[OF wf, of Q] by blast 

114 

115 
lemma wfI_min: 

116 
assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q" 

117 
shows "wf R" 

118 
proof (rule wfI_pf) 

119 
fix A assume b: "A \<subseteq> R `` A" 

120 
{ fix x assume "x \<in> A" 

121 
from a[OF this] b have "False" by blast 

122 
} 

123 
thus "A = {}" by blast 

124 
qed 

125 

126 
lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q > (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r > y\<notin>Q))" 

127 
apply auto 

128 
apply (erule wfE_min, assumption, blast) 

129 
apply (rule wfI_min, auto) 

130 
done 

131 

132 
lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] 

133 

134 
text{* Wellfoundedness of transitive closure *} 

135 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

136 
lemma wf_trancl: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

137 
assumes "wf r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

138 
shows "wf (r^+)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

139 
proof  
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

140 
{ 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

141 
fix P and x 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

142 
assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

143 
have "P x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

144 
proof (rule induct_step) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

145 
fix y assume "(y, x) : r^+" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

146 
with `wf r` show "P y" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

147 
proof (induct x arbitrary: y) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

148 
case (less x) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

149 
note hyp = `\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'` 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

150 
from `(y, x) : r^+` show "P y" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

151 
proof cases 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

152 
case base 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

153 
show "P y" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

154 
proof (rule induct_step) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

155 
fix y' assume "(y', y) : r^+" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

156 
with `(y, x) : r` show "P y'" by (rule hyp [of y y']) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

157 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

158 
next 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

159 
case step 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

160 
then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

161 
then show "P y" by (rule hyp [of x' y]) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32704
diff
changeset

162 
qed 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

163 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

164 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

165 
} then show ?thesis unfolding wf_def by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

166 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

167 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

168 
lemmas wfP_trancl = wf_trancl [to_pred] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

169 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

170 
lemma wf_converse_trancl: "wf (r^1) ==> wf ((r^+)^1)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

171 
apply (subst trancl_converse [symmetric]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

172 
apply (erule wf_trancl) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

173 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

174 

33216  175 
text {* Wellfoundedness of subsets *} 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

176 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

177 
lemma wf_subset: "[ wf(r); p<=r ] ==> wf(p)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

178 
apply (simp (no_asm_use) add: wf_eq_minimal) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

179 
apply fast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

180 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

181 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

182 
lemmas wfP_subset = wf_subset [to_pred] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

183 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

184 
text {* Wellfoundedness of the empty relation *} 
33216  185 

186 
lemma wf_empty [iff]: "wf {}" 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

187 
by (simp add: wf_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

188 

32205  189 
lemma wfP_empty [iff]: 
190 
"wfP (\<lambda>x y. False)" 

191 
proof  

192 
have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2]) 

193 
then show ?thesis by (simp add: bot_fun_eq bot_bool_eq) 

194 
qed 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

195 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

196 
lemma wf_Int1: "wf r ==> wf (r Int r')" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

197 
apply (erule wf_subset) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

198 
apply (rule Int_lower1) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

199 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

200 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

201 
lemma wf_Int2: "wf r ==> wf (r' Int r)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

202 
apply (erule wf_subset) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

203 
apply (rule Int_lower2) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

204 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

205 

33216  206 
text {* Exponentiation *} 
207 

208 
lemma wf_exp: 

209 
assumes "wf (R ^^ n)" 

210 
shows "wf R" 

211 
proof (rule wfI_pf) 

212 
fix A assume "A \<subseteq> R `` A" 

213 
then have "A \<subseteq> (R ^^ n) `` A" by (induct n) force+ 

214 
with `wf (R ^^ n)` 

215 
show "A = {}" by (rule wfE_pf) 

216 
qed 

217 

218 
text {* Wellfoundedness of insert *} 

219 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

220 
lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

221 
apply (rule iffI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

222 
apply (blast elim: wf_trancl [THEN wf_irrefl] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

223 
intro: rtrancl_into_trancl1 wf_subset 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

224 
rtrancl_mono [THEN [2] rev_subsetD]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

225 
apply (simp add: wf_eq_minimal, safe) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

226 
apply (rule allE, assumption, erule impE, blast) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

227 
apply (erule bexE) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

228 
apply (rename_tac "a", case_tac "a = x") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

229 
prefer 2 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

230 
apply blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

231 
apply (case_tac "y:Q") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

232 
prefer 2 apply blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

233 
apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

234 
apply assumption 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

235 
apply (erule_tac V = "ALL Q. (EX x. x : Q) > ?P Q" in thin_rl) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

236 
{*essential for speed*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

237 
txt{*Blast with new substOccur fails*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

238 
apply (fast intro: converse_rtrancl_into_rtrancl) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

239 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

240 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

241 
text{*Wellfoundedness of image*} 
33216  242 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

243 
lemma wf_prod_fun_image: "[ wf r; inj f ] ==> wf(prod_fun f f ` r)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

244 
apply (simp only: wf_eq_minimal, clarify) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

245 
apply (case_tac "EX p. f p : Q") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

246 
apply (erule_tac x = "{p. f p : Q}" in allE) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

247 
apply (fast dest: inj_onD, blast) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

248 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

249 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

250 

26976  251 
subsection {* WellFoundedness Results for Unions *} 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

252 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

253 
lemma wf_union_compatible: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

254 
assumes "wf R" "wf S" 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
32205
diff
changeset

255 
assumes "R O S \<subseteq> R" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

256 
shows "wf (R \<union> S)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

257 
proof (rule wfI_min) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

258 
fix x :: 'a and Q 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

259 
let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

260 
assume "x \<in> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

261 
obtain a where "a \<in> ?Q'" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

262 
by (rule wfE_min [OF `wf R` `x \<in> Q`]) blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

263 
with `wf S` 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

264 
obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

265 
{ 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

266 
fix y assume "(y, z) \<in> S" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

267 
then have "y \<notin> ?Q'" by (rule zmin) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

268 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

269 
have "y \<notin> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

270 
proof 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

271 
assume "y \<in> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

272 
with `y \<notin> ?Q'` 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

273 
obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
32205
diff
changeset

274 
from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule rel_compI) 
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
32205
diff
changeset

275 
with `R O S \<subseteq> R` have "(w, z) \<in> R" .. 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

276 
with `z \<in> ?Q'` have "w \<notin> Q" by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

277 
with `w \<in> Q` show False by contradiction 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

278 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

279 
} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

280 
with `z \<in> ?Q'` show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

281 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

282 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

283 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

284 
text {* Wellfoundedness of indexed union with disjoint domains and ranges *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

285 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

286 
lemma wf_UN: "[ ALL i:I. wf(r i); 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

287 
ALL i:I. ALL j:I. r i ~= r j > Domain(r i) Int Range(r j) = {} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

288 
] ==> wf(UN i:I. r i)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

289 
apply (simp only: wf_eq_minimal, clarify) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

290 
apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

291 
prefer 2 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

292 
apply force 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

293 
apply clarify 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

294 
apply (drule bspec, assumption) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

295 
apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

296 
apply (blast elim!: allE) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

297 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

298 

32263  299 
lemma wfP_SUP: 
300 
"\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)" 

32704  301 
by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2]) 
302 
(simp_all add: Collect_def) 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

303 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

304 
lemma wf_Union: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

305 
"[ ALL r:R. wf r; 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

306 
ALL r:R. ALL s:R. r ~= s > Domain r Int Range s = {} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

307 
] ==> wf(Union R)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

308 
apply (simp add: Union_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

309 
apply (blast intro: wf_UN) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

310 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

311 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

312 
(*Intuition: we find an (R u S)min element of a nonempty subset A 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

313 
by case distinction. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

314 
1. There is a step a R> b with a,b : A. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

315 
Pick an Rmin element z of the (nonempty) set {a:A  EX b:A. a R> b}. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

316 
By definition, there is z':A s.t. z R> z'. Because z is Rmin in the 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

317 
subset, z' must be Rmin in A. Because z' has an Rpredecessor, it cannot 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

318 
have an Ssuccessor and is thus Smin in A as well. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

319 
2. There is no such step. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

320 
Pick an Smin element of A. In this case it must be an Rmin 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

321 
element of A as well. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

322 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

323 
*) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

324 
lemma wf_Un: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

325 
"[ wf r; wf s; Domain r Int Range s = {} ] ==> wf(r Un s)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

326 
using wf_union_compatible[of s r] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

327 
by (auto simp: Un_ac) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

328 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

329 
lemma wf_union_merge: 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
32205
diff
changeset

330 
"wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" (is "wf ?A = wf ?B") 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

331 
proof 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

332 
assume "wf ?A" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

333 
with wf_trancl have wfT: "wf (?A^+)" . 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

334 
moreover have "?B \<subseteq> ?A^+" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

335 
by (subst trancl_unfold, subst trancl_unfold) blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

336 
ultimately show "wf ?B" by (rule wf_subset) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

337 
next 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

338 
assume "wf ?B" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

339 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

340 
show "wf ?A" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

341 
proof (rule wfI_min) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

342 
fix Q :: "'a set" and x 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

343 
assume "x \<in> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

344 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

345 
with `wf ?B` 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

346 
obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

347 
by (erule wfE_min) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

348 
then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
32205
diff
changeset

349 
and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

350 
and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

351 
by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

352 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

353 
show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

354 
proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

355 
case True 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

356 
with `z \<in> Q` A3 show ?thesis by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

357 
next 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

358 
case False 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

359 
then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

360 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

361 
have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

362 
proof (intro allI impI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

363 
fix y assume "(y, z') \<in> ?A" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

364 
then show "y \<notin> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

365 
proof 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

366 
assume "(y, z') \<in> R" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

367 
then have "(y, z) \<in> R O R" using `(z', z) \<in> R` .. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

368 
with A1 show "y \<notin> Q" . 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

369 
next 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

370 
assume "(y, z') \<in> S" 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
32205
diff
changeset

371 
then have "(y, z) \<in> S O R" using `(z', z) \<in> R` .. 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

372 
with A2 show "y \<notin> Q" . 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

373 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

374 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

375 
with `z' \<in> Q` show ?thesis .. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

376 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

377 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

378 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

379 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

380 
lemma wf_comp_self: "wf R = wf (R O R)"  {* special case *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

381 
by (rule wf_union_merge [where S = "{}", simplified]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

382 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

383 

33217  384 
subsection {* Acyclic relations *} 
385 

386 
definition acyclic :: "('a * 'a) set => bool" where 

387 
"acyclic r == !x. (x,x) ~: r^+" 

388 

389 
abbreviation acyclicP :: "('a => 'a => bool) => bool" where 

390 
"acyclicP r == acyclic {(x, y). r x y}" 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

391 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

392 
lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

393 
by (simp add: acyclic_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

394 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

395 
lemma wf_acyclic: "wf r ==> acyclic r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

396 
apply (simp add: acyclic_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

397 
apply (blast elim: wf_trancl [THEN wf_irrefl]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

398 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

399 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

400 
lemmas wfP_acyclicP = wf_acyclic [to_pred] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

401 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

402 
lemma acyclic_insert [iff]: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

403 
"acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

404 
apply (simp add: acyclic_def trancl_insert) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

405 
apply (blast intro: rtrancl_trans) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

406 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

407 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

408 
lemma acyclic_converse [iff]: "acyclic(r^1) = acyclic r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

409 
by (simp add: acyclic_def trancl_converse) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

410 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

411 
lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

412 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

413 
lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

414 
apply (simp add: acyclic_def antisym_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

415 
apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

416 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

417 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

418 
(* Other direction: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

419 
acyclic = no loops 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

420 
antisym = only self loops 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

421 
Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r  Id) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

422 
==> antisym( r^* ) = acyclic(r  Id)"; 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

423 
*) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

424 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

425 
lemma acyclic_subset: "[ acyclic s; r <= s ] ==> acyclic r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

426 
apply (simp add: acyclic_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

427 
apply (blast intro: trancl_mono) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

428 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

429 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

430 
text{* Wellfoundedness of finite acyclic relations*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

431 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

432 
lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r > wf r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

433 
apply (erule finite_induct, blast) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

434 
apply (simp (no_asm_simp) only: split_tupled_all) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

435 
apply simp 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

436 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

437 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

438 
lemma finite_acyclic_wf_converse: "[finite r; acyclic r] ==> wf (r^1)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

439 
apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

440 
apply (erule acyclic_converse [THEN iffD2]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

441 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

442 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

443 
lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

444 
by (blast intro: finite_acyclic_wf wf_acyclic) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

445 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

446 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

447 
subsection {* @{typ nat} is wellfounded *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

448 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

449 
lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

450 
proof (rule ext, rule ext, rule iffI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

451 
fix n m :: nat 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

452 
assume "m < n" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

453 
then show "(\<lambda>m n. n = Suc m)^++ m n" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

454 
proof (induct n) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

455 
case 0 then show ?case by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

456 
next 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

457 
case (Suc n) then show ?case 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

458 
by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

459 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

460 
next 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

461 
fix n m :: nat 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

462 
assume "(\<lambda>m n. n = Suc m)^++ m n" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

463 
then show "m < n" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

464 
by (induct n) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

465 
(simp_all add: less_Suc_eq_le reflexive le_less) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

466 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

467 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

468 
definition 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

469 
pred_nat :: "(nat * nat) set" where 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

470 
"pred_nat = {(m, n). n = Suc m}" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

471 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

472 
definition 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

473 
less_than :: "(nat * nat) set" where 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

474 
"less_than = pred_nat^+" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

475 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

476 
lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

477 
unfolding less_nat_rel pred_nat_def trancl_def by simp 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

478 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

479 
lemma pred_nat_trancl_eq_le: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

480 
"(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

481 
unfolding less_eq rtrancl_eq_or_trancl by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

482 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

483 
lemma wf_pred_nat: "wf pred_nat" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

484 
apply (unfold wf_def pred_nat_def, clarify) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

485 
apply (induct_tac x, blast+) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

486 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

487 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

488 
lemma wf_less_than [iff]: "wf less_than" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

489 
by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

490 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

491 
lemma trans_less_than [iff]: "trans less_than" 
35216  492 
by (simp add: less_than_def) 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

493 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

494 
lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

495 
by (simp add: less_than_def less_eq) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

496 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

497 
lemma wf_less: "wf {(x, y::nat). x < y}" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

498 
using wf_less_than by (simp add: less_than_def less_eq [symmetric]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

499 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

500 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

501 
subsection {* Accessible Part *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

502 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

503 
text {* 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

504 
Inductive definition of the accessible part @{term "acc r"} of a 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

505 
relation; see also \cite{paulintlca}. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

506 
*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

507 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

508 
inductive_set 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

509 
acc :: "('a * 'a) set => 'a set" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

510 
for r :: "('a * 'a) set" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

511 
where 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

512 
accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

513 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

514 
abbreviation 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

515 
termip :: "('a => 'a => bool) => 'a => bool" where 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

516 
"termip r == accp (r\<inverse>\<inverse>)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

517 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

518 
abbreviation 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

519 
termi :: "('a * 'a) set => 'a set" where 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

520 
"termi r == acc (r\<inverse>)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

521 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

522 
lemmas accpI = accp.accI 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

523 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

524 
text {* Induction rules *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

525 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

526 
theorem accp_induct: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

527 
assumes major: "accp r a" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

528 
assumes hyp: "!!x. accp r x ==> \<forall>y. r y x > P y ==> P x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

529 
shows "P a" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

530 
apply (rule major [THEN accp.induct]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

531 
apply (rule hyp) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

532 
apply (rule accp.accI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

533 
apply fast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

534 
apply fast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

535 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

536 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

537 
theorems accp_induct_rule = accp_induct [rule_format, induct set: accp] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

538 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

539 
theorem accp_downward: "accp r b ==> r a b ==> accp r a" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

540 
apply (erule accp.cases) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

541 
apply fast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

542 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

543 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

544 
lemma not_accp_down: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

545 
assumes na: "\<not> accp R x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

546 
obtains z where "R z x" and "\<not> accp R z" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

547 
proof  
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

548 
assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

549 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

550 
show thesis 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

551 
proof (cases "\<forall>z. R z x \<longrightarrow> accp R z") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

552 
case True 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

553 
hence "\<And>z. R z x \<Longrightarrow> accp R z" by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

554 
hence "accp R x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

555 
by (rule accp.accI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

556 
with na show thesis .. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

557 
next 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

558 
case False then obtain z where "R z x" and "\<not> accp R z" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

559 
by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

560 
with a show thesis . 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

561 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

562 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

563 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

564 
lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a > accp r b" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

565 
apply (erule rtranclp_induct) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

566 
apply blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

567 
apply (blast dest: accp_downward) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

568 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

569 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

570 
theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

571 
apply (blast dest: accp_downwards_aux) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

572 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

573 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

574 
theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

575 
apply (rule wfPUNIVI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

576 
apply (induct_tac P x rule: accp_induct) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

577 
apply blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

578 
apply blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

579 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

580 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

581 
theorem accp_wfPD: "wfP r ==> accp r x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

582 
apply (erule wfP_induct_rule) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

583 
apply (rule accp.accI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

584 
apply blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

585 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

586 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

587 
theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

588 
apply (blast intro: accp_wfPI dest: accp_wfPD) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

589 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

590 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

591 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

592 
text {* Smaller relations have bigger accessible parts: *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

593 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

594 
lemma accp_subset: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

595 
assumes sub: "R1 \<le> R2" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

596 
shows "accp R2 \<le> accp R1" 
26803
0af0f674845d
 Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
berghofe
parents:
26748
diff
changeset

597 
proof (rule predicate1I) 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

598 
fix x assume "accp R2 x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

599 
then show "accp R1 x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

600 
proof (induct x) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

601 
fix x 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

602 
assume ih: "\<And>y. R2 y x \<Longrightarrow> accp R1 y" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

603 
with sub show "accp R1 x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

604 
by (blast intro: accp.accI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

605 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

606 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

607 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

608 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

609 
text {* This is a generalized induction theorem that works on 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

610 
subsets of the accessible part. *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

611 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

612 
lemma accp_subset_induct: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

613 
assumes subset: "D \<le> accp R" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

614 
and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

615 
and "D x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

616 
and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

617 
shows "P x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

618 
proof  
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

619 
from subset and `D x` 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

620 
have "accp R x" .. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

621 
then show "P x" using `D x` 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

622 
proof (induct x) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

623 
fix x 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

624 
assume "D x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

625 
and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

626 
with dcl and istep show "P x" by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

627 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

628 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

629 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

630 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

631 
text {* Set versions of the above theorems *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

632 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

633 
lemmas acc_induct = accp_induct [to_set] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

634 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

635 
lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

636 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

637 
lemmas acc_downward = accp_downward [to_set] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

638 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

639 
lemmas not_acc_down = not_accp_down [to_set] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

640 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

641 
lemmas acc_downwards_aux = accp_downwards_aux [to_set] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

642 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

643 
lemmas acc_downwards = accp_downwards [to_set] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

644 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

645 
lemmas acc_wfI = accp_wfPI [to_set] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

646 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

647 
lemmas acc_wfD = accp_wfPD [to_set] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

648 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

649 
lemmas wf_acc_iff = wfP_accp_iff [to_set] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

650 

26803
0af0f674845d
 Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
berghofe
parents:
26748
diff
changeset

651 
lemmas acc_subset = accp_subset [to_set pred_subset_eq] 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

652 

26803
0af0f674845d
 Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
berghofe
parents:
26748
diff
changeset

653 
lemmas acc_subset_induct = accp_subset_induct [to_set pred_subset_eq] 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

654 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

655 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

656 
subsection {* Tools for building wellfounded relations *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

657 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

658 
text {* Inverse Image *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

659 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

660 
lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

661 
apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

662 
apply clarify 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

663 
apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

664 
prefer 2 apply (blast del: allE) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

665 
apply (erule allE) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

666 
apply (erule (1) notE impE) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

667 
apply blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

668 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

669 

31775  670 
text {* Measure Datatypes into @{typ nat} *} 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

671 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

672 
definition measure :: "('a => nat) => ('a * 'a)set" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

673 
where "measure == inv_image less_than" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

674 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

675 
lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

676 
by (simp add:measure_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

677 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

678 
lemma wf_measure [iff]: "wf (measure f)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

679 
apply (unfold measure_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

680 
apply (rule wf_less_than [THEN wf_inv_image]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

681 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

682 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

683 
text{* Lexicographic combinations *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

684 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

685 
definition 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

686 
lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

687 
(infixr "<*lex*>" 80) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

688 
where 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

689 
"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra  a=a' & (b,b') : rb}" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

690 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

691 
lemma wf_lex_prod [intro!]: "[ wf(ra); wf(rb) ] ==> wf(ra <*lex*> rb)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

692 
apply (unfold wf_def lex_prod_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

693 
apply (rule allI, rule impI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

694 
apply (simp (no_asm_use) only: split_paired_All) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

695 
apply (drule spec, erule mp) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

696 
apply (rule allI, rule impI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

697 
apply (drule spec, erule mp, blast) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

698 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

699 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

700 
lemma in_lex_prod[simp]: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

701 
"(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

702 
by (auto simp:lex_prod_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

703 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

704 
text{* @{term "op <*lex*>"} preserves transitivity *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

705 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

706 
lemma trans_lex_prod [intro!]: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

707 
"[ trans R1; trans R2 ] ==> trans (R1 <*lex*> R2)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

708 
by (unfold trans_def lex_prod_def, blast) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

709 

31775  710 
text {* lexicographic combinations with measure Datatypes *} 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

711 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

712 
definition 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

713 
mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

714 
where 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

715 
"f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

716 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

717 
lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

718 
unfolding mlex_prod_def 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

719 
by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

720 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

721 
lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

722 
unfolding mlex_prod_def by simp 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

723 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

724 
lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

725 
unfolding mlex_prod_def by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

726 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

727 
text {* proper subset relation on finite sets *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

728 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

729 
definition finite_psubset :: "('a set * 'a set) set" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

730 
where "finite_psubset == {(A,B). A < B & finite B}" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

731 

28260  732 
lemma wf_finite_psubset[simp]: "wf(finite_psubset)" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

733 
apply (unfold finite_psubset_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

734 
apply (rule wf_measure [THEN wf_subset]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

735 
apply (simp add: measure_def inv_image_def less_than_def less_eq) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

736 
apply (fast elim!: psubset_card_mono) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

737 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

738 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

739 
lemma trans_finite_psubset: "trans finite_psubset" 
26803
0af0f674845d
 Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
berghofe
parents:
26748
diff
changeset

740 
by (simp add: finite_psubset_def less_le trans_def, blast) 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

741 

28260  742 
lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset = (A < B & finite B)" 
743 
unfolding finite_psubset_def by auto 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

744 

28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

745 
text {* max and minextension of order to finite sets *} 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

746 

bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

747 
inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

748 
for R :: "('a \<times> 'a) set" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

749 
where 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

750 
max_extI[intro]: "finite X \<Longrightarrow> finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> R) \<Longrightarrow> (X, Y) \<in> max_ext R" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

751 

bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

752 
lemma max_ext_wf: 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

753 
assumes wf: "wf r" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

754 
shows "wf (max_ext r)" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

755 
proof (rule acc_wfI, intro allI) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

756 
fix M show "M \<in> acc (max_ext r)" (is "_ \<in> ?W") 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

757 
proof cases 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

758 
assume "finite M" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

759 
thus ?thesis 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

760 
proof (induct M) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

761 
show "{} \<in> ?W" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

762 
by (rule accI) (auto elim: max_ext.cases) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

763 
next 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

764 
fix M a assume "M \<in> ?W" "finite M" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

765 
with wf show "insert a M \<in> ?W" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

766 
proof (induct arbitrary: M) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

767 
fix M a 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

768 
assume "M \<in> ?W" and [intro]: "finite M" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

769 
assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

770 
{ 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

771 
fix N M :: "'a set" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

772 
assume "finite N" "finite M" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

773 
then 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

774 
have "\<lbrakk>M \<in> ?W ; (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r)\<rbrakk> \<Longrightarrow> N \<union> M \<in> ?W" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

775 
by (induct N arbitrary: M) (auto simp: hyp) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

776 
} 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

777 
note add_less = this 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

778 

bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

779 
show "insert a M \<in> ?W" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

780 
proof (rule accI) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

781 
fix N assume Nless: "(N, insert a M) \<in> max_ext r" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

782 
hence asm1: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

783 
by (auto elim!: max_ext.cases) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

784 

bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

785 
let ?N1 = "{ n \<in> N. (n, a) \<in> r }" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

786 
let ?N2 = "{ n \<in> N. (n, a) \<notin> r }" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

787 
have N: "?N1 \<union> ?N2 = N" by (rule set_ext) auto 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

788 
from Nless have "finite N" by (auto elim: max_ext.cases) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

789 
then have finites: "finite ?N1" "finite ?N2" by auto 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

790 

bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

791 
have "?N2 \<in> ?W" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

792 
proof cases 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

793 
assume [simp]: "M = {}" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

794 
have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

795 

bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

796 
from asm1 have "?N2 = {}" by auto 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

797 
with Mw show "?N2 \<in> ?W" by (simp only:) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

798 
next 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

799 
assume "M \<noteq> {}" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

800 
have N2: "(?N2, M) \<in> max_ext r" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

801 
by (rule max_extI[OF _ _ `M \<noteq> {}`]) (insert asm1, auto intro: finites) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

802 

bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

803 
with `M \<in> ?W` show "?N2 \<in> ?W" by (rule acc_downward) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

804 
qed 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

805 
with finites have "?N1 \<union> ?N2 \<in> ?W" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

806 
by (rule add_less) simp 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

807 
then show "N \<in> ?W" by (simp only: N) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

808 
qed 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

809 
qed 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

810 
qed 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

811 
next 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

812 
assume [simp]: "\<not> finite M" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

813 
show ?thesis 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

814 
by (rule accI) (auto elim: max_ext.cases) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

815 
qed 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

816 
qed 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

817 

29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
28845
diff
changeset

818 
lemma max_ext_additive: 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
28845
diff
changeset

819 
"(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow> 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
28845
diff
changeset

820 
(A \<union> C, B \<union> D) \<in> max_ext R" 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
28845
diff
changeset

821 
by (force elim!: max_ext.cases) 
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
28845
diff
changeset

822 

28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

823 

bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

824 
definition 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

825 
min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

826 
where 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

827 
[code del]: "min_ext r = {(X, Y)  X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

828 

bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

829 
lemma min_ext_wf: 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

830 
assumes "wf r" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

831 
shows "wf (min_ext r)" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

832 
proof (rule wfI_min) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

833 
fix Q :: "'a set set" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

834 
fix x 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

835 
assume nonempty: "x \<in> Q" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

836 
show "\<exists>m \<in> Q. (\<forall> n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

837 
proof cases 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

838 
assume "Q = {{}}" thus ?thesis by (simp add: min_ext_def) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

839 
next 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

840 
assume "Q \<noteq> {{}}" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

841 
with nonempty 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

842 
obtain e x where "x \<in> Q" "e \<in> x" by force 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

843 
then have eU: "e \<in> \<Union>Q" by auto 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

844 
with `wf r` 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

845 
obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

846 
by (erule wfE_min) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

847 
from z obtain m where "m \<in> Q" "z \<in> m" by auto 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

848 
from `m \<in> Q` 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

849 
show ?thesis 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

850 
proof (rule, intro bexI allI impI) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

851 
fix n 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

852 
assume smaller: "(n, m) \<in> min_ext r" 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

853 
with `z \<in> m` obtain y where y: "y \<in> n" "(y, z) \<in> r" by (auto simp: min_ext_def) 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

854 
then show "n \<notin> Q" using z(2) by auto 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

855 
qed 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

856 
qed 
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

857 
qed 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

858 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

859 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

860 
subsection{*Weakly decreasing sequences (w.r.t. some wellfounded order) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

861 
stabilize.*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

862 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

863 
text{*This material does not appear to be used any longer.*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

864 

28845  865 
lemma sequence_trans: "[ ALL i. (f (Suc i), f i) : r^* ] ==> (f (i+k), f i) : r^*" 
866 
by (induct k) (auto intro: rtrancl_trans) 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

867 

28845  868 
lemma wf_weak_decr_stable: 
869 
assumes as: "ALL i. (f (Suc i), f i) : r^*" "wf (r^+)" 

870 
shows "EX i. ALL k. f (i+k) = f i" 

871 
proof  

872 
have lem: "!!x. [ ALL i. (f (Suc i), f i) : r^*; wf (r^+) ] 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

873 
==> ALL m. f m = x > (EX i. ALL k. f (m+i+k) = f (m+i))" 
28845  874 
apply (erule wf_induct, clarify) 
875 
apply (case_tac "EX j. (f (m+j), f m) : r^+") 

876 
apply clarify 

877 
apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ") 

878 
apply clarify 

879 
apply (rule_tac x = "j+i" in exI) 

880 
apply (simp add: add_ac, blast) 

881 
apply (rule_tac x = 0 in exI, clarsimp) 

882 
apply (drule_tac i = m and k = k in sequence_trans) 

883 
apply (blast elim: rtranclE dest: rtrancl_into_trancl1) 

884 
done 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

885 

28845  886 
from lem[OF as, THEN spec, of 0, simplified] 
887 
show ?thesis by auto 

888 
qed 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

889 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

890 
(* special case of the theorem above: <= *) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

891 
lemma weak_decr_stable: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

892 
"ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

893 
apply (rule_tac r = pred_nat in wf_weak_decr_stable) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

894 
apply (simp add: pred_nat_trancl_eq_le) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

895 
apply (intro wf_trancl wf_pred_nat) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

896 
done 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

897 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

898 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

899 
subsection {* size of a datatype value *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

900 

31775  901 
use "Tools/Function/size.ML" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

902 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

903 
setup Size.setup 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

904 

28562  905 
lemma size_bool [code]: 
27823  906 
"size (b\<Colon>bool) = 0" by (cases b) auto 
907 

28562  908 
lemma nat_size [simp, code]: "size (n\<Colon>nat) = n" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

909 
by (induct n) simp_all 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

910 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35727
diff
changeset

911 
declare "prod.size" [no_atp] 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

912 

30430
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
29609
diff
changeset

913 
lemma [code]: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
29609
diff
changeset

914 
"size (P :: 'a Predicate.pred) = 0" by (cases P) simp 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
29609
diff
changeset

915 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
29609
diff
changeset

916 
lemma [code]: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
29609
diff
changeset

917 
"pred_size f P = 0" by (cases P) simp 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
29609
diff
changeset

918 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

919 
end 