8 inductive |
8 inductive |
9 big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55) |
9 big_step :: "penv \<Rightarrow> com \<times> state \<Rightarrow> state \<Rightarrow> bool" ("_ \<turnstile> _ \<Rightarrow> _" [60,0,60] 55) |
10 where |
10 where |
11 Skip: "pe \<turnstile> (SKIP,s) \<Rightarrow> s" | |
11 Skip: "pe \<turnstile> (SKIP,s) \<Rightarrow> s" | |
12 Assign: "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" | |
12 Assign: "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" | |
13 Semi: "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow> |
13 Seq: "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow> |
14 pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" | |
14 pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" | |
15 |
15 |
16 IfTrue: "\<lbrakk> bval b s; pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
16 IfTrue: "\<lbrakk> bval b s; pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
17 pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" | |
17 pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" | |
18 IfFalse: "\<lbrakk> \<not>bval b s; pe \<turnstile> (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
18 IfFalse: "\<lbrakk> \<not>bval b s; pe \<turnstile> (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |