Stream: Beginner Questions

Topic: Understanding syntax definitions

view this post on Zulip pdc20 (Feb 03 2022 at 02:38):

So I'm looking into a file called AExp.thy (link here: and I'm trying to understand the syntax and translations from line 30.

definition null_state ("<>") where
  "null_state ≡ λx. 0"
  "_State" :: "updbinds => 'a" ("<_>")
  "_State ms" == "_Update <> ms"
  "_State (_updbinds b bs)" <= "_Update (_State b) bs"

The writer(s) then demonstrate the translation in effect through a lemma

lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))" by (rule refl)

Could I please know how Isabelle managed to translate <a := 1, b := 2> into (<> (a := 1)) (b := (2::int))? My initial thought process went as follows but I'm not sure if it's right.

<a := 1, b := 2> = <b := 2> (a := 1)
                 = (<> (a := 1)) (b := 2)

My teammates would also like to change the definition such that it now uses option types. They would prefer <a := 1, b := 2> to be translated into (<> (a := Some 1)) (b := Some 2) so they proposed

definition null_state :: "'a => 'b option" ("<>") where
  "null_state ≡ λx. None"
  "_State" :: "updbinds => 'a" ("<_>")
  "_State ms" == "_Update <> (Some ms)"
  "_State (_updbinds b bs)" <= "_Update (_State b) bs"

Unfortunately they got the following error:

Error in syntax translation rule: rhs contains extra variables
("_State" ms) ↝ ("_Update" "\<^const>AExp.null_state" (Some ms))

We aren't exactly sure why this error pops up. Could we please have some help?

Thanks in advance!

view this post on Zulip Florian Sextl (Feb 03 2022 at 09:24):

I'm not an expert in using the syntax and translation commands but I hope that I can still help you.

First of all, you seem to want to switch from states that are simple functions of type 'a ⇒ nat to maps of type 'a ⇀ 'b. Thus, you can leverage the map update syntax, e.g. exchange _Update with _MapUpd and updbinds with maplets. This will directly wrap the values that you map to in a Some.

Now about the error you get: Some is just an unknown variable on a syntactic level so you can't use it in this way. You can use constant names like Some if you add a CONST in front of them (e.g. m(x := CONST Some y) is the base case of the map update syntax). Another problem with your approach is that you would not wrap the value in a Some in your code but, afaict, the result of the function update, which isn't what you'd want.

Lastly, let my try to explain how the syntax translation works. <a := 1, b := 2> is on the syntactic level an application of _State to an object of updbinds (which is several := notations separated by a comma). The second translation rule for _State is just a print rule, so it doesn't matter in this case. The first rule however tells us that <a:=1,b:=2> is the same as <> (a:=1,b:=2) which is just the syntax for function updates and thus the same as fun_upd (fun_upd (λ_. 0) a 1) b 2.

Last updated: Jul 15 2022 at 23:21 UTC