dest_Free error while interpreting statespace locale · Beginner Questions

Stream: Beginner Questions

Topic: dest_Free error while interpreting statespace locale

Lukas Stevens (Sep 08 2023 at 12:33):

More minimal example:

Scratch1.thy

theory Scratch1
  imports Main "HOL-Statespace.StateSpaceLocale"  "HOL-Library.FSet"
begin

statespace ('k, 'm) set_adt =
  empty :: 'm

datatype set_adt_fset_op_kind = EmptyO

datatype 'a set_adt_fset_op = aF (af: "'a fset")

definition "mk_set_adt_fset_op kind ≡ case kind of EmptyO ⇒ aF fempty"

interpretation set_adt_fset: set_adt
    EmptyO
    af aF
  apply(unfold_locales)
  apply(auto simp: lookup_def)
  done ― ‹‹dest_Free› error here›

end

Lukas Stevens (Sep 08 2023 at 12:56):

I found the culprit, it is in state_space.ML:100

Lukas Stevens (Sep 08 2023 at 13:07):

Replacing

fun comps_of_distinct_thm thm = Thm.prop_of thm
  |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free) |> sort_strings;

with

fun comps_of_distinct_thm thm = Thm.prop_of thm
  |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map Term.term_name |> sort_strings;

in state_space.ML seems to work.

Last updated: Apr 27 2024 at 12:25 UTC