src/translations/translationsLibScript.sml

63 (* |- !b1 b2 DS l pf.
65           (l,b1,b2,pf) IN DS.B ==>
68                ((LTL_NOT l,b2,b1,(\sv. P_NOT (pf sv))) INSERT DS.B))
175       (prove (``!b1 b2 p.
178                 {(LTL_PROP p,b1,b2,(\sv. p))} (P_USED_VARS p))``,
185     !b1 b2 DS l pf.
187             (DS.B = {(l,b2,b1,pf)}) ==>
190                   {(LTL_NOT l,b1,b2,(\sv. P_NOT (pf sv)))})``,
194     Q_SPECL_NO_ASSUM 0 [`b2`, `b1`, `DS`, `l`, `pf`] THEN
207     !b1 b2 DS1 DS2 l1 l2 pf1 pf2.
210             (DS1.B = {(l1,b1,b2,pf1)}) ==>
211             (DS2.B = {(l2,b1,b2,pf2)}) ==>
215                   {(LTL_AND (l1, l2), b1,b2,(\sv. P_AND(pf1 sv, pf2 (\n. sv (n + DS1.SN)))))})``,
219     SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\
220                  (l2,b1,b2,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 (
228     Q_SPECL_NO_ASSUM 0 [`DS'`, `b1`,`b2`, `b1`, `b2`, `l1`, `l2`, `pf1`, `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN
242     !b1 b2 DS1 DS2 l1 l2 pf1 pf2.
245             (DS1.B = {(l1,b1,b2,pf1)}) ==>
246             (DS2.B = {(l2,b1,b2,pf2)}) ==>
250                   {(LTL_OR (l1, l2), b1,b2,(\sv. P_OR(pf1 sv, pf2 (\n. sv (n + DS1.SN)))))})``,
254     SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\
255                  (l2,b1,b2,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 (
263     Q_SPECL_NO_ASSUM 0 [`DS'`, `b1`, `b2`, `b1`, `b2`, `l1`, `l2`, `pf1`, `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN
276     !b1 b2 DS1 DS2 l1 l2 pf1 pf2.
284                   {(LTL_EQUIV (l1, l2),b1,b2,(\sv. P_EQUIV(pf1 sv, pf2 (\n. sv (n + DS1.SN)))))})``,
301                {(LTL_EQUIV (l1,l2),b1,b2,
319     !b1 b2 DS l pf.
321             (DS.B = {(l,b1,b2,pf)}) ==>
325               DS.FC {(LTL_NEXT l,b1,b2,(\sv. P_PROP (sv DS.SN)))})
329     Q_SPECL_NO_ASSUM 0 [`b1`,`b2`, `DS`, `l`, `pf`] THEN
337     !b1 b2 DS l pf.
339             (DS.B = {(l,b1,b2,pf)}) ==>
343               DS.FC {(LTL_PSNEXT l,b1,b2,(\sv. P_PROP (sv DS.SN)))})
347     Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `DS`, `l`, `pf`] THEN
355     !b1 b2 DS l pf.
357             (DS.B = {(l,b1,b2,pf)}) ==>
361               DS.FC {(LTL_PNEXT l,b1,b2,(\sv. P_NOT (P_PROP (sv DS.SN))))})
365     Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `DS`, `l`, `pf`] THEN
373     !b1 b2 DS1 DS2 l1 l2 pf1 pf2 DS'.
377             (DS1.B = {(l1,b1,b2,pf1)}) ==>
378             (DS2.B = {(l2,b1,b2,pf2)}) ==>
396                 {(LTL_SUNTIL (l1,l2),b1,b2,(\sv. P_PROP (sv DS'.SN)))})``,
399     SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\
400                  (l2,b1,b2,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 (
408     Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `b1`, `b2`, `b1`, `DS'`, `l1`, `l2`, `pf1`,
420     !b1 b2 DS1 DS2 l1 l2 pf1 pf2 DS'.
424             (DS1.B = {(l1,b1,b2,pf1)}) ==>
425             (DS2.B = {(l2,b1,b2,pf2)}) ==>
435               {(LTL_PSUNTIL (l1,l2),b1,b2,
442     SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\
443                  (l2,b1,b2,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 (
451     Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `b1`, `b2`, `DS'`, `l1`, `l2`, `pf1`,
463     !b1 b2 DS1 DS2 l1 l2 pf1 pf2 DS'.
467             (DS1.B = {(l1,b1,b2,pf1)}) ==>
468             (DS2.B = {(l2,b2,b1,pf2)}) ==>
479               ((if ~b2 then
486               {(LTL_BEFORE (l1,l2),b1,b2,(\sv. P_NOT (P_PROP (sv DS'.SN))))})``,
489     SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\
490                  (l2,b2,b1,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 (
498     Q_SPECL_NO_ASSUM 0 [`b1`,`b2`,`b2`,`b1`,`b2`, `DS'`, `l1`, `l2`, `pf1`, `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN
510     !b1 b2 DS1 DS2 l1 l2 pf1 pf2 DS'.
514             (DS1.B = {(l1,b1,b2,pf1)}) ==>
515             (DS2.B = {(l2,b2,b1,pf2)}) ==>
525                 {(LTL_PBEFORE (l1,l2),b1,b2,
532     SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\
533                  (l2,b2,b1,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 (
541     Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `b2`, `b1`, `DS'`, `l1`, `l2`, `pf1`, `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN