pdc20 (Feb 03 2022 at 02:38): pdc20 (Feb 03 2022 at 02:38):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!
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.
Notification Bot (Feb 05 2022 at 03:40):pdc20 has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC