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 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> |
20 Seq: "\<lbrakk> e \<turnstile> (c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2; e \<turnstile> (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> |
21 e \<turnstile> (c\<^isub>1;;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" | |
21 e \<turnstile> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>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\<^sub>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\<^sub>1 ELSE c\<^sub>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\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
26 e \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" | |
26 e \<turnstile> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" | |
27 |
27 |
28 WhileFalse: "\<not>bval b (s \<circ> venv e) \<Longrightarrow> e \<turnstile> (WHILE b DO c,s) \<Rightarrow> s" | |
28 WhileFalse: "\<not>bval b (s \<circ> venv e) \<Longrightarrow> e \<turnstile> (WHILE b DO c,s) \<Rightarrow> s" | |
29 WhileTrue: |
29 WhileTrue: |
30 "\<lbrakk> bval b (s\<^isub>1 \<circ> venv e); e \<turnstile> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2; |
30 "\<lbrakk> bval b (s\<^sub>1 \<circ> venv e); e \<turnstile> (c,s\<^sub>1) \<Rightarrow> s\<^sub>2; |
31 e \<turnstile> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow> |
31 e \<turnstile> (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> |
32 e \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" | |
32 e \<turnstile> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3" | |
33 |
33 |
34 Var: "(pe,ve(x:=f),f+1) \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> |
34 Var: "(pe,ve(x:=f),f+1) \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> |
35 (pe,ve,f) \<turnstile> ({VAR x; c}, s) \<Rightarrow> t" | |
35 (pe,ve,f) \<turnstile> ({VAR x; c}, s) \<Rightarrow> t" | |
36 |
36 |
37 Call1: "((p,c,ve)#pe,ve,f) \<turnstile> (c, s) \<Rightarrow> t \<Longrightarrow> |
37 Call1: "((p,c,ve)#pe,ve,f) \<turnstile> (c, s) \<Rightarrow> t \<Longrightarrow> |