So I'm looking into a file called `AExp.thy`

(link here: https://github.com/seL4/isabelle/blob/master/src/HOL/IMP/AExp.thy) and I'm trying to understand the syntax and translations from line 30.

```
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"
```

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"
syntax
"_State" :: "updbinds => 'a" ("<_>")
translations
"_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!

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