--- 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"