equal
deleted
inserted
replaced
5 |
5 |
6 Lemmas for theory Porder.thy |
6 Lemmas for theory Porder.thy |
7 *) |
7 *) |
8 |
8 |
9 open Porder; |
9 open Porder; |
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* the reverse law of anti--symmetrie of << *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 qed_goal "antisym_less_inverse" thy "x=y ==> x << y & y << x" |
|
16 (fn prems => |
|
17 [ |
|
18 (cut_facts_tac prems 1), |
|
19 (rtac conjI 1), |
|
20 ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)), |
|
21 ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1)) |
|
22 ]); |
|
23 |
|
24 |
|
25 qed_goal "box_less" thy |
|
26 "[| a << b; c << a; b << d|] ==> c << d" |
|
27 (fn prems => |
|
28 [ |
|
29 (cut_facts_tac prems 1), |
|
30 (etac trans_less 1), |
|
31 (etac trans_less 1), |
|
32 (atac 1) |
|
33 ]); |
|
34 |
10 |
35 (* ------------------------------------------------------------------------ *) |
11 (* ------------------------------------------------------------------------ *) |
36 (* lubs are unique *) |
12 (* lubs are unique *) |
37 (* ------------------------------------------------------------------------ *) |
13 (* ------------------------------------------------------------------------ *) |
38 |
14 |