Theory Def_Init_Small

(* Author: Tobias Nipkow *)

theory Def_Init_Small
imports Star Com Def_Init_Exp
begin

subsection "Initialization-Sensitive Small Step Semantics"

inductive
  small_step :: "(com × state) => (com × state) => bool" (infix "->" 55)
where
Assign:  "aval a s = Some i ==> (x ::= a, s) -> (SKIP, s(x := Some i))" |

Seq1:   "(SKIP;c,s) -> (c,s)" |
Seq2:   "(c⇣1,s) -> (c⇣1',s') ==> (c⇣1;c⇣2,s) -> (c⇣1';c⇣2,s')" |

IfTrue:  "bval b s = Some True ==> (IF b THEN c⇣1 ELSE c⇣2,s) -> (c⇣1,s)" |
IfFalse: "bval b s = Some False ==> (IF b THEN c⇣1 ELSE c⇣2,s) -> (c⇣2,s)" |

While:   "(WHILE b DO c,s) -> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"

lemmas small_step_induct = small_step.induct[split_format(complete)]

abbreviation small_steps :: "com * state => com * state => bool" (infix "->*" 55)
where "x ->* y == star small_step x y"

end