author  wenzelm 
Mon, 06 Sep 2010 14:18:16 +0200  
changeset 39157  b98909faaea8 
parent 37599  src/HOL/Extraction/Warshall.thy@b8e3400dab19 
child 51272  9c8d63b4b6be 
permissions  rwrr 
39157
b98909faaea8
more explicit HOLProofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
37599
diff
changeset

1 
(* Title: HOL/Proofs/Extraction/Warshall.thy 
13405  2 
Author: Stefan Berghofer, TU Muenchen 
3 
*) 

4 

5 
header {* Warshall's algorithm *} 

6 

16761  7 
theory Warshall 
8 
imports Main 

9 
begin 

13405  10 

11 
text {* 

12 
Derivation of Warshall's algorithm using program extraction, 

13 
based on Berger, Schwichtenberg and Seisenberger \cite{BergerJAR2001}. 

14 
*} 

15 

16 
datatype b = T  F 

17 

25976  18 
primrec 
13405  19 
is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool" 
25976  20 
where 
21 
"is_path' r x [] z = (r x z = T)" 

22 
 "is_path' r x (y # ys) z = (r x y = T \<and> is_path' r y ys z)" 

13405  23 

25976  24 
definition 
13405  25 
is_path :: "(nat \<Rightarrow> nat \<Rightarrow> b) \<Rightarrow> (nat * nat list * nat) \<Rightarrow> 
26 
nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" 

25976  27 
where 
28 
"is_path r p i j k \<longleftrightarrow> fst p = j \<and> snd (snd p) = k \<and> 

13405  29 
list_all (\<lambda>x. x < i) (fst (snd p)) \<and> 
30 
is_path' r (fst p) (fst (snd p)) (snd (snd p))" 

31 

25976  32 
definition 
13405  33 
conc :: "('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a)" 
25976  34 
where 
35 
"conc p q = (fst p, fst (snd p) @ fst q # fst (snd q), snd (snd q))" 

13405  36 

37 
theorem is_path'_snoc [simp]: 

38 
"\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)" 

39 
by (induct ys) simp+ 

40 

37599  41 
theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \<longleftrightarrow> P x \<and> list_all P xs" 
17604  42 
by (induct xs, simp+, iprover) 
13405  43 

44 
theorem list_all_lemma: 

45 
"list_all P xs \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> list_all Q xs" 

46 
proof  

47 
assume PQ: "\<And>x. P x \<Longrightarrow> Q x" 

48 
show "list_all P xs \<Longrightarrow> list_all Q xs" 

49 
proof (induct xs) 

50 
case Nil 

51 
show ?case by simp 

52 
next 

53 
case (Cons y ys) 

54 
hence Py: "P y" by simp 

55 
from Cons have Pys: "list_all P ys" by simp 

56 
show ?case 

57 
by simp (rule conjI PQ Py Cons Pys)+ 

58 
qed 

59 
qed 

60 

61 
theorem lemma1: "\<And>p. is_path r p i j k \<Longrightarrow> is_path r p (Suc i) j k" 

62 
apply (unfold is_path_def) 

63 
apply (simp cong add: conj_cong add: split_paired_all) 

64 
apply (erule conjE)+ 

65 
apply (erule list_all_lemma) 

66 
apply simp 

67 
done 

68 

69 
theorem lemma2: "\<And>p. is_path r p 0 j k \<Longrightarrow> r j k = T" 

70 
apply (unfold is_path_def) 

71 
apply (simp cong add: conj_cong add: split_paired_all) 

72 
apply (case_tac "aa") 

73 
apply simp+ 

74 
done 

75 

76 
theorem is_path'_conc: "is_path' r j xs i \<Longrightarrow> is_path' r i ys k \<Longrightarrow> 

77 
is_path' r j (xs @ i # ys) k" 

78 
proof  

79 
assume pys: "is_path' r i ys k" 

80 
show "\<And>j. is_path' r j xs i \<Longrightarrow> is_path' r j (xs @ i # ys) k" 

81 
proof (induct xs) 

82 
case (Nil j) 

83 
hence "r j i = T" by simp 

84 
with pys show ?case by simp 

85 
next 

86 
case (Cons z zs j) 

87 
hence jzr: "r j z = T" by simp 

88 
from Cons have pzs: "is_path' r z zs i" by simp 

89 
show ?case 

90 
by simp (rule conjI jzr Cons pzs)+ 

91 
qed 

92 
qed 

93 

94 
theorem lemma3: 

95 
"\<And>p q. is_path r p i j i \<Longrightarrow> is_path r q i i k \<Longrightarrow> 

96 
is_path r (conc p q) (Suc i) j k" 

97 
apply (unfold is_path_def conc_def) 

98 
apply (simp cong add: conj_cong add: split_paired_all) 

99 
apply (erule conjE)+ 

100 
apply (rule conjI) 

101 
apply (erule list_all_lemma) 

102 
apply simp 

103 
apply (rule conjI) 

104 
apply (erule list_all_lemma) 

105 
apply simp 

106 
apply (rule is_path'_conc) 

107 
apply assumption+ 

108 
done 

109 

110 
theorem lemma5: 

111 
"\<And>p. is_path r p (Suc i) j k \<Longrightarrow> ~ is_path r p i j k \<Longrightarrow> 

112 
(\<exists>q. is_path r q i j i) \<and> (\<exists>q'. is_path r q' i i k)" 

113 
proof (simp cong add: conj_cong add: split_paired_all is_path_def, (erule conjE)+) 

114 
fix xs 

23373  115 
assume asms: 
116 
"list_all (\<lambda>x. x < Suc i) xs" 

117 
"is_path' r j xs k" 

118 
"\<not> list_all (\<lambda>x. x < i) xs" 

13405  119 
show "(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i) \<and> 
120 
(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k)" 

121 
proof 

122 
show "\<And>j. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow> 

123 
\<not> list_all (\<lambda>x. x < i) xs \<Longrightarrow> 

124 
\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i" (is "PROP ?ih xs") 

125 
proof (induct xs) 

126 
case Nil 

127 
thus ?case by simp 

128 
next 

129 
case (Cons a as j) 

130 
show ?case 

131 
proof (cases "a=i") 

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

132 
case True 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

133 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

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

135 
from True and Cons have "r j i = T" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

136 
thus "list_all (\<lambda>x. x < i) [] \<and> is_path' r j [] i" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

137 
qed 
13405  138 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

139 
case False 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

140 
have "PROP ?ih as" by (rule Cons) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

141 
then obtain ys where ys: "list_all (\<lambda>x. x < i) ys \<and> is_path' r a ys i" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

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

143 
from Cons show "list_all (\<lambda>x. x < Suc i) as" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

144 
from Cons show "is_path' r a as k" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

145 
from Cons and False show "\<not> list_all (\<lambda>x. x < i) as" by (simp) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

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

147 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

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

149 
from Cons False ys 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

150 
show "list_all (\<lambda>x. x<i) (a#ys) \<and> is_path' r j (a#ys) i" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

151 
qed 
13405  152 
qed 
153 
qed 

154 
show "\<And>k. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow> 

155 
\<not> list_all (\<lambda>x. x < i) xs \<Longrightarrow> 

156 
\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k" (is "PROP ?ih xs") 

157 
proof (induct xs rule: rev_induct) 

158 
case Nil 

159 
thus ?case by simp 

160 
next 

161 
case (snoc a as k) 

162 
show ?case 

163 
proof (cases "a=i") 

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

164 
case True 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

165 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

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

167 
from True and snoc have "r i k = T" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

168 
thus "list_all (\<lambda>x. x < i) [] \<and> is_path' r i [] k" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

169 
qed 
13405  170 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

171 
case False 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

172 
have "PROP ?ih as" by (rule snoc) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

173 
then obtain ys where ys: "list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys a" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

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

175 
from snoc show "list_all (\<lambda>x. x < Suc i) as" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

176 
from snoc show "is_path' r j as a" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

177 
from snoc and False show "\<not> list_all (\<lambda>x. x < i) as" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

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

179 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

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

181 
from snoc False ys 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

182 
show "list_all (\<lambda>x. x < i) (ys @ [a]) \<and> is_path' r i (ys @ [a]) k" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

183 
by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

184 
qed 
13405  185 
qed 
186 
qed 

23373  187 
qed (rule asms)+ 
13405  188 
qed 
189 

190 
theorem lemma5': 

191 
"\<And>p. is_path r p (Suc i) j k \<Longrightarrow> \<not> is_path r p i j k \<Longrightarrow> 

192 
\<not> (\<forall>q. \<not> is_path r q i j i) \<and> \<not> (\<forall>q'. \<not> is_path r q' i i k)" 

17604  193 
by (iprover dest: lemma5) 
13405  194 

195 
theorem warshall: 

196 
"\<And>j k. \<not> (\<exists>p. is_path r p i j k) \<or> (\<exists>p. is_path r p i j k)" 

197 
proof (induct i) 

198 
case (0 j k) 

199 
show ?case 

200 
proof (cases "r j k") 

201 
assume "r j k = T" 

202 
hence "is_path r (j, [], k) 0 j k" 

203 
by (simp add: is_path_def) 

204 
hence "\<exists>p. is_path r p 0 j k" .. 

205 
thus ?thesis .. 

206 
next 

207 
assume "r j k = F" 

208 
hence "r j k ~= T" by simp 

209 
hence "\<not> (\<exists>p. is_path r p 0 j k)" 

17604  210 
by (iprover dest: lemma2) 
13405  211 
thus ?thesis .. 
212 
qed 

213 
next 

214 
case (Suc i j k) 

215 
thus ?case 

216 
proof 

217 
assume h1: "\<not> (\<exists>p. is_path r p i j k)" 

218 
from Suc show ?case 

219 
proof 

220 
assume "\<not> (\<exists>p. is_path r p i j i)" 

221 
with h1 have "\<not> (\<exists>p. is_path r p (Suc i) j k)" 

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

222 
by (iprover dest: lemma5') 
13405  223 
thus ?case .. 
224 
next 

225 
assume "\<exists>p. is_path r p i j i" 

226 
then obtain p where h2: "is_path r p i j i" .. 

227 
from Suc show ?case 

228 
proof 

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

229 
assume "\<not> (\<exists>p. is_path r p i i k)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

230 
with h1 have "\<not> (\<exists>p. is_path r p (Suc i) j k)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

231 
by (iprover dest: lemma5') 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

232 
thus ?case .. 
13405  233 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

234 
assume "\<exists>q. is_path r q i i k" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

235 
then obtain q where "is_path r q i i k" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

236 
with h2 have "is_path r (conc p q) (Suc i) j k" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

237 
by (rule lemma3) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

238 
hence "\<exists>pq. is_path r pq (Suc i) j k" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29823
diff
changeset

239 
thus ?case .. 
13405  240 
qed 
241 
qed 

242 
next 

243 
assume "\<exists>p. is_path r p i j k" 

244 
hence "\<exists>p. is_path r p (Suc i) j k" 

17604  245 
by (iprover intro: lemma1) 
13405  246 
thus ?case .. 
247 
qed 

248 
qed 

249 

250 
extract warshall 

251 

252 
text {* 

253 
The program extracted from the above proof looks as follows 

13671
eec2582923f6
Eta contraction is now switched off when printing extracted program.
berghofe
parents:
13471
diff
changeset

254 
@{thm [display, eta_contract=false] warshall_def [no_vars]} 
13405  255 
The corresponding correctness theorem is 
256 
@{thm [display] warshall_correctness [no_vars]} 

257 
*} 

258 

27982  259 
ML "@{code warshall}" 
260 

13405  261 
end 