src/translations/translationsLib.sml

72 fun getBindingFor b1 b2 l [] = (false, false, ``dummy:num``)
73   | getBindingFor b1 b2 l (h::l1) =
78         if ((l' ~~ l) andalso ((not b1) orelse a1) andalso ((not b2) orelse a2)) then
81           getBindingFor b1 b2 l l1
178   fun ltl2omega_internal2 b1 b2 l dsThm TSPECL =
189         fun addBindingFor b1 b2 l dsThm =
192             val (b1', b2', pf) = getBindingFor b1 b2 l dsB;
194             if (b1' orelse b2') then (b1', b2', pf, dsThm) else (
196                 val dsThm = ltl2omega_internal2 b1 b2 l dsThm TSPECL;
198                 val (b1', b2', pf) = (getBindingFor b1 b2 l dsB);
199                 val _ = if (b1' orelse b2') then T else
206                     val _ = print_term (boolToHOL b2);
214                 (b1', b2', pf, dsThm)
233             val (b2', b1', pf, dsThm) = addBindingFor b2 b1 (hd args) dsThm;
235             val thm = TSPECL [boolToHOL b2', boolToHOL b1']
247             val (b1', b2', pf, dsThm) = addBindingFor b1 b2 (hd args) dsThm;
249             val thm = TSPECL [(boolToHOL b1'), (boolToHOL b2'), ds, hd args, pf]
261             val (b1', b2', pf, dsThm) = addBindingFor b1 b2 (hd args) dsThm;
263             val thm = TSPECL [(boolToHOL b1'), (boolToHOL b2'), ds, hd args, pf]
275             val (b1', b2', pf, dsThm) = addBindingFor b1 b2 (hd args) dsThm;
277             val thm = TSPECL [(boolToHOL b1'), (boolToHOL b2'), ds, hd args, pf]
291             val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm;
292             val (b21, b22, pf2, dsThm) = addBindingFor b1 b2 l2 dsThm;
306             val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm;
307             val (b21, b22, pf2, dsThm) = addBindingFor b1 b2 l2 dsThm;
336             val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm;
337             val (b21, b22, pf2, dsThm) = addBindingFor b1 b2 l2 dsThm;
355             val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm;
356             val (b21, b22, pf2, dsThm) = addBindingFor b2 b1 l2 dsThm;
359               (boolToHOL b22), (boolToHOL b2)]               CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE___eval;
374             val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm;
375             val (b21, b22, pf2, dsThm) = addBindingFor b2 b1 l2 dsThm;
393             val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm;
394             val (b21, b22, pf2, dsThm) = addBindingFor b1 b2 l2 dsThm;
426       val (l, b1, b2, pf) = (el 1 hList, HOLToBool(el 2 hList), HOLToBool(el 3 hList), el 4 hList);
428       (ds, l, b1, b2, pf)
446   fun ltl2omega_internal3_forget b1 b2 l TSPECL =
457         fun oneAncestor b1 b2 b11 b12 A thm =
461             val thm = TSPECL [boolToHOL b1, boolToHOL b2, ds, l, pf]  thm;
468         fun twoAncestors b1 b2 b11 b12 b21 b22 aPair thm = (
478             val thm = TSPECL [(boolToHOL b1), (boolToHOL b2), ds1, ds2, l1, l2, pf1, pf2] thm;
488             val thm = TSPECL [(boolToHOL b1), (boolToHOL b2), hd args]
495           oneAncestor b1 b2 b2 b1 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT___forget_eval
497           oneAncestor b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT___forget_eval
499           oneAncestor b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT___forget_eval
501           oneAncestor b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PNEXT___forget_eval
503           twoAncestors b1 b2 b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND___forget_eval
505           twoAncestors b1 b2 true true true true (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV___forget_eval
507           twoAncestors b1 b2 b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR___forget_eval
509           twoAncestors b1 b2 b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL___forget_eval
511           twoAncestors b1 b2 b1 b2 b2 b1 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE___forget_eval
513           twoAncestors b1 b2 b1 b2 b2 b1 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE___forget_eval
515           twoAncestors b1 b2 b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL___forget_eval
530   fun ltl2omega_internal2_forget b1 b2 l TSPECL =
532         val thm = ltl2omega_internal3_forget b1 b2 l TSPECL;
571   fun ltl2omega_internal fast b1 b2 t =
585                   ltl2omega_internal2_forget b1 b2 l TSPECL
587                   ltl2omega_internal2 b1 b2 l dsThm TSPECL;
592       val (b1', b2', pf) = (getBindingFor b1 b2 l dsB);
594       (l, equivTHM, thm, ds, pf, b1', b2')
602         val (b1, b2) = if neg then (true, false) else (false, true);
603         val (equivL, equivTHM, dsThm, ds, pf, b1', b2') = ltl2omega_internal fast b1 b2 l;
607         val a = if neg then b2' else b1';
653       val (equivL, equivTHM, dsThm, ds, pf, b1', b2') = ltl2omega_internal fast true false l;
657       val thm = SPECL [ds, l, equivL, pf, boolToHOL b2'] thm;
693       val (equivL, equivTHM, dsThm, ds, pf, b1', b2') = ltl2omega_internal fast false true l;