examples/CCS/CoarsestCongrScript.sml

27    |- !E E'. OBS_CONGR (sum E (prefix tau (sum E' E))) (prefix tau (sum E' E))
31   ``!E E'. OBS_CONGR (sum E (prefix tau (sum E' E))) (prefix tau (sum E' E))``,
89   ``!p q. (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q) \/
90                             OBS_CONGR (prefix tau p) q) ==> WEAK_EQUIV p q``,
107   ``!p q. WEAK_EQUIV p q ==> (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q)
108                                             \/ OBS_CONGR (prefix tau p) q)``,
122           take [`prefix tau q`, `q`] \\
150             take [`prefix tau p`, `p`] \\
162   ``!p q. WEAK_EQUIV p q = (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q)
163                                           \/ OBS_CONGR (prefix tau p) q)``,
231       ASSUME_TAC (Q.SPEC `prefix (label a) nil`
234       POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) nil`)) \\
239                              (ASSUME ``WEAK_EQUIV (sum p (prefix (label a) nil))
240                                                   (sum q (prefix (label a) nil))``)) \\
251           PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) tau u``
263                              (ASSUME ``WEAK_EQUIV (sum p (prefix (label a) nil))
264                                                   (sum q (prefix (label a) nil))``)) \\
268           PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) tau E'``
277           PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) (label L) E'``
291       ASSUME_TAC (Q.SPEC `prefix (label a') nil`
294       POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a') nil`)) \\
299                              (ASSUME ``WEAK_EQUIV (sum p (prefix (label a') nil))
300                                                   (sum q (prefix (label a') nil))``)) \\
311           PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) tau u``
323                              (ASSUME ``WEAK_EQUIV (sum p (prefix (label a') nil))
324                                                   (sum q (prefix (label a') nil))``)) \\
328           PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) tau E'``
337           PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) (label L) E'``
377                 (ASSUME_TAC o (Q.SPEC `prefix (label a) k`))
382       POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) k`)) \\
383       PAT_X_ASSUM ``WEAK_EQUIV (sum p (prefix (label a) k)) (sum q (prefix (label a) k))``
388         PAT_X_ASSUM ``EPS (sum q (prefix (label a) k)) E2``
398           PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) tau u``
413             PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) tau E'``
421             PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) (label a) E'``
435             PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) tau E'``
443             PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) (label x) E'``
452       POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) k`)) \\
453       PAT_X_ASSUM ``WEAK_EQUIV (sum p (prefix (label a) k)) (sum h (prefix (label a) k))``
458         PAT_X_ASSUM ``EPS (sum p (prefix (label a) k)) E1``
469           PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau u``
484             PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau E'``
492             PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) (label a) E'``
506             PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau E'``
514             PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) (label x) E'``
528    (KLOP a (SUC n) = sum (KLOP a n) (prefix (label a) (KLOP a n))) `;
855     KLOP_INF X a = rec X (sum (var X) (prefix (label a) (var X)))`;