Stream: General

Topic: Datatype record update

view this post on Zulip Gergely Buday (Apr 19 2023 at 15:22):

When I have

    ( case ltl (input s) of
                                  LNil ⇒ s
                                | tail ⇒ s ⦇ input := tail ⦈
     )

for a coinductive list, I get

Undefined constant: "input_update"

where my datatype record definition is

datatype state = State (funs: "dec list") (clock: nat) (input: "char llist") ("output": "char list")

I got the record update syntax from src/HOL/ex/Datatype_Record_Examples.thy

Am I doing something wrong or this is a bug in the datatype package?

view this post on Zulip Dmitriy Traytel (Apr 19 2023 at 15:50):

To use the infrastructure from HOL-Library.Datatype_Record, you need to use the command datatype_record explicitly (as the example file shows) instead of the datatype command.

view this post on Zulip Gergely Buday (Apr 20 2023 at 08:59):

Thanks @Dmitriy Traytel . Now I got an ambigous parse tree error:

--- parsetree1.txt  2023-04-20 09:47:12.084782007 +0100
+++ parsetree2.txt  2023-04-20 09:47:31.740761144 +0100
@@ -25,4 +25,4 @@
                         ("_cargs" ("_applC" ("_position" next_char) ("_applC" ("_position" input) ("_position" s)))
                           ("_case_syntax" ("_applC" ("_position" ltl) ("_applC" ("_position" input) ("_position" s)))
                             ("_case2" ("_case1" ("_position" LNil) ("_position" s))
-                              ("_case1" ("_position" tail) ("_datatype_record_update" ("_position" s) ("_datatype_field_update" ("_constify" input) ("_position" tail))))))))))))))))))
+                              ("_case1" ("_position" tail) ("_record_update" ("_position" s) ("_field_update" ("_constify" input) ("_position" tail))))))))))))))))))

so Isabelle cannot differentiate between datatype record update and classical record update syntax: both are (| ... |) . How can I inform Isabelle that I use datatype record update? My function definition contains a type prescription what my record's type is, and it was defined through a datatype declaration. Is that not enough?

Last updated: May 02 2024 at 08:19 UTC