author  krauss 
Tue, 18 Nov 2008 21:17:14 +0100  
changeset 28845  cdfc8ef54a99 
parent 28735  bed31381e6b6 
child 29125  d41182a8135c 
permissions  rwrr 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

1 
(* ID: $Id$ 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

4 
Author: Konrad Slind, Alexander Krauss 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

5 
Copyright 19922008 University of Cambridge and TU Muenchen 
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 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

12 
uses ("Tools/function_package/size.ML") 
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 

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

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

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

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

20 
and F :: "('a => 'b) => 'a => 'b" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

22 
wfrecI: "ALL z. (z, x) : R > wfrec_rel R F z (g z) ==> 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

23 
wfrec_rel R F x (F g x)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

24 

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

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

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

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

28 

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

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

30 
"wfP r == wf {(x, y). r x y}" 
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 
acyclic :: "('a*'a)set => bool" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

33 
"acyclic r == !x. (x,x) ~: r^+" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

34 

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

35 
cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" 
28524  36 
"cut f r x == (%y. if (y,x):r then f y else undefined)" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

37 

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

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

39 
"adm_wf R F == ALL f g x. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

40 
(ALL z. (z, x) : R > f z = g z) > F f x = F g x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

41 

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

42 
wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" 
28562  43 
[code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

44 

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

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

46 
"acyclicP r == acyclic {(x, y). r x y}" 
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 
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

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

50 

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

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

52 
"(!!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

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

54 

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

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

56 

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

57 
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

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

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

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

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

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

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

64 

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

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

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

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

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

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

70 

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

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

72 

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

73 
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

74 

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

75 
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

76 

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

77 
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

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

79 

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

80 
(* [ wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z ] ==> Z *) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

81 
lemmas wf_asym = wf_not_sym [elim_format] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

82 

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

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

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

85 

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

86 
(* [ wf r; (a,a) ~: r ==> PROP W ] ==> PROP W *) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

87 
lemmas wf_irrefl = wf_not_refl [elim_format] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

88 

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

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

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

93 
using lin by (rule wellorder_class.intro) 

94 
(blast intro: wellorder_axioms.intro wf_induct_rule [OF wf]) 

95 

96 
lemma (in wellorder) wf: 

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

98 
unfolding wf_def by (blast intro: less_induct) 

99 

100 

26976  101 
subsection {* Basic Results *} 
102 

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

103 
text{*transitive closure of a wellfounded relation is wellfounded! *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

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

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

110 
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

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

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

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

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

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

116 
case (less x) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

117 
note hyp = `\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'` 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

118 
from `(y, x) : r^+` show "P y" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

121 
show "P y" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

124 
with `(y, x) : r` show "P y'" by (rule hyp [of y y']) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

128 
then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

129 
then show "P y" by (rule hyp [of x' y]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

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

135 

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

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

137 

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

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

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

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

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

142 

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

143 

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

144 
text{*Minimalelement characterization of wellfoundedness*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

145 
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))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

146 
proof (intro iffI strip) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

151 
by (blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

153 
assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

156 
fix P :: "'a \<Rightarrow> bool" and x 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

157 
assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

158 
let ?Q = "{x. \<not> P x}" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

160 
by (rule 1 [THEN spec, THEN spec]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

161 
then have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

162 
with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

163 
then show "P x" by simp 
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 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

166 

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

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

168 
assumes "wf R" "x \<in> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

169 
obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

170 
using assms unfolding wf_eq_minimal by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

171 

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

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

173 
"(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

174 
\<Longrightarrow> wf R" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

175 
unfolding wf_eq_minimal by blast 
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 
lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

178 

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

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

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

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

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

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

184 

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

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

186 

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

187 
text {* Wellfoundedness of the empty relation *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

188 
lemma wf_empty [iff]: "wf({})" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

190 

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

191 
lemmas wfP_empty [iff] = 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

192 
wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

193 

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

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

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

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

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

198 

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

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

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

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

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

203 

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

204 
text{*Wellfoundedness of insert*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

205 
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

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

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

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

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

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

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

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

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

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

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

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

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

218 
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

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

220 
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

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

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

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

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

225 

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

226 
text{*Wellfoundedness of image*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

227 
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

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

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

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

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

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

233 

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

234 

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

236 

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

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

238 
assumes "wf R" "wf S" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

243 
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

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

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

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

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

248 
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

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

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

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

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

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

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

257 
obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

258 
from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> S O R" by (rule rel_compI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

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

264 
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

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

266 

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

267 

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

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

269 

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

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

271 
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

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

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

274 
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

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

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

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

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

279 
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

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

281 
done 
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 
lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", 
26803
0af0f674845d
 Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
berghofe
parents:
26748
diff
changeset

284 
to_pred SUP_UN_eq2 bot_empty_eq pred_equals_eq, simplified, standard] 
26748
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_Union: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

288 
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

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

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

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

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

293 

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

294 
(*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

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

296 
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

297 
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

298 
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

299 
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

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

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

302 
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

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

304 

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

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

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

307 
"[ 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

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

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

310 

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

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

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

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

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

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

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

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

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

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

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

321 

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

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

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

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

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

326 

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

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

328 
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

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

330 
then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

332 
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

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

334 

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

335 
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

336 
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

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

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

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

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

341 
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

342 

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

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

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

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

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

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

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

349 
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

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

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

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

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

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

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

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

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

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

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

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

361 

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

362 
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

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

364 

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

365 

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

366 
subsubsection {* acyclic *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

367 

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

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

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

370 

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

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

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

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

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

375 

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

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

377 

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

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

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

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

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

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

383 

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

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

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

386 

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

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

388 

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

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

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

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

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

393 

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

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

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

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

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

398 
==> antisym( r^* ) = acyclic(r  Id)"; 
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 

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

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

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

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

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

405 

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

406 
text{* Wellfoundedness of finite acyclic relations*} 
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 finite_acyclic_wf [rule_format]: "finite r ==> acyclic r > wf r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

413 

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

414 
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

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

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

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

418 

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

419 
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

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

421 

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

422 

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

423 
subsection{*WellFounded Recursion*} 
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 
text{*cut*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

426 

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

427 
lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r > f(y)=g(y))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

428 
by (simp add: expand_fun_eq cut_def) 
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 
lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

432 

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

433 
text{*Inductive characterization of wfrec combinator; for details see: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

434 
John Harrison, "Inductive definitions: automation and application"*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

435 

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

436 
lemma wfrec_unique: "[ adm_wf R F; wf R ] ==> EX! y. wfrec_rel R F x y" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

438 
apply (erule_tac a=x in wf_induct) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

440 
apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

441 
apply (fast dest!: theI') 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

442 
apply (erule wfrec_rel.cases, simp) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

444 
apply (fast intro: the_equality [symmetric]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

445 
done 
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 
lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

450 
apply (rule cuts_eq [THEN iffD2, THEN subst], assumption) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

453 

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

454 
lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

456 
apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

459 
apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

461 

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

462 
subsection {* Code generator setup *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

463 

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

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

465 
"wfrec" ("\<module>wfrec?") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

467 
fun wfrec f x = f (wfrec f) x; 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

469 

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

470 

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

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

472 

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

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

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

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

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

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

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

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

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

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

482 
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

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

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

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

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

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

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

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

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

491 

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

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

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

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

495 

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

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

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

498 
"less_than = pred_nat^+" 
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 
lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

501 
unfolding less_nat_rel pred_nat_def trancl_def by simp 
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 
lemma pred_nat_trancl_eq_le: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

505 
unfolding less_eq rtrancl_eq_or_trancl by auto 
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 
lemma wf_pred_nat: "wf pred_nat" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

511 

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

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

513 
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

514 

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

515 
lemma trans_less_than [iff]: "trans less_than" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

516 
by (simp add: less_than_def trans_trancl) 
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 
lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

520 

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

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

522 
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

523 

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

524 

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

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

526 

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

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

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

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

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

531 

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

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

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

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

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

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

537 

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

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

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

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

541 

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

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

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

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

545 

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

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

547 

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

548 
text {* Induction rules *} 
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 
theorem accp_induct: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

552 
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

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

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

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

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

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

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

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

560 

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

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

562 

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

563 
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

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

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

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

567 

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

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

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

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

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

572 
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

573 

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

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

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

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

577 
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

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

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

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

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

582 
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

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

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

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

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

587 

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

588 
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

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

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

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

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

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

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

597 

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

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

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

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

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

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

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

604 

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

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

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

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

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

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

610 

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

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

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

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

614 

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

615 

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

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

617 

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

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

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

620 
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

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

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

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

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

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

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

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

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

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

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

631 

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 
text {* This is a generalized induction theorem that works on 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

635 

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

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

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

638 
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

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

640 
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

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

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

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

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

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

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

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

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

649 
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

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

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

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

653 

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 
text {* Set versions of the above theorems *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

656 

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

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

658 

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

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

660 

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

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

662 

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

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

664 

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

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

666 

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

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

668 

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

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

670 

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

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

672 

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

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

674 

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

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

676 

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

677 
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

678 

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

679 

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

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

681 

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

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

683 

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

684 
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

685 
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

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

687 
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

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

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

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

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

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

693 

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

694 
lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

696 

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

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

698 

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

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

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

701 

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

702 
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

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

704 

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

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

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

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

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

709 

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

710 
text{* Lexicographic combinations *} 
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 
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

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

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

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

717 

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

718 
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

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

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

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

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

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

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

725 
done 
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 
lemma in_lex_prod[simp]: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

728 
"(((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

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

730 

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

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

732 

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

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

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

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

736 

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

737 
text {* lexicographic combinations with measure functions *} 
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 
definition 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

740 
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

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

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

743 

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

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

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

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

747 

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

748 
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

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

750 

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

751 
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

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

753 

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

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

755 

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

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

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

758 

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

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

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

762 
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

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

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

765 

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

766 
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

767 
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

768 

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

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

771 

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

772 
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

773 

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

774 
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

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

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

777 
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

778 

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

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

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

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

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

783 
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

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

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

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

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

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

789 
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

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

791 
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

792 
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

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

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

795 
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

796 
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

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

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

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

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

801 
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

802 
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

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

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

805 

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

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

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

808 
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

809 
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

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

811 

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

812 
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

813 
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

814 
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

815 
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

816 
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

817 

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

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

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

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

821 
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

822 

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

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

824 
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

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

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

827 
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

828 
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

829 

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

830 
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

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

832 
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

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

834 
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

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

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

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

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

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

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

841 
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

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

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

844 

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

845 

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

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

847 
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

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

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

850 

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

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

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

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

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

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

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

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

858 
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

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

860 
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

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

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

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

864 
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

865 
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

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

867 
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

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

869 
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

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

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

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

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

874 
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

875 
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

876 
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

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

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

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

880 

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

881 
text {*Wellfoundedness of @{text same_fst}*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

882 

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

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

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

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

886 
"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

887 
{*For @{text rec_def} declarations where the first n parameters 
28735
bed31381e6b6
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
krauss
parents:
28562
diff
changeset

888 
stay unchanged in the recursive call. *} 
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 
lemma same_fstI [intro!]: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

891 
"[ P x; (y',y) : R x ] ==> ((x,y'),(x,y)) : same_fst P R" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

893 

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

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

895 
assumes prem: "(!!x. P x ==> wf(R x))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

896 
shows "wf(same_fst P R)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

897 
apply (simp cong del: imp_cong add: wf_def same_fst_def) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

899 
apply (rename_tac a b) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

900 
apply (case_tac "wf (R a)") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

901 
apply (erule_tac a = b in wf_induct, blast) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

904 

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

905 

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

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

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

908 

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

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

910 

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

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

913 

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

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

917 
proof  

918 
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

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

922 
apply clarify 

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

924 
apply clarify 

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

926 
apply (simp add: add_ac, blast) 

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

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

929 
apply (blast elim: rtranclE dest: rtrancl_into_trancl1) 

930 
done 

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

931 

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

934 
qed 

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

935 

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

936 
(* special case of the theorem above: <= *) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

939 
apply (rule_tac r = pred_nat in wf_weak_decr_stable) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

943 

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

944 

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

945 
subsection {* size of a datatype value *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

946 

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

947 
use "Tools/function_package/size.ML" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

948 

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

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

950 

28562  951 
lemma size_bool [code]: 
27823  952 
"size (b\<Colon>bool) = 0" by (cases b) auto 
953 

28562  954 
lemma nat_size [simp, code]: "size (n\<Colon>nat) = n" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

956 

27823  957 
declare "prod.size" [noatp] 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

958 

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

959 
end 