equal
deleted
inserted
replaced
472 |
472 |
473 locale antisym = |
473 locale antisym = |
474 fixes R |
474 fixes R |
475 assumes "R x y --> R y x --> x = y" |
475 assumes "R x y --> R y x --> x = y" |
476 |
476 |
477 interpretation equal : antisym "op =" by standard simp |
477 interpretation equal : antisym "(=)" by standard simp |
478 interpretation order_nat : antisym "op <= :: nat => _ => _" by standard simp |
478 interpretation order_nat : antisym "(<=) :: nat => _ => _" by standard simp |
479 |
479 |
480 lemma (in antisym) |
480 lemma (in antisym) |
481 "R x y --> R y z --> R x z" |
481 "R x y --> R y z --> R x z" |
482 quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample] |
482 quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample] |
483 quickcheck[exhaustive, expect = counterexample] |
483 quickcheck[exhaustive, expect = counterexample] |