265 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
263 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
266 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
264 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
267 apply - |
265 apply - |
268 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
266 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
269 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
267 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
270 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
268 prefer 2 |
271 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
272 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
273 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
274 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
275 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
276 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
277 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
278 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
279 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
280 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
281 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
282 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
283 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
284 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
285 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
286 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
287 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
288 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
289 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
290 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
291 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
292 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
293 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
294 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
295 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
296 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
297 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
298 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
299 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
300 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
301 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
302 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
303 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
304 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
305 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
306 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
307 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
308 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
309 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
310 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
311 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
312 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
313 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
314 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
315 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
316 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
317 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
318 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
319 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
320 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
321 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
322 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
323 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
324 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
325 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
326 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
327 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
328 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
329 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
330 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
331 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
332 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
333 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
334 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
335 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
336 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
337 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
338 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
339 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
340 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
341 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
342 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
343 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
344 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
345 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
346 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
347 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
348 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
349 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
350 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
351 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
352 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
353 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
354 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
355 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
356 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
357 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
358 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
359 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
360 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
361 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
362 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
363 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
364 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
365 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
366 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
367 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
368 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
369 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
370 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
371 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
372 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
373 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
374 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
375 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
376 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
377 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
378 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
379 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
380 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
381 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
382 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
383 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
384 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
385 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
386 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
387 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
388 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
389 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
390 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
391 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
392 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
393 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
394 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
395 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
396 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
397 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
398 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
399 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
400 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
401 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
402 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
403 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
404 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
405 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
406 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
407 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
408 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
409 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
410 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
411 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
412 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
413 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
414 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
415 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
416 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
417 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
418 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
419 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
420 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
421 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
422 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
423 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
424 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
425 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
426 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
427 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
428 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
429 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
430 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
431 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
432 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
433 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
434 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
435 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
436 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
437 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
438 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
439 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
440 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
441 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
442 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
443 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
444 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
445 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
446 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
447 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
448 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
449 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
450 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
451 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
452 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
453 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
454 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
455 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
456 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
457 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*}) |
|
458 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
|
459 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*}) |
|
460 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*}) |
|
461 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
269 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
|
270 apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
462 done |
271 done |
463 |
272 |
464 (* Does not work: |
273 (* Does not work: |
465 lemma |
274 lemma |
466 assumes a0: "P1 TYP" |
275 assumes a0: "P1 TYP" |
485 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
294 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
486 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
295 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
487 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
296 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
488 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
297 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
489 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
298 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
490 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
299 apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
491 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
|
492 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *}) |
|
493 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
494 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
495 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
496 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
497 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
498 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
499 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
500 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
501 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
502 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
503 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
504 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
505 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
506 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
507 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
508 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
509 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *}) |
|
510 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
511 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
512 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
513 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
514 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
515 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
516 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
517 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
518 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
519 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
520 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
521 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
522 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
523 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
524 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *}) |
|
525 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
526 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
527 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
528 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
529 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
530 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
531 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
532 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
533 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
534 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
535 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
536 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
537 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
538 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
539 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
540 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
541 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
542 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
543 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
544 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
545 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
546 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
547 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
548 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
549 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
|
550 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
551 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
552 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
553 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
554 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
555 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
556 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
557 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
558 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
559 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
560 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
561 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
562 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
563 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
564 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
565 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
566 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
567 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
568 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
569 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
570 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
571 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
572 (* LOOP! *) |
|
573 (* apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) *) |
|
574 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
575 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
576 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
577 apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *}) |
|
578 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
579 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) |
|
580 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *}) |
|
581 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
300 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
582 done |
301 done |
583 |
302 |
584 print_quotients |
303 print_quotients |
585 |
304 |