equal
deleted
inserted
replaced
|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Def_Init_Small |
|
4 imports Star Com Def_Init_Exp |
|
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 |
|
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')" | |
|
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 |