[listSimps] Improved LIST_EQ_SIMP_CONV knowing SNOC

[binghe]

Hi,

The conversion listSimps.LIST_EQ_SIMP_CONV was able to handle list equations with SNOC by first unconditionally normalise all SNOC by SNOC_APPEND. This is equivalent to hanving SNOC_APPEND as part of automatic simp rules. After #1518, SNOC_APPEND has been removed from the normalisation process but (as @ordinarymath pointed out) list equations containing SNOC should still be simplified whenever possible, e.g. many proofs has trivial subgoals like SNOC x l = l ++ [x] by rw []. More complicated cases are the following (now part of list selftests):

            (“[a;b;c;d] = SNOC d l”, “[a; b; c] = l”),
            (“[a;b;c;d] = SNOC d (SNOC c l)”, “[a; b] = l”),
            (“SNOC x l = l' ++ [y]”, “l = (l' :'a list) /\ x = (y :'a)”),
            (“SNOC x l = l ++ [c]”, “x = c :'a”),
            (“SNOC x l = l ++ [x]”, “T”),
            (“SNOC a b = SNOC c d”, “b = (d :'a list) /\ a = (c :'a)”),
            (“l ++ [x] = SNOC y l'”, “l = (l' :'a list) /\ x = (y :'a)”)

(Note that SNOC a b = SNOC c d is simplified to b = d /\ a = c but a = c /\ b = d is more natural. I found hard to support the later version.)

Furthermore, non-simplifiable list equations like SNOC x l = l2 should remain unchanged.

This PR implements the above idea with very local changes to the main function of LIST_EQ_SIMP_CONV. The detailed algorithm is the following: (assuming the input list equation term is t, the original conversion is conv)

1. val th = PURE_REWRITE_CONV [SNOC_APPEND] t. This tests if the input term contains any SNOC. If not, the original conversion is used. (NOTE: PURE_REWRITE_CONV (instead of REWRITE_CONV) is necessary to not rewrite list tautology like SNOC x l = l ++ [x] to T, which is no more an equation.)
2. If t contains some SNOC, then th can be decomposed to t1 (same with t) and t2 (the new input without SNOC), now the original conversion is called on t2 but wrapped by UNCHANGED: val th' = CHANGED_CONV conv t2.
3. If val th' = CHANGED_CONV conv t2 returns HOL_ERR (meaning unchanged), the entire conversion must return unchanged. This prevent non-simplifiable inputs like SNOC x l = l2 returns l ++ [x] = l2.
4. In case the original conversion actually changed something, a final TRANS th th' will return the equation between the original input equation (possibly with SNOC) and the simplified equation.

In listSyntax I added strip_snoc_to_lists and strip_snoc but eventually they are not used. I consider them useful and thus are kept in the PR.

--Chun

[binghe]

A potential issue of my above algorithm is that, if a list equation is partially-simplifiable, then the output will have all SNOC eliminated:

> listSimps.LIST_EQ_SIMP_CONV ``a::SNOC x l = a::l2``;
val it = |- a::SNOC x l = a::l2 <=> l ++ [x] = l2: thm

Therefore it's still possible that some proofs can be broken by this PR.

[mn200]

Thanks!