401 begin |
401 begin |
402 |
402 |
403 (* The type constraint on @{term op =} below is necessary since the operation |
403 (* The type constraint on @{term op =} below is necessary since the operation |
404 is not a parameter of the locale. *) |
404 is not a parameter of the locale. *) |
405 |
405 |
406 lemmas |
406 declare less_irrefl [THEN notE, order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"] |
407 [order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"] = |
407 |
408 less_irrefl [THEN notE] |
408 declare order_refl [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
409 lemmas |
409 |
410 [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
410 declare less_imp_le [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
411 order_refl |
411 |
412 lemmas |
412 declare antisym [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
413 [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
413 |
414 less_imp_le |
414 declare eq_refl [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
415 lemmas |
415 |
416 [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
416 declare sym [THEN eq_refl, order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
417 antisym |
417 |
418 lemmas |
418 declare less_trans [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
419 [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
419 |
420 eq_refl |
420 declare less_le_trans [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
421 lemmas |
421 |
422 [order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
422 declare le_less_trans [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
423 sym [THEN eq_refl] |
423 |
424 lemmas |
424 declare order_trans [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
425 [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
425 |
426 less_trans |
426 declare le_neq_trans [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
427 lemmas |
427 |
428 [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
428 declare neq_le_trans [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
429 less_le_trans |
429 |
430 lemmas |
430 declare less_imp_neq [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
431 [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
431 |
432 le_less_trans |
432 declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
433 lemmas |
433 |
434 [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
434 declare not_sym [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] |
435 order_trans |
|
436 lemmas |
|
437 [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
438 le_neq_trans |
|
439 lemmas |
|
440 [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
441 neq_le_trans |
|
442 lemmas |
|
443 [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
444 less_imp_neq |
|
445 lemmas |
|
446 [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
447 eq_neq_eq_imp_neq |
|
448 lemmas |
|
449 [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
450 not_sym |
|
451 |
435 |
452 end |
436 end |
453 |
437 |
454 context linorder |
438 context linorder |
455 begin |
439 begin |
456 |
440 |
457 lemmas |
441 declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]] |
458 [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _ |
442 |
459 |
443 declare less_irrefl [THEN notE, order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
460 lemmas |
444 |
461 [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
445 declare order_refl [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
462 less_irrefl [THEN notE] |
446 |
463 lemmas |
447 declare less_imp_le [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
464 [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
448 |
465 order_refl |
449 declare not_less [THEN iffD2, order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
466 lemmas |
450 |
467 [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
451 declare not_le [THEN iffD2, order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
468 less_imp_le |
452 |
469 lemmas |
453 declare not_less [THEN iffD1, order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
470 [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
454 |
471 not_less [THEN iffD2] |
455 declare not_le [THEN iffD1, order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
472 lemmas |
456 |
473 [order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
457 declare antisym [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
474 not_le [THEN iffD2] |
458 |
475 lemmas |
459 declare eq_refl [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
476 [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
460 |
477 not_less [THEN iffD1] |
461 declare sym [THEN eq_refl, order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
478 lemmas |
462 |
479 [order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
463 declare less_trans [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
480 not_le [THEN iffD1] |
464 |
481 lemmas |
465 declare less_le_trans [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
482 [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
466 |
483 antisym |
467 declare le_less_trans [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
484 lemmas |
468 |
485 [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
469 declare order_trans [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
486 eq_refl |
470 |
487 lemmas |
471 declare le_neq_trans [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
488 [order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
472 |
489 sym [THEN eq_refl] |
473 declare neq_le_trans [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
490 lemmas |
474 |
491 [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
475 declare less_imp_neq [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
492 less_trans |
476 |
493 lemmas |
477 declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
494 [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
478 |
495 less_le_trans |
479 declare not_sym [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] |
496 lemmas |
|
497 [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
498 le_less_trans |
|
499 lemmas |
|
500 [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
501 order_trans |
|
502 lemmas |
|
503 [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
504 le_neq_trans |
|
505 lemmas |
|
506 [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
507 neq_le_trans |
|
508 lemmas |
|
509 [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
510 less_imp_neq |
|
511 lemmas |
|
512 [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
513 eq_neq_eq_imp_neq |
|
514 lemmas |
|
515 [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = |
|
516 not_sym |
|
517 |
480 |
518 end |
481 end |
519 |
482 |
520 |
483 |
521 setup {* |
484 setup {* |