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

― ‹SYNTAX›

― ‹Commands for the multi-threaded while language with fork (to instantiate 'com)›
datatype ('exp, 'id) MWLfCom 
  = Skip (‹skip›)
  | Assign "'id" "'exp" 
       (‹_:=_› [70,70] 70)

  | Seq "('exp, 'id) MWLfCom" "('exp, 'id) MWLfCom" 
       (‹_;_› [61,60] 60)
 
  | If_Else "'exp" "('exp, 'id) MWLfCom" "('exp, 'id) MWLfCom"
       (‹if _ then _ else _ fi› [80,79,79] 70)

  | While_Do "'exp" "('exp, 'id) MWLfCom" 
       (‹while _ do _ od› [80,79] 70)

  | Fork "('exp, 'id) MWLfCom" "(('exp, 'id) MWLfCom) list"
       (‹fork _ _› [70,70] 70)

― ‹SEMANTICS›

locale MWLf_semantics =
fixes E :: "('exp, 'id, 'val) Evalfunction"
and BMap :: "'val → bool"
begin

― ‹steps semantics, set of deterministic steps from single threads to either single threads or thread pools›
inductive_set 
MWLfSteps_det :: "('exp, 'id, 'val, ('exp, 'id) MWLfCom) TSteps"
and MWLfSteps_det' :: "('exp, 'id, 'val, ('exp, 'id) MWLfCom) TSteps_curry"
  (‹(1⟨_,/_⟩) →/ (1⟨_,/_⟩)› [0,0,0,0] 81)
where
"⟨c1,m1⟩ → ⟨c2,m2⟩ ≡ ((c1,m1),(c2,m2)) ∈ MWLfSteps_det" |
skip: "⟨skip,m⟩ → ⟨[],m⟩" |
assign: "(E e m) = v ==> ⟨x := e,m⟩ → ⟨[],m(x := v)⟩" |
seq1: "⟨c1,m⟩ → ⟨[],m'⟩ ==> ⟨c1;c2,m⟩ → ⟨[c2],m'⟩" |
seq2: "⟨c1,m⟩ → ⟨c1'#V,m'⟩ ==> ⟨c1;c2,m⟩ → ⟨(c1';c2)#V,m'⟩" |
iftrue: "BMap (E b m) = True ==>
    ⟨if b then c1 else c2 fi,m⟩ → ⟨[c1],m⟩" |
iffalse: "BMap (E b m) = False ==>
    ⟨if b then c1 else c2 fi,m⟩ → ⟨[c2],m⟩" |
whiletrue: "BMap (E b m) = True ==>
    ⟨while b do c od,m⟩ → ⟨[c;(while b do c od)],m⟩" |
whilefalse: "BMap (E b m) = False ==>
    ⟨while b do c od,m⟩ → ⟨[],m⟩" |
fork: "⟨fork c V,m⟩ → ⟨c#V,m⟩"

inductive_cases MWLfSteps_det_cases:
"⟨skip,m⟩ → ⟨W,m'⟩"
"⟨x := e,m⟩ → ⟨W,m'⟩"
"⟨c1;c2,m⟩ → ⟨W,m'⟩"
"⟨if b then c1 else c2 fi,m⟩ → ⟨W,m'⟩"
"⟨while b do c od,m⟩ → ⟨W,m'⟩"
"⟨fork c V,m⟩ → ⟨W,m'⟩"

― ‹non-deterministic, possibilistic system step (added for intuition, not used in the proofs)›
inductive_set
MWLfSteps_ndet :: "('exp, 'id, 'val, ('exp,'id) MWLfCom) TPSteps"
and MWLfSteps_ndet' :: "('exp, 'id, 'val, ('exp,'id) MWLfCom) TPSteps_curry"
(‹(1⟨_,/_⟩) →/ (1⟨_,/_⟩)› [0,0,0,0] 81)
where
"⟨V1,m1⟩ → ⟨V2,m2⟩ ≡ ((V1,m1),(V2,m2)) ∈ MWLfSteps_ndet" |
"⟨ci,m⟩ → ⟨c,m'⟩ ==> ⟨Vf @ [ci] @ Va,m⟩ → ⟨Vf @ c @ Va,m'⟩"

end


end