diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Compiler0.thy
--- a/src/HOL/IMP/Compiler0.thy	Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/IMP/Compiler0.thy	Wed Jul 11 11:14:51 2007 +0200
@@ -20,48 +20,32 @@
 text {* We describe execution of programs in the machine by
   an operational (small step) semantics:
 *}
-consts  stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
-
-syntax
-  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-               ("_ |- (3<_,_>/ -1-> <_,_>)" [50,0,0,0,0] 50)
-  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-               ("_ |-/ (3<_,_>/ -*-> <_,_>)" [50,0,0,0,0] 50)
-
-  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
-               ("_ |-/ (3<_,_>/ -(_)-> <_,_>)" [50,0,0,0,0,0] 50)
-
-syntax (xsymbols)
-  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-               ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
-  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-               ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
-  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
-               ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
 
-syntax (HTML output)
-  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-               ("_ |- (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
-  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
-               ("_ |-/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
-  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
-               ("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
+inductive_set
+  stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
+  and stepa1' :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+    ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
+  for P :: "instr list"
+where
+  "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : stepa1 P"
+| ASIN[simp]:
+  "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s[x\<mapsto> a s],Suc n\<rangle>"
+| JMPFT[simp,intro]:
+  "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,Suc n\<rangle>"
+| JMPFF[simp,intro]:
+  "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,m\<rangle>"
+| JMPB[simp]:
+  "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,j\<rangle>"
 
-translations
-  "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
-  "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
-  "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^i)"
+abbreviation
+  stepa :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+    ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)  where
+  "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^*)"
 
-inductive "stepa1 P"
-intros
-ASIN[simp]:
-  "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s[x\<mapsto> a s],Suc n\<rangle>"
-JMPFT[simp,intro]:
-  "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,Suc n\<rangle>"
-JMPFF[simp,intro]:
-  "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,m\<rangle>"
-JMPB[simp]:
-  "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,j\<rangle>"
+abbreviation
+  stepan :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
+    ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)  where
+  "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^i)"
 
 subsection "The compiler"