Irvin

One such example that is currently manually proved is `xs x :: xs`

quotient simps cannot deal with conjuncts.

3

``` Theorem PAIR_MAP_I[simp,quotient_simp]: (I ## I) = (I : 'a # 'b -> 'a # 'b) /\ ((\x. x) ## (\x. x)) = ((\x. x) : 'a # 'b ->...

Creating a clear interface to add and remove thms from the thmsetdata.

1

Currently the thmsetdata api provides functions for api users to define. This has resulted in very inconsistent naming. One such example would be to add a theorem `FOO` to `[compute]`...

LET_ELIM_TAC does not pull out stuff in a existential.

1

Consider something like ``` ?t. (let v = (FOO FOO2) in BAR t v) ``` Calling LET_ELIM_TAC causes you to get this. ``` ∃t. ∀v. Abbrev (v = FOO FOO2)...

With the termination checker slowness, it could be made much faster if isabelle style compute a matrix is done. Reduces the number of solver calls required. https://www21.in.tum.de/~nipkow/pubs/tphols07.pdf

Add simplification for bool_equality stuff.

5

Simplify stuff like this. (A ==> B) (A ==> C) (A /\ B) (A /\ C) There some discord discussion here https://discord.com/channels/1171421764379742258/1171423803553878117/1323470362805145653. Where @mn200 wants to use a custom conversion...

There are random redefinitions of MAX_LIST defined in various places. see https://github.com/HOL-Theorem-Prover/HOL/blob/fcb208759e1eb31a235ed87a5dbe5e2bd2fc498b/examples/logic/modal-tableaux/tableauKTScript.sml#L39C1-L42C4 https://github.com/HOL-Theorem-Prover/HOL/blob/fcb208759e1eb31a235ed87a5dbe5e2bd2fc498b/examples/separationLogic/src/treeScript.sml#L266 Note that there's one duplication in holfoot which is fine to keep as its for automation demonstration.

Given a proof like ``` Theorem foo: FOO a b Proof fs[Abbr`NON_EXISTENT`] ``` Gives the error message `Exception raised at Tactical.FIRST_ASSUM: Exception- HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure...