Understanding syntax definitions · Beginner Questions

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

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"
syntax
  "_State" :: "updbinds => 'a" ("<_>")
translations
  "_State ms" == "_Update <> (Some ms)"
  "_State (_updbinds b bs)" <= "_Update (_State b) bs"

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

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.

Stream: Beginner Questions

Topic: Understanding syntax definitions

pdc20 (Feb 03 2022 at 02:38):

Florian Sextl (Feb 03 2022 at 09:24):