equal
deleted
inserted
replaced
62 by (Fast_tac 1); |
62 by (Fast_tac 1); |
63 qed "id_O_R"; |
63 qed "id_O_R"; |
64 |
64 |
65 Addsimps [R_O_id,id_O_R]; |
65 Addsimps [R_O_id,id_O_R]; |
66 |
66 |
|
67 goal thy "(R O S) O T = R O (S O T)"; |
|
68 by (Blast_tac 1); |
|
69 qed "O_assoc"; |
|
70 |
67 goal thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; |
71 goal thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; |
68 by (Blast_tac 1); |
72 by (Blast_tac 1); |
69 qed "comp_mono"; |
73 qed "comp_mono"; |
70 |
74 |
71 goal thy |
75 goal thy |