Theory Strong_Security.Types

(*
Title: Strong-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
*)
theory Types
imports Main
begin

― ‹type parameters:›
― ‹'exp: expressions (arithmetic, boolean...)›
― ‹'val: values›
― ‹'id: identifier names›
― ‹'com: commands›
― ‹'d: domains›

text‹This is a collection of type synonyms. Note that not all of these type synonyms are 
  used within Strong-Security - some are used in WHATandWHERE-Security.›

― ‹type for memory states - map ids to values›
type_synonym ('id, 'val) State = "'id ⇒ 'val"

― ‹type for evaluation functions mapping expressions to a values depending on a state›
type_synonym ('exp, 'id, 'val) Evalfunction = 
  "'exp ⇒ ('id, 'val) State ⇒ 'val"

― ‹define configurations with threads as pair of commands and states›
type_synonym ('id, 'val, 'com) TConfig = "'com × ('id, 'val) State"

― ‹define configurations with thread pools as pair of command lists (thread pool) and states›
type_synonym ('id, 'val, 'com) TPConfig = 
  "('com list) × ('id, 'val) State"

― ‹type for program states (including the set of commands and a symbol for terminating - None)›
type_synonym 'com ProgramState = "'com option"

― ‹type for configurations with program states›
type_synonym ('id, 'val, 'com) PSConfig = 
  "'com ProgramState × ('id, 'val) State"

― ‹type for labels with a list of spawned threads›
type_synonym 'com Label = "'com list"

― ‹type for step relations from single commands to a program state, with a label›
type_synonym ('exp, 'id, 'val, 'com) TLSteps = "
  (('id, 'val, 'com) TConfig × 'com Label 
    × ('id, 'val, 'com) PSConfig) set"

― ‹curried version of previously defined type›
type_synonym ('exp, 'id, 'val, 'com) TLSteps_curry =
"'com ⇒ ('id, 'val) State ⇒ 'com Label ⇒ 'com ProgramState 
  ⇒ ('id, 'val) State ⇒ bool"

― ‹type for step relations from thread pools to thread pools›
type_synonym ('exp, 'id, 'val, 'com) TPSteps = "
  (('id, 'val, 'com) TPConfig × ('id, 'val, 'com) TPConfig) set"

― ‹curried version of previously defined type›
type_synonym ('exp, 'id, 'val, 'com) TPSteps_curry =
"'com list ⇒ ('id, 'val) State ⇒ 'com list ⇒ ('id, 'val) State ⇒ bool"

― ‹define type of step relations for single threads to thread pools›
type_synonym ('exp, 'id, 'val, 'com) TSteps = 
  "(('id, 'val, 'com) TConfig × ('id, 'val, 'com) TPConfig) set"

― ‹define the same type as TSteps, but in a curried version (allowing syntax abbreviations)›
type_synonym ('exp, 'id, 'val, 'com) TSteps_curry =
"'com ⇒ ('id, 'val) State ⇒ 'com list ⇒ ('id, 'val) State ⇒ bool"

― ‹type for simple domain assignments; 'd has to be an instance of order (partial order›
type_synonym ('id, 'd) DomainAssignment = "'id ⇒ 'd::order"

type_synonym 'com Bisimulation_type = "(('com list) × ('com list)) set"

― ‹type for escape hatches›
type_synonym ('d, 'exp) Hatch = "'d × 'exp"

― ‹type for sets of escape hatches›
type_synonym ('d, 'exp) Hatches = "(('d, 'exp) Hatch) set"

― ‹type for local escape hatches›
type_synonym ('d, 'exp) lHatch = "'d × 'exp × nat"

― ‹type for sets of local escape hatches›
type_synonym ('d, 'exp) lHatches = "(('d, 'exp) lHatch) set"


end