--- a/src/HOL/IMP/Big_Step.thy Tue Jun 18 17:38:07 2013 +0200
+++ b/src/HOL/IMP/Big_Step.thy Tue Jun 18 15:52:47 2013 -0700
@@ -14,19 +14,15 @@
inductive
big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
where
-Skip: "(SKIP,s) \<Rightarrow> s" |
-Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
-Seq: "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
- (c\<^isub>1;;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
-
-IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
- (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
-IfFalse: "\<lbrakk> \<not>bval b s; (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
- (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
-
+Skip: "(SKIP,s) \<Rightarrow> s" |
+Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
+Seq: "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow> (c\<^isub>1;;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
+IfFalse: "\<lbrakk> \<not>bval b s; (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
-WhileTrue: "\<lbrakk> bval b s\<^isub>1; (c,s\<^isub>1) \<Rightarrow> s\<^isub>2; (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk>
- \<Longrightarrow> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
+WhileTrue:
+"\<lbrakk> bval b s\<^isub>1; (c,s\<^isub>1) \<Rightarrow> s\<^isub>2; (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk>
+\<Longrightarrow> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
text_raw{*}%endsnip*}
text_raw{*\snip{BigStepEx}{1}{2}{% *}