author  krauss 
Fri, 25 Apr 2008 15:30:33 +0200  
changeset 26748  4d51ddd6aa5c 
child 26803  0af0f674845d 
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 

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

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

16 
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

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

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

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

20 
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

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

22 

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

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

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

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

26 

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

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

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

29 

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

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

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

32 

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

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

34 
"cut f r x == (%y. if (y,x):r then f y else arbitrary)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

35 

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

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

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

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

39 

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

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

41 
[code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

42 

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

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

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

45 

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

46 
class wellorder = linorder + 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

48 

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

49 

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

50 
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

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

52 

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

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

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

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

58 

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

59 
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

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

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

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

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

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

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

66 

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

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

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

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

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

71 
unfolding wf_def by blast 
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 wfP_induct = wf_induct [to_pred] 
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 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

76 

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

77 
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

78 

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

79 
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

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

81 

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

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

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

84 

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

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

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

87 

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

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

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

90 

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

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

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

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

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

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

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

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

98 
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

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

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

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

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

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

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

105 
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

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

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

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

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

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

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

112 
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

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

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

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

116 
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

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

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

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

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

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

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

123 

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

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

125 

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

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

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

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

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

130 

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

131 

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

132 
subsubsection {* Other simple wellfoundedness results *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

133 

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

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

135 
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

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

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

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

139 
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

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

141 
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

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

143 
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

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

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

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

147 
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

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

149 
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

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

151 
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

152 
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

153 
then show "P x" by simp 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

156 

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

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

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

159 
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

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

161 

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

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

163 
"(\<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

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

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

168 

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

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

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

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

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

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

174 

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

175 
lemmas wfP_subset = wf_subset [to_pred] 
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 
text {* Wellfoundedness of the empty relation *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

180 

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

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

182 
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

183 

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

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

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

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

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

188 

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

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

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

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

192 
done 
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 
text{*Wellfoundedness of insert*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

195 
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

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

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

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

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

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

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

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

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

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

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

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

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

208 
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

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

210 
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

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

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

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

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

215 

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

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

217 
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

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

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

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

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

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

223 

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

224 

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

225 
subsubsection {* WellFoundedness Results for Unions *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

226 

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

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

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

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

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

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

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

233 
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

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

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

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

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

238 
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

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

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

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

242 

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

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

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

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

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

247 
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

248 
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

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

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

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

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

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

254 
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

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

256 

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

257 

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

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

259 

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

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

261 
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

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

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

264 
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

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

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

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

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

269 
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

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

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

272 

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

273 
lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

274 
to_pred SUP_UN_eq2 bot_empty_eq, simplified, standard] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

275 

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

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

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

278 
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

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

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

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

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

283 

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

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

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

286 
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

287 
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

288 
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

289 
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

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

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

292 
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

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

294 

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

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

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

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

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

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

300 

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

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

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

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

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

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

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

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

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

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

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

311 

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

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

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

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

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

316 

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

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

318 
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

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

320 
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

321 
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

322 
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

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

324 

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

325 
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

326 
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

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

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

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

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

331 
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

332 

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

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

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

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

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

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

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

339 
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

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

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

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

343 
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

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

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

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

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

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

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

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

351 

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

352 
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

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

354 

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

355 

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

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

357 

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

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

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

360 

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

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

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

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

364 
done 
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 
lemmas wfP_acyclicP = wf_acyclic [to_pred] 
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 acyclic_insert [iff]: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

373 

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

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

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

376 

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

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

378 

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

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

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

381 
apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) 
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 
(* Other direction: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

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

390 

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

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

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

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

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

395 

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

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

397 

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

398 
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

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

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

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

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

403 

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

404 
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

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

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

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

408 

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

409 
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

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

411 

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

412 

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

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

414 

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

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

416 

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

417 
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

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

419 

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

420 
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

421 
by (simp add: cut_def) 
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 
text{*Inductive characterization of wfrec combinator; for details see: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

425 

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

426 
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

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

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

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

430 
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

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

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

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

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

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

436 

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

437 
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

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

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

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

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

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

443 

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

444 
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

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

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

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

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

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

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

451 

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

452 
subsection {* Code generator setup *} 
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 
consts_code 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

459 

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

460 

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

461 
subsection {*LEAST and wellorderings*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

462 

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

463 
text{* See also @{text wf_linord_ex_has_least} and its consequences in 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

464 
@{text Wellfounded_Relations.ML}*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

465 

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

466 
lemma wellorder_Least_lemma [rule_format]: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

467 
"P (k::'a::wellorder) > P (LEAST x. P(x)) & (LEAST x. P(x)) <= k" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

468 
apply (rule_tac a = k in wf [THEN wf_induct]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

471 
apply (rule_tac s = x in Least_equality [THEN ssubst], auto) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

472 
apply (auto simp add: linorder_not_less [symmetric]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

474 

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

475 
lemmas LeastI = wellorder_Least_lemma [THEN conjunct1, standard] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

476 
lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

477 

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

478 
 "The following 3 lemmas are due to Brian Huffman" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

479 
lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

483 

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

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

485 
"[ P (a::'a::wellorder); !!x. P x ==> Q x ] ==> Q (Least P)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

487 

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

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

489 
"[ EX a::'a::wellorder. P a; !!x. P x ==> Q x ] ==> Q (Least P)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

490 
by (blast intro: LeastI_ex) 
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 
lemma not_less_Least: "[ k < (LEAST x. P x) ] ==> ~P (k::'a::wellorder)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

493 
apply (simp (no_asm_use) add: linorder_not_le [symmetric]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

497 

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

498 
subsection {* @{typ nat} is wellfounded *} 
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_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

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

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

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

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

509 
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

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

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

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

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

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

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

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

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

518 

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

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

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

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

522 

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

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

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

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

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

529 

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

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

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

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

533 

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

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

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

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

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

538 

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

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

540 
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

541 

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

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

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

544 

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

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

546 
by (simp add: less_than_def less_eq) 
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 
lemma wf_less: "wf {(x, y::nat). x < y}" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

549 
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

550 

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

551 
text {* Type @{typ nat} is a wellfounded order *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

552 

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

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

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

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

556 
rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+ 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

557 

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

558 
text {* @{text LEAST} theorems for type @{typ nat}*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

559 

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

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

561 
"[ P n; ~ P 0 ] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

562 
apply (case_tac "n", auto) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

563 
apply (frule LeastI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

564 
apply (drule_tac P = "%x. P (Suc x) " in LeastI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

565 
apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

566 
apply (erule_tac [2] Least_le) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

567 
apply (case_tac "LEAST x. P x", auto) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

568 
apply (drule_tac P = "%x. P (Suc x) " in Least_le) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

571 

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

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

573 
"[P n; Q m; ~P 0; !k. P (Suc k) = Q k] ==> Least P = Suc (Least Q)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

574 
apply (erule (1) Least_Suc [THEN ssubst]) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

577 

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

578 
lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

581 
apply (rule_tac x="LEAST k. P(k)" in exI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

582 
apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

584 

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

585 
lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

588 
apply (frule (1) ex_least_nat_le) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

590 
apply (case_tac k) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

593 
apply (rule_tac x=k1 in exI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

596 

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

599 

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

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

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

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

603 
*} 
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 
inductive_set 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

609 
accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r" 
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 
abbreviation 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

613 
"termip r == accp (r\<inverse>\<inverse>)" 
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 
abbreviation 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

618 

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

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

620 

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

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

622 

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

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

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

625 
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

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

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

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

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

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

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

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

633 

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

634 
theorems accp_induct_rule = accp_induct [rule_format, induct set: accp] 
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 
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

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

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

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

640 

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

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

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

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

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

645 
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

646 

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

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

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

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

650 
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

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

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

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

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

655 
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

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

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

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

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

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

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

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

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

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

669 
done 
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 
theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

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

677 

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

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

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

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

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

682 
done 
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 
theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

687 

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

688 

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

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

690 

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

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

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

693 
shows "accp R2 \<le> accp R1" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

708 

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

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

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

711 
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

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

713 
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

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

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

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

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

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

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

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

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

722 
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

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

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

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

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

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

729 

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

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

731 

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

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

733 

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

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

735 

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

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

737 

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

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

739 

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

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

741 

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

742 
lemmas acc_wfI = accp_wfPI [to_set] 
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 
lemmas acc_wfD = accp_wfPD [to_set] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

745 

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

746 
lemmas wf_acc_iff = wfP_accp_iff [to_set] 
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 
lemmas acc_subset = accp_subset [to_set] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

749 

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

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

751 

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

752 

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

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

754 

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

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

756 

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

757 
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

758 
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

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

760 
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

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

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

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

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

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

766 

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

767 
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

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

769 

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

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

771 

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

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

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

774 

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

775 
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

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

777 

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

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

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

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

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

782 

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

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

784 

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

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

786 
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

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

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

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

790 

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

791 
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

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

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

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

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

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

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

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

799 

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

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

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

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

803 

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

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

805 

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

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

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

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

809 

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

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

811 

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

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

813 
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

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

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

816 

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

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

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

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

820 

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

821 
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

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

823 

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

824 
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

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

826 

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

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

828 

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

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

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

831 

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

832 
lemma wf_finite_psubset: "wf(finite_psubset)" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

835 
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

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

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

838 

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

839 
lemma trans_finite_psubset: "trans finite_psubset" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

841 

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

842 

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

843 

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

844 

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

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

846 

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

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

848 
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

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

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

851 
{*For @{text rec_def} declarations where the first n parameters 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

852 
stay unchanged in the recursive call. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

853 
See @{text "Library/While_Combinator.thy"} for an application.*} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

854 

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

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

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

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

858 

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

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

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

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

862 
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

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

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

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

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

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

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

869 

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

870 

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

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

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

873 

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

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

875 

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

876 
lemma lemma1: "[ ALL i. (f (Suc i), f i) : r^* ] ==> (f (i+k), f i) : r^*" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

877 
apply (induct_tac "k", simp_all) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

879 
done 
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 
lemma lemma2: "[ ALL i. (f (Suc i), f i) : r^*; wf (r^+) ] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

882 
==> ALL m. f m = x > (EX i. ALL k. f (m+i+k) = f (m+i))" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

883 
apply (erule wf_induct, clarify) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

884 
apply (case_tac "EX j. (f (m+j), f m) : r^+") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

886 
apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ") 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

888 
apply (rule_tac x = "j+i" in exI) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

889 
apply (simp add: add_ac, blast) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

890 
apply (rule_tac x = 0 in exI, clarsimp) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

891 
apply (drule_tac i = m and k = k in lemma1) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

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

894 

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

895 
lemma wf_weak_decr_stable: "[ ALL i. (f (Suc i), f i) : r^*; wf (r^+) ] 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

896 
==> EX i. ALL k. f (i+k) = f i" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

897 
apply (drule_tac x = 0 in lemma2 [THEN spec], auto) 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

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

899 

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

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

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

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

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

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

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

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

907 

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 
subsection {* size of a datatype value *} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
diff
changeset

910 

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

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

912 

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

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

914 

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

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

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

917 

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

918 

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

919 
end 