14 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')" | |
14 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')" | |
15 |
15 |
16 IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" | |
16 IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" | |
17 IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
17 IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
18 |
18 |
19 While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)" |
19 While: "(WHILE b DO c,s) \<rightarrow> |
|
20 (IF b THEN c; WHILE b DO c ELSE SKIP,s)" |
20 text_raw{*}%endsnip*} |
21 text_raw{*}%endsnip*} |
21 |
22 |
22 |
23 |
23 abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55) |
24 abbreviation |
|
25 small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55) |
24 where "x \<rightarrow>* y == star small_step x y" |
26 where "x \<rightarrow>* y == star small_step x y" |
25 |
27 |
26 subsection{* Executability *} |
28 subsection{* Executability *} |
27 |
29 |
28 code_pred small_step . |
30 code_pred small_step . |