diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-08-17 16:27:25 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-08-17 16:27:25 +0000 |
| commit | e7c86841f0574ff2024c5fd54bf338a5af3ed3df (patch) | |
| tree | b686654d117d0483f00cd20c582d58800def1877 /etc/isar | |
| parent | 8465a954bceaaf378ec6bb61b2cf6f6738135bdd (diff) | |
Update some examples
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/AThousandComments.thy | 1005 | ||||
| -rw-r--r-- | etc/isar/AThousandTheorems.thy | 1008 | ||||
| -rw-r--r-- | etc/isar/CommentParsingBug.thy | 2 | ||||
| -rw-r--r-- | etc/isar/CommentParsingBug2.thy | 2 | ||||
| -rw-r--r-- | etc/isar/Depends.thy | 4 | ||||
| -rw-r--r-- | etc/isar/FaultyErrors.thy | 4 | ||||
| -rw-r--r-- | etc/isar/Fibonacci.thy | 145 |
7 files changed, 2099 insertions, 71 deletions
diff --git a/etc/isar/AThousandComments.thy b/etc/isar/AThousandComments.thy new file mode 100644 index 00000000..a84d6018 --- /dev/null +++ b/etc/isar/AThousandComments.thy @@ -0,0 +1,1005 @@ +theory AThousandComments imports Main +begin +(* This is comment 1. Skipped by the interface, not even sent to the prover. *) + +(* This is comment 2. Skipped by the interface, not even sent to the prover. *) +(* This is comment 3. Skipped by the interface, not even sent to the prover. *) +(* This is comment 4. Skipped by the interface, not even sent to the prover. *) +(* This is comment 5. Skipped by the interface, not even sent to the prover. *) +(* This is comment 6. Skipped by the interface, not even sent to the prover. *) +(* This is comment 7. Skipped by the interface, not even sent to the prover. *) +(* This is comment 8. Skipped by the interface, not even sent to the prover. *) +(* This is comment 9. Skipped by the interface, not even sent to the prover. *) +(* This is comment 10. Skipped by the interface, not even sent to the prover. *) +(* This is comment 11. Skipped by the interface, not even sent to the prover. *) +(* This is comment 12. Skipped by the interface, not even sent to the prover. *) +(* This is comment 13. Skipped by the interface, not even sent to the prover. *) +(* This is comment 14. Skipped by the interface, not even sent to the prover. *) +(* This is comment 15. Skipped by the interface, not even sent to the prover. *) +(* This is comment 16. Skipped by the interface, not even sent to the prover. *) +(* This is comment 17. Skipped by the interface, not even sent to the prover. *) +(* This is comment 18. Skipped by the interface, not even sent to the prover. *) +(* This is comment 19. Skipped by the interface, not even sent to the prover. *) +(* This is comment 20. Skipped by the interface, not even sent to the prover. *) +(* This is comment 21. Skipped by the interface, not even sent to the prover. *) +(* This is comment 22. Skipped by the interface, not even sent to the prover. *) +(* This is comment 23. Skipped by the interface, not even sent to the prover. *) +(* This is comment 24. Skipped by the interface, not even sent to the prover. *) +(* This is comment 25. Skipped by the interface, not even sent to the prover. *) +(* This is comment 26. Skipped by the interface, not even sent to the prover. *) +(* This is comment 27. Skipped by the interface, not even sent to the prover. *) +(* This is comment 28. Skipped by the interface, not even sent to the prover. *) +(* This is comment 29. Skipped by the interface, not even sent to the prover. *) +(* This is comment 30. Skipped by the interface, not even sent to the prover. *) +(* This is comment 31. Skipped by the interface, not even sent to the prover. *) +(* This is comment 32. Skipped by the interface, not even sent to the prover. *) +(* This is comment 33. Skipped by the interface, not even sent to the prover. *) +(* This is comment 34. Skipped by the interface, not even sent to the prover. *) +(* This is comment 35. Skipped by the interface, not even sent to the prover. *) +(* This is comment 36. Skipped by the interface, not even sent to the prover. *) +(* This is comment 37. Skipped by the interface, not even sent to the prover. *) +(* This is comment 38. Skipped by the interface, not even sent to the prover. *) +(* This is comment 39. Skipped by the interface, not even sent to the prover. *) +(* This is comment 40. Skipped by the interface, not even sent to the prover. *) +(* This is comment 41. Skipped by the interface, not even sent to the prover. *) +(* This is comment 42. Skipped by the interface, not even sent to the prover. *) +(* This is comment 43. Skipped by the interface, not even sent to the prover. *) +(* This is comment 44. Skipped by the interface, not even sent to the prover. *) +(* This is comment 45. Skipped by the interface, not even sent to the prover. *) +(* This is comment 46. Skipped by the interface, not even sent to the prover. *) +(* This is comment 47. Skipped by the interface, not even sent to the prover. *) +(* This is comment 48. Skipped by the interface, not even sent to the prover. *) +(* This is comment 49. Skipped by the interface, not even sent to the prover. *) +(* This is comment 50. Skipped by the interface, not even sent to the prover. *) +(* This is comment 51. Skipped by the interface, not even sent to the prover. *) +(* This is comment 52. Skipped by the interface, not even sent to the prover. *) +(* This is comment 53. Skipped by the interface, not even sent to the prover. *) +(* This is comment 54. Skipped by the interface, not even sent to the prover. *) +(* This is comment 55. Skipped by the interface, not even sent to the prover. *) +(* This is comment 56. Skipped by the interface, not even sent to the prover. *) +(* This is comment 57. Skipped by the interface, not even sent to the prover. *) +(* This is comment 58. Skipped by the interface, not even sent to the prover. *) +(* This is comment 59. Skipped by the interface, not even sent to the prover. *) +(* This is comment 60. Skipped by the interface, not even sent to the prover. *) +(* This is comment 61. Skipped by the interface, not even sent to the prover. *) +(* This is comment 62. Skipped by the interface, not even sent to the prover. *) +(* This is comment 63. Skipped by the interface, not even sent to the prover. *) +(* This is comment 64. Skipped by the interface, not even sent to the prover. *) +(* This is comment 65. Skipped by the interface, not even sent to the prover. *) +(* This is comment 66. Skipped by the interface, not even sent to the prover. *) +(* This is comment 67. Skipped by the interface, not even sent to the prover. *) +(* This is comment 68. Skipped by the interface, not even sent to the prover. *) +(* This is comment 69. Skipped by the interface, not even sent to the prover. *) +(* This is comment 70. Skipped by the interface, not even sent to the prover. *) +(* This is comment 71. Skipped by the interface, not even sent to the prover. *) +(* This is comment 72. Skipped by the interface, not even sent to the prover. *) +(* This is comment 73. Skipped by the interface, not even sent to the prover. *) +(* This is comment 74. Skipped by the interface, not even sent to the prover. *) +(* This is comment 75. Skipped by the interface, not even sent to the prover. *) +(* This is comment 76. Skipped by the interface, not even sent to the prover. *) +(* This is comment 77. Skipped by the interface, not even sent to the prover. *) +(* This is comment 78. Skipped by the interface, not even sent to the prover. *) +(* This is comment 79. Skipped by the interface, not even sent to the prover. *) +(* This is comment 80. Skipped by the interface, not even sent to the prover. *) +(* This is comment 81. Skipped by the interface, not even sent to the prover. *) +(* This is comment 82. Skipped by the interface, not even sent to the prover. *) +(* This is comment 83. Skipped by the interface, not even sent to the prover. *) +(* This is comment 84. Skipped by the interface, not even sent to the prover. *) +(* This is comment 85. Skipped by the interface, not even sent to the prover. *) +(* This is comment 86. Skipped by the interface, not even sent to the prover. *) +(* This is comment 87. Skipped by the interface, not even sent to the prover. *) +(* This is comment 88. Skipped by the interface, not even sent to the prover. *) +(* This is comment 89. Skipped by the interface, not even sent to the prover. *) +(* This is comment 90. Skipped by the interface, not even sent to the prover. *) +(* This is comment 91. Skipped by the interface, not even sent to the prover. *) +(* This is comment 92. Skipped by the interface, not even sent to the prover. *) +(* This is comment 93. Skipped by the interface, not even sent to the prover. *) +(* This is comment 94. Skipped by the interface, not even sent to the prover. *) +(* This is comment 95. Skipped by the interface, not even sent to the prover. *) +(* This is comment 96. Skipped by the interface, not even sent to the prover. *) +(* This is comment 97. Skipped by the interface, not even sent to the prover. *) +(* This is comment 98. Skipped by the interface, not even sent to the prover. *) +(* This is comment 99. Skipped by the interface, not even sent to the prover. *) +(* This is comment 100. Skipped by the interface, not even sent to the prover. *) +(* This is comment 101. Skipped by the interface, not even sent to the prover. *) +(* This is comment 102. Skipped by the interface, not even sent to the prover. *) +(* This is comment 103. Skipped by the interface, not even sent to the prover. *) +(* This is comment 104. Skipped by the interface, not even sent to the prover. *) +(* This is comment 105. Skipped by the interface, not even sent to the prover. *) +(* This is comment 106. Skipped by the interface, not even sent to the prover. *) +(* This is comment 107. Skipped by the interface, not even sent to the prover. *) +(* This is comment 108. Skipped by the interface, not even sent to the prover. *) +(* This is comment 109. Skipped by the interface, not even sent to the prover. *) +(* This is comment 110. Skipped by the interface, not even sent to the prover. *) +(* This is comment 111. Skipped by the interface, not even sent to the prover. *) +(* This is comment 112. Skipped by the interface, not even sent to the prover. *) +(* This is comment 113. Skipped by the interface, not even sent to the prover. *) +(* This is comment 114. Skipped by the interface, not even sent to the prover. *) +(* This is comment 115. Skipped by the interface, not even sent to the prover. *) +(* This is comment 116. Skipped by the interface, not even sent to the prover. *) +(* This is comment 117. Skipped by the interface, not even sent to the prover. *) +(* This is comment 118. Skipped by the interface, not even sent to the prover. *) +(* This is comment 119. Skipped by the interface, not even sent to the prover. *) +(* This is comment 120. Skipped by the interface, not even sent to the prover. *) +(* This is comment 121. Skipped by the interface, not even sent to the prover. *) +(* This is comment 122. Skipped by the interface, not even sent to the prover. *) +(* This is comment 123. Skipped by the interface, not even sent to the prover. *) +(* This is comment 124. Skipped by the interface, not even sent to the prover. *) +(* This is comment 125. Skipped by the interface, not even sent to the prover. *) +(* This is comment 126. Skipped by the interface, not even sent to the prover. *) +(* This is comment 127. Skipped by the interface, not even sent to the prover. *) +(* This is comment 128. Skipped by the interface, not even sent to the prover. *) +(* This is comment 129. Skipped by the interface, not even sent to the prover. *) +(* This is comment 130. Skipped by the interface, not even sent to the prover. *) +(* This is comment 131. Skipped by the interface, not even sent to the prover. *) +(* This is comment 132. Skipped by the interface, not even sent to the prover. *) +(* This is comment 133. Skipped by the interface, not even sent to the prover. *) +(* This is comment 134. Skipped by the interface, not even sent to the prover. *) +(* This is comment 135. Skipped by the interface, not even sent to the prover. *) +(* This is comment 136. Skipped by the interface, not even sent to the prover. *) +(* This is comment 137. Skipped by the interface, not even sent to the prover. *) +(* This is comment 138. Skipped by the interface, not even sent to the prover. *) +(* This is comment 139. Skipped by the interface, not even sent to the prover. *) +(* This is comment 140. Skipped by the interface, not even sent to the prover. *) +(* This is comment 141. Skipped by the interface, not even sent to the prover. *) +(* This is comment 142. Skipped by the interface, not even sent to the prover. *) +(* This is comment 143. Skipped by the interface, not even sent to the prover. *) +(* This is comment 144. Skipped by the interface, not even sent to the prover. *) +(* This is comment 145. Skipped by the interface, not even sent to the prover. *) +(* This is comment 146. Skipped by the interface, not even sent to the prover. *) +(* This is comment 147. Skipped by the interface, not even sent to the prover. *) +(* This is comment 148. Skipped by the interface, not even sent to the prover. *) +(* This is comment 149. Skipped by the interface, not even sent to the prover. *) +(* This is comment 150. Skipped by the interface, not even sent to the prover. *) +(* This is comment 151. Skipped by the interface, not even sent to the prover. *) +(* This is comment 152. Skipped by the interface, not even sent to the prover. *) +(* This is comment 153. Skipped by the interface, not even sent to the prover. *) +(* This is comment 154. Skipped by the interface, not even sent to the prover. *) +(* This is comment 155. Skipped by the interface, not even sent to the prover. *) +(* This is comment 156. Skipped by the interface, not even sent to the prover. *) +(* This is comment 157. Skipped by the interface, not even sent to the prover. *) +(* This is comment 158. Skipped by the interface, not even sent to the prover. *) +(* This is comment 159. Skipped by the interface, not even sent to the prover. *) +(* This is comment 160. Skipped by the interface, not even sent to the prover. *) +(* This is comment 161. Skipped by the interface, not even sent to the prover. *) +(* This is comment 162. Skipped by the interface, not even sent to the prover. *) +(* This is comment 163. Skipped by the interface, not even sent to the prover. *) +(* This is comment 164. Skipped by the interface, not even sent to the prover. *) +(* This is comment 165. Skipped by the interface, not even sent to the prover. *) +(* This is comment 166. Skipped by the interface, not even sent to the prover. *) +(* This is comment 167. Skipped by the interface, not even sent to the prover. *) +(* This is comment 168. Skipped by the interface, not even sent to the prover. *) +(* This is comment 169. Skipped by the interface, not even sent to the prover. *) +(* This is comment 170. Skipped by the interface, not even sent to the prover. *) +(* This is comment 171. Skipped by the interface, not even sent to the prover. *) +(* This is comment 172. Skipped by the interface, not even sent to the prover. *) +(* This is comment 173. Skipped by the interface, not even sent to the prover. *) +(* This is comment 174. Skipped by the interface, not even sent to the prover. *) +(* This is comment 175. Skipped by the interface, not even sent to the prover. *) +(* This is comment 176. Skipped by the interface, not even sent to the prover. *) +(* This is comment 177. Skipped by the interface, not even sent to the prover. *) +(* This is comment 178. Skipped by the interface, not even sent to the prover. *) +(* This is comment 179. Skipped by the interface, not even sent to the prover. *) +(* This is comment 180. Skipped by the interface, not even sent to the prover. *) +(* This is comment 181. Skipped by the interface, not even sent to the prover. *) +(* This is comment 182. Skipped by the interface, not even sent to the prover. *) +(* This is comment 183. Skipped by the interface, not even sent to the prover. *) +(* This is comment 184. Skipped by the interface, not even sent to the prover. *) +(* This is comment 185. Skipped by the interface, not even sent to the prover. *) +(* This is comment 186. Skipped by the interface, not even sent to the prover. *) +(* This is comment 187. Skipped by the interface, not even sent to the prover. *) +(* This is comment 188. Skipped by the interface, not even sent to the prover. *) +(* This is comment 189. Skipped by the interface, not even sent to the prover. *) +(* This is comment 190. Skipped by the interface, not even sent to the prover. *) +(* This is comment 191. Skipped by the interface, not even sent to the prover. *) +(* This is comment 192. Skipped by the interface, not even sent to the prover. *) +(* This is comment 193. Skipped by the interface, not even sent to the prover. *) +(* This is comment 194. Skipped by the interface, not even sent to the prover. *) +(* This is comment 195. Skipped by the interface, not even sent to the prover. *) +(* This is comment 196. Skipped by the interface, not even sent to the prover. *) +(* This is comment 197. Skipped by the interface, not even sent to the prover. *) +(* This is comment 198. Skipped by the interface, not even sent to the prover. *) +(* This is comment 199. Skipped by the interface, not even sent to the prover. *) +(* This is comment 200. Skipped by the interface, not even sent to the prover. *) +(* This is comment 201. Skipped by the interface, not even sent to the prover. *) +(* This is comment 202. Skipped by the interface, not even sent to the prover. *) +(* This is comment 203. Skipped by the interface, not even sent to the prover. *) +(* This is comment 204. Skipped by the interface, not even sent to the prover. *) +(* This is comment 205. Skipped by the interface, not even sent to the prover. *) +(* This is comment 206. Skipped by the interface, not even sent to the prover. *) +(* This is comment 207. Skipped by the interface, not even sent to the prover. *) +(* This is comment 208. Skipped by the interface, not even sent to the prover. *) +(* This is comment 209. Skipped by the interface, not even sent to the prover. *) +(* This is comment 210. Skipped by the interface, not even sent to the prover. *) +(* This is comment 211. Skipped by the interface, not even sent to the prover. *) +(* This is comment 212. Skipped by the interface, not even sent to the prover. *) +(* This is comment 213. Skipped by the interface, not even sent to the prover. *) +(* This is comment 214. Skipped by the interface, not even sent to the prover. *) +(* This is comment 215. Skipped by the interface, not even sent to the prover. *) +(* This is comment 216. Skipped by the interface, not even sent to the prover. *) +(* This is comment 217. Skipped by the interface, not even sent to the prover. *) +(* This is comment 218. Skipped by the interface, not even sent to the prover. *) +(* This is comment 219. Skipped by the interface, not even sent to the prover. *) +(* This is comment 220. Skipped by the interface, not even sent to the prover. *) +(* This is comment 221. Skipped by the interface, not even sent to the prover. *) +(* This is comment 222. Skipped by the interface, not even sent to the prover. *) +(* This is comment 223. Skipped by the interface, not even sent to the prover. *) +(* This is comment 224. Skipped by the interface, not even sent to the prover. *) +(* This is comment 225. Skipped by the interface, not even sent to the prover. *) +(* This is comment 226. Skipped by the interface, not even sent to the prover. *) +(* This is comment 227. Skipped by the interface, not even sent to the prover. *) +(* This is comment 228. Skipped by the interface, not even sent to the prover. *) +(* This is comment 229. Skipped by the interface, not even sent to the prover. *) +(* This is comment 230. Skipped by the interface, not even sent to the prover. *) +(* This is comment 231. Skipped by the interface, not even sent to the prover. *) +(* This is comment 232. Skipped by the interface, not even sent to the prover. *) +(* This is comment 233. Skipped by the interface, not even sent to the prover. *) +(* This is comment 234. Skipped by the interface, not even sent to the prover. *) +(* This is comment 235. Skipped by the interface, not even sent to the prover. *) +(* This is comment 236. Skipped by the interface, not even sent to the prover. *) +(* This is comment 237. Skipped by the interface, not even sent to the prover. *) +(* This is comment 238. Skipped by the interface, not even sent to the prover. *) +(* This is comment 239. Skipped by the interface, not even sent to the prover. *) +(* This is comment 240. Skipped by the interface, not even sent to the prover. *) +(* This is comment 241. Skipped by the interface, not even sent to the prover. *) +(* This is comment 242. Skipped by the interface, not even sent to the prover. *) +(* This is comment 243. Skipped by the interface, not even sent to the prover. *) +(* This is comment 244. Skipped by the interface, not even sent to the prover. *) +(* This is comment 245. Skipped by the interface, not even sent to the prover. *) +(* This is comment 246. Skipped by the interface, not even sent to the prover. *) +(* This is comment 247. Skipped by the interface, not even sent to the prover. *) +(* This is comment 248. Skipped by the interface, not even sent to the prover. *) +(* This is comment 249. Skipped by the interface, not even sent to the prover. *) +(* This is comment 250. Skipped by the interface, not even sent to the prover. *) +(* This is comment 251. Skipped by the interface, not even sent to the prover. *) +(* This is comment 252. Skipped by the interface, not even sent to the prover. *) +(* This is comment 253. Skipped by the interface, not even sent to the prover. *) +(* This is comment 254. Skipped by the interface, not even sent to the prover. *) +(* This is comment 255. Skipped by the interface, not even sent to the prover. *) +(* This is comment 256. Skipped by the interface, not even sent to the prover. *) +(* This is comment 257. Skipped by the interface, not even sent to the prover. *) +(* This is comment 258. Skipped by the interface, not even sent to the prover. *) +(* This is comment 259. Skipped by the interface, not even sent to the prover. *) +(* This is comment 260. Skipped by the interface, not even sent to the prover. *) +(* This is comment 261. Skipped by the interface, not even sent to the prover. *) +(* This is comment 262. Skipped by the interface, not even sent to the prover. *) +(* This is comment 263. Skipped by the interface, not even sent to the prover. *) +(* This is comment 264. Skipped by the interface, not even sent to the prover. *) +(* This is comment 265. Skipped by the interface, not even sent to the prover. *) +(* This is comment 266. Skipped by the interface, not even sent to the prover. *) +(* This is comment 267. Skipped by the interface, not even sent to the prover. *) +(* This is comment 268. Skipped by the interface, not even sent to the prover. *) +(* This is comment 269. Skipped by the interface, not even sent to the prover. *) +(* This is comment 270. Skipped by the interface, not even sent to the prover. *) +(* This is comment 271. Skipped by the interface, not even sent to the prover. *) +(* This is comment 272. Skipped by the interface, not even sent to the prover. *) +(* This is comment 273. Skipped by the interface, not even sent to the prover. *) +(* This is comment 274. Skipped by the interface, not even sent to the prover. *) +(* This is comment 275. Skipped by the interface, not even sent to the prover. *) +(* This is comment 276. Skipped by the interface, not even sent to the prover. *) +(* This is comment 277. Skipped by the interface, not even sent to the prover. *) +(* This is comment 278. Skipped by the interface, not even sent to the prover. *) +(* This is comment 279. Skipped by the interface, not even sent to the prover. *) +(* This is comment 280. Skipped by the interface, not even sent to the prover. *) +(* This is comment 281. Skipped by the interface, not even sent to the prover. *) +(* This is comment 282. Skipped by the interface, not even sent to the prover. *) +(* This is comment 283. Skipped by the interface, not even sent to the prover. *) +(* This is comment 284. Skipped by the interface, not even sent to the prover. *) +(* This is comment 285. Skipped by the interface, not even sent to the prover. *) +(* This is comment 286. Skipped by the interface, not even sent to the prover. *) +(* This is comment 287. Skipped by the interface, not even sent to the prover. *) +(* This is comment 288. Skipped by the interface, not even sent to the prover. *) +(* This is comment 289. Skipped by the interface, not even sent to the prover. *) +(* This is comment 290. Skipped by the interface, not even sent to the prover. *) +(* This is comment 291. Skipped by the interface, not even sent to the prover. *) +(* This is comment 292. Skipped by the interface, not even sent to the prover. *) +(* This is comment 293. Skipped by the interface, not even sent to the prover. *) +(* This is comment 294. Skipped by the interface, not even sent to the prover. *) +(* This is comment 295. Skipped by the interface, not even sent to the prover. *) +(* This is comment 296. Skipped by the interface, not even sent to the prover. *) +(* This is comment 297. Skipped by the interface, not even sent to the prover. *) +(* This is comment 298. Skipped by the interface, not even sent to the prover. *) +(* This is comment 299. Skipped by the interface, not even sent to the prover. *) +(* This is comment 300. Skipped by the interface, not even sent to the prover. *) +(* This is comment 301. Skipped by the interface, not even sent to the prover. *) +(* This is comment 302. Skipped by the interface, not even sent to the prover. *) +(* This is comment 303. Skipped by the interface, not even sent to the prover. *) +(* This is comment 304. Skipped by the interface, not even sent to the prover. *) +(* This is comment 305. Skipped by the interface, not even sent to the prover. *) +(* This is comment 306. Skipped by the interface, not even sent to the prover. *) +(* This is comment 307. Skipped by the interface, not even sent to the prover. *) +(* This is comment 308. Skipped by the interface, not even sent to the prover. *) +(* This is comment 309. Skipped by the interface, not even sent to the prover. *) +(* This is comment 310. Skipped by the interface, not even sent to the prover. *) +(* This is comment 311. Skipped by the interface, not even sent to the prover. *) +(* This is comment 312. Skipped by the interface, not even sent to the prover. *) +(* This is comment 313. Skipped by the interface, not even sent to the prover. *) +(* This is comment 314. Skipped by the interface, not even sent to the prover. *) +(* This is comment 315. Skipped by the interface, not even sent to the prover. *) +(* This is comment 316. Skipped by the interface, not even sent to the prover. *) +(* This is comment 317. Skipped by the interface, not even sent to the prover. *) +(* This is comment 318. Skipped by the interface, not even sent to the prover. *) +(* This is comment 319. Skipped by the interface, not even sent to the prover. *) +(* This is comment 320. Skipped by the interface, not even sent to the prover. *) +(* This is comment 321. Skipped by the interface, not even sent to the prover. *) +(* This is comment 322. Skipped by the interface, not even sent to the prover. *) +(* This is comment 323. Skipped by the interface, not even sent to the prover. *) +(* This is comment 324. Skipped by the interface, not even sent to the prover. *) +(* This is comment 325. Skipped by the interface, not even sent to the prover. *) +(* This is comment 326. Skipped by the interface, not even sent to the prover. *) +(* This is comment 327. Skipped by the interface, not even sent to the prover. *) +(* This is comment 328. Skipped by the interface, not even sent to the prover. *) +(* This is comment 329. Skipped by the interface, not even sent to the prover. *) +(* This is comment 330. Skipped by the interface, not even sent to the prover. *) +(* This is comment 331. Skipped by the interface, not even sent to the prover. *) +(* This is comment 332. Skipped by the interface, not even sent to the prover. *) +(* This is comment 333. Skipped by the interface, not even sent to the prover. *) +(* This is comment 334. Skipped by the interface, not even sent to the prover. *) +(* This is comment 335. Skipped by the interface, not even sent to the prover. *) +(* This is comment 336. Skipped by the interface, not even sent to the prover. *) +(* This is comment 337. Skipped by the interface, not even sent to the prover. *) +(* This is comment 338. Skipped by the interface, not even sent to the prover. *) +(* This is comment 339. Skipped by the interface, not even sent to the prover. *) +(* This is comment 340. Skipped by the interface, not even sent to the prover. *) +(* This is comment 341. Skipped by the interface, not even sent to the prover. *) +(* This is comment 342. Skipped by the interface, not even sent to the prover. *) +(* This is comment 343. Skipped by the interface, not even sent to the prover. *) +(* This is comment 344. Skipped by the interface, not even sent to the prover. *) +(* This is comment 345. Skipped by the interface, not even sent to the prover. *) +(* This is comment 346. Skipped by the interface, not even sent to the prover. *) +(* This is comment 347. Skipped by the interface, not even sent to the prover. *) +(* This is comment 348. Skipped by the interface, not even sent to the prover. *) +(* This is comment 349. Skipped by the interface, not even sent to the prover. *) +(* This is comment 350. Skipped by the interface, not even sent to the prover. *) +(* This is comment 351. Skipped by the interface, not even sent to the prover. *) +(* This is comment 352. Skipped by the interface, not even sent to the prover. *) +(* This is comment 353. Skipped by the interface, not even sent to the prover. *) +(* This is comment 354. Skipped by the interface, not even sent to the prover. *) +(* This is comment 355. Skipped by the interface, not even sent to the prover. *) +(* This is comment 356. Skipped by the interface, not even sent to the prover. *) +(* This is comment 357. Skipped by the interface, not even sent to the prover. *) +(* This is comment 358. Skipped by the interface, not even sent to the prover. *) +(* This is comment 359. Skipped by the interface, not even sent to the prover. *) +(* This is comment 360. Skipped by the interface, not even sent to the prover. *) +(* This is comment 361. Skipped by the interface, not even sent to the prover. *) +(* This is comment 362. Skipped by the interface, not even sent to the prover. *) +(* This is comment 363. Skipped by the interface, not even sent to the prover. *) +(* This is comment 364. Skipped by the interface, not even sent to the prover. *) +(* This is comment 365. Skipped by the interface, not even sent to the prover. *) +(* This is comment 366. Skipped by the interface, not even sent to the prover. *) +(* This is comment 367. Skipped by the interface, not even sent to the prover. *) +(* This is comment 368. Skipped by the interface, not even sent to the prover. *) +(* This is comment 369. Skipped by the interface, not even sent to the prover. *) +(* This is comment 370. Skipped by the interface, not even sent to the prover. *) +(* This is comment 371. Skipped by the interface, not even sent to the prover. *) +(* This is comment 372. Skipped by the interface, not even sent to the prover. *) +(* This is comment 373. Skipped by the interface, not even sent to the prover. *) +(* This is comment 374. Skipped by the interface, not even sent to the prover. *) +(* This is comment 375. Skipped by the interface, not even sent to the prover. *) +(* This is comment 376. Skipped by the interface, not even sent to the prover. *) +(* This is comment 377. Skipped by the interface, not even sent to the prover. *) +(* This is comment 378. Skipped by the interface, not even sent to the prover. *) +(* This is comment 379. Skipped by the interface, not even sent to the prover. *) +(* This is comment 380. Skipped by the interface, not even sent to the prover. *) +(* This is comment 381. Skipped by the interface, not even sent to the prover. *) +(* This is comment 382. Skipped by the interface, not even sent to the prover. *) +(* This is comment 383. Skipped by the interface, not even sent to the prover. *) +(* This is comment 384. Skipped by the interface, not even sent to the prover. *) +(* This is comment 385. Skipped by the interface, not even sent to the prover. *) +(* This is comment 386. Skipped by the interface, not even sent to the prover. *) +(* This is comment 387. Skipped by the interface, not even sent to the prover. *) +(* This is comment 388. Skipped by the interface, not even sent to the prover. *) +(* This is comment 389. Skipped by the interface, not even sent to the prover. *) +(* This is comment 390. Skipped by the interface, not even sent to the prover. *) +(* This is comment 391. Skipped by the interface, not even sent to the prover. *) +(* This is comment 392. Skipped by the interface, not even sent to the prover. *) +(* This is comment 393. Skipped by the interface, not even sent to the prover. *) +(* This is comment 394. Skipped by the interface, not even sent to the prover. *) +(* This is comment 395. Skipped by the interface, not even sent to the prover. *) +(* This is comment 396. Skipped by the interface, not even sent to the prover. *) +(* This is comment 397. Skipped by the interface, not even sent to the prover. *) +(* This is comment 398. Skipped by the interface, not even sent to the prover. *) +(* This is comment 399. Skipped by the interface, not even sent to the prover. *) +(* This is comment 400. Skipped by the interface, not even sent to the prover. *) +(* This is comment 401. Skipped by the interface, not even sent to the prover. *) +(* This is comment 402. Skipped by the interface, not even sent to the prover. *) +(* This is comment 403. Skipped by the interface, not even sent to the prover. *) +(* This is comment 404. Skipped by the interface, not even sent to the prover. *) +(* This is comment 405. Skipped by the interface, not even sent to the prover. *) +(* This is comment 406. Skipped by the interface, not even sent to the prover. *) +(* This is comment 407. Skipped by the interface, not even sent to the prover. *) +(* This is comment 408. Skipped by the interface, not even sent to the prover. *) +(* This is comment 409. Skipped by the interface, not even sent to the prover. *) +(* This is comment 410. Skipped by the interface, not even sent to the prover. *) +(* This is comment 411. Skipped by the interface, not even sent to the prover. *) +(* This is comment 412. Skipped by the interface, not even sent to the prover. *) +(* This is comment 413. Skipped by the interface, not even sent to the prover. *) +(* This is comment 414. Skipped by the interface, not even sent to the prover. *) +(* This is comment 415. Skipped by the interface, not even sent to the prover. *) +(* This is comment 416. Skipped by the interface, not even sent to the prover. *) +(* This is comment 417. Skipped by the interface, not even sent to the prover. *) +(* This is comment 418. Skipped by the interface, not even sent to the prover. *) +(* This is comment 419. Skipped by the interface, not even sent to the prover. *) +(* This is comment 420. Skipped by the interface, not even sent to the prover. *) +(* This is comment 421. Skipped by the interface, not even sent to the prover. *) +(* This is comment 422. Skipped by the interface, not even sent to the prover. *) +(* This is comment 423. Skipped by the interface, not even sent to the prover. *) +(* This is comment 424. Skipped by the interface, not even sent to the prover. *) +(* This is comment 425. Skipped by the interface, not even sent to the prover. *) +(* This is comment 426. Skipped by the interface, not even sent to the prover. *) +(* This is comment 427. Skipped by the interface, not even sent to the prover. *) +(* This is comment 428. Skipped by the interface, not even sent to the prover. *) +(* This is comment 429. Skipped by the interface, not even sent to the prover. *) +(* This is comment 430. Skipped by the interface, not even sent to the prover. *) +(* This is comment 431. Skipped by the interface, not even sent to the prover. *) +(* This is comment 432. Skipped by the interface, not even sent to the prover. *) +(* This is comment 433. Skipped by the interface, not even sent to the prover. *) +(* This is comment 434. Skipped by the interface, not even sent to the prover. *) +(* This is comment 435. Skipped by the interface, not even sent to the prover. *) +(* This is comment 436. Skipped by the interface, not even sent to the prover. *) +(* This is comment 437. Skipped by the interface, not even sent to the prover. *) +(* This is comment 438. Skipped by the interface, not even sent to the prover. *) +(* This is comment 439. Skipped by the interface, not even sent to the prover. *) +(* This is comment 440. Skipped by the interface, not even sent to the prover. *) +(* This is comment 441. Skipped by the interface, not even sent to the prover. *) +(* This is comment 442. Skipped by the interface, not even sent to the prover. *) +(* This is comment 443. Skipped by the interface, not even sent to the prover. *) +(* This is comment 444. Skipped by the interface, not even sent to the prover. *) +(* This is comment 445. Skipped by the interface, not even sent to the prover. *) +(* This is comment 446. Skipped by the interface, not even sent to the prover. *) +(* This is comment 447. Skipped by the interface, not even sent to the prover. *) +(* This is comment 448. Skipped by the interface, not even sent to the prover. *) +(* This is comment 449. Skipped by the interface, not even sent to the prover. *) +(* This is comment 450. Skipped by the interface, not even sent to the prover. *) +(* This is comment 451. Skipped by the interface, not even sent to the prover. *) +(* This is comment 452. Skipped by the interface, not even sent to the prover. *) +(* This is comment 453. Skipped by the interface, not even sent to the prover. *) +(* This is comment 454. Skipped by the interface, not even sent to the prover. *) +(* This is comment 455. Skipped by the interface, not even sent to the prover. *) +(* This is comment 456. Skipped by the interface, not even sent to the prover. *) +(* This is comment 457. Skipped by the interface, not even sent to the prover. *) +(* This is comment 458. Skipped by the interface, not even sent to the prover. *) +(* This is comment 459. Skipped by the interface, not even sent to the prover. *) +(* This is comment 460. Skipped by the interface, not even sent to the prover. *) +(* This is comment 461. Skipped by the interface, not even sent to the prover. *) +(* This is comment 462. Skipped by the interface, not even sent to the prover. *) +(* This is comment 463. Skipped by the interface, not even sent to the prover. *) +(* This is comment 464. Skipped by the interface, not even sent to the prover. *) +(* This is comment 465. Skipped by the interface, not even sent to the prover. *) +(* This is comment 466. Skipped by the interface, not even sent to the prover. *) +(* This is comment 467. Skipped by the interface, not even sent to the prover. *) +(* This is comment 468. Skipped by the interface, not even sent to the prover. *) +(* This is comment 469. Skipped by the interface, not even sent to the prover. *) +(* This is comment 470. Skipped by the interface, not even sent to the prover. *) +(* This is comment 471. Skipped by the interface, not even sent to the prover. *) +(* This is comment 472. Skipped by the interface, not even sent to the prover. *) +(* This is comment 473. Skipped by the interface, not even sent to the prover. *) +(* This is comment 474. Skipped by the interface, not even sent to the prover. *) +(* This is comment 475. Skipped by the interface, not even sent to the prover. *) +(* This is comment 476. Skipped by the interface, not even sent to the prover. *) +(* This is comment 477. Skipped by the interface, not even sent to the prover. *) +(* This is comment 478. Skipped by the interface, not even sent to the prover. *) +(* This is comment 479. Skipped by the interface, not even sent to the prover. *) +(* This is comment 480. Skipped by the interface, not even sent to the prover. *) +(* This is comment 481. Skipped by the interface, not even sent to the prover. *) +(* This is comment 482. Skipped by the interface, not even sent to the prover. *) +(* This is comment 483. Skipped by the interface, not even sent to the prover. *) +(* This is comment 484. Skipped by the interface, not even sent to the prover. *) +(* This is comment 485. Skipped by the interface, not even sent to the prover. *) +(* This is comment 486. Skipped by the interface, not even sent to the prover. *) +(* This is comment 487. Skipped by the interface, not even sent to the prover. *) +(* This is comment 488. Skipped by the interface, not even sent to the prover. *) +(* This is comment 489. Skipped by the interface, not even sent to the prover. *) +(* This is comment 490. Skipped by the interface, not even sent to the prover. *) +(* This is comment 491. Skipped by the interface, not even sent to the prover. *) +(* This is comment 492. Skipped by the interface, not even sent to the prover. *) +(* This is comment 493. Skipped by the interface, not even sent to the prover. *) +(* This is comment 494. Skipped by the interface, not even sent to the prover. *) +(* This is comment 495. Skipped by the interface, not even sent to the prover. *) +(* This is comment 496. Skipped by the interface, not even sent to the prover. *) +(* This is comment 497. Skipped by the interface, not even sent to the prover. *) +(* This is comment 498. Skipped by the interface, not even sent to the prover. *) +(* This is comment 499. Skipped by the interface, not even sent to the prover. *) +(* This is comment 500. Skipped by the interface, not even sent to the prover. *) +(* This is comment 501. Skipped by the interface, not even sent to the prover. *) +(* This is comment 502. Skipped by the interface, not even sent to the prover. *) +(* This is comment 503. Skipped by the interface, not even sent to the prover. *) +(* This is comment 504. Skipped by the interface, not even sent to the prover. *) +(* This is comment 505. Skipped by the interface, not even sent to the prover. *) +(* This is comment 506. Skipped by the interface, not even sent to the prover. *) +(* This is comment 507. Skipped by the interface, not even sent to the prover. *) +(* This is comment 508. Skipped by the interface, not even sent to the prover. *) +(* This is comment 509. Skipped by the interface, not even sent to the prover. *) +(* This is comment 510. Skipped by the interface, not even sent to the prover. *) +(* This is comment 511. Skipped by the interface, not even sent to the prover. *) +(* This is comment 512. Skipped by the interface, not even sent to the prover. *) +(* This is comment 513. Skipped by the interface, not even sent to the prover. *) +(* This is comment 514. Skipped by the interface, not even sent to the prover. *) +(* This is comment 515. Skipped by the interface, not even sent to the prover. *) +(* This is comment 516. Skipped by the interface, not even sent to the prover. *) +(* This is comment 517. Skipped by the interface, not even sent to the prover. *) +(* This is comment 518. Skipped by the interface, not even sent to the prover. *) +(* This is comment 519. Skipped by the interface, not even sent to the prover. *) +(* This is comment 520. Skipped by the interface, not even sent to the prover. *) +(* This is comment 521. Skipped by the interface, not even sent to the prover. *) +(* This is comment 522. Skipped by the interface, not even sent to the prover. *) +(* This is comment 523. Skipped by the interface, not even sent to the prover. *) +(* This is comment 524. Skipped by the interface, not even sent to the prover. *) +(* This is comment 525. Skipped by the interface, not even sent to the prover. *) +(* This is comment 526. Skipped by the interface, not even sent to the prover. *) +(* This is comment 527. Skipped by the interface, not even sent to the prover. *) +(* This is comment 528. Skipped by the interface, not even sent to the prover. *) +(* This is comment 529. Skipped by the interface, not even sent to the prover. *) +(* This is comment 530. Skipped by the interface, not even sent to the prover. *) +(* This is comment 531. Skipped by the interface, not even sent to the prover. *) +(* This is comment 532. Skipped by the interface, not even sent to the prover. *) +(* This is comment 533. Skipped by the interface, not even sent to the prover. *) +(* This is comment 534. Skipped by the interface, not even sent to the prover. *) +(* This is comment 535. Skipped by the interface, not even sent to the prover. *) +(* This is comment 536. Skipped by the interface, not even sent to the prover. *) +(* This is comment 537. Skipped by the interface, not even sent to the prover. *) +(* This is comment 538. Skipped by the interface, not even sent to the prover. *) +(* This is comment 539. Skipped by the interface, not even sent to the prover. *) +(* This is comment 540. Skipped by the interface, not even sent to the prover. *) +(* This is comment 541. Skipped by the interface, not even sent to the prover. *) +(* This is comment 542. Skipped by the interface, not even sent to the prover. *) +(* This is comment 543. Skipped by the interface, not even sent to the prover. *) +(* This is comment 544. Skipped by the interface, not even sent to the prover. *) +(* This is comment 545. Skipped by the interface, not even sent to the prover. *) +(* This is comment 546. Skipped by the interface, not even sent to the prover. *) +(* This is comment 547. Skipped by the interface, not even sent to the prover. *) +(* This is comment 548. Skipped by the interface, not even sent to the prover. *) +(* This is comment 549. Skipped by the interface, not even sent to the prover. *) +(* This is comment 550. Skipped by the interface, not even sent to the prover. *) +(* This is comment 551. Skipped by the interface, not even sent to the prover. *) +(* This is comment 552. Skipped by the interface, not even sent to the prover. *) +(* This is comment 553. Skipped by the interface, not even sent to the prover. *) +(* This is comment 554. Skipped by the interface, not even sent to the prover. *) +(* This is comment 555. Skipped by the interface, not even sent to the prover. *) +(* This is comment 556. Skipped by the interface, not even sent to the prover. *) +(* This is comment 557. Skipped by the interface, not even sent to the prover. *) +(* This is comment 558. Skipped by the interface, not even sent to the prover. *) +(* This is comment 559. Skipped by the interface, not even sent to the prover. *) +(* This is comment 560. Skipped by the interface, not even sent to the prover. *) +(* This is comment 561. Skipped by the interface, not even sent to the prover. *) +(* This is comment 562. Skipped by the interface, not even sent to the prover. *) +(* This is comment 563. Skipped by the interface, not even sent to the prover. *) +(* This is comment 564. Skipped by the interface, not even sent to the prover. *) +(* This is comment 565. Skipped by the interface, not even sent to the prover. *) +(* This is comment 566. Skipped by the interface, not even sent to the prover. *) +(* This is comment 567. Skipped by the interface, not even sent to the prover. *) +(* This is comment 568. Skipped by the interface, not even sent to the prover. *) +(* This is comment 569. Skipped by the interface, not even sent to the prover. *) +(* This is comment 570. Skipped by the interface, not even sent to the prover. *) +(* This is comment 571. Skipped by the interface, not even sent to the prover. *) +(* This is comment 572. Skipped by the interface, not even sent to the prover. *) +(* This is comment 573. Skipped by the interface, not even sent to the prover. *) +(* This is comment 574. Skipped by the interface, not even sent to the prover. *) +(* This is comment 575. Skipped by the interface, not even sent to the prover. *) +(* This is comment 576. Skipped by the interface, not even sent to the prover. *) +(* This is comment 577. Skipped by the interface, not even sent to the prover. *) +(* This is comment 578. Skipped by the interface, not even sent to the prover. *) +(* This is comment 579. Skipped by the interface, not even sent to the prover. *) +(* This is comment 580. Skipped by the interface, not even sent to the prover. *) +(* This is comment 581. Skipped by the interface, not even sent to the prover. *) +(* This is comment 582. Skipped by the interface, not even sent to the prover. *) +(* This is comment 583. Skipped by the interface, not even sent to the prover. *) +(* This is comment 584. Skipped by the interface, not even sent to the prover. *) +(* This is comment 585. Skipped by the interface, not even sent to the prover. *) +(* This is comment 586. Skipped by the interface, not even sent to the prover. *) +(* This is comment 587. Skipped by the interface, not even sent to the prover. *) +(* This is comment 588. Skipped by the interface, not even sent to the prover. *) +(* This is comment 589. Skipped by the interface, not even sent to the prover. *) +(* This is comment 590. Skipped by the interface, not even sent to the prover. *) +(* This is comment 591. Skipped by the interface, not even sent to the prover. *) +(* This is comment 592. Skipped by the interface, not even sent to the prover. *) +(* This is comment 593. Skipped by the interface, not even sent to the prover. *) +(* This is comment 594. Skipped by the interface, not even sent to the prover. *) +(* This is comment 595. Skipped by the interface, not even sent to the prover. *) +(* This is comment 596. Skipped by the interface, not even sent to the prover. *) +(* This is comment 597. Skipped by the interface, not even sent to the prover. *) +(* This is comment 598. Skipped by the interface, not even sent to the prover. *) +(* This is comment 599. Skipped by the interface, not even sent to the prover. *) +(* This is comment 600. Skipped by the interface, not even sent to the prover. *) +(* This is comment 601. Skipped by the interface, not even sent to the prover. *) +(* This is comment 602. Skipped by the interface, not even sent to the prover. *) +(* This is comment 603. Skipped by the interface, not even sent to the prover. *) +(* This is comment 604. Skipped by the interface, not even sent to the prover. *) +(* This is comment 605. Skipped by the interface, not even sent to the prover. *) +(* This is comment 606. Skipped by the interface, not even sent to the prover. *) +(* This is comment 607. Skipped by the interface, not even sent to the prover. *) +(* This is comment 608. Skipped by the interface, not even sent to the prover. *) +(* This is comment 609. Skipped by the interface, not even sent to the prover. *) +(* This is comment 610. Skipped by the interface, not even sent to the prover. *) +(* This is comment 611. Skipped by the interface, not even sent to the prover. *) +(* This is comment 612. Skipped by the interface, not even sent to the prover. *) +(* This is comment 613. Skipped by the interface, not even sent to the prover. *) +(* This is comment 614. Skipped by the interface, not even sent to the prover. *) +(* This is comment 615. Skipped by the interface, not even sent to the prover. *) +(* This is comment 616. Skipped by the interface, not even sent to the prover. *) +(* This is comment 617. Skipped by the interface, not even sent to the prover. *) +(* This is comment 618. Skipped by the interface, not even sent to the prover. *) +(* This is comment 619. Skipped by the interface, not even sent to the prover. *) +(* This is comment 620. Skipped by the interface, not even sent to the prover. *) +(* This is comment 621. Skipped by the interface, not even sent to the prover. *) +(* This is comment 622. Skipped by the interface, not even sent to the prover. *) +(* This is comment 623. Skipped by the interface, not even sent to the prover. *) +(* This is comment 624. Skipped by the interface, not even sent to the prover. *) +(* This is comment 625. Skipped by the interface, not even sent to the prover. *) +(* This is comment 626. Skipped by the interface, not even sent to the prover. *) +(* This is comment 627. Skipped by the interface, not even sent to the prover. *) +(* This is comment 628. Skipped by the interface, not even sent to the prover. *) +(* This is comment 629. Skipped by the interface, not even sent to the prover. *) +(* This is comment 630. Skipped by the interface, not even sent to the prover. *) +(* This is comment 631. Skipped by the interface, not even sent to the prover. *) +(* This is comment 632. Skipped by the interface, not even sent to the prover. *) +(* This is comment 633. Skipped by the interface, not even sent to the prover. *) +(* This is comment 634. Skipped by the interface, not even sent to the prover. *) +(* This is comment 635. Skipped by the interface, not even sent to the prover. *) +(* This is comment 636. Skipped by the interface, not even sent to the prover. *) +(* This is comment 637. Skipped by the interface, not even sent to the prover. *) +(* This is comment 638. Skipped by the interface, not even sent to the prover. *) +(* This is comment 639. Skipped by the interface, not even sent to the prover. *) +(* This is comment 640. Skipped by the interface, not even sent to the prover. *) +(* This is comment 641. Skipped by the interface, not even sent to the prover. *) +(* This is comment 642. Skipped by the interface, not even sent to the prover. *) +(* This is comment 643. Skipped by the interface, not even sent to the prover. *) +(* This is comment 644. Skipped by the interface, not even sent to the prover. *) +(* This is comment 645. Skipped by the interface, not even sent to the prover. *) +(* This is comment 646. Skipped by the interface, not even sent to the prover. *) +(* This is comment 647. Skipped by the interface, not even sent to the prover. *) +(* This is comment 648. Skipped by the interface, not even sent to the prover. *) +(* This is comment 649. Skipped by the interface, not even sent to the prover. *) +(* This is comment 650. Skipped by the interface, not even sent to the prover. *) +(* This is comment 651. Skipped by the interface, not even sent to the prover. *) +(* This is comment 652. Skipped by the interface, not even sent to the prover. *) +(* This is comment 653. Skipped by the interface, not even sent to the prover. *) +(* This is comment 654. Skipped by the interface, not even sent to the prover. *) +(* This is comment 655. Skipped by the interface, not even sent to the prover. *) +(* This is comment 656. Skipped by the interface, not even sent to the prover. *) +(* This is comment 657. Skipped by the interface, not even sent to the prover. *) +(* This is comment 658. Skipped by the interface, not even sent to the prover. *) +(* This is comment 659. Skipped by the interface, not even sent to the prover. *) +(* This is comment 660. Skipped by the interface, not even sent to the prover. *) +(* This is comment 661. Skipped by the interface, not even sent to the prover. *) +(* This is comment 662. Skipped by the interface, not even sent to the prover. *) +(* This is comment 663. Skipped by the interface, not even sent to the prover. *) +(* This is comment 664. Skipped by the interface, not even sent to the prover. *) +(* This is comment 665. Skipped by the interface, not even sent to the prover. *) +(* This is comment 666. Skipped by the interface, not even sent to the prover. *) +(* This is comment 667. Skipped by the interface, not even sent to the prover. *) +(* This is comment 668. Skipped by the interface, not even sent to the prover. *) +(* This is comment 669. Skipped by the interface, not even sent to the prover. *) +(* This is comment 670. Skipped by the interface, not even sent to the prover. *) +(* This is comment 671. Skipped by the interface, not even sent to the prover. *) +(* This is comment 672. Skipped by the interface, not even sent to the prover. *) +(* This is comment 673. Skipped by the interface, not even sent to the prover. *) +(* This is comment 674. Skipped by the interface, not even sent to the prover. *) +(* This is comment 675. Skipped by the interface, not even sent to the prover. *) +(* This is comment 676. Skipped by the interface, not even sent to the prover. *) +(* This is comment 677. Skipped by the interface, not even sent to the prover. *) +(* This is comment 678. Skipped by the interface, not even sent to the prover. *) +(* This is comment 679. Skipped by the interface, not even sent to the prover. *) +(* This is comment 680. Skipped by the interface, not even sent to the prover. *) +(* This is comment 681. Skipped by the interface, not even sent to the prover. *) +(* This is comment 682. Skipped by the interface, not even sent to the prover. *) +(* This is comment 683. Skipped by the interface, not even sent to the prover. *) +(* This is comment 684. Skipped by the interface, not even sent to the prover. *) +(* This is comment 685. Skipped by the interface, not even sent to the prover. *) +(* This is comment 686. Skipped by the interface, not even sent to the prover. *) +(* This is comment 687. Skipped by the interface, not even sent to the prover. *) +(* This is comment 688. Skipped by the interface, not even sent to the prover. *) +(* This is comment 689. Skipped by the interface, not even sent to the prover. *) +(* This is comment 690. Skipped by the interface, not even sent to the prover. *) +(* This is comment 691. Skipped by the interface, not even sent to the prover. *) +(* This is comment 692. Skipped by the interface, not even sent to the prover. *) +(* This is comment 693. Skipped by the interface, not even sent to the prover. *) +(* This is comment 694. Skipped by the interface, not even sent to the prover. *) +(* This is comment 695. Skipped by the interface, not even sent to the prover. *) +(* This is comment 696. Skipped by the interface, not even sent to the prover. *) +(* This is comment 697. Skipped by the interface, not even sent to the prover. *) +(* This is comment 698. Skipped by the interface, not even sent to the prover. *) +(* This is comment 699. Skipped by the interface, not even sent to the prover. *) +(* This is comment 700. Skipped by the interface, not even sent to the prover. *) +(* This is comment 701. Skipped by the interface, not even sent to the prover. *) +(* This is comment 702. Skipped by the interface, not even sent to the prover. *) +(* This is comment 703. Skipped by the interface, not even sent to the prover. *) +(* This is comment 704. Skipped by the interface, not even sent to the prover. *) +(* This is comment 705. Skipped by the interface, not even sent to the prover. *) +(* This is comment 706. Skipped by the interface, not even sent to the prover. *) +(* This is comment 707. Skipped by the interface, not even sent to the prover. *) +(* This is comment 708. Skipped by the interface, not even sent to the prover. *) +(* This is comment 709. Skipped by the interface, not even sent to the prover. *) +(* This is comment 710. Skipped by the interface, not even sent to the prover. *) +(* This is comment 711. Skipped by the interface, not even sent to the prover. *) +(* This is comment 712. Skipped by the interface, not even sent to the prover. *) +(* This is comment 713. Skipped by the interface, not even sent to the prover. *) +(* This is comment 714. Skipped by the interface, not even sent to the prover. *) +(* This is comment 715. Skipped by the interface, not even sent to the prover. *) +(* This is comment 716. Skipped by the interface, not even sent to the prover. *) +(* This is comment 717. Skipped by the interface, not even sent to the prover. *) +(* This is comment 718. Skipped by the interface, not even sent to the prover. *) +(* This is comment 719. Skipped by the interface, not even sent to the prover. *) +(* This is comment 720. Skipped by the interface, not even sent to the prover. *) +(* This is comment 721. Skipped by the interface, not even sent to the prover. *) +(* This is comment 722. Skipped by the interface, not even sent to the prover. *) +(* This is comment 723. Skipped by the interface, not even sent to the prover. *) +(* This is comment 724. Skipped by the interface, not even sent to the prover. *) +(* This is comment 725. Skipped by the interface, not even sent to the prover. *) +(* This is comment 726. Skipped by the interface, not even sent to the prover. *) +(* This is comment 727. Skipped by the interface, not even sent to the prover. *) +(* This is comment 728. Skipped by the interface, not even sent to the prover. *) +(* This is comment 729. Skipped by the interface, not even sent to the prover. *) +(* This is comment 730. Skipped by the interface, not even sent to the prover. *) +(* This is comment 731. Skipped by the interface, not even sent to the prover. *) +(* This is comment 732. Skipped by the interface, not even sent to the prover. *) +(* This is comment 733. Skipped by the interface, not even sent to the prover. *) +(* This is comment 734. Skipped by the interface, not even sent to the prover. *) +(* This is comment 735. Skipped by the interface, not even sent to the prover. *) +(* This is comment 736. Skipped by the interface, not even sent to the prover. *) +(* This is comment 737. Skipped by the interface, not even sent to the prover. *) +(* This is comment 738. Skipped by the interface, not even sent to the prover. *) +(* This is comment 739. Skipped by the interface, not even sent to the prover. *) +(* This is comment 740. Skipped by the interface, not even sent to the prover. *) +(* This is comment 741. Skipped by the interface, not even sent to the prover. *) +(* This is comment 742. Skipped by the interface, not even sent to the prover. *) +(* This is comment 743. Skipped by the interface, not even sent to the prover. *) +(* This is comment 744. Skipped by the interface, not even sent to the prover. *) +(* This is comment 745. Skipped by the interface, not even sent to the prover. *) +(* This is comment 746. Skipped by the interface, not even sent to the prover. *) +(* This is comment 747. Skipped by the interface, not even sent to the prover. *) +(* This is comment 748. Skipped by the interface, not even sent to the prover. *) +(* This is comment 749. Skipped by the interface, not even sent to the prover. *) +(* This is comment 750. Skipped by the interface, not even sent to the prover. *) +(* This is comment 751. Skipped by the interface, not even sent to the prover. *) +(* This is comment 752. Skipped by the interface, not even sent to the prover. *) +(* This is comment 753. Skipped by the interface, not even sent to the prover. *) +(* This is comment 754. Skipped by the interface, not even sent to the prover. *) +(* This is comment 755. Skipped by the interface, not even sent to the prover. *) +(* This is comment 756. Skipped by the interface, not even sent to the prover. *) +(* This is comment 757. Skipped by the interface, not even sent to the prover. *) +(* This is comment 758. Skipped by the interface, not even sent to the prover. *) +(* This is comment 759. Skipped by the interface, not even sent to the prover. *) +(* This is comment 760. Skipped by the interface, not even sent to the prover. *) +(* This is comment 761. Skipped by the interface, not even sent to the prover. *) +(* This is comment 762. Skipped by the interface, not even sent to the prover. *) +(* This is comment 763. Skipped by the interface, not even sent to the prover. *) +(* This is comment 764. Skipped by the interface, not even sent to the prover. *) +(* This is comment 765. Skipped by the interface, not even sent to the prover. *) +(* This is comment 766. Skipped by the interface, not even sent to the prover. *) +(* This is comment 767. Skipped by the interface, not even sent to the prover. *) +(* This is comment 768. Skipped by the interface, not even sent to the prover. *) +(* This is comment 769. Skipped by the interface, not even sent to the prover. *) +(* This is comment 770. Skipped by the interface, not even sent to the prover. *) +(* This is comment 771. Skipped by the interface, not even sent to the prover. *) +(* This is comment 772. Skipped by the interface, not even sent to the prover. *) +(* This is comment 773. Skipped by the interface, not even sent to the prover. *) +(* This is comment 774. Skipped by the interface, not even sent to the prover. *) +(* This is comment 775. Skipped by the interface, not even sent to the prover. *) +(* This is comment 776. Skipped by the interface, not even sent to the prover. *) +(* This is comment 777. Skipped by the interface, not even sent to the prover. *) +(* This is comment 778. Skipped by the interface, not even sent to the prover. *) +(* This is comment 779. Skipped by the interface, not even sent to the prover. *) +(* This is comment 780. Skipped by the interface, not even sent to the prover. *) +(* This is comment 781. Skipped by the interface, not even sent to the prover. *) +(* This is comment 782. Skipped by the interface, not even sent to the prover. *) +(* This is comment 783. Skipped by the interface, not even sent to the prover. *) +(* This is comment 784. Skipped by the interface, not even sent to the prover. *) +(* This is comment 785. Skipped by the interface, not even sent to the prover. *) +(* This is comment 786. Skipped by the interface, not even sent to the prover. *) +(* This is comment 787. Skipped by the interface, not even sent to the prover. *) +(* This is comment 788. Skipped by the interface, not even sent to the prover. *) +(* This is comment 789. Skipped by the interface, not even sent to the prover. *) +(* This is comment 790. Skipped by the interface, not even sent to the prover. *) +(* This is comment 791. Skipped by the interface, not even sent to the prover. *) +(* This is comment 792. Skipped by the interface, not even sent to the prover. *) +(* This is comment 793. Skipped by the interface, not even sent to the prover. *) +(* This is comment 794. Skipped by the interface, not even sent to the prover. *) +(* This is comment 795. Skipped by the interface, not even sent to the prover. *) +(* This is comment 796. Skipped by the interface, not even sent to the prover. *) +(* This is comment 797. Skipped by the interface, not even sent to the prover. *) +(* This is comment 798. Skipped by the interface, not even sent to the prover. *) +(* This is comment 799. Skipped by the interface, not even sent to the prover. *) +(* This is comment 800. Skipped by the interface, not even sent to the prover. *) +(* This is comment 801. Skipped by the interface, not even sent to the prover. *) +(* This is comment 802. Skipped by the interface, not even sent to the prover. *) +(* This is comment 803. Skipped by the interface, not even sent to the prover. *) +(* This is comment 804. Skipped by the interface, not even sent to the prover. *) +(* This is comment 805. Skipped by the interface, not even sent to the prover. *) +(* This is comment 806. Skipped by the interface, not even sent to the prover. *) +(* This is comment 807. Skipped by the interface, not even sent to the prover. *) +(* This is comment 808. Skipped by the interface, not even sent to the prover. *) +(* This is comment 809. Skipped by the interface, not even sent to the prover. *) +(* This is comment 810. Skipped by the interface, not even sent to the prover. *) +(* This is comment 811. Skipped by the interface, not even sent to the prover. *) +(* This is comment 812. Skipped by the interface, not even sent to the prover. *) +(* This is comment 813. Skipped by the interface, not even sent to the prover. *) +(* This is comment 814. Skipped by the interface, not even sent to the prover. *) +(* This is comment 815. Skipped by the interface, not even sent to the prover. *) +(* This is comment 816. Skipped by the interface, not even sent to the prover. *) +(* This is comment 817. Skipped by the interface, not even sent to the prover. *) +(* This is comment 818. Skipped by the interface, not even sent to the prover. *) +(* This is comment 819. Skipped by the interface, not even sent to the prover. *) +(* This is comment 820. Skipped by the interface, not even sent to the prover. *) +(* This is comment 821. Skipped by the interface, not even sent to the prover. *) +(* This is comment 822. Skipped by the interface, not even sent to the prover. *) +(* This is comment 823. Skipped by the interface, not even sent to the prover. *) +(* This is comment 824. Skipped by the interface, not even sent to the prover. *) +(* This is comment 825. Skipped by the interface, not even sent to the prover. *) +(* This is comment 826. Skipped by the interface, not even sent to the prover. *) +(* This is comment 827. Skipped by the interface, not even sent to the prover. *) +(* This is comment 828. Skipped by the interface, not even sent to the prover. *) +(* This is comment 829. Skipped by the interface, not even sent to the prover. *) +(* This is comment 830. Skipped by the interface, not even sent to the prover. *) +(* This is comment 831. Skipped by the interface, not even sent to the prover. *) +(* This is comment 832. Skipped by the interface, not even sent to the prover. *) +(* This is comment 833. Skipped by the interface, not even sent to the prover. *) +(* This is comment 834. Skipped by the interface, not even sent to the prover. *) +(* This is comment 835. Skipped by the interface, not even sent to the prover. *) +(* This is comment 836. Skipped by the interface, not even sent to the prover. *) +(* This is comment 837. Skipped by the interface, not even sent to the prover. *) +(* This is comment 838. Skipped by the interface, not even sent to the prover. *) +(* This is comment 839. Skipped by the interface, not even sent to the prover. *) +(* This is comment 840. Skipped by the interface, not even sent to the prover. *) +(* This is comment 841. Skipped by the interface, not even sent to the prover. *) +(* This is comment 842. Skipped by the interface, not even sent to the prover. *) +(* This is comment 843. Skipped by the interface, not even sent to the prover. *) +(* This is comment 844. Skipped by the interface, not even sent to the prover. *) +(* This is comment 845. Skipped by the interface, not even sent to the prover. *) +(* This is comment 846. Skipped by the interface, not even sent to the prover. *) +(* This is comment 847. Skipped by the interface, not even sent to the prover. *) +(* This is comment 848. Skipped by the interface, not even sent to the prover. *) +(* This is comment 849. Skipped by the interface, not even sent to the prover. *) +(* This is comment 850. Skipped by the interface, not even sent to the prover. *) +(* This is comment 851. Skipped by the interface, not even sent to the prover. *) +(* This is comment 852. Skipped by the interface, not even sent to the prover. *) +(* This is comment 853. Skipped by the interface, not even sent to the prover. *) +(* This is comment 854. Skipped by the interface, not even sent to the prover. *) +(* This is comment 855. Skipped by the interface, not even sent to the prover. *) +(* This is comment 856. Skipped by the interface, not even sent to the prover. *) +(* This is comment 857. Skipped by the interface, not even sent to the prover. *) +(* This is comment 858. Skipped by the interface, not even sent to the prover. *) +(* This is comment 859. Skipped by the interface, not even sent to the prover. *) +(* This is comment 860. Skipped by the interface, not even sent to the prover. *) +(* This is comment 861. Skipped by the interface, not even sent to the prover. *) +(* This is comment 862. Skipped by the interface, not even sent to the prover. *) +(* This is comment 863. Skipped by the interface, not even sent to the prover. *) +(* This is comment 864. Skipped by the interface, not even sent to the prover. *) +(* This is comment 865. Skipped by the interface, not even sent to the prover. *) +(* This is comment 866. Skipped by the interface, not even sent to the prover. *) +(* This is comment 867. Skipped by the interface, not even sent to the prover. *) +(* This is comment 868. Skipped by the interface, not even sent to the prover. *) +(* This is comment 869. Skipped by the interface, not even sent to the prover. *) +(* This is comment 870. Skipped by the interface, not even sent to the prover. *) +(* This is comment 871. Skipped by the interface, not even sent to the prover. *) +(* This is comment 872. Skipped by the interface, not even sent to the prover. *) +(* This is comment 873. Skipped by the interface, not even sent to the prover. *) +(* This is comment 874. Skipped by the interface, not even sent to the prover. *) +(* This is comment 875. Skipped by the interface, not even sent to the prover. *) +(* This is comment 876. Skipped by the interface, not even sent to the prover. *) +(* This is comment 877. Skipped by the interface, not even sent to the prover. *) +(* This is comment 878. Skipped by the interface, not even sent to the prover. *) +(* This is comment 879. Skipped by the interface, not even sent to the prover. *) +(* This is comment 880. Skipped by the interface, not even sent to the prover. *) +(* This is comment 881. Skipped by the interface, not even sent to the prover. *) +(* This is comment 882. Skipped by the interface, not even sent to the prover. *) +(* This is comment 883. Skipped by the interface, not even sent to the prover. *) +(* This is comment 884. Skipped by the interface, not even sent to the prover. *) +(* This is comment 885. Skipped by the interface, not even sent to the prover. *) +(* This is comment 886. Skipped by the interface, not even sent to the prover. *) +(* This is comment 887. Skipped by the interface, not even sent to the prover. *) +(* This is comment 888. Skipped by the interface, not even sent to the prover. *) +(* This is comment 889. Skipped by the interface, not even sent to the prover. *) +(* This is comment 890. Skipped by the interface, not even sent to the prover. *) +(* This is comment 891. Skipped by the interface, not even sent to the prover. *) +(* This is comment 892. Skipped by the interface, not even sent to the prover. *) +(* This is comment 893. Skipped by the interface, not even sent to the prover. *) +(* This is comment 894. Skipped by the interface, not even sent to the prover. *) +(* This is comment 895. Skipped by the interface, not even sent to the prover. *) +(* This is comment 896. Skipped by the interface, not even sent to the prover. *) +(* This is comment 897. Skipped by the interface, not even sent to the prover. *) +(* This is comment 898. Skipped by the interface, not even sent to the prover. *) +(* This is comment 899. Skipped by the interface, not even sent to the prover. *) +(* This is comment 900. Skipped by the interface, not even sent to the prover. *) +(* This is comment 901. Skipped by the interface, not even sent to the prover. *) +(* This is comment 902. Skipped by the interface, not even sent to the prover. *) +(* This is comment 903. Skipped by the interface, not even sent to the prover. *) +(* This is comment 904. Skipped by the interface, not even sent to the prover. *) +(* This is comment 905. Skipped by the interface, not even sent to the prover. *) +(* This is comment 906. Skipped by the interface, not even sent to the prover. *) +(* This is comment 907. Skipped by the interface, not even sent to the prover. *) +(* This is comment 908. Skipped by the interface, not even sent to the prover. *) +(* This is comment 909. Skipped by the interface, not even sent to the prover. *) +(* This is comment 910. Skipped by the interface, not even sent to the prover. *) +(* This is comment 911. Skipped by the interface, not even sent to the prover. *) +(* This is comment 912. Skipped by the interface, not even sent to the prover. *) +(* This is comment 913. Skipped by the interface, not even sent to the prover. *) +(* This is comment 914. Skipped by the interface, not even sent to the prover. *) +(* This is comment 915. Skipped by the interface, not even sent to the prover. *) +(* This is comment 916. Skipped by the interface, not even sent to the prover. *) +(* This is comment 917. Skipped by the interface, not even sent to the prover. *) +(* This is comment 918. Skipped by the interface, not even sent to the prover. *) +(* This is comment 919. Skipped by the interface, not even sent to the prover. *) +(* This is comment 920. Skipped by the interface, not even sent to the prover. *) +(* This is comment 921. Skipped by the interface, not even sent to the prover. *) +(* This is comment 922. Skipped by the interface, not even sent to the prover. *) +(* This is comment 923. Skipped by the interface, not even sent to the prover. *) +(* This is comment 924. Skipped by the interface, not even sent to the prover. *) +(* This is comment 925. Skipped by the interface, not even sent to the prover. *) +(* This is comment 926. Skipped by the interface, not even sent to the prover. *) +(* This is comment 927. Skipped by the interface, not even sent to the prover. *) +(* This is comment 928. Skipped by the interface, not even sent to the prover. *) +(* This is comment 929. Skipped by the interface, not even sent to the prover. *) +(* This is comment 930. Skipped by the interface, not even sent to the prover. *) +(* This is comment 931. Skipped by the interface, not even sent to the prover. *) +(* This is comment 932. Skipped by the interface, not even sent to the prover. *) +(* This is comment 933. Skipped by the interface, not even sent to the prover. *) +(* This is comment 934. Skipped by the interface, not even sent to the prover. *) +(* This is comment 935. Skipped by the interface, not even sent to the prover. *) +(* This is comment 936. Skipped by the interface, not even sent to the prover. *) +(* This is comment 937. Skipped by the interface, not even sent to the prover. *) +(* This is comment 938. Skipped by the interface, not even sent to the prover. *) +(* This is comment 939. Skipped by the interface, not even sent to the prover. *) +(* This is comment 940. Skipped by the interface, not even sent to the prover. *) +(* This is comment 941. Skipped by the interface, not even sent to the prover. *) +(* This is comment 942. Skipped by the interface, not even sent to the prover. *) +(* This is comment 943. Skipped by the interface, not even sent to the prover. *) +(* This is comment 944. Skipped by the interface, not even sent to the prover. *) +(* This is comment 945. Skipped by the interface, not even sent to the prover. *) +(* This is comment 946. Skipped by the interface, not even sent to the prover. *) +(* This is comment 947. Skipped by the interface, not even sent to the prover. *) +(* This is comment 948. Skipped by the interface, not even sent to the prover. *) +(* This is comment 949. Skipped by the interface, not even sent to the prover. *) +(* This is comment 950. Skipped by the interface, not even sent to the prover. *) +(* This is comment 951. Skipped by the interface, not even sent to the prover. *) +(* This is comment 952. Skipped by the interface, not even sent to the prover. *) +(* This is comment 953. Skipped by the interface, not even sent to the prover. *) +(* This is comment 954. Skipped by the interface, not even sent to the prover. *) +(* This is comment 955. Skipped by the interface, not even sent to the prover. *) +(* This is comment 956. Skipped by the interface, not even sent to the prover. *) +(* This is comment 957. Skipped by the interface, not even sent to the prover. *) +(* This is comment 958. Skipped by the interface, not even sent to the prover. *) +(* This is comment 959. Skipped by the interface, not even sent to the prover. *) +(* This is comment 960. Skipped by the interface, not even sent to the prover. *) +(* This is comment 961. Skipped by the interface, not even sent to the prover. *) +(* This is comment 962. Skipped by the interface, not even sent to the prover. *) +(* This is comment 963. Skipped by the interface, not even sent to the prover. *) +(* This is comment 964. Skipped by the interface, not even sent to the prover. *) +(* This is comment 965. Skipped by the interface, not even sent to the prover. *) +(* This is comment 966. Skipped by the interface, not even sent to the prover. *) +(* This is comment 967. Skipped by the interface, not even sent to the prover. *) +(* This is comment 968. Skipped by the interface, not even sent to the prover. *) +(* This is comment 969. Skipped by the interface, not even sent to the prover. *) +(* This is comment 970. Skipped by the interface, not even sent to the prover. *) +(* This is comment 971. Skipped by the interface, not even sent to the prover. *) +(* This is comment 972. Skipped by the interface, not even sent to the prover. *) +(* This is comment 973. Skipped by the interface, not even sent to the prover. *) +(* This is comment 974. Skipped by the interface, not even sent to the prover. *) +(* This is comment 975. Skipped by the interface, not even sent to the prover. *) +(* This is comment 976. Skipped by the interface, not even sent to the prover. *) +(* This is comment 977. Skipped by the interface, not even sent to the prover. *) +(* This is comment 978. Skipped by the interface, not even sent to the prover. *) +(* This is comment 979. Skipped by the interface, not even sent to the prover. *) +(* This is comment 980. Skipped by the interface, not even sent to the prover. *) +(* This is comment 981. Skipped by the interface, not even sent to the prover. *) +(* This is comment 982. Skipped by the interface, not even sent to the prover. *) +(* This is comment 983. Skipped by the interface, not even sent to the prover. *) +(* This is comment 984. Skipped by the interface, not even sent to the prover. *) +(* This is comment 985. Skipped by the interface, not even sent to the prover. *) +(* This is comment 986. Skipped by the interface, not even sent to the prover. *) +(* This is comment 987. Skipped by the interface, not even sent to the prover. *) +(* This is comment 988. Skipped by the interface, not even sent to the prover. *) +(* This is comment 989. Skipped by the interface, not even sent to the prover. *) +(* This is comment 990. Skipped by the interface, not even sent to the prover. *) +(* This is comment 991. Skipped by the interface, not even sent to the prover. *) +(* This is comment 992. Skipped by the interface, not even sent to the prover. *) +(* This is comment 993. Skipped by the interface, not even sent to the prover. *) +(* This is comment 994. Skipped by the interface, not even sent to the prover. *) +(* This is comment 995. Skipped by the interface, not even sent to the prover. *) +(* This is comment 996. Skipped by the interface, not even sent to the prover. *) +(* This is comment 997. Skipped by the interface, not even sent to the prover. *) +(* This is comment 998. Skipped by the interface, not even sent to the prover. *) +(* This is comment 999. Skipped by the interface, not even sent to the prover. *) +(* This is comment 1000. Skipped by the interface, not even sent to the prover. *) + +end diff --git a/etc/isar/AThousandTheorems.thy b/etc/isar/AThousandTheorems.thy new file mode 100644 index 00000000..77be15b0 --- /dev/null +++ b/etc/isar/AThousandTheorems.thy @@ -0,0 +1,1008 @@ +theory AThousandLines imports Main +begin + +(* set global_timing *) + +lemma foo: "P --> P" by auto +lemma foo2: "P --> P" by auto +lemma foo3: "P --> P" by auto +lemma foo4: "P --> P" by auto +lemma foo5: "P --> P" by auto +lemma foo6: "P --> P" by auto +lemma foo7: "P --> P" by auto +lemma foo8: "P --> P" by auto +lemma foo9: "P --> P" by auto +lemma foo10: "P --> P" by auto +lemma foo11: "P --> P" by auto +lemma foo12: "P --> P" by auto +lemma foo13: "P --> P" by auto +lemma foo14: "P --> P" by auto +lemma foo15: "P --> P" by auto +lemma foo16: "P --> P" by auto +lemma foo17: "P --> P" by auto +lemma foo18: "P --> P" by auto +lemma foo19: "P --> P" by auto +lemma foo20: "P --> P" by auto +lemma foo21: "P --> P" by auto +lemma foo22: "P --> P" by auto +lemma foo23: "P --> P" by auto +lemma foo24: "P --> P" by auto +lemma foo25: "P --> P" by auto +lemma foo26: "P --> P" by auto +lemma foo27: "P --> P" by auto +lemma foo28: "P --> P" by auto +lemma foo29: "P --> P" by auto +lemma foo30: "P --> P" by auto +lemma foo31: "P --> P" by auto +lemma foo32: "P --> P" by auto +lemma foo33: "P --> P" by auto +lemma foo34: "P --> P" by auto +lemma foo35: "P --> P" by auto +lemma foo36: "P --> P" by auto +lemma foo37: "P --> P" by auto +lemma foo38: "P --> P" by auto +lemma foo39: "P --> P" by auto +lemma foo40: "P --> P" by auto +lemma foo41: "P --> P" by auto +lemma foo42: "P --> P" by auto +lemma foo43: "P --> P" by auto +lemma foo44: "P --> P" by auto +lemma foo45: "P --> P" by auto +lemma foo46: "P --> P" by auto +lemma foo47: "P --> P" by auto +lemma foo48: "P --> P" by auto +lemma foo49: "P --> P" by auto +lemma foo50: "P --> P" by auto +lemma foo51: "P --> P" by auto +lemma foo52: "P --> P" by auto +lemma foo53: "P --> P" by auto +lemma foo54: "P --> P" by auto +lemma foo55: "P --> P" by auto +lemma foo56: "P --> P" by auto +lemma foo57: "P --> P" by auto +lemma foo58: "P --> P" by auto +lemma foo59: "P --> P" by auto +lemma foo60: "P --> P" by auto +lemma foo61: "P --> P" by auto +lemma foo62: "P --> P" by auto +lemma foo63: "P --> P" by auto +lemma foo64: "P --> P" by auto +lemma foo65: "P --> P" by auto +lemma foo66: "P --> P" by auto +lemma foo67: "P --> P" by auto +lemma foo68: "P --> P" by auto +lemma foo69: "P --> P" by auto +lemma foo70: "P --> P" by auto +lemma foo71: "P --> P" by auto +lemma foo72: "P --> P" by auto +lemma foo73: "P --> P" by auto +lemma foo74: "P --> P" by auto +lemma foo75: "P --> P" by auto +lemma foo76: "P --> P" by auto +lemma foo77: "P --> P" by auto +lemma foo78: "P --> P" by auto +lemma foo79: "P --> P" by auto +lemma foo80: "P --> P" by auto +lemma foo81: "P --> P" by auto +lemma foo82: "P --> P" by auto +lemma foo83: "P --> P" by auto +lemma foo84: "P --> P" by auto +lemma foo85: "P --> P" by auto +lemma foo86: "P --> P" by auto +lemma foo87: "P --> P" by auto +lemma foo88: "P --> P" by auto +lemma foo89: "P --> P" by auto +lemma foo90: "P --> P" by auto +lemma foo91: "P --> P" by auto +lemma foo92: "P --> P" by auto +lemma foo93: "P --> P" by auto +lemma foo94: "P --> P" by auto +lemma foo95: "P --> P" by auto +lemma foo96: "P --> P" by auto +lemma foo97: "P --> P" by auto +lemma foo98: "P --> P" by auto +lemma foo99: "P --> P" by auto +lemma foo100: "P --> P" by auto +lemma foo101: "P --> P" by auto +lemma foo102: "P --> P" by auto +lemma foo103: "P --> P" by auto +lemma foo104: "P --> P" by auto +lemma foo105: "P --> P" by auto +lemma foo106: "P --> P" by auto +lemma foo107: "P --> P" by auto +lemma foo108: "P --> P" by auto +lemma foo109: "P --> P" by auto +lemma foo110: "P --> P" by auto +lemma foo111: "P --> P" by auto +lemma foo112: "P --> P" by auto +lemma foo113: "P --> P" by auto +lemma foo114: "P --> P" by auto +lemma foo115: "P --> P" by auto +lemma foo116: "P --> P" by auto +lemma foo117: "P --> P" by auto +lemma foo118: "P --> P" by auto +lemma foo119: "P --> P" by auto +lemma foo120: "P --> P" by auto +lemma foo121: "P --> P" by auto +lemma foo122: "P --> P" by auto +lemma foo123: "P --> P" by auto +lemma foo124: "P --> P" by auto +lemma foo125: "P --> P" by auto +lemma foo126: "P --> P" by auto +lemma foo127: "P --> P" by auto +lemma foo128: "P --> P" by auto +lemma foo129: "P --> P" by auto +lemma foo130: "P --> P" by auto +lemma foo131: "P --> P" by auto +lemma foo132: "P --> P" by auto +lemma foo133: "P --> P" by auto +lemma foo134: "P --> P" by auto +lemma foo135: "P --> P" by auto +lemma foo136: "P --> P" by auto +lemma foo137: "P --> P" by auto +lemma foo138: "P --> P" by auto +lemma foo139: "P --> P" by auto +lemma foo140: "P --> P" by auto +lemma foo141: "P --> P" by auto +lemma foo142: "P --> P" by auto +lemma foo143: "P --> P" by auto +lemma foo144: "P --> P" by auto +lemma foo145: "P --> P" by auto +lemma foo146: "P --> P" by auto +lemma foo147: "P --> P" by auto +lemma foo148: "P --> P" by auto +lemma foo149: "P --> P" by auto +lemma foo150: "P --> P" by auto +lemma foo151: "P --> P" by auto +lemma foo152: "P --> P" by auto +lemma foo153: "P --> P" by auto +lemma foo154: "P --> P" by auto +lemma foo155: "P --> P" by auto +lemma foo156: "P --> P" by auto +lemma foo157: "P --> P" by auto +lemma foo158: "P --> P" by auto +lemma foo159: "P --> P" by auto +lemma foo160: "P --> P" by auto +lemma foo161: "P --> P" by auto +lemma foo162: "P --> P" by auto +lemma foo163: "P --> P" by auto +lemma foo164: "P --> P" by auto +lemma foo165: "P --> P" by auto +lemma foo166: "P --> P" by auto +lemma foo167: "P --> P" by auto +lemma foo168: "P --> P" by auto +lemma foo169: "P --> P" by auto +lemma foo170: "P --> P" by auto +lemma foo171: "P --> P" by auto +lemma foo172: "P --> P" by auto +lemma foo173: "P --> P" by auto +lemma foo174: "P --> P" by auto +lemma foo175: "P --> P" by auto +lemma foo176: "P --> P" by auto +lemma foo177: "P --> P" by auto +lemma foo178: "P --> P" by auto +lemma foo179: "P --> P" by auto +lemma foo180: "P --> P" by auto +lemma foo181: "P --> P" by auto +lemma foo182: "P --> P" by auto +lemma foo183: "P --> P" by auto +lemma foo184: "P --> P" by auto +lemma foo185: "P --> P" by auto +lemma foo186: "P --> P" by auto +lemma foo187: "P --> P" by auto +lemma foo188: "P --> P" by auto +lemma foo189: "P --> P" by auto +lemma foo190: "P --> P" by auto +lemma foo191: "P --> P" by auto +lemma foo192: "P --> P" by auto +lemma foo193: "P --> P" by auto +lemma foo194: "P --> P" by auto +lemma foo195: "P --> P" by auto +lemma foo196: "P --> P" by auto +lemma foo197: "P --> P" by auto +lemma foo198: "P --> P" by auto +lemma foo199: "P --> P" by auto +lemma foo200: "P --> P" by auto +lemma foo201: "P --> P" by auto +lemma foo202: "P --> P" by auto +lemma foo203: "P --> P" by auto +lemma foo204: "P --> P" by auto +lemma foo205: "P --> P" by auto +lemma foo206: "P --> P" by auto +lemma foo207: "P --> P" by auto +lemma foo208: "P --> P" by auto +lemma foo209: "P --> P" by auto +lemma foo210: "P --> P" by auto +lemma foo211: "P --> P" by auto +lemma foo212: "P --> P" by auto +lemma foo213: "P --> P" by auto +lemma foo214: "P --> P" by auto +lemma foo215: "P --> P" by auto +lemma foo216: "P --> P" by auto +lemma foo217: "P --> P" by auto +lemma foo218: "P --> P" by auto +lemma foo219: "P --> P" by auto +lemma foo220: "P --> P" by auto +lemma foo221: "P --> P" by auto +lemma foo222: "P --> P" by auto +lemma foo223: "P --> P" by auto +lemma foo224: "P --> P" by auto +lemma foo225: "P --> P" by auto +lemma foo226: "P --> P" by auto +lemma foo227: "P --> P" by auto +lemma foo228: "P --> P" by auto +lemma foo229: "P --> P" by auto +lemma foo230: "P --> P" by auto +lemma foo231: "P --> P" by auto +lemma foo232: "P --> P" by auto +lemma foo233: "P --> P" by auto +lemma foo234: "P --> P" by auto +lemma foo235: "P --> P" by auto +lemma foo236: "P --> P" by auto +lemma foo237: "P --> P" by auto +lemma foo238: "P --> P" by auto +lemma foo239: "P --> P" by auto +lemma foo240: "P --> P" by auto +lemma foo241: "P --> P" by auto +lemma foo242: "P --> P" by auto +lemma foo243: "P --> P" by auto +lemma foo244: "P --> P" by auto +lemma foo245: "P --> P" by auto +lemma foo246: "P --> P" by auto +lemma foo247: "P --> P" by auto +lemma foo248: "P --> P" by auto +lemma foo249: "P --> P" by auto +lemma foo250: "P --> P" by auto +lemma foo251: "P --> P" by auto +lemma foo252: "P --> P" by auto +lemma foo253: "P --> P" by auto +lemma foo254: "P --> P" by auto +lemma foo255: "P --> P" by auto +lemma foo256: "P --> P" by auto +lemma foo257: "P --> P" by auto +lemma foo258: "P --> P" by auto +lemma foo259: "P --> P" by auto +lemma foo260: "P --> P" by auto +lemma foo261: "P --> P" by auto +lemma foo262: "P --> P" by auto +lemma foo263: "P --> P" by auto +lemma foo264: "P --> P" by auto +lemma foo265: "P --> P" by auto +lemma foo266: "P --> P" by auto +lemma foo267: "P --> P" by auto +lemma foo268: "P --> P" by auto +lemma foo269: "P --> P" by auto +lemma foo270: "P --> P" by auto +lemma foo271: "P --> P" by auto +lemma foo272: "P --> P" by auto +lemma foo273: "P --> P" by auto +lemma foo274: "P --> P" by auto +lemma foo275: "P --> P" by auto +lemma foo276: "P --> P" by auto +lemma foo277: "P --> P" by auto +lemma foo278: "P --> P" by auto +lemma foo279: "P --> P" by auto +lemma foo280: "P --> P" by auto +lemma foo281: "P --> P" by auto +lemma foo282: "P --> P" by auto +lemma foo283: "P --> P" by auto +lemma foo284: "P --> P" by auto +lemma foo285: "P --> P" by auto +lemma foo286: "P --> P" by auto +lemma foo287: "P --> P" by auto +lemma foo288: "P --> P" by auto +lemma foo289: "P --> P" by auto +lemma foo290: "P --> P" by auto +lemma foo291: "P --> P" by auto +lemma foo292: "P --> P" by auto +lemma foo293: "P --> P" by auto +lemma foo294: "P --> P" by auto +lemma foo295: "P --> P" by auto +lemma foo296: "P --> P" by auto +lemma foo297: "P --> P" by auto +lemma foo298: "P --> P" by auto +lemma foo299: "P --> P" by auto +lemma foo300: "P --> P" by auto +lemma foo301: "P --> P" by auto +lemma foo302: "P --> P" by auto +lemma foo303: "P --> P" by auto +lemma foo304: "P --> P" by auto +lemma foo305: "P --> P" by auto +lemma foo306: "P --> P" by auto +lemma foo307: "P --> P" by auto +lemma foo308: "P --> P" by auto +lemma foo309: "P --> P" by auto +lemma foo310: "P --> P" by auto +lemma foo311: "P --> P" by auto +lemma foo312: "P --> P" by auto +lemma foo313: "P --> P" by auto +lemma foo314: "P --> P" by auto +lemma foo315: "P --> P" by auto +lemma foo316: "P --> P" by auto +lemma foo317: "P --> P" by auto +lemma foo318: "P --> P" by auto +lemma foo319: "P --> P" by auto +lemma foo320: "P --> P" by auto +lemma foo321: "P --> P" by auto +lemma foo322: "P --> P" by auto +lemma foo323: "P --> P" by auto +lemma foo324: "P --> P" by auto +lemma foo325: "P --> P" by auto +lemma foo326: "P --> P" by auto +lemma foo327: "P --> P" by auto +lemma foo328: "P --> P" by auto +lemma foo329: "P --> P" by auto +lemma foo330: "P --> P" by auto +lemma foo331: "P --> P" by auto +lemma foo332: "P --> P" by auto +lemma foo333: "P --> P" by auto +lemma foo334: "P --> P" by auto +lemma foo335: "P --> P" by auto +lemma foo336: "P --> P" by auto +lemma foo337: "P --> P" by auto +lemma foo338: "P --> P" by auto +lemma foo339: "P --> P" by auto +lemma foo340: "P --> P" by auto +lemma foo341: "P --> P" by auto +lemma foo342: "P --> P" by auto +lemma foo343: "P --> P" by auto +lemma foo344: "P --> P" by auto +lemma foo345: "P --> P" by auto +lemma foo346: "P --> P" by auto +lemma foo347: "P --> P" by auto +lemma foo348: "P --> P" by auto +lemma foo349: "P --> P" by auto +lemma foo350: "P --> P" by auto +lemma foo351: "P --> P" by auto +lemma foo352: "P --> P" by auto +lemma foo353: "P --> P" by auto +lemma foo354: "P --> P" by auto +lemma foo355: "P --> P" by auto +lemma foo356: "P --> P" by auto +lemma foo357: "P --> P" by auto +lemma foo358: "P --> P" by auto +lemma foo359: "P --> P" by auto +lemma foo360: "P --> P" by auto +lemma foo361: "P --> P" by auto +lemma foo362: "P --> P" by auto +lemma foo363: "P --> P" by auto +lemma foo364: "P --> P" by auto +lemma foo365: "P --> P" by auto +lemma foo366: "P --> P" by auto +lemma foo367: "P --> P" by auto +lemma foo368: "P --> P" by auto +lemma foo369: "P --> P" by auto +lemma foo370: "P --> P" by auto +lemma foo371: "P --> P" by auto +lemma foo372: "P --> P" by auto +lemma foo373: "P --> P" by auto +lemma foo374: "P --> P" by auto +lemma foo375: "P --> P" by auto +lemma foo376: "P --> P" by auto +lemma foo377: "P --> P" by auto +lemma foo378: "P --> P" by auto +lemma foo379: "P --> P" by auto +lemma foo380: "P --> P" by auto +lemma foo381: "P --> P" by auto +lemma foo382: "P --> P" by auto +lemma foo383: "P --> P" by auto +lemma foo384: "P --> P" by auto +lemma foo385: "P --> P" by auto +lemma foo386: "P --> P" by auto +lemma foo387: "P --> P" by auto +lemma foo388: "P --> P" by auto +lemma foo389: "P --> P" by auto +lemma foo390: "P --> P" by auto +lemma foo391: "P --> P" by auto +lemma foo392: "P --> P" by auto +lemma foo393: "P --> P" by auto +lemma foo394: "P --> P" by auto +lemma foo395: "P --> P" by auto +lemma foo396: "P --> P" by auto +lemma foo397: "P --> P" by auto +lemma foo398: "P --> P" by auto +lemma foo399: "P --> P" by auto +lemma foo400: "P --> P" by auto +lemma foo401: "P --> P" by auto +lemma foo402: "P --> P" by auto +lemma foo403: "P --> P" by auto +lemma foo404: "P --> P" by auto +lemma foo405: "P --> P" by auto +lemma foo406: "P --> P" by auto +lemma foo407: "P --> P" by auto +lemma foo408: "P --> P" by auto +lemma foo409: "P --> P" by auto +lemma foo410: "P --> P" by auto +lemma foo411: "P --> P" by auto +lemma foo412: "P --> P" by auto +lemma foo413: "P --> P" by auto +lemma foo414: "P --> P" by auto +lemma foo415: "P --> P" by auto +lemma foo416: "P --> P" by auto +lemma foo417: "P --> P" by auto +lemma foo418: "P --> P" by auto +lemma foo419: "P --> P" by auto +lemma foo420: "P --> P" by auto +lemma foo421: "P --> P" by auto +lemma foo422: "P --> P" by auto +lemma foo423: "P --> P" by auto +lemma foo424: "P --> P" by auto +lemma foo425: "P --> P" by auto +lemma foo426: "P --> P" by auto +lemma foo427: "P --> P" by auto +lemma foo428: "P --> P" by auto +lemma foo429: "P --> P" by auto +lemma foo430: "P --> P" by auto +lemma foo431: "P --> P" by auto +lemma foo432: "P --> P" by auto +lemma foo433: "P --> P" by auto +lemma foo434: "P --> P" by auto +lemma foo435: "P --> P" by auto +lemma foo436: "P --> P" by auto +lemma foo437: "P --> P" by auto +lemma foo438: "P --> P" by auto +lemma foo439: "P --> P" by auto +lemma foo440: "P --> P" by auto +lemma foo441: "P --> P" by auto +lemma foo442: "P --> P" by auto +lemma foo443: "P --> P" by auto +lemma foo444: "P --> P" by auto +lemma foo445: "P --> P" by auto +lemma foo446: "P --> P" by auto +lemma foo447: "P --> P" by auto +lemma foo448: "P --> P" by auto +lemma foo449: "P --> P" by auto +lemma foo450: "P --> P" by auto +lemma foo451: "P --> P" by auto +lemma foo452: "P --> P" by auto +lemma foo453: "P --> P" by auto +lemma foo454: "P --> P" by auto +lemma foo455: "P --> P" by auto +lemma foo456: "P --> P" by auto +lemma foo457: "P --> P" by auto +lemma foo458: "P --> P" by auto +lemma foo459: "P --> P" by auto +lemma foo460: "P --> P" by auto +lemma foo461: "P --> P" by auto +lemma foo462: "P --> P" by auto +lemma foo463: "P --> P" by auto +lemma foo464: "P --> P" by auto +lemma foo465: "P --> P" by auto +lemma foo466: "P --> P" by auto +lemma foo467: "P --> P" by auto +lemma foo468: "P --> P" by auto +lemma foo469: "P --> P" by auto +lemma foo470: "P --> P" by auto +lemma foo471: "P --> P" by auto +lemma foo472: "P --> P" by auto +lemma foo473: "P --> P" by auto +lemma foo474: "P --> P" by auto +lemma foo475: "P --> P" by auto +lemma foo476: "P --> P" by auto +lemma foo477: "P --> P" by auto +lemma foo478: "P --> P" by auto +lemma foo479: "P --> P" by auto +lemma foo480: "P --> P" by auto +lemma foo481: "P --> P" by auto +lemma foo482: "P --> P" by auto +lemma foo483: "P --> P" by auto +lemma foo484: "P --> P" by auto +lemma foo485: "P --> P" by auto +lemma foo486: "P --> P" by auto +lemma foo487: "P --> P" by auto +lemma foo488: "P --> P" by auto +lemma foo489: "P --> P" by auto +lemma foo490: "P --> P" by auto +lemma foo491: "P --> P" by auto +lemma foo492: "P --> P" by auto +lemma foo493: "P --> P" by auto +lemma foo494: "P --> P" by auto +lemma foo495: "P --> P" by auto +lemma foo496: "P --> P" by auto +lemma foo497: "P --> P" by auto +lemma foo498: "P --> P" by auto +lemma foo499: "P --> P" by auto +lemma foo500: "P --> P" by auto +(*lemma foo500: "P --> P" by auto *) +lemma foo501: "P --> P" by auto +lemma foo502: "P --> P" by auto +lemma foo503: "P --> P" by auto +lemma foo504: "P --> P" by auto +lemma foo505: "P --> P" by auto +lemma foo506: "P --> P" by auto +lemma foo507: "P --> P" by auto +lemma foo508: "P --> P" by auto +lemma foo509: "P --> P" by auto +lemma foo510: "P --> P" by auto +lemma foo511: "P --> P" by auto +lemma foo512: "P --> P" by auto +lemma foo513: "P --> P" by auto +lemma foo514: "P --> P" by auto +lemma foo515: "P --> P" by auto +lemma foo516: "P --> P" by auto +lemma foo517: "P --> P" by auto +lemma foo518: "P --> P" by auto +lemma foo519: "P --> P" by auto +lemma foo520: "P --> P" by auto +lemma foo521: "P --> P" by auto +lemma foo522: "P --> P" by auto +lemma foo523: "P --> P" by auto +lemma foo524: "P --> P" by auto +lemma foo525: "P --> P" by auto +lemma foo526: "P --> P" by auto +lemma foo527: "P --> P" by auto +lemma foo528: "P --> P" by auto +lemma foo529: "P --> P" by auto +lemma foo530: "P --> P" by auto +lemma foo531: "P --> P" by auto +lemma foo532: "P --> P" by auto +lemma foo533: "P --> P" by auto +lemma foo534: "P --> P" by auto +lemma foo535: "P --> P" by auto +lemma foo536: "P --> P" by auto +lemma foo537: "P --> P" by auto +lemma foo538: "P --> P" by auto +lemma foo539: "P --> P" by auto +lemma foo540: "P --> P" by auto +lemma foo541: "P --> P" by auto +lemma foo542: "P --> P" by auto +lemma foo543: "P --> P" by auto +lemma foo544: "P --> P" by auto +lemma foo545: "P --> P" by auto +lemma foo546: "P --> P" by auto +lemma foo547: "P --> P" by auto +lemma foo548: "P --> P" by auto +lemma foo549: "P --> P" by auto +lemma foo550: "P --> P" by auto +lemma foo551: "P --> P" by auto +lemma foo552: "P --> P" by auto +lemma foo553: "P --> P" by auto +lemma foo554: "P --> P" by auto +lemma foo555: "P --> P" by auto +lemma foo556: "P --> P" by auto +lemma foo557: "P --> P" by auto +lemma foo558: "P --> P" by auto +lemma foo559: "P --> P" by auto +lemma foo560: "P --> P" by auto +lemma foo561: "P --> P" by auto +lemma foo562: "P --> P" by auto +lemma foo563: "P --> P" by auto +lemma foo564: "P --> P" by auto +lemma foo565: "P --> P" by auto +lemma foo566: "P --> P" by auto +lemma foo567: "P --> P" by auto +lemma foo568: "P --> P" by auto +lemma foo569: "P --> P" by auto +lemma foo570: "P --> P" by auto +lemma foo571: "P --> P" by auto +lemma foo572: "P --> P" by auto +lemma foo573: "P --> P" by auto +lemma foo574: "P --> P" by auto +lemma foo575: "P --> P" by auto +lemma foo576: "P --> P" by auto +lemma foo577: "P --> P" by auto +lemma foo578: "P --> P" by auto +lemma foo579: "P --> P" by auto +lemma foo580: "P --> P" by auto +lemma foo581: "P --> P" by auto +lemma foo582: "P --> P" by auto +lemma foo583: "P --> P" by auto +lemma foo584: "P --> P" by auto +lemma foo585: "P --> P" by auto +lemma foo586: "P --> P" by auto +lemma foo587: "P --> P" by auto +lemma foo588: "P --> P" by auto +lemma foo589: "P --> P" by auto +lemma foo590: "P --> P" by auto +lemma foo591: "P --> P" by auto +lemma foo592: "P --> P" by auto +lemma foo593: "P --> P" by auto +lemma foo594: "P --> P" by auto +lemma foo595: "P --> P" by auto +lemma foo596: "P --> P" by auto +lemma foo597: "P --> P" by auto +lemma foo598: "P --> P" by auto +lemma foo599: "P --> P" by auto +lemma foo600: "P --> P" by auto +lemma foo601: "P --> P" by auto +lemma foo602: "P --> P" by auto +lemma foo603: "P --> P" by auto +lemma foo604: "P --> P" by auto +lemma foo605: "P --> P" by auto +lemma foo606: "P --> P" by auto +lemma foo607: "P --> P" by auto +lemma foo608: "P --> P" by auto +lemma foo609: "P --> P" by auto +lemma foo610: "P --> P" by auto +lemma foo611: "P --> P" by auto +lemma foo612: "P --> P" by auto +lemma foo613: "P --> P" by auto +lemma foo614: "P --> P" by auto +lemma foo615: "P --> P" by auto +lemma foo616: "P --> P" by auto +lemma foo617: "P --> P" by auto +lemma foo618: "P --> P" by auto +lemma foo619: "P --> P" by auto +lemma foo620: "P --> P" by auto +lemma foo621: "P --> P" by auto +lemma foo622: "P --> P" by auto +lemma foo623: "P --> P" by auto +lemma foo624: "P --> P" by auto +lemma foo625: "P --> P" by auto +lemma foo626: "P --> P" by auto +lemma foo627: "P --> P" by auto +lemma foo628: "P --> P" by auto +lemma foo629: "P --> P" by auto +lemma foo630: "P --> P" by auto +lemma foo631: "P --> P" by auto +lemma foo632: "P --> P" by auto +lemma foo633: "P --> P" by auto +lemma foo634: "P --> P" by auto +lemma foo635: "P --> P" by auto +lemma foo636: "P --> P" by auto +lemma foo637: "P --> P" by auto +lemma foo638: "P --> P" by auto +lemma foo639: "P --> P" by auto +lemma foo640: "P --> P" by auto +lemma foo641: "P --> P" by auto +lemma foo642: "P --> P" by auto +lemma foo643: "P --> P" by auto +lemma foo644: "P --> P" by auto +lemma foo645: "P --> P" by auto +lemma foo646: "P --> P" by auto +lemma foo647: "P --> P" by auto +lemma foo648: "P --> P" by auto +lemma foo649: "P --> P" by auto +lemma foo650: "P --> P" by auto +lemma foo651: "P --> P" by auto +lemma foo652: "P --> P" by auto +lemma foo653: "P --> P" by auto +lemma foo654: "P --> P" by auto +lemma foo655: "P --> P" by auto +lemma foo656: "P --> P" by auto +lemma foo657: "P --> P" by auto +lemma foo658: "P --> P" by auto +lemma foo659: "P --> P" by auto +lemma foo660: "P --> P" by auto +lemma foo661: "P --> P" by auto +lemma foo662: "P --> P" by auto +lemma foo663: "P --> P" by auto +lemma foo664: "P --> P" by auto +lemma foo665: "P --> P" by auto +lemma foo666: "P --> P" by auto +lemma foo667: "P --> P" by auto +lemma foo668: "P --> P" by auto +lemma foo669: "P --> P" by auto +lemma foo670: "P --> P" by auto +lemma foo671: "P --> P" by auto +lemma foo672: "P --> P" by auto +lemma foo673: "P --> P" by auto +lemma foo674: "P --> P" by auto +lemma foo675: "P --> P" by auto +lemma foo676: "P --> P" by auto +lemma foo677: "P --> P" by auto +lemma foo678: "P --> P" by auto +lemma foo679: "P --> P" by auto +lemma foo680: "P --> P" by auto +lemma foo681: "P --> P" by auto +lemma foo682: "P --> P" by auto +lemma foo683: "P --> P" by auto +lemma foo684: "P --> P" by auto +lemma foo685: "P --> P" by auto +lemma foo686: "P --> P" by auto +lemma foo687: "P --> P" by auto +lemma foo688: "P --> P" by auto +lemma foo689: "P --> P" by auto +lemma foo690: "P --> P" by auto +lemma foo691: "P --> P" by auto +lemma foo692: "P --> P" by auto +lemma foo693: "P --> P" by auto +lemma foo694: "P --> P" by auto +lemma foo695: "P --> P" by auto +lemma foo696: "P --> P" by auto +lemma foo697: "P --> P" by auto +lemma foo698: "P --> P" by auto +lemma foo699: "P --> P" by auto +lemma foo700: "P --> P" by auto +lemma foo701: "P --> P" by auto +lemma foo702: "P --> P" by auto +lemma foo703: "P --> P" by auto +lemma foo704: "P --> P" by auto +lemma foo705: "P --> P" by auto +lemma foo706: "P --> P" by auto +lemma foo707: "P --> P" by auto +lemma foo708: "P --> P" by auto +lemma foo709: "P --> P" by auto +lemma foo710: "P --> P" by auto +lemma foo711: "P --> P" by auto +lemma foo712: "P --> P" by auto +lemma foo713: "P --> P" by auto +lemma foo714: "P --> P" by auto +lemma foo715: "P --> P" by auto +lemma foo716: "P --> P" by auto +lemma foo717: "P --> P" by auto +lemma foo718: "P --> P" by auto +lemma foo719: "P --> P" by auto +lemma foo720: "P --> P" by auto +lemma foo721: "P --> P" by auto +lemma foo722: "P --> P" by auto +lemma foo723: "P --> P" by auto +lemma foo724: "P --> P" by auto +lemma foo725: "P --> P" by auto +lemma foo726: "P --> P" by auto +lemma foo727: "P --> P" by auto +lemma foo728: "P --> P" by auto +lemma foo729: "P --> P" by auto +lemma foo730: "P --> P" by auto +lemma foo731: "P --> P" by auto +lemma foo732: "P --> P" by auto +lemma foo733: "P --> P" by auto +lemma foo734: "P --> P" by auto +lemma foo735: "P --> P" by auto +lemma foo736: "P --> P" by auto +lemma foo737: "P --> P" by auto +lemma foo738: "P --> P" by auto +lemma foo739: "P --> P" by auto +lemma foo740: "P --> P" by auto +lemma foo741: "P --> P" by auto +lemma foo742: "P --> P" by auto +lemma foo743: "P --> P" by auto +lemma foo744: "P --> P" by auto +lemma foo745: "P --> P" by auto +lemma foo746: "P --> P" by auto +lemma foo747: "P --> P" by auto +lemma foo748: "P --> P" by auto +lemma foo749: "P --> P" by auto +lemma foo750: "P --> P" by auto +lemma foo751: "P --> P" by auto +lemma foo752: "P --> P" by auto +lemma foo753: "P --> P" by auto +lemma foo754: "P --> P" by auto +lemma foo755: "P --> P" by auto +lemma foo756: "P --> P" by auto +lemma foo757: "P --> P" by auto +lemma foo758: "P --> P" by auto +lemma foo759: "P --> P" by auto +lemma foo760: "P --> P" by auto +lemma foo761: "P --> P" by auto +lemma foo762: "P --> P" by auto +lemma foo763: "P --> P" by auto +lemma foo764: "P --> P" by auto +lemma foo765: "P --> P" by auto +lemma foo766: "P --> P" by auto +lemma foo767: "P --> P" by auto +lemma foo768: "P --> P" by auto +lemma foo769: "P --> P" by auto +lemma foo770: "P --> P" by auto +lemma foo771: "P --> P" by auto +lemma foo772: "P --> P" by auto +lemma foo773: "P --> P" by auto +lemma foo774: "P --> P" by auto +lemma foo775: "P --> P" by auto +lemma foo776: "P --> P" by auto +lemma foo777: "P --> P" by auto +lemma foo778: "P --> P" by auto +lemma foo779: "P --> P" by auto +lemma foo780: "P --> P" by auto +lemma foo781: "P --> P" by auto +lemma foo782: "P --> P" by auto +lemma foo783: "P --> P" by auto +lemma foo784: "P --> P" by auto +lemma foo785: "P --> P" by auto +lemma foo786: "P --> P" by auto +lemma foo787: "P --> P" by auto +lemma foo788: "P --> P" by auto +lemma foo789: "P --> P" by auto +lemma foo790: "P --> P" by auto +lemma foo791: "P --> P" by auto +lemma foo792: "P --> P" by auto +lemma foo793: "P --> P" by auto +lemma foo794: "P --> P" by auto +lemma foo795: "P --> P" by auto +lemma foo796: "P --> P" by auto +lemma foo797: "P --> P" by auto +lemma foo798: "P --> P" by auto +lemma foo799: "P --> P" by auto +lemma foo800: "P --> P" by auto +lemma foo801: "P --> P" by auto +lemma foo802: "P --> P" by auto +lemma foo803: "P --> P" by auto +lemma foo804: "P --> P" by auto +lemma foo805: "P --> P" by auto +lemma foo806: "P --> P" by auto +lemma foo807: "P --> P" by auto +lemma foo808: "P --> P" by auto +lemma foo809: "P --> P" by auto +lemma foo810: "P --> P" by auto +lemma foo811: "P --> P" by auto +lemma foo812: "P --> P" by auto +lemma foo813: "P --> P" by auto +lemma foo814: "P --> P" by auto +lemma foo815: "P --> P" by auto +lemma foo816: "P --> P" by auto +lemma foo817: "P --> P" by auto +lemma foo818: "P --> P" by auto +lemma foo819: "P --> P" by auto +lemma foo820: "P --> P" by auto +lemma foo821: "P --> P" by auto +lemma foo822: "P --> P" by auto +lemma foo823: "P --> P" by auto +lemma foo824: "P --> P" by auto +lemma foo825: "P --> P" by auto +lemma foo826: "P --> P" by auto +lemma foo827: "P --> P" by auto +lemma foo828: "P --> P" by auto +lemma foo829: "P --> P" by auto +lemma foo830: "P --> P" by auto +lemma foo831: "P --> P" by auto +lemma foo832: "P --> P" by auto +lemma foo833: "P --> P" by auto +lemma foo834: "P --> P" by auto +lemma foo835: "P --> P" by auto +lemma foo836: "P --> P" by auto +lemma foo837: "P --> P" by auto +lemma foo838: "P --> P" by auto +lemma foo839: "P --> P" by auto +lemma foo840: "P --> P" by auto +lemma foo841: "P --> P" by auto +lemma foo842: "P --> P" by auto +lemma foo843: "P --> P" by auto +lemma foo844: "P --> P" by auto +lemma foo845: "P --> P" by auto +lemma foo846: "P --> P" by auto +lemma foo847: "P --> P" by auto +lemma foo848: "P --> P" by auto +lemma foo849: "P --> P" by auto +lemma foo850: "P --> P" by auto +lemma foo851: "P --> P" by auto +lemma foo852: "P --> P" by auto +lemma foo853: "P --> P" by auto +lemma foo854: "P --> P" by auto +lemma foo855: "P --> P" by auto +lemma foo856: "P --> P" by auto +lemma foo857: "P --> P" by auto +lemma foo858: "P --> P" by auto +lemma foo859: "P --> P" by auto +lemma foo860: "P --> P" by auto +lemma foo861: "P --> P" by auto +lemma foo862: "P --> P" by auto +lemma foo863: "P --> P" by auto +lemma foo864: "P --> P" by auto +lemma foo865: "P --> P" by auto +lemma foo866: "P --> P" by auto +lemma foo867: "P --> P" by auto +lemma foo868: "P --> P" by auto +lemma foo869: "P --> P" by auto +lemma foo870: "P --> P" by auto +lemma foo871: "P --> P" by auto +lemma foo872: "P --> P" by auto +lemma foo873: "P --> P" by auto +lemma foo874: "P --> P" by auto +lemma foo875: "P --> P" by auto +lemma foo876: "P --> P" by auto +lemma foo877: "P --> P" by auto +lemma foo878: "P --> P" by auto +lemma foo879: "P --> P" by auto +lemma foo880: "P --> P" by auto +lemma foo881: "P --> P" by auto +lemma foo882: "P --> P" by auto +lemma foo883: "P --> P" by auto +lemma foo884: "P --> P" by auto +lemma foo885: "P --> P" by auto +lemma foo886: "P --> P" by auto +lemma foo887: "P --> P" by auto +lemma foo888: "P --> P" by auto +lemma foo889: "P --> P" by auto +lemma foo890: "P --> P" by auto +lemma foo891: "P --> P" by auto +lemma foo892: "P --> P" by auto +lemma foo893: "P --> P" by auto +lemma foo894: "P --> P" by auto +lemma foo895: "P --> P" by auto +lemma foo896: "P --> P" by auto +lemma foo897: "P --> P" by auto +lemma foo898: "P --> P" by auto +lemma foo899: "P --> P" by auto +lemma foo900: "P --> P" by auto +lemma foo901: "P --> P" by auto +lemma foo902: "P --> P" by auto +lemma foo903: "P --> P" by auto +lemma foo904: "P --> P" by auto +lemma foo905: "P --> P" by auto +lemma foo906: "P --> P" by auto +lemma foo907: "P --> P" by auto +lemma foo908: "P --> P" by auto +lemma foo909: "P --> P" by auto +lemma foo910: "P --> P" by auto +lemma foo911: "P --> P" by auto +lemma foo912: "P --> P" by auto +lemma foo913: "P --> P" by auto +lemma foo914: "P --> P" by auto +lemma foo915: "P --> P" by auto +lemma foo916: "P --> P" by auto +lemma foo917: "P --> P" by auto +lemma foo918: "P --> P" by auto +lemma foo919: "P --> P" by auto +lemma foo920: "P --> P" by auto +lemma foo921: "P --> P" by auto +lemma foo922: "P --> P" by auto +lemma foo923: "P --> P" by auto +lemma foo924: "P --> P" by auto +lemma foo925: "P --> P" by auto +lemma foo926: "P --> P" by auto +lemma foo927: "P --> P" by auto +lemma foo928: "P --> P" by auto +lemma foo929: "P --> P" by auto +lemma foo930: "P --> P" by auto +lemma foo931: "P --> P" by auto +lemma foo932: "P --> P" by auto +lemma foo933: "P --> P" by auto +lemma foo934: "P --> P" by auto +lemma foo935: "P --> P" by auto +lemma foo936: "P --> P" by auto +lemma foo937: "P --> P" by auto +lemma foo938: "P --> P" by auto +lemma foo939: "P --> P" by auto +lemma foo940: "P --> P" by auto +lemma foo941: "P --> P" by auto +lemma foo942: "P --> P" by auto +lemma foo943: "P --> P" by auto +lemma foo944: "P --> P" by auto +lemma foo945: "P --> P" by auto +lemma foo946: "P --> P" by auto +lemma foo947: "P --> P" by auto +lemma foo948: "P --> P" by auto +lemma foo949: "P --> P" by auto +lemma foo950: "P --> P" by auto +lemma foo951: "P --> P" by auto +lemma foo952: "P --> P" by auto +lemma foo953: "P --> P" by auto +lemma foo954: "P --> P" by auto +lemma foo955: "P --> P" by auto +lemma foo956: "P --> P" by auto +lemma foo957: "P --> P" by auto +lemma foo958: "P --> P" by auto +lemma foo959: "P --> P" by auto +lemma foo960: "P --> P" by auto +lemma foo961: "P --> P" by auto +lemma foo962: "P --> P" by auto +lemma foo963: "P --> P" by auto +lemma foo964: "P --> P" by auto +lemma foo965: "P --> P" by auto +lemma foo966: "P --> P" by auto +lemma foo967: "P --> P" by auto +lemma foo968: "P --> P" by auto +lemma foo969: "P --> P" by auto +lemma foo970: "P --> P" by auto +lemma foo971: "P --> P" by auto +lemma foo972: "P --> P" by auto +lemma foo973: "P --> P" by auto +lemma foo974: "P --> P" by auto +lemma foo975: "P --> P" by auto +lemma foo976: "P --> P" by auto +lemma foo977: "P --> P" by auto +lemma foo978: "P --> P" by auto +lemma foo979: "P --> P" by auto +lemma foo980: "P --> P" by auto +lemma foo981: "P --> P" by auto +lemma foo982: "P --> P" by auto +lemma foo983: "P --> P" by auto +lemma foo984: "P --> P" by auto +lemma foo985: "P --> P" by auto +lemma foo986: "P --> P" by auto +lemma foo987: "P --> P" by auto +lemma foo988: "P --> P" by auto +lemma foo989: "P --> P" by auto +lemma foo990: "P --> P" by auto +lemma foo991: "P --> P" by auto +lemma foo992: "P --> P" by auto +lemma foo993: "P --> P" by auto +lemma foo994: "P --> P" by auto +lemma foo995: "P --> P" by auto +lemma foo996: "P --> P" by auto +lemma foo997: "P --> P" by auto +lemma foo998: "P --> P" by auto +lemma foo999: "P --> P" by auto +lemma foo1000: "P --> P" by auto + +end diff --git a/etc/isar/CommentParsingBug.thy b/etc/isar/CommentParsingBug.thy index e279fb68..6a59a383 100644 --- a/etc/isar/CommentParsingBug.thy +++ b/etc/isar/CommentParsingBug.thy @@ -1,3 +1,3 @@ (**)(**) -theory Scratch = Main: +theory Scratch imports Main begin diff --git a/etc/isar/CommentParsingBug2.thy b/etc/isar/CommentParsingBug2.thy index e92bd687..0c1a303e 100644 --- a/etc/isar/CommentParsingBug2.thy +++ b/etc/isar/CommentParsingBug2.thy @@ -1,5 +1,5 @@ (* Tobias reported 24.1.03. Could not repeat prob *) -theory test = Main: +theory test imports Main begin (* defs diff --git a/etc/isar/Depends.thy b/etc/isar/Depends.thy index d69e663d..2d13c0f4 100644 --- a/etc/isar/Depends.thy +++ b/etc/isar/Depends.thy @@ -1,6 +1,6 @@ (* In order to test the latest thm deps setup, consider this example: *) -theory Depends = Main: +theory Depends imports Main begin lemma I: "A ==> A" and K: "A ==> B ==> A" . @@ -8,8 +8,6 @@ theory Depends = Main: This reports I, K depending on several things; for your internal dependency graph you may interpret this as each member of {I, K} depending on all the deps. - - Markus *) end diff --git a/etc/isar/FaultyErrors.thy b/etc/isar/FaultyErrors.thy index 81e8be1d..5106ce75 100644 --- a/etc/isar/FaultyErrors.thy +++ b/etc/isar/FaultyErrors.thy @@ -3,8 +3,8 @@ begin lemma foo: "P --> P" by auto -ML_setup {* Output.error_msg "Fake error"; *} (* now *not* an error *) -ML_setup {* error "Real error" :unit; *} (* a true error, command fails *) +ML {* Output.error_msg "Fake error"; *} (* now *not* an error *) +ML {* error "Real error" :unit; *} (* a true error, command fails *) (* After an error message, the system wrongly thinks the command has succeeded, currently 03.01.07. diff --git a/etc/isar/Fibonacci.thy b/etc/isar/Fibonacci.thy index 0cbc8090..8e57b459 100644 --- a/etc/isar/Fibonacci.thy +++ b/etc/isar/Fibonacci.thy @@ -1,25 +1,47 @@ -(* Fibonacci.thy taken from Isabelle distribution - Gertrud Bauer / Larry Paulson *) +(* Title: HOL/Isar_examples/Fibonacci.thy + ID: $Id$ + Author: Gertrud Bauer + Copyright 1999 Technische Universitaet Muenchen + +The Fibonacci function. Demonstrates the use of recdef. Original +tactic script by Lawrence C Paulson. + +Fibonacci numbers: proofs of laws taken from + + R. L. Graham, D. E. Knuth, O. Patashnik. + Concrete Mathematics. + (Addison-Wesley, 1989) +*) + +header {* Fib and Gcd commute *} + +theory Fibonacci +imports Primes +begin + +text_raw {* + \footnote{Isar version by Gertrud Bauer. Original tactic script by + Larry Paulson. A few proofs of laws taken from + \cite{Concrete-Math}.} +*} -theory Fibonacci = Primes: subsection {* Fibonacci numbers *} -consts fib :: "nat => nat" -recdef fib less_than - "fib 0 = 0" - "fib (Suc 0) = 1" - "fib (Suc (Suc x)) = fib x + fib (Suc x)" +fun fib :: "nat \<Rightarrow> nat" where + "fib 0 = 0" + | "fib (Suc 0) = 1" + | "fib (Suc (Suc x)) = fib x + fib (Suc x)" lemma [simp]: "0 < fib (Suc n)" - by (induct n rule: fib.induct) (simp+) + by (induct n rule: fib.induct) simp_all text {* Alternative induction rule. *} theorem fib_induct: - "\<lbrakk>P 0; P 1; \<And>n. \<lbrakk>P (n + 1); P n\<rbrakk> \<Longrightarrow> P (n + 2)\<rbrakk> \<Longrightarrow> P (n::nat)" - by (induct rule: fib.induct, simp+) + "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)" + by (induct rule: fib.induct) simp_all subsection {* Fib and gcd commute *} @@ -48,102 +70,97 @@ proof (induct n rule: fib_induct) finally show "?P (n + 2)" . qed -lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n") +lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n") proof (induct n rule: fib_induct) show "?P 0" by simp show "?P 1" by simp fix n have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)" by simp - also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))" + also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))" by (simp only: gcd_add2') - also have "... = gcd (fib (n + 1), fib (n + 1 + 1))" + also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))" by (simp add: gcd_commute) also assume "... = 1" finally show "?P (n + 2)" . qed -lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)" +lemma gcd_mult_add: "0 < n ==> gcd (n * k + m) n = gcd m n" proof - assume "0 < n" - hence "gcd (n * k + m, n) = gcd (n, m mod n)" + then have "gcd (n * k + m) n = gcd n (m mod n)" by (simp add: gcd_non_0 add_commute) - also have "... = gcd (m, n)" by (simp! add: gcd_non_0) + also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0) finally show ?thesis . qed -lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)" +lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" proof (cases m) - assume "m = 0" - thus ?thesis by simp + case 0 + then show ?thesis by simp next - fix k assume "m = Suc k" - hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))" + case (Suc k) + then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))" by (simp add: gcd_commute) also have "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" by (rule fib_add) - also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))" + also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))" by (simp add: gcd_mult_add) - also have "... = gcd (fib n, fib (k + 1))" + also have "... = gcd (fib n) (fib (k + 1))" by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel) - also have "... = gcd (fib m, fib n)" - by (simp! add: gcd_commute) + also have "... = gcd (fib m) (fib n)" + using Suc by (simp add: gcd_commute) finally show ?thesis . qed lemma gcd_fib_diff: - "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)" + assumes "m <= n" + shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" proof - - assume "m <= n" - have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))" + have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))" by (simp add: gcd_fib_add) - also have "n - m + m = n" by (simp!) + also from `m <= n` have "n - m + m = n" by simp finally show ?thesis . qed lemma gcd_fib_mod: - "0 < m \<Longrightarrow> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" -proof - - assume m: "0 < m" - show ?thesis - proof (induct n rule: nat_less_induct) - fix n - assume hyp: "ALL ma. ma < n - --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)" - show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" - proof - - have "n mod m = (if n < m then n else (n - m) mod m)" - by (rule mod_if) - also have "gcd (fib m, fib ...) = gcd (fib m, fib n)" - proof cases - assume "n < m" thus ?thesis by simp - next - assume not_lt: "~ n < m" hence le: "m <= n" by simp - have "n - m < n" by (simp! add: diff_less) - with hyp have "gcd (fib m, fib ((n - m) mod m)) - = gcd (fib m, fib (n - m))" by simp - also from le have "... = gcd (fib m, fib n)" - by (rule gcd_fib_diff) - finally have "gcd (fib m, fib ((n - m) mod m)) = - gcd (fib m, fib n)" . - with not_lt show ?thesis by simp - qed - finally show ?thesis . + assumes "0 < m" + shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" +proof (induct n rule: nat_less_induct) + case (1 n) note hyp = this + show ?case + proof - + have "n mod m = (if n < m then n else (n - m) mod m)" + by (rule mod_if) + also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)" + proof (cases "n < m") + case True then show ?thesis by simp + next + case False then have "m <= n" by simp + from `0 < m` and False have "n - m < n" by simp + with hyp have "gcd (fib m) (fib ((n - m) mod m)) + = gcd (fib m) (fib (n - m))" by simp + also have "... = gcd (fib m) (fib n)" + using `m <= n` by (rule gcd_fib_diff) + finally have "gcd (fib m) (fib ((n - m) mod m)) = + gcd (fib m) (fib n)" . + with False show ?thesis by simp qed + finally show ?thesis . qed qed -theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n") +theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n") proof (induct m n rule: gcd_induct) - fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp + fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp fix n :: nat assume n: "0 < n" - hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0) - also assume hyp: "fib ... = gcd (fib n, fib (m mod n))" - also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod) - also have "... = gcd (fib m, fib n)" by (rule gcd_commute) - finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" . + then have "gcd m n = gcd n (m mod n)" by (rule gcd_non_0) + also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))" + also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod) + also have "... = gcd (fib m) (fib n)" by (rule gcd_commute) + finally show "fib (gcd m n) = gcd (fib m) (fib n)" . qed end |