JSON (JavaScript Object Notation) is common format for exchanging data. Thus, sometimes it would be handy to be able to “import” JSON-formatted data into Isabelle/HOL, e.g., as part of a datatype package (implemented in Isabelle/ML) for using the data as part of a system verification (in Isabelle/HOL).

Using our AFP entry “Nano JSON” [1] this is now easy. It provides both import and export of JSON-formatted data into Isabelle - both on the level of Isabelle/ML and Isabelle/HOL. Thus, it allows users of Isabelle/HOL to work with JSON-formatted data in Isabelle without needing to implement import or export functionalities in ML. At the same time, user that want to implement their own datatype package can use the Isabelle/ML API provided by AFP entry “Nano JSON”.

For example, assuming a simple JSON encoded data like

{
    "menu": {
        "id": "file",
        "value": "File",
        "popup": {
            "menuitem": [
                {"value": "New", "onclick": "CreateNewDoc()"},
                {"value": "Open", "onclick": "OpenDoc()"},
                {"value": "Close", "onclick": "CloseDoc()"}
            ]
        }  
    }, 
    "flag":true, 
    "number":42
}

stored in a file example.json, you can now import this data into Isabelle

JSON_file "example.json" defining example

and use it in a formal context, such as

lemma ‹([STR ''onclick''], STRING STR ''CreateNewDoc()'') ∈ set(nj_filter (STR ''onclick'') example_literal_literal)›
  by(normalization)

Alternative ways of importing JSON

For short JSON-snippets, you can use an antiquotation:

lemma ‹y == JSON ‹{"name": true}› ›
  oops

Moreover, for you can also use a new Isar command that allows for inlining JSON into Isabelle theories:

JSON ‹
{
    "menu": {
        "id": "file",
        "value": "File",
        "popup": {
            "menuitem": [
                {"value": "New", "onclick": "CreateNewDoc()"},
                {"value": "Open", "onclick": "OpenDoc()"},
                {"value": "Close", "onclick": "CloseDoc()"}
            ]
        }  
    }, 
    "flag":true, 
    "number":42
}
› defining example04

Exporting JSON

Exporting JSON is easy, assuming that the data has already been converted the HOL-representation of JSON provided:

JSON_export example file example

References