author  haftmann 
Sun, 23 Jul 2006 07:20:52 +0200  
changeset 20185  183f08468e19 
parent 20105  454f4be984b7 
child 20435  d2a30fed7596 
permissions  rwrr 
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

1 
(* ID: $Id$ 
10213  2 
Author: Tobias Nipkow 
3 
Copyright 1992 University of Cambridge 

4 
*) 

5 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

6 
header {*Wellfounded Recursion*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

7 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

8 
theory Wellfounded_Recursion 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

9 
imports Transitive_Closure 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

10 
begin 
10213  11 

11328  12 
consts 
13 
wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => ('a * 'b) set" 

14 

15 
inductive "wfrec_rel R F" 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

16 
intros 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

17 
wfrecI: "ALL z. (z, x) : R > (z, g z) : wfrec_rel R F ==> 
11328  18 
(x, F g x) : wfrec_rel R F" 
19 

10213  20 
constdefs 
21 
wf :: "('a * 'a)set => bool" 

22 
"wf(r) == (!P. (!x. (!y. (y,x):r > P(y)) > P(x)) > (!x. P(x)))" 

23 

24 
acyclic :: "('a*'a)set => bool" 

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

26 

27 
cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" 

28 
"cut f r x == (%y. if (y,x):r then f y else arbitrary)" 

29 

11328  30 
adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" 
31 
"adm_wf R F == ALL f g x. 

32 
(ALL z. (z, x) : R > f z = g z) > F f x = F g x" 

10213  33 

11328  34 
wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11328
diff
changeset

35 
"wfrec R F == %x. THE y. (x, y) : wfrec_rel R (%f x. F (cut f R x) x)" 
10213  36 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

37 
axclass wellorder \<subseteq> linorder 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

38 
wf: "wf {(x,y::'a::ord). x<y}" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

39 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

40 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

41 
lemma wfUNIVI: 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

42 
"(!!P x. (ALL x. (ALL y. (y,x) : r > P(y)) > P(x)) ==> P(x)) ==> wf(r)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

43 
by (unfold wf_def, blast) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

44 

19766  45 
text{*Restriction to domain @{term A} and range @{term B}. If @{term r} is 
46 
wellfounded over their intersection, then @{term "wf r"}*} 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

47 
lemma wfI: 
19766  48 
"[ r \<subseteq> A <*> B; 
49 
!!x P. [\<forall>x. (\<forall>y. (y,x) : r > P y) > P x; x : A; x : B ] ==> P x ] 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

50 
==> wf r" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

51 
by (unfold wf_def, blast) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

52 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

53 
lemma wf_induct: 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

54 
"[ wf(r); 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

55 
!!x.[ ALL y. (y,x): r > P(y) ] ==> P(x) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

56 
] ==> P(a)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

57 
by (unfold wf_def, blast) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

58 

18458  59 
lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] 
17042
da5cfaa258f7
moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy
nipkow
parents:
15950
diff
changeset

60 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

61 
lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r > (x,a)~:r" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

62 
by (erule_tac a=a in wf_induct, blast) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

63 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

64 
(* [ wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z ] ==> Z *) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

65 
lemmas wf_asym = wf_not_sym [elim_format] 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

66 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

67 
lemma wf_not_refl [simp]: "wf(r) ==> (a,a) ~: r" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

68 
by (blast elim: wf_asym) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

69 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

70 
(* [ wf r; (a,a) ~: r ==> PROP W ] ==> PROP W *) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

71 
lemmas wf_irrefl = wf_not_refl [elim_format] 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

72 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

73 
text{*transitive closure of a wellfounded relation is wellfounded! *} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

74 
lemma wf_trancl: "wf(r) ==> wf(r^+)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

75 
apply (subst wf_def, clarify) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

76 
apply (rule allE, assumption) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

77 
{*Retains the universal formula for later use!*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

78 
apply (erule mp) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

79 
apply (erule_tac a = x in wf_induct) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

80 
apply (blast elim: tranclE) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

81 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

82 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

83 
lemma wf_converse_trancl: "wf (r^1) ==> wf ((r^+)^1)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

84 
apply (subst trancl_converse [symmetric]) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

85 
apply (erule wf_trancl) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

86 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

87 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

88 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

89 
subsubsection{*Other simple wellfoundedness results*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

90 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

91 

19870  92 
text{*Minimalelement characterization of wellfoundedness*} 
93 
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))" 

94 
proof (intro iffI strip) 

95 
fix Q::"'a set" and x 

96 
assume "wf r" and "x \<in> Q" 

97 
thus "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q" 

98 
by (unfold wf_def, 

99 
blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"]) 

100 
next 

101 
assume "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)" 

102 
thus "wf r" by (unfold wf_def, force) 

103 
qed 

104 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

105 
text{*Wellfoundedness of subsets*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

106 
lemma wf_subset: "[ wf(r); p<=r ] ==> wf(p)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

107 
apply (simp (no_asm_use) add: wf_eq_minimal) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

108 
apply fast 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

109 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

110 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

111 
text{*Wellfoundedness of the empty relation*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

112 
lemma wf_empty [iff]: "wf({})" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

113 
by (simp add: wf_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

114 

19870  115 
lemma wf_Int1: "wf r ==> wf (r Int r')" 
116 
by (erule wf_subset, rule Int_lower1) 

117 

118 
lemma wf_Int2: "wf r ==> wf (r' Int r)" 

119 
by (erule wf_subset, rule Int_lower2) 

120 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

121 
text{*Wellfoundedness of insert*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

122 
lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

123 
apply (rule iffI) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

124 
apply (blast elim: wf_trancl [THEN wf_irrefl] 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

125 
intro: rtrancl_into_trancl1 wf_subset 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

126 
rtrancl_mono [THEN [2] rev_subsetD]) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

127 
apply (simp add: wf_eq_minimal, safe) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

128 
apply (rule allE, assumption, erule impE, blast) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

129 
apply (erule bexE) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

130 
apply (rename_tac "a", case_tac "a = x") 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

131 
prefer 2 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

132 
apply blast 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

133 
apply (case_tac "y:Q") 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

134 
prefer 2 apply blast 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

135 
apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

136 
apply assumption 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

137 
apply (erule_tac V = "ALL Q. (EX x. x : Q) > ?P Q" in thin_rl) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

138 
{*essential for speed*} 
15343  139 
txt{*Blast with new substOccur fails*} 
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

140 
apply (fast intro: converse_rtrancl_into_rtrancl) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

141 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

142 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

143 
text{*Wellfoundedness of image*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

144 
lemma wf_prod_fun_image: "[ wf r; inj f ] ==> wf(prod_fun f f ` r)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

145 
apply (simp only: wf_eq_minimal, clarify) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

146 
apply (case_tac "EX p. f p : Q") 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

147 
apply (erule_tac x = "{p. f p : Q}" in allE) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

148 
apply (fast dest: inj_onD, blast) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

149 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

150 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

151 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

152 
subsubsection{*WellFoundedness Results for Unions*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

153 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

154 
text{*Wellfoundedness of indexed union with disjoint domains and ranges*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

155 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

156 
lemma wf_UN: "[ ALL i:I. wf(r i); 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

157 
ALL i:I. ALL j:I. r i ~= r j > Domain(r i) Int Range(r j) = {} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

158 
] ==> wf(UN i:I. r i)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

159 
apply (simp only: wf_eq_minimal, clarify) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

160 
apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i") 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

161 
prefer 2 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

162 
apply force 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

163 
apply clarify 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

164 
apply (drule bspec, assumption) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

165 
apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

166 
apply (blast elim!: allE) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

167 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

168 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

169 
lemma wf_Union: 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

170 
"[ ALL r:R. wf r; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

171 
ALL r:R. ALL s:R. r ~= s > Domain r Int Range s = {} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

172 
] ==> wf(Union R)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

173 
apply (simp add: Union_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

174 
apply (blast intro: wf_UN) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

175 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

176 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

177 
(*Intuition: we find an (R u S)min element of a nonempty subset A 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

178 
by case distinction. 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

179 
1. There is a step a R> b with a,b : A. 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

180 
Pick an Rmin element z of the (nonempty) set {a:A  EX b:A. a R> b}. 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

181 
By definition, there is z':A s.t. z R> z'. Because z is Rmin in the 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

182 
subset, z' must be Rmin in A. Because z' has an Rpredecessor, it cannot 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

183 
have an Ssuccessor and is thus Smin in A as well. 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

184 
2. There is no such step. 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

185 
Pick an Smin element of A. In this case it must be an Rmin 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

186 
element of A as well. 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

187 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

188 
*) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

189 
lemma wf_Un: 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

190 
"[ wf r; wf s; Domain r Int Range s = {} ] ==> wf(r Un s)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

191 
apply (simp only: wf_eq_minimal, clarify) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

192 
apply (rename_tac A a) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

193 
apply (case_tac "EX a:A. EX b:A. (b,a) : r") 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

194 
prefer 2 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

195 
apply simp 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

196 
apply (drule_tac x=A in spec)+ 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

197 
apply blast 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

198 
apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r) }" in allE)+ 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

199 
apply (blast elim!: allE) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

200 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

201 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

202 
subsubsection {*acyclic*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

203 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

204 
lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

205 
by (simp add: acyclic_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

206 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

207 
lemma wf_acyclic: "wf r ==> acyclic r" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

208 
apply (simp add: acyclic_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

209 
apply (blast elim: wf_trancl [THEN wf_irrefl]) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

210 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

211 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

212 
lemma acyclic_insert [iff]: 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

213 
"acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

214 
apply (simp add: acyclic_def trancl_insert) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

215 
apply (blast intro: rtrancl_trans) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

216 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

217 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

218 
lemma acyclic_converse [iff]: "acyclic(r^1) = acyclic r" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

219 
by (simp add: acyclic_def trancl_converse) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

220 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

221 
lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

222 
apply (simp add: acyclic_def antisym_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

223 
apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

224 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

225 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

226 
(* Other direction: 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

227 
acyclic = no loops 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

228 
antisym = only self loops 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

229 
Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r  Id) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

230 
==> antisym( r^* ) = acyclic(r  Id)"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

231 
*) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

232 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

233 
lemma acyclic_subset: "[ acyclic s; r <= s ] ==> acyclic r" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

234 
apply (simp add: acyclic_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

235 
apply (blast intro: trancl_mono) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

236 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

237 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

238 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

239 
subsection{*WellFounded Recursion*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

240 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

241 
text{*cut*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

242 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

243 
lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r > f(y)=g(y))" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

244 
by (simp add: expand_fun_eq cut_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

245 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

246 
lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

247 
by (simp add: cut_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

248 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

249 
text{*Inductive characterization of wfrec combinator; for details see: 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

250 
John Harrison, "Inductive definitions: automation and application"*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

251 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

252 
lemma wfrec_unique: "[ adm_wf R F; wf R ] ==> EX! y. (x, y) : wfrec_rel R F" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

253 
apply (simp add: adm_wf_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

254 
apply (erule_tac a=x in wf_induct) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

255 
apply (rule ex1I) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

256 
apply (rule_tac g = "%x. THE y. (x, y) : wfrec_rel R F" in wfrec_rel.wfrecI) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

257 
apply (fast dest!: theI') 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

258 
apply (erule wfrec_rel.cases, simp) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

259 
apply (erule allE, erule allE, erule allE, erule mp) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

260 
apply (fast intro: the_equality [symmetric]) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

261 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

262 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

263 
lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

264 
apply (simp add: adm_wf_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

265 
apply (intro strip) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

266 
apply (rule cuts_eq [THEN iffD2, THEN subst], assumption) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

267 
apply (rule refl) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

268 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

269 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

270 
lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

271 
apply (simp add: wfrec_def) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

272 
apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

273 
apply (rule wfrec_rel.wfrecI) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

274 
apply (intro strip) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

275 
apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

276 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

277 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

278 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

279 
text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

280 
lemma def_wfrec: "[ f==wfrec r H; wf(r) ] ==> f(a) = H (cut f r a) a" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

281 
apply auto 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

282 
apply (blast intro: wfrec) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

283 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

284 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

285 

17459  286 
subsection {* Code generator setup *} 
287 

288 
consts_code 

17654
38496187809d
Renamed wf_rec to wfrec in consts_code declaration.
berghofe
parents:
17459
diff
changeset

289 
"wfrec" ("\<module>wfrec?") 
17459  290 
attach {* 
17654
38496187809d
Renamed wf_rec to wfrec in consts_code declaration.
berghofe
parents:
17459
diff
changeset

291 
fun wfrec f x = f (wfrec f) x; 
17459  292 
*} 
293 

19602  294 
setup {* 
20105  295 
CodegenPackage.add_appconst ("wfrec", CodegenPackage.appgen_wfrec) 
18702  296 
*} 
297 

19890  298 
code_constapp 
18702  299 
wfrec 
20185  300 
ml (target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)") 
301 
haskell (target_atom "(wfrec where wfrec f x = f (wfrec f) x)") 

17459  302 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

303 
subsection{*Variants for TFL: the Recdef Package*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

304 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

305 
lemma tfl_wf_induct: "ALL R. wf R > 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

306 
(ALL P. (ALL x. (ALL y. (y,x):R > P y) > P x) > (ALL x. P x))" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

307 
apply clarify 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

308 
apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

309 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

310 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

311 
lemma tfl_cut_apply: "ALL f R. (x,a):R > (cut f R a)(x) = f(x)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

312 
apply clarify 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

313 
apply (rule cut_apply, assumption) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

314 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

315 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

316 
lemma tfl_wfrec: 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

317 
"ALL M R f. (f=wfrec R M) > wf R > (ALL x. f x = M (cut f R x) x)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

318 
apply clarify 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

319 
apply (erule wfrec) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

320 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

321 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

322 
subsection {*LEAST and wellorderings*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

323 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

324 
text{* See also @{text wf_linord_ex_has_least} and its consequences in 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

325 
@{text Wellfounded_Relations.ML}*} 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

326 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

327 
lemma wellorder_Least_lemma [rule_format]: 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

328 
"P (k::'a::wellorder) > P (LEAST x. P(x)) & (LEAST x. P(x)) <= k" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

329 
apply (rule_tac a = k in wf [THEN wf_induct]) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

330 
apply (rule impI) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

331 
apply (rule classical) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

332 
apply (rule_tac s = x in Least_equality [THEN ssubst], auto) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

333 
apply (auto simp add: linorder_not_less [symmetric]) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

334 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

335 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

336 
lemmas LeastI = wellorder_Least_lemma [THEN conjunct1, standard] 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

337 
lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard] 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

338 

15950  339 
 "The following 3 lemmas are due to Brian Huffman" 
340 
lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)" 

341 
apply (erule exE) 

342 
apply (erule LeastI) 

343 
done 

344 

345 
lemma LeastI2: 

346 
"[ P (a::'a::wellorder); !!x. P x ==> Q x ] ==> Q (Least P)" 

347 
by (blast intro: LeastI) 

348 

349 
lemma LeastI2_ex: 

350 
"[ EX a::'a::wellorder. P a; !!x. P x ==> Q x ] ==> Q (Least P)" 

351 
by (blast intro: LeastI_ex) 

352 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

353 
lemma not_less_Least: "[ k < (LEAST x. P x) ] ==> ~P (k::'a::wellorder)" 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

354 
apply (simp (no_asm_use) add: linorder_not_le [symmetric]) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

355 
apply (erule contrapos_nn) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

356 
apply (erule Least_le) 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

357 
done 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

358 

254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

359 
ML 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

360 
{* 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

361 
val wf_def = thm "wf_def"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

362 
val wfUNIVI = thm "wfUNIVI"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

363 
val wfI = thm "wfI"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

364 
val wf_induct = thm "wf_induct"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

365 
val wf_not_sym = thm "wf_not_sym"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

366 
val wf_asym = thm "wf_asym"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

367 
val wf_not_refl = thm "wf_not_refl"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

368 
val wf_irrefl = thm "wf_irrefl"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

369 
val wf_trancl = thm "wf_trancl"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

370 
val wf_converse_trancl = thm "wf_converse_trancl"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

371 
val wf_eq_minimal = thm "wf_eq_minimal"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

372 
val wf_subset = thm "wf_subset"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

373 
val wf_empty = thm "wf_empty"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

374 
val wf_insert = thm "wf_insert"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

375 
val wf_UN = thm "wf_UN"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

376 
val wf_Union = thm "wf_Union"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

377 
val wf_Un = thm "wf_Un"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

378 
val wf_prod_fun_image = thm "wf_prod_fun_image"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

379 
val acyclicI = thm "acyclicI"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

380 
val wf_acyclic = thm "wf_acyclic"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

381 
val acyclic_insert = thm "acyclic_insert"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

382 
val acyclic_converse = thm "acyclic_converse"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

383 
val acyclic_impl_antisym_rtrancl = thm "acyclic_impl_antisym_rtrancl"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

384 
val acyclic_subset = thm "acyclic_subset"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

385 
val cuts_eq = thm "cuts_eq"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

386 
val cut_apply = thm "cut_apply"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

387 
val wfrec_unique = thm "wfrec_unique"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

388 
val wfrec = thm "wfrec"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

389 
val def_wfrec = thm "def_wfrec"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

390 
val tfl_wf_induct = thm "tfl_wf_induct"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

391 
val tfl_cut_apply = thm "tfl_cut_apply"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

392 
val tfl_wfrec = thm "tfl_wfrec"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

393 
val LeastI = thm "LeastI"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

394 
val Least_le = thm "Least_le"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

395 
val not_less_Least = thm "not_less_Least"; 
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset

396 
*} 
11137  397 

10213  398 
end 