(***********************************************************************************
 * 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 Real›
theory 
  Example_Real
imports 
  Nano_JSON_Main
  Complex_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 make use @{type
 "real"}. This is possible, as this theory imports the theory @{theory
 "Complex_Main"}.
 ›



declare [[JSON_num_type = real]]

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

thm example_default_real_def

JSON_export example_default_real
JSON_export example_default_real file example_default_real  

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 = real]]
JSON ‹
 "menu": {
 "id": "file",
 "value": "File",
 "popup": {
 "menuitem": [
 {"value": "New", "onclick": "CreateNewDoc()"},
 {"value": "Open", "onclick": "OpenDoc()"},
 {"value": "Close", "onclick": "CloseDoc()"}
 ]
 }
 , "flag":true, "number": 42.8}
 › defining example_string_real
thm example_string_real_def
JSON_export example_string_real
JSON_export example_string_real file example_string_real

declare [[JSON_string_type=String.literal, JSON_num_type = real]]
JSON ‹
 "menu": {
 "id": "file",
 "value": "File",
 "popup": {
 "menuitem": [
 {"value": "New", "onclick": "CreateNewDoc()"},
 {"value": "Open", "onclick": "OpenDoc()"},
 {"value": "Close", "onclick": "CloseDoc()"}
 ]
 }
 , "flag":true, "number":42.8}
 › defining example_literal_real 
thm example_literal_real_def
JSON_export example_literal_real
JSON_export example_literal_real file example_literal_real


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.5}
 › defining example_string_string
thm example_string_string_def 
JSON_export example_string_string
JSON_export example_string_string file example_literal_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.5}
 › defining example_literal_literal
thm example_literal_literal_def
JSON_export example_literal_literal
JSON_export example_literal_literal file example_literal_literal

end