diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/IMP/Machines.thy	Wed Jul 11 11:14:51 2007 +0200
@@ -36,43 +36,28 @@
 
 subsection "M0 with PC"
 
-consts  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
-syntax
-  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
-               ("(_/ |- (1<_,/_>)/ -1-> (1<_,/_>))" [50,0,0,0,0] 50)
-  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
-               ("(_/ |- (1<_,/_>)/ -*-> (1<_,/_>))" [50,0,0,0,0] 50)
-  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
-               ("(_/ |- (1<_,/_>)/ -_-> (1<_,/_>))" [50,0,0,0,0] 50)
-
-syntax (xsymbols)
-  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
-               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
-  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
-               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
-  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
-               ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+inductive_set
+  exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
+  and exec01' :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
+    ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+  for P :: "instr list"
+where
+  "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)"
+| SET: "\<lbrakk> n<size P; P!n = SET x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s[x\<mapsto> a s]\<rangle>"
+| JMPFT: "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s\<rangle>"
+| JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk>
+        \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>"
+| JMPB:  "\<lbrakk> n<size P; P!n = JMPB i; i \<le> n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>j,s\<rangle>"
 
-syntax (HTML output)
-  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
-               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
-  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
-               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
-  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
-               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+abbreviation
+  exec0s :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
+    ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)  where
+  "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^*"
 
-translations
-  "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
-  "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
-  "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^n"
-
-inductive "exec01 P"
-intros
-SET: "\<lbrakk> n<size P; P!n = SET x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s[x\<mapsto> a s]\<rangle>"
-JMPFT: "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s\<rangle>"
-JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk>
-        \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>"
-JMPB:  "\<lbrakk> n<size P; P!n = JMPB i; i \<le> n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>j,s\<rangle>"
+abbreviation
+  exec0n :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
+    ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)  where
+  "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^n"
 
 subsection "M0 with lists"
 
@@ -82,40 +67,31 @@
 
 types config = "instrs \<times> instrs \<times> state"
 
-consts  stepa1 :: "(config \<times> config)set"
 
-syntax
-  "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
-               ("((1<_,/_,/_>)/ -1-> (1<_,/_,/_>))" 50)
-  "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
-               ("((1<_,/_,/_>)/ -*-> (1<_,/_,/_>))" 50)
-  "_stepan" :: "[state,instrs,instrs, nat, instrs,instrs,state] \<Rightarrow> bool"
-               ("((1<_,/_,/_>)/ -_-> (1<_,/_,/_>))" 50)
-
-syntax (xsymbols)
-  "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
-               ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
-  "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
-               ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
-  "_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
-               ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
-
-translations
-  "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : stepa1"
-  "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^*)"
-  "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^i)"
-
-
-inductive "stepa1"
-intros
-  "\<langle>SET x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,SET x a#q,s[x\<mapsto> a s]\<rangle>"
-  "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>"
-  "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk>
+inductive_set
+  stepa1 :: "(config \<times> config)set"
+  and stepa1' :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
+    ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
+where
+  "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : stepa1"
+| "\<langle>SET x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,SET x a#q,s[x\<mapsto> a s]\<rangle>"
+| "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>"
+| "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk>
    \<Longrightarrow> \<langle>JMPF b i # p, q, s\<rangle> -1\<rightarrow> \<langle>drop i p, rev(take i p) @ JMPF b i # q, s\<rangle>"
-  "i \<le> size q
+| "i \<le> size q
    \<Longrightarrow> \<langle>JMPB i # p, q, s\<rangle> -1\<rightarrow> \<langle>rev(take i q) @ JMPB i # p, drop i q, s\<rangle>"
 
-inductive_cases execE: "((i#is,p,s),next) : stepa1"
+abbreviation
+  stepa :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
+    ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)  where
+  "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^*)"
+
+abbreviation
+  stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
+    ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where
+  "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^i)"
+
+inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1"
 
 lemma exec_simp[simp]:
  "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of