15 big_step :: "penv \<times> venv \<times> nat \<Rightarrow> com \<times> store \<Rightarrow> store \<Rightarrow> bool" |
15 big_step :: "penv \<times> venv \<times> nat \<Rightarrow> com \<times> store \<Rightarrow> store \<Rightarrow> bool" |
16 ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55) |
16 ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55) |
17 where |
17 where |
18 Skip: "e \<turnstile> (SKIP,s) \<Rightarrow> s" | |
18 Skip: "e \<turnstile> (SKIP,s) \<Rightarrow> s" | |
19 Assign: "(pe,ve,f) \<turnstile> (x ::= a,s) \<Rightarrow> s(ve x := aval a (s o ve))" | |
19 Assign: "(pe,ve,f) \<turnstile> (x ::= a,s) \<Rightarrow> s(ve x := aval a (s o ve))" | |
20 Semi: "\<lbrakk> e \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; e \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow> |
20 Seq: "\<lbrakk> e \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; e \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow> |
21 e \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" | |
21 e \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" | |
22 |
22 |
23 IfTrue: "\<lbrakk> bval b (s \<circ> venv e); e \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
23 IfTrue: "\<lbrakk> bval b (s \<circ> venv e); e \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
24 e \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" | |
24 e \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" | |
25 IfFalse: "\<lbrakk> \<not>bval b (s \<circ> venv e); e \<turnstile> (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
25 IfFalse: "\<lbrakk> \<not>bval b (s \<circ> venv e); e \<turnstile> (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |