separationLogic/src/separationLogicScript.sml

1611    (PRODUCT_SEPARATION_COMBINATOR (f1:'a bin_option_function) (f2:'b bin_option_function) NONE _ = NONE) /\
1612    (PRODUCT_SEPARATION_COMBINATOR f1 f2 _ NONE = NONE) /\
1613    (PRODUCT_SEPARATION_COMBINATOR f1 f2 (SOME (x1,x2)) (SOME (y1,y2)) =
1615       let z2 = f2 (SOME x2) (SOME y2) in
1623 ``(PRODUCT_SEPARATION_COMBINATOR f1 f2 X NONE = NONE) /\
1624 (PRODUCT_SEPARATION_COMBINATOR f1 f2 NONE X = NONE) /\
1625 (PRODUCT_SEPARATION_COMBINATOR f1 f2 (SOME x) (SOME y) =
1627    let z2 = f2 (SOME (SND x)) (SOME (SND y)) in
1632 ((PRODUCT_SEPARATION_COMBINATOR f1 f2 (SOME x) (SOME y) = SOME z) =
1634    (f2 (SOME (SND x)) (SOME (SND y)) =  SOME (SND z)))
1661 ``!f1 f2.
1663 IS_SEPARATION_COMBINATOR f2 ==>
1664 IS_SEPARATION_COMBINATOR (PRODUCT_SEPARATION_COMBINATOR f1 f2)``,
1668 `!x. (PRODUCT_SEPARATION_COMBINATOR f1 f2 NONE x = NONE) /\
1669        (PRODUCT_SEPARATION_COMBINATOR f1 f2 x NONE = NONE)` by (
1713       Cases_on `IS_SOME (f2 (SOME r') (SOME r))` THEN (
1721       Cases_on `IS_SOME (f2 (SOME r') (SOME r))` THEN (
1755 !f1 f2 uf1 uf2 uf.
1757 IS_SEPARATION_COMBINATOR f2 /\
1759 IS_SEPARATION_COMBINATOR_NEUTRAL_ELEMENT_FUNCTION f2 uf2 /\
1760 IS_SEPARATION_COMBINATOR_NEUTRAL_ELEMENT_FUNCTION (PRODUCT_SEPARATION_COMBINATOR f1 f2) uf) ==>
1779 ``!f1 f2 u1 u2.
1781 IS_SEPARATION_ALGEBRA f2 u2 ==>
1782 IS_SEPARATION_ALGEBRA (PRODUCT_SEPARATION_COMBINATOR f1 f2) (u1,u2)``,
1802 ``!f1 f2 s1 s2.
1803 ASL_IS_SUBSTATE (PRODUCT_SEPARATION_COMBINATOR f1 f2) s1 s2 =
1805 ASL_IS_SUBSTATE f2 (SND s1) (SND s2)``,
1858 val asl_inl_def = Define `asl_inl f1 f2 x = \X. ((FST X) IN x) /\ ((SND X) IN (asl_emp f2))`
1859 val asl_inr_def = Define `asl_inr f1 f2 x = \X. ((SND X) IN x) /\ ((FST X) IN (asl_emp f1))`
1863    ``IS_SEPARATION_COMBINATOR f1 /\ IS_SEPARATION_COMBINATOR f2 ==>
1864       (((asl_inl f1 f2 x1 = asl_inl f1 f2 x2) = (x1 = x2)) /\
1865       ((asl_inr f1 f2 x1 = asl_inr f1 f2 x2) = (x1 = x2)))``,
1877 ``!f1 f2.
1878 asl_emp (PRODUCT_SEPARATION_COMBINATOR f1 f2) =
1879 (\s. FST s IN asl_emp f1 /\ SND s IN asl_emp f2)``,
1889 ``!f1 f2.
1890 (((asl_inl f1 f2 (asl_emp f1)) = asl_emp (PRODUCT_SEPARATION_COMBINATOR f1 f2)) /\
1891 ((asl_inr f1 f2 (asl_emp f2)) = asl_emp (PRODUCT_SEPARATION_COMBINATOR f1 f2)))``,
1902 ``!f1 f2.
1904 IS_SEPARATION_COMBINATOR f2) ==>
1906 ((asl_star (PRODUCT_SEPARATION_COMBINATOR f1 f2)
1907 (asl_inl f1 f2 UNIV) (asl_inr f1 f2 UNIV) = UNIV) /\
1908 (asl_star (PRODUCT_SEPARATION_COMBINATOR f1 f2)
1909 UNIV (asl_inr f1 f2 UNIV) = UNIV) /\
1910 (asl_star (PRODUCT_SEPARATION_COMBINATOR f1 f2)
1911 (asl_inl f1 f2 UNIV) UNIV = UNIV))
1928 ``!f1 f2.
1929 ((asl_inl f1 f2 {} = {}) /\ (asl_inr f1 f2 {} = {}))``,
1937 ``!f1 f2 P1 P2.
1938 asl_star (PRODUCT_SEPARATION_COMBINATOR f1 f2) P1 P2 =
1940                       (f2 (SOME y1) (SOME y2) = SOME y) /\
1950 ``!f1 f2 X Y.
1952 IS_SEPARATION_COMBINATOR f2) ==>
1954 ((asl_star (PRODUCT_SEPARATION_COMBINATOR f1 f2) (asl_inl f1 f2 X) (asl_inl f1 f2 Y) =
1955 asl_inl f1 f2 (asl_star f1 X Y)) /\
1956 (asl_star (PRODUCT_SEPARATION_COMBINATOR f1 f2) (asl_inr f1 f2 X) (asl_inr f1 f2 Y) =
1957 asl_inr f1 f2 (asl_star f2 X Y)))``,
1973 ``!f1 f2 s1 s2. IS_SOME (PRODUCT_SEPARATION_COMBINATOR f1 f2 s1 s2) =
1976     IS_SOME (f2 (SOME (SND (THE s1))) (SOME (SND (THE s2)))))``,