src/deep_embeddings/prop_logicScript.sml

39    (P_SEM s (P_AND(b1,b2)) = (P_SEM s b1 /\ P_SEM s b2))`;
49    `P_OR (b1, b2) = P_NOT (P_AND (P_NOT b1, P_NOT b2))`;
52    `P_IMPL (b1, b2) = P_OR (P_NOT b1, b2)`;
55    `P_COND (c, b1, b2) = P_AND (P_IMPL (c, b1), P_IMPL (P_NOT c, b2))`;
58    `P_EQUIV (b1, b2) = P_AND (P_IMPL (b1, b2), P_IMPL (b2, b1))`;
61    `PROP_LOGIC_EQUIVALENT b1 b2 = (!s. (P_SEM s b1) = (P_SEM s b2))`;
67    (P_USED_VARS (P_AND(b1,b2)) = ((P_USED_VARS b1) UNION (P_USED_VARS b2)))`;
135    (P_NEGATE_VARS (P_AND(b1,b2)) = P_AND(P_NEGATE_VARS b1, P_NEGATE_VARS b2))`;
157    (P_ASSIGN_TRUE V (P_AND(b1,b2)) =
158       P_AND (P_ASSIGN_TRUE V b1, P_ASSIGN_TRUE V b2))`;
164    (P_ASSIGN_FALSE V (P_AND(b1,b2)) =
165       P_AND (P_ASSIGN_FALSE V b1, P_ASSIGN_FALSE V b2))`;
171    (P_SUBSTITUTION f (P_AND(b1,b2)) =
172       P_AND (P_SUBSTITUTION f b1, P_SUBSTITUTION f b2))`;
191    ``!s b1 b2 c b p.
195     (P_SEM s (P_AND(b1,b2)) = (P_SEM s b1 /\ P_SEM s b2)) /\
196     (P_SEM s (P_OR(b1,b2)) = (P_SEM s b1 \/ P_SEM s b2)) /\
197     (P_SEM s (P_IMPL(b1,b2)) = (P_SEM s b1 ==> P_SEM s b2)) /\
198     (P_SEM s (P_COND(c, b1,b2)) = (P_SEM s c /\ P_SEM s b1) \/ (~P_SEM s c /\ P_SEM s b2)) /\
199     (P_SEM s (P_EQUIV(b1,b2)) = (P_SEM s b1 = P_SEM s b2)))``,
241    ``!p b b1 b2. (
246     (P_USED_VARS (P_AND(b1, b2)) = P_USED_VARS b1 UNION P_USED_VARS b2) /\
247     (P_USED_VARS (P_OR(b1, b2)) = P_USED_VARS b1 UNION P_USED_VARS b2) /\
248     (P_USED_VARS (P_IMPL(b1, b2)) = P_USED_VARS b1 UNION P_USED_VARS b2) /\
249     (P_USED_VARS (P_EQUIV(b1, b2)) = P_USED_VARS b1 UNION P_USED_VARS b2)
264     (P_VAR_RENAMING f (P_AND(b1,b2)) = (P_AND(P_VAR_RENAMING f b1, P_VAR_RENAMING f b2)))`;
294    ``!p f b b1 b2. (
299     (P_VAR_RENAMING f (P_AND(b1, b2)) = P_AND(P_VAR_RENAMING f b1, P_VAR_RENAMING f b2)) /\
300     (P_VAR_RENAMING f (P_OR(b1, b2)) = P_OR(P_VAR_RENAMING f b1, P_VAR_RENAMING f b2)) /\
301     (P_VAR_RENAMING f (P_IMPL(b1, b2)) = P_IMPL(P_VAR_RENAMING f b1, P_VAR_RENAMING f b2)) /\
302     (P_VAR_RENAMING f (P_EQUIV(b1, b2)) = P_EQUIV(P_VAR_RENAMING f b1, P_VAR_RENAMING f  b2))
999       (P_ASSIGN_TRUE V (P_AND(b1,b2)) = P_AND (P_ASSIGN_TRUE V b1, P_ASSIGN_TRUE V b2)) /\
1000       (P_ASSIGN_TRUE V (P_OR(b1,b2)) = P_OR (P_ASSIGN_TRUE V b1, P_ASSIGN_TRUE V b2)) /\
1001       (P_ASSIGN_TRUE V (P_IMPL(b1,b2)) = P_IMPL (P_ASSIGN_TRUE V b1, P_ASSIGN_TRUE V b2)) /\
1002       (P_ASSIGN_TRUE V (P_COND(c, b1,b2)) = P_COND (P_ASSIGN_TRUE V c, P_ASSIGN_TRUE V b1, P_ASSIGN_TRUE V b2)) /\
1003       (P_ASSIGN_TRUE V (P_EQUIV(b1,b2)) = P_EQUIV (P_ASSIGN_TRUE V b1, P_ASSIGN_TRUE V b2)) /\
1009       (P_ASSIGN_FALSE V (P_AND(b1,b2)) = P_AND (P_ASSIGN_FALSE V b1, P_ASSIGN_FALSE V b2)) /\
1010       (P_ASSIGN_FALSE V (P_OR(b1,b2)) = P_OR (P_ASSIGN_FALSE V b1, P_ASSIGN_FALSE V b2)) /\
1011       (P_ASSIGN_FALSE V (P_IMPL(b1,b2)) = P_IMPL (P_ASSIGN_FALSE V b1, P_ASSIGN_FALSE V b2)) /\
1012       (P_ASSIGN_FALSE V (P_COND(c, b1,b2)) = P_COND (P_ASSIGN_FALSE V c, P_ASSIGN_FALSE V b1, P_ASSIGN_FALSE V b2)) /\
1013       (P_ASSIGN_FALSE V (P_EQUIV(b1,b2)) = P_EQUIV (P_ASSIGN_FALSE V b1, P_ASSIGN_FALSE V b2))``,