Theory Def_Init_Big

(* Author: Tobias Nipkow *)

theory Def_Init_Big
imports Com Def_Init_Exp
begin

subsection "Initialization-Sensitive Big Step Semantics"

inductive
  big_step :: "(com × state option) => state option => bool" (infix "=>" 55)
where
None: "(c,None) => None" |
Skip: "(SKIP,s) => s" |
AssignNone: "aval a s = None ==> (x ::= a, Some s) => None" |
Assign: "aval a s = Some i ==> (x ::= a, Some s) => Some(s(x := Some i))" |
Seq:    "(c⇣1,s⇣1) => s⇣2 ==> (c⇣2,s⇣2) => s⇣3 ==> (c⇣1;c⇣2,s⇣1) => s⇣3" |

IfNone:  "bval b s = None ==> (IF b THEN c⇣1 ELSE c⇣2,Some s) => None" |
IfTrue:  "[| bval b s = Some True;  (c⇣1,Some s) => s' |] ==>
  (IF b THEN c⇣1 ELSE c⇣2,Some s) => s'" |
IfFalse: "[| bval b s = Some False;  (c⇣2,Some s) => s' |] ==>
  (IF b THEN c⇣1 ELSE c⇣2,Some s) => s'" |

WhileNone: "bval b s = None ==> (WHILE b DO c,Some s) => None" |
WhileFalse: "bval b s = Some False ==> (WHILE b DO c,Some s) => Some s" |
WhileTrue:
  "[| bval b s = Some True;  (c,Some s) => s';  (WHILE b DO c,s') => s'' |] ==>
  (WHILE b DO c,Some s) => s''"

lemmas big_step_induct = big_step.induct[split_format(complete)]

end