equal
deleted
inserted
replaced
|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Def_Ass_Small imports Star Com Def_Ass_Exp |
|
4 begin |
|
5 |
|
6 subsection "Initialization-Sensitive Small Step Semantics" |
|
7 |
|
8 inductive |
|
9 small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55) |
|
10 where |
|
11 Assign: "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" | |
|
12 |
|
13 Semi1: "(SKIP;c,s) \<rightarrow> (c,s)" | |
|
14 Semi2: "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" | |
|
15 |
|
16 IfTrue: "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" | |
|
17 IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
|
18 |
|
19 While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)" |
|
20 |
|
21 lemmas small_step_induct = small_step.induct[split_format(complete)] |
|
22 |
|
23 abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55) |
|
24 where "x \<rightarrow>* y == star small_step x y" |
|
25 |
|
26 end |