src/tools/psl_lemmataScript.sml

922    (F_SERE_FREE (F_AND(f1,f2))      = F_SERE_FREE f1 /\ F_SERE_FREE f2)
930    (F_SERE_FREE (F_UNTIL(f1,f2))    = F_SERE_FREE f1 /\ F_SERE_FREE f2)
958          [`P`,`\(f1,f2). P f1 /\ P f2`]
2339    (IS_TOP_BOTTOM_WELL_BEHAVED (F_AND(f1,f2))      = IS_TOP_BOTTOM_WELL_BEHAVED f1 /\ IS_TOP_BOTTOM_WELL_BEHAVED f2)
2347    (IS_TOP_BOTTOM_WELL_BEHAVED (F_UNTIL(f1,f2))    = IS_TOP_BOTTOM_WELL_BEHAVED f1 /\ IS_TOP_BOTTOM_WELL_BEHAVED f2)
3093    ``!v f1 f2. IS_PROPER_PATH v ==>
3094       (UF_SEM v (F_WEAK_UNTIL(f1,f2)) =
3095        UF_SEM v (F_NOT (F_UNTIL(F_NOT f2, F_AND(F_NOT f1, F_NOT f2)))))``,
3107       Cases_on `UF_SEM (RESTN v k') f2` THEN ASM_SIMP_TAC std_ss [] THEN
3126       Cases_on `UF_SEM (RESTN v k') f2` THEN1 METIS_TAC[] THEN
3127       `?j. j < k' /\ UF_SEM (RESTN v j) f2` by METIS_TAC[RESTN_COMPLEMENT, COMPLEMENT_COMPLEMENT] THEN
3964  Define `UF_EQUIVALENT f1 f2 =
3965          !v. ((UF_SEM v f1 = UF_SEM v f2))`
3969  Define `UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 =
3970          !v. IS_INFINITE_TOP_BOTTOM_FREE_PATH v ==> ((UF_SEM v f1 = UF_SEM v f2))`
3973  Define `F_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 =
3974          !v c. IS_INFINITE_TOP_BOTTOM_FREE_PATH v ==> ((F_SEM v c f1 = F_SEM v c f2))`
4029   ``!f1 f2. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 =
4030             UF_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE (F_NOT(F_IFF(f1, f2)))``,
4045   ``!f1 f2. F_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 =
4046             F_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE (F_NOT(F_IFF(f1, f2)))``,
4066    ``!f1 f2 f3. (UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 /\
4067                  UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f2 f3) ==>