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: Apr 19 2024 at 20:15 UTC