Theory Example

(***********************************************************************************
 * Copyright (c) 2019-2022 Achim D. Brucker
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Examples›

theory
  Example
imports 
  Nano_JSON_Main
begin

text‹
  In this theory, we illustrate various small examples of importing or exporting
  of JSON data from Isabelle/HOL. The examples in this theory do not use the
  type @{term "real"} to avoid the need to depend on the theory
  ``Complex\_Main``.
›

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 example_default
thm example_default_def       
JSON_export example_default
JSON_export example_default file example_default

declare [[JSON_string_type=string, JSON_num_type = nat]]
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 example_string_nat 
thm example_string_nat_def
JSON_export example_string_nat
JSON_export example_string_nat file example_string_nat

declare [[JSON_string_type=string, JSON_num_type = int]]
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 example_string_int

thm example_string_int_def
JSON_export example_string_int
JSON_export example_string_int file example_string_int

declare [[JSON_string_type=String.literal, JSON_num_type = int]]
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 example_literal_int
thm example_literal_int_def
JSON_export example_literal_int
JSON_export example_literal_int file example_literal_int


declare [[JSON_string_type=string, JSON_num_type = string]]
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 example_string_string
thm example_string_string_def
JSON_export example_string_string
JSON_export example_string_string file example_string_string

declare [[JSON_string_type=String.literal, JSON_num_type = String.literal]]
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 example_literal_literal
thm example_literal_literal_def
JSON_export example_literal_literal
JSON_export example_literal_literal file example_literal_literal

text‹xxxx›



text‹
  Using the top level Isar commands defined in the last section, we can now easily define
  JSON-like data: 
›

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 example02


thm example02_def

declare [[JSON_string_type = String.literal]]
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 example02'

thm example02'_def


ML‹ 
@{term ‹JSON‹{"number":31}››}
›


text‹
  Moreover, we can import JSON from external files:
›

lemma "example01 = example03"
  by(simp add: example01_def example03_def)


end