examples/CCS/CoarsestCongrScript.sml

54  >> rpt STRIP_TAC (* 2 sub-goals here *)
56       Cases_on `u` >| (* 2 sub-goals here *)
71       Cases_on `u` >| (* 2 sub-goals here *)
91     rpt STRIP_TAC (* 3 sub-goals here *)
110  >> Cases_on `?E. TRANS p tau E /\ WEAK_EQUIV E q` (* 2 sub-goals here *)
113       REWRITE_TAC [OBS_CONGR] >> rpt STRIP_TAC >| (* 2 sub-goals here *)
115         Cases_on `u` \\ (* 2 sub-goals here, sharing initial tacticals *)
132       Cases_on `?E. TRANS q tau E /\ WEAK_EQUIV p E` >| (* 2 sub-goals here *)
135         REWRITE_TAC [OBS_CONGR] >> rpt STRIP_TAC >| (* 2 sub-goals here *)
143           Cases_on `u` \\ (* 2 sub-goals here, sharing initial tacticals *)
156         IMP_RES_TAC DENG_LEMMA \\ (* 2 sub-goals here, same tactical *)
229  >> rpt STRIP_TAC (* 2 sub-goals here *)
235       Cases_on `u` >| (* 2 sub-goals here *)
242         IMP_RES_TAC EPS_cases1 >| (* 2 sub-goals here *)
249           RES_TAC,                              (* initial assumption of `p` is used here *)
252                       (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
266         IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *)
269                       (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
278                       (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
289             RES_TAC ] ] ],                      (* initial assumption of `p` is used here *)
295       Cases_on `u` >| (* 2 sub-goals here *)
302         IMP_RES_TAC EPS_cases1 >| (* 2 sub-goals here *)
309           RES_TAC,                              (* initial assumption of `q` is used here *)
312                       (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
326         IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *)
329                       (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
338                       (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
348             RES_TAC ] ] ] ] );                  (* initial assumption of `q` is used here *)
379  >> rpt STRIP_TAC (* 2 sub-goals here *)
385       Cases_on `u` >| (* 2 sub-goals here *)
389           (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [EPS_cases1])) >| (* 2 sub-goals here *)
399             (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
407         Cases_on `x = a` >| (* 2 sub-goals here *)
411           IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *)
414                 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
422                 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
433           IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *)
436                 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
444                 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
455       Cases_on `u` >| (* 2 sub-goals here *)
459           (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [EPS_cases1])) >| (* 2 sub-goals here *)
470             (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
478         Cases_on `x = a` >| (* 2 sub-goals here *)
482           IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *)
485                 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
493                 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
504           IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *)
507                 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
515                 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *)
540  >> Induct_on `n` (* 2 sub-goals here *)
545  >> IMP_RES_TAC TRANS_SUM (* 2 sub-goals here *)
556  >> Induct_on `n` (* 2 sub-goals here, first one is easy *)
560  >> IMP_RES_TAC TRANS_SUM (* 2 sub-goals here *)
576  >> Induct_on `n` (* 2 sub-goals here *)
580  >> IMP_RES_TAC LESS_LEMMA1 (* 2 sub-goals here *)
593  >> EQ_TAC (* 2 sub-goals here *)
604  >> EQ_TAC (* 2 sub-goals here *)
607       IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *)
613         IMP_RES_TAC EPS_cases1 >| (* 2 sub-goals here *)
663  >> `x1 < x2 \/ x2 < x1` by PROVE_TAC [LESS_LESS_CASES] (* 2 sub-goals here *)
721       RW_TAC std_ss [IN_DEF] >| (* 2 sub-goals here *)
723         MATCH_MP_TAC SELECT_ELIM_THM \\ (* eliminated `Q (@P)` here *)
745       Cases_on `?y. y IN B /\ R n y` >| (* 2 sub-goals here *)
749         METIS_TAC [], (* PROVE_TAC doesn't work here *)
756       RES_TAC >| (* 2 sub-goals here *)
805       STRIP_ASSUME_TAC (Q.SPECL [`m`, `n`] LESS_LESS_CASES) >| (* 3 sub-goals here *)
826  >> CONJ_TAC (* 2 sub-goals here *)
833  >> CONJ_TAC (* 2 sub-goals here *)