## Stream: Isabelle/ML

### Topic: Test for equality-by-simplification in ML

#### Hanno Becker (Mar 03 2023 at 08:12):

Hi! What would be the shortest/cleanest way to check, within SML, whether within a given proof context, the simplifier would be able to prove two terms equal? In other words, given terms `s` and `t` of the same type, I'd like to know, in ML, whether

``````lemma: <s = t>
by simp
``````

would succeed.

#### Kevin Kappelmann (Mar 03 2023 at 08:57):

That's how I would do it:

``````ML‹
(*example values*)
val (s, t) = (@{cterm "0 :: nat"}, @{cterm "0 + 0 :: nat "})

val ctxt = @{context}
val cT = Thm.ctyp_of_cterm s
val goal = \<^instantiate>‹'a = cT and s and t in
cterm ‹Trueprop (s = t)› for s :: 'a and t›
val simp_tac = Simplifier.simp_tac ctxt |> SOLVED' |> HEADGOAL |> SINGLE
val thmOpt = Goal.init goal |> simp_tac |> Option.map Goal.conclude
val _ = @{print} thmOpt
›
``````

#### Kevin Kappelmann (Mar 03 2023 at 09:00):

Edit: fixed a line

#### Hanno Becker (Mar 04 2023 at 06:04):

Awesome, thank you @Kevin Kappelmann !

Last updated: Dec 07 2023 at 16:21 UTC