Theory DEAK_Core_SE

theory (*calc_name_core_se-BEGIN*)DEAK_Core_SE(*calc_name_core_se-END*)
imports Main
begin

(*calc_structure_se-BEGIN*)
type_synonym Action = string

type_synonym Agent = string

type_synonym Atprop = string

datatype Formula = Formula_FboxA Action Formula ("fboxA⇩F _ _" [330,330] 331)
                 | Formula_FdiamA Action Formula ("fdiamA⇩F _ _" [330,330] 331)
                 | Formula_BboxA Action Formula ("bboxA⇩F _ _" [330,330] 331)
                 | Formula_BdiamA Action Formula ("bdiamA⇩F _ _" [330,330] 331)
                 | Formula_FboxK Agent Formula ("fboxK⇩F _ _" [330,330] 331)
                 | Formula_FdiamK Agent Formula ("fdiamK⇩F _ _" [330,330] 331)
                 | Formula_BboxK Agent Formula ("bboxK⇩F _ _" [330,330] 331)
                 | Formula_BdiamK Agent Formula ("bdiamK⇩F _ _" [330,330] 331)
                 | Formula_Atprop Atprop ("_ ⇩F" [320] 330)
                 | Formula_And Formula Formula (infix "∧⇩F" 330)
                 | Formula_ImpL Formula Formula (infix "←⇩F" 330)
                 | Formula_DImpL Formula Formula (infix "-<⇩F" 330)
                 | Formula_DImpR Formula Formula (infix ">-⇩F" 330)
                 | Formula_Or Formula Formula (infix "∨⇩F" 330)
                 | Formula_ImpR Formula Formula (infix "→⇩F" 330)
                 | Formula_Precondition Action ("One⇩F _" [340] 330)
                 | Formula_Top ("⊤⇩F")
                 | Formula_Bot ("⊥⇩F")

datatype Structure = Structure_ForwA Action Structure ("forwA⇩S _ _" [330,330] 331)
                   | Structure_BackA Action Structure ("backA⇩S _ _" [330,330] 331)
                   | Structure_BackK Agent Structure ("backK⇩S _ _" [330,330] 331)
                   | Structure_ForwK Agent Structure ("forwK⇩S _ _" [330,330] 331)
                   | Structure_Bigcomma "Structure list" (";;⇩S _" [330] 331)
                   | Structure_Comma Structure Structure (infix ";⇩S" 340)
                   | Structure_ImpL Structure Structure (infix "←⇩S" 340)
                   | Structure_ImpR Structure Structure (infix "→⇩S" 340)
                   | Structure_Formula Formula ("_ ⇩S" [330] 340)
                   | Structure_Phi Action ("Phi⇩S _" [340] 330)
                   | Structure_Neutral ("I⇩S")

datatype Sequent = Sequent Structure Structure ("_ ⊢⇩S _" [311,311] 310)
(*calc_structure_se-END*)


end