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