1.1 --- a/src/HOL/IMP/Compiler.thy	Thu Jul 28 16:32:49 2011 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Jul 28 16:56:14 2011 +0200
     1.3 @@ -40,10 +40,6 @@
     1.4    JMPFLESS int |
     1.5    JMPFGE int
     1.6  
     1.7 -(* reads slightly nicer *)
     1.8 -abbreviation
     1.9 -  "JMPB i == JMP (-i)"
    1.10 -
    1.11  type_synonym stack = "val list"
    1.12  type_synonym config = "int\<times>state\<times>stack"
    1.13  
    1.14 @@ -51,7 +47,7 @@
    1.15  abbreviation "tl2 xs == tl(tl xs)"
    1.16  
    1.17  inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
    1.18 -    ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [50,0,0] 50)
    1.19 +    ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [59,0,59] 60)
    1.20  where
    1.21  "LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
    1.22  "LOAD x  \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
    1.23 @@ -66,16 +62,17 @@
    1.24  declare iexec1.intros
    1.25  
    1.26  definition
    1.27 -  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) 
    1.28 +  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
    1.29  where
    1.30    "P \<turnstile> c \<rightarrow> c' = 
    1.31 -   (\<exists>i s stk. c = (i,s,stk) \<and> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c' \<and> 0 \<le> i \<and> i < isize P)"
    1.32 +  (\<exists>i s stk. c = (i,s,stk) \<and> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c' \<and> 0 \<le> i \<and> i < isize P)"
    1.33  
    1.34  declare exec1_def [simp] 
    1.35  
    1.36  lemma exec1I [intro, code_pred_intro]:
    1.37 -  "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
    1.38 -  by simp
    1.39 +  assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P" 
    1.40 +  shows "P \<turnstile> (i,s,stk) \<rightarrow> c'"
    1.41 +  using assms by simp
    1.42  
    1.43  inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
    1.44  where
    1.45 @@ -245,7 +242,8 @@
    1.46     in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" |
    1.47  "ccomp (WHILE b DO c) =
    1.48   (let cc = ccomp c; cb = bcomp b False (isize cc + 1)
    1.49 -  in cb @ cc @ [JMPB (isize cb + isize cc + 1)])"
    1.50 +  in cb @ cc @ [JMP (-(isize cb + isize cc + 1))])"
    1.51 +
    1.52  
    1.53  value "ccomp
    1.54   (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)