Theory fancy_tabs

(***********************************************************************************
 * Copyright (c) 2016-2020 The University of Sheffield, UK
 *               2019-2020 University of Exeter, UK
 *
 * 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
 *   list of conditions and the following disclaimer.
 *
 * * 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
 ***********************************************************************************)

(* This file is automatically generated, please do not modify! *)

section‹Testing fancy\_tabs›
text‹This theory contains the test cases for fancy\_tabs.›

theory fancy_tabs
imports
  "Shadow_DOM.Shadow_DOM"
begin

definition fancy_tabs_heap :: "heap⇩f⇩i⇩n⇩a⇩l" where
  "fancy_tabs_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])),
    (cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 4)] fmempty None)),
    (cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3)] fmempty None)),
    (cast (element_ptr.Ref 3), cast (create_element_obj ''title'' [cast (character_data_ptr.Ref 1)] fmempty None)),
    (cast (character_data_ptr.Ref 1), cast (create_character_data_obj ''Global%20News'')),
    (cast (element_ptr.Ref 4), cast (create_element_obj ''body'' [cast (element_ptr.Ref 5), cast (element_ptr.Ref 6), cast (element_ptr.Ref 7), cast (element_ptr.Ref 8), cast (element_ptr.Ref 9), cast (element_ptr.Ref 10), cast (element_ptr.Ref 30)] fmempty None)),
    (cast (element_ptr.Ref 5), cast (create_element_obj ''h1'' [cast (character_data_ptr.Ref 2)] fmempty None)),
    (cast (character_data_ptr.Ref 2), cast (create_character_data_obj ''Global%20News'')),
    (cast (element_ptr.Ref 6), cast (create_element_obj ''button'' [cast (character_data_ptr.Ref 3)] fmempty None)),
    (cast (character_data_ptr.Ref 3), cast (create_character_data_obj ''Search'')),
    (cast (element_ptr.Ref 7), cast (create_element_obj ''button'' [cast (character_data_ptr.Ref 4)] fmempty None)),
    (cast (character_data_ptr.Ref 4), cast (create_character_data_obj ''Sign%20In'')),
    (cast (element_ptr.Ref 8), cast (create_element_obj ''br'' [] fmempty None)),
    (cast (element_ptr.Ref 9), cast (create_element_obj ''br'' [] fmempty None)),
    (cast (element_ptr.Ref 10), cast (create_element_obj ''fancy-tabs'' [cast (element_ptr.Ref 11), cast (element_ptr.Ref 12), cast (element_ptr.Ref 13), cast (element_ptr.Ref 14), cast (element_ptr.Ref 15), cast (element_ptr.Ref 22)] (fmap_of_list [(''background'', '''')]) (Some (cast (shadow_root_ptr.Ref 1))))),
    (cast (element_ptr.Ref 11), cast (create_element_obj ''button'' [cast (character_data_ptr.Ref 5)] (fmap_of_list [(''slot'', ''title'')]) None)),
    (cast (character_data_ptr.Ref 5), cast (create_character_data_obj ''Politics'')),
    (cast (element_ptr.Ref 12), cast (create_element_obj ''button'' [cast (character_data_ptr.Ref 6)] (fmap_of_list [(''slot'', ''title''), (''selected'', '''')]) None)),
    (cast (character_data_ptr.Ref 6), cast (create_character_data_obj ''Sports'')),
    (cast (element_ptr.Ref 13), cast (create_element_obj ''button'' [cast (character_data_ptr.Ref 7)] (fmap_of_list [(''slot'', ''title'')]) None)),
    (cast (character_data_ptr.Ref 7), cast (create_character_data_obj ''Culture'')),
    (cast (element_ptr.Ref 14), cast (create_element_obj ''section'' [cast (character_data_ptr.Ref 8)] fmempty None)),
    (cast (character_data_ptr.Ref 8), cast (create_character_data_obj ''content%20panel%201'')),
    (cast (element_ptr.Ref 15), cast (create_element_obj ''ul'' [cast (element_ptr.Ref 16), cast (element_ptr.Ref 18), cast (element_ptr.Ref 20)] fmempty None)),
    (cast (element_ptr.Ref 16), cast (create_element_obj ''li'' [cast (character_data_ptr.Ref 9), cast (element_ptr.Ref 17)] fmempty None)),
    (cast (character_data_ptr.Ref 9), cast (create_character_data_obj ''News%20Item%201'')),
    (cast (element_ptr.Ref 17), cast (create_element_obj ''button'' [cast (character_data_ptr.Ref 10)] fmempty None)),
    (cast (character_data_ptr.Ref 10), cast (create_character_data_obj ''Share'')),
    (cast (element_ptr.Ref 18), cast (create_element_obj ''li'' [cast (character_data_ptr.Ref 11), cast (element_ptr.Ref 19)] fmempty None)),
    (cast (character_data_ptr.Ref 11), cast (create_character_data_obj ''News%20Item%202'')),
    (cast (element_ptr.Ref 19), cast (create_element_obj ''button'' [cast (character_data_ptr.Ref 12)] fmempty None)),
    (cast (character_data_ptr.Ref 12), cast (create_character_data_obj ''Share'')),
    (cast (element_ptr.Ref 20), cast (create_element_obj ''li'' [cast (character_data_ptr.Ref 13), cast (element_ptr.Ref 21)] fmempty None)),
    (cast (character_data_ptr.Ref 13), cast (create_character_data_obj ''News%20Item%203'')),
    (cast (element_ptr.Ref 21), cast (create_element_obj ''button'' [cast (character_data_ptr.Ref 14)] fmempty None)),
    (cast (character_data_ptr.Ref 14), cast (create_character_data_obj ''Share'')),
    (cast (element_ptr.Ref 22), cast (create_element_obj ''section'' [cast (character_data_ptr.Ref 15)] fmempty None)),
    (cast (character_data_ptr.Ref 15), cast (create_character_data_obj ''content%20panel%203'')),
    (cast (shadow_root_ptr.Ref 1), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 23), cast (element_ptr.Ref 24), cast (element_ptr.Ref 26), cast (element_ptr.Ref 28), cast (element_ptr.Ref 29)])),
    (cast (element_ptr.Ref 23), cast (create_element_obj ''style'' [cast (character_data_ptr.Ref 16)] fmempty None)),
    (cast (character_data_ptr.Ref 16), cast (create_character_data_obj ''---shortened---'')),
    (cast (element_ptr.Ref 24), cast (create_element_obj ''div'' [cast (element_ptr.Ref 25)] (fmap_of_list [(''id'', ''tabs'')]) None)),
    (cast (element_ptr.Ref 25), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''tabsSlot''), (''name'', ''title'')]) None)),
    (cast (element_ptr.Ref 26), cast (create_element_obj ''div'' [cast (element_ptr.Ref 27)] (fmap_of_list [(''id'', ''panels'')]) None)),
    (cast (element_ptr.Ref 27), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''panelsSlot'')]) None)),
    (cast (element_ptr.Ref 28), cast (create_element_obj ''button'' [cast (character_data_ptr.Ref 17)] fmempty None)),
    (cast (character_data_ptr.Ref 17), cast (create_character_data_obj ''Previous%20Tab'')),
    (cast (element_ptr.Ref 29), cast (create_element_obj ''button'' [cast (character_data_ptr.Ref 18)] (fmap_of_list [(''style'', ''float:right'')]) None)),
    (cast (character_data_ptr.Ref 18), cast (create_character_data_obj ''Next%20Tab'')),
    (cast (element_ptr.Ref 30), cast (create_element_obj ''script'' [] fmempty None))]"

definition fancy_tabs_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "fancy_tabs_document = Some (cast (document_ptr.Ref 1))"


end