Quelle  Language.thy

(*
 * Copyright 2016, Data61, CSIRO
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)

section ‹The COMPLX Syntax›

theory Language
imports Main
begin

subsection ‹The Core Language›

text ‹We use a shallow embedding of boolean expressions as well as assertions
  sets of states.
 ›

type_synonym 's bexp = "'s set"
type_synonym 's assn = "'s set"

datatype ('s, 'p, 'f) com =
    Skip
  | Basic "'s ==> 's"
  | Spec "('s × 's) set"
  | Seq "('s ,'p, 'f) com" "('s,'p, 'f) com"    
  | Cond "'s bexp" "('s,'p,'f) com"  "('s,'p,'f) com"
  | While "'s bexp" "('s,'p,'f) com"
  | Call "'p"
  | DynCom "'s ==> ('s,'p,'f) com" 
  | Guard "'f" "'s bexp" "('s,'p,'f) com" 
  | Throw
  | Catch "('s,'p,'f) com" "('s,'p,'f) com"
  | Parallel "('s, 'p, 'f) com list"
  | Await "'s bexp" "('s,'p,'f) com"


subsection ‹Derived Language Constructs›

text ‹We inherit the remainder of derived language constructs from SIMPL›

definition
  raise:: "('s ==> 's) ==> ('s,'p,'f) com" where
  "raise f = Seq (Basic f) Throw"

definition
  condCatch:: "('s,'p,'f) com ==> 's bexp ==> ('s,'p,'f) com ==> ('s,'p,'f) com" where
  "condCatch c₁ b c₂ = Catch c₁ (Cond b c₂ Throw)"

definition
  bind:: "('s ==> 'v) ==> ('v ==> ('s,'p,'f) com) ==> ('s,'p,'f) com" where
  "bind e c = DynCom (λs. c (e s))"

definition
  bseq:: "('s,'p,'f) com ==> ('s,'p,'f) com ==> ('s,'p,'f) com" where
  "bseq = Seq"
 
definition
  block:: "['s==>'s ,('s,'p,'f) com,'s==>'s==>'s,'s==>'s==>('s,'p,'f) com]==>('s,'p,'f) com"
where
  "block init bdy restore return =
    DynCom (λs. (Seq (Catch (Seq (Basic init) bdy) (Seq (Basic (restore s)) Throw))
                            (DynCom (λt. Seq (Basic (restore s)) (return s t))))
                        )" 

definition
  call:: "('s==>'s) ==> 'p ==> ('s ==> 's ==> 's)==>('s==>'s==>('s,'p,'f) com)==>('s,'p,'f)com" where
  "call init p restore return = block init (Call p) restore return"

definition
  dynCall:: "('s==>'s) ==> ('s ==> 'p) ==> ('s ==> 's ==> 's) ==>
             ('s ==> 's ==> ('s,'p,'f) com) ==> ('s,'p,'f) com" where
  "dynCall init p restore return = DynCom (λs. call init (p s) restore return)"

definition
  fcall:: "('s==>'s) ==> 'p ==> ('s ==> 's ==> 's)==>('s ==> 'v) ==> ('v==>('s,'p,'f) com)
            ==>('s,'p,'f) com" where
  "fcall init p restore result return = call init p restore (λs t. return (result t))"

definition
  lem:: "'x ==> ('s,'p,'f)com ==>('s,'p,'f)com" where
  "lem x c = c"

primrec switch:: "('s ==> 'v) ==> ('v set × ('s,'p,'f) com) list ==> ('s,'p,'f) com" 
where
"switch v [] = Skip" |
"switch v (Vc#vs) = Cond {s. v s ∈ fst Vc} (snd Vc) (switch v vs)"

definition guaranteeStrip:: "'f ==> 's set ==> ('s,'p,'f) com ==> ('s,'p,'f) com"
  where "guaranteeStrip f g c = Guard f g c"

definition guaranteeStripPair:: "'f ==> 's set ==> ('f × 's set)"
  where "guaranteeStripPair f g = (f,g)"

primrec guards:: "('f × 's set ) list ==> ('s,'p,'f) com ==> ('s,'p,'f) com"
where
"guards [] c = c" |
"guards (g#gs) c = Guard (fst g) (snd g) (guards gs c)"

definition
  while::  "('f × 's set) list ==> 's bexp ==> ('s,'p,'f) com ==> ('s, 'p, 'f) com"
where
  "while gs b c = guards gs (While b (Seq c (guards gs Skip)))"

definition
  whileAnno:: 
  "'s bexp ==> 's assn ==> ('s × 's) assn ==> ('s,'p,'f) com ==> ('s,'p,'f) com" where
  "whileAnno b I V c = While b c"

definition
  whileAnnoG:: 
  "('f × 's set) list ==> 's bexp ==> 's assn ==> ('s × 's) assn ==>
     ('s,'p,'f) com ==> ('s,'p,'f) com" where
  "whileAnnoG gs b I V c = while gs b c"
 
definition
  specAnno::  "('a ==> 's assn) ==> ('a ==> ('s,'p,'f) com) ==>
                         ('a ==> 's assn) ==> ('a ==> 's assn) ==> ('s,'p,'f) com"
  where "specAnno P c Q A = (c undefined)"

definition
  whileAnnoFix:: 
  "'s bexp ==> ('a ==> 's assn) ==> ('a ==> ('s × 's) assn) ==> ('a ==> ('s,'p,'f) com) ==>
     ('s,'p,'f) com" where
  "whileAnnoFix b I V c = While b (c undefined)"

definition
  whileAnnoGFix:: 
  "('f × 's set) list ==> 's bexp ==> ('a ==> 's assn) ==> ('a ==> ('s × 's) assn) ==>
     ('a ==> ('s,'p,'f) com) ==> ('s,'p,'f) com" where
  "whileAnnoGFix gs b I V c = while gs b (c undefined)"

definition if_rel::"('s ==> bool) ==> ('s ==> 's) ==> ('s ==> 's) ==> ('s ==> 's) ==> ('s × 's) set" 
  where "if_rel b f g h = {(s,t). if b s then t = f s else t = g s ∨ t = h s}"

lemma fst_guaranteeStripPair: "fst (guaranteeStripPair f g) = f"
  by (simp add: guaranteeStripPair_def)

lemma snd_guaranteeStripPair: "snd (guaranteeStripPair f g) = g"
  by (simp add: guaranteeStripPair_def)

end