1.1 --- a/src/HOL/IMP/Comp_Rev.thy	Thu Jul 28 16:32:49 2011 +0200
     1.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Thu Jul 28 16:56:14 2011 +0200
     1.3 @@ -22,7 +22,6 @@
     1.4     | JMPFGE j \<Rightarrow> {n + 1 + j, n + 1}
     1.5     | _ \<Rightarrow> {n +1}"
     1.6  
     1.7 -(* FIXME: _Collect? *)
     1.8  text {* The possible successors pc's of an instruction list *}
     1.9  definition
    1.10    "succs P n = {s. \<exists>i. 0 \<le> i \<and> i < isize P \<and> s \<in> isuccs (P!!i) (n+i)}" 
    1.11 @@ -36,7 +35,7 @@
    1.12  
    1.13  lemma exec_n_exec:
    1.14    "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'"
    1.15 -  by (induct n arbitrary: c)  (auto intro: exec.step)
    1.16 +  by (induct n arbitrary: c) auto
    1.17  
    1.18  lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
    1.19  
    1.20 @@ -56,7 +55,7 @@
    1.21    "[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)"
    1.22    by (induct k) auto
    1.23  
    1.24 -lemma exec1_exec_n [elim,intro!]:
    1.25 +lemma exec1_exec_n [intro!]:
    1.26    "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'"
    1.27    by (cases c') simp
    1.28  
    1.29 @@ -133,8 +132,9 @@
    1.30  qed
    1.31  
    1.32  lemma succs_iexec1:
    1.33 -  "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> fst c' \<in> succs P 0"
    1.34 -  by (auto elim!: iexec1.cases simp: succs_def isuccs_def)
    1.35 +  assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P"
    1.36 +  shows "fst c' \<in> succs P 0"
    1.37 +  using assms by (auto elim!: iexec1.cases simp: succs_def isuccs_def)
    1.38  
    1.39  lemma succs_shift:
    1.40    "(p - n \<in> succs P 0) = (p \<in> succs P n)" 
    1.41 @@ -256,14 +256,15 @@
    1.42    by (auto elim!: iexec1.cases)
    1.43  
    1.44  lemma exec_n_split:
    1.45 -  shows "\<lbrakk> P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow>^n (j, s');
    1.46 -           0 \<le> i; i < isize c; j \<notin> {isize P ..< isize P + isize c} \<rbrakk> \<Longrightarrow>
    1.47 -         \<exists>s'' i' k m. 
    1.48 +  assumes "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow>^n (j, s')"
    1.49 +          "0 \<le> i" "i < isize c" 
    1.50 +          "j \<notin> {isize P ..< isize P + isize c}"
    1.51 +  shows "\<exists>s'' i' k m. 
    1.52                     c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and>
    1.53                     i' \<in> exits c \<and> 
    1.54                     P @ c @ P' \<turnstile> (isize P + i', s'') \<rightarrow>^m (j, s') \<and>
    1.55                     n = k + m" 
    1.56 -proof (induct n arbitrary: i j s)
    1.57 +using assms proof (induct n arbitrary: i j s)
    1.58    case 0
    1.59    thus ?case by simp
    1.60  next
    1.61 @@ -304,14 +305,14 @@
    1.62  qed
    1.63  
    1.64  lemma exec_n_drop_right:
    1.65 -  shows "\<lbrakk> c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s'); j \<notin> {0..<isize c} \<rbrakk> \<Longrightarrow>
    1.66 -         \<exists>s'' i' k m. 
    1.67 -                   (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
    1.68 -                   else
    1.69 -                   c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
    1.70 -                   i' \<in> exits c) \<and> 
    1.71 -                   c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and>
    1.72 -                   n = k + m"
    1.73 +  assumes "c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s')" "j \<notin> {0..<isize c}"
    1.74 +  shows "\<exists>s'' i' k m. 
    1.75 +          (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
    1.76 +           else c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
    1.77 +           i' \<in> exits c) \<and> 
    1.78 +           c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and>
    1.79 +           n = k + m"
    1.80 +  using assms
    1.81    by (cases "c = []")
    1.82       (auto dest: exec_n_split [where P="[]", simplified])
    1.83    
    1.84 @@ -334,10 +335,10 @@
    1.85  qed
    1.86  
    1.87  lemma exec_n_drop_left:
    1.88 -  "\<lbrakk> P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk'); 
    1.89 -     isize P \<le> i; exits P' \<subseteq> {0..} \<rbrakk> \<Longrightarrow>
    1.90 -     P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')"
    1.91 -proof (induct k arbitrary: i s stk)
    1.92 +  assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
    1.93 +          "isize P \<le> i" "exits P' \<subseteq> {0..}"
    1.94 +  shows "P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')"
    1.95 +using assms proof (induct k arbitrary: i s stk)
    1.96    case 0 thus ?case by simp
    1.97  next
    1.98    case (Suc k)
    1.99 @@ -427,22 +428,21 @@
   1.100  qed (auto simp: exec_n_simps)
   1.101  
   1.102  lemma bcomp_split:
   1.103 -  shows "\<lbrakk> bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk'); 
   1.104 -           j \<notin> {0..<isize (bcomp b c i)}; 0 \<le> i \<rbrakk> \<Longrightarrow>
   1.105 -         \<exists>s'' stk'' i' k m. 
   1.106 +  assumes "bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')" 
   1.107 +          "j \<notin> {0..<isize (bcomp b c i)}" "0 \<le> i"
   1.108 +  shows "\<exists>s'' stk'' i' k m. 
   1.109             bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and>
   1.110             (i' = isize (bcomp b c i) \<or> i' = i + isize (bcomp b c i)) \<and>
   1.111             bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and>
   1.112             n = k + m"
   1.113 -  by (cases "bcomp b c i = []")
   1.114 -     (fastsimp dest!: exec_n_drop_right)+
   1.115 +  using assms by (cases "bcomp b c i = []") (fastsimp dest!: exec_n_drop_right)+
   1.116  
   1.117  lemma bcomp_exec_n [dest]:
   1.118 -  "\<lbrakk> bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk');
   1.119 -     isize (bcomp b c j) \<le> i; 0 \<le> j \<rbrakk> \<Longrightarrow>
   1.120 -  i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
   1.121 -  s' = s \<and> stk' = stk"
   1.122 -proof (induct b arbitrary: c j i n s' stk')
   1.123 +  assumes "bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')"
   1.124 +          "isize (bcomp b c j) \<le> i" "0 \<le> j"
   1.125 +  shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
   1.126 +         s' = s \<and> stk' = stk"
   1.127 +using assms proof (induct b arbitrary: c j i n s' stk')
   1.128    case B thus ?case 
   1.129      by (simp split: split_if_asm add: exec_n_simps)
   1.130  next
   1.131 @@ -554,7 +554,7 @@
   1.132        let ?c0 = "WHILE b DO c"
   1.133        let ?cs = "ccomp ?c0"
   1.134        let ?bs = "bcomp b False (isize (ccomp c) + 1)"
   1.135 -      let ?jmp = "[JMPB (isize ?bs + isize (ccomp c) + 1)]"
   1.136 +      let ?jmp = "[JMP (-((isize ?bs + isize (ccomp c) + 1)))]"
   1.137        
   1.138        from "1.prems" b
   1.139        obtain k where

     2.1 --- a/src/HOL/IMP/Compiler.thy	Thu Jul 28 16:32:49 2011 +0200
     2.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Jul 28 16:56:14 2011 +0200
     2.3 @@ -40,10 +40,6 @@
     2.4    JMPFLESS int |
     2.5    JMPFGE int
     2.6  
     2.7 -(* reads slightly nicer *)
     2.8 -abbreviation
     2.9 -  "JMPB i == JMP (-i)"
    2.10 -
    2.11  type_synonym stack = "val list"
    2.12  type_synonym config = "int\<times>state\<times>stack"
    2.13  
    2.14 @@ -51,7 +47,7 @@
    2.15  abbreviation "tl2 xs == tl(tl xs)"
    2.16  
    2.17  inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
    2.18 -    ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [50,0,0] 50)
    2.19 +    ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [59,0,59] 60)
    2.20  where
    2.21  "LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
    2.22  "LOAD x  \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
    2.23 @@ -66,16 +62,17 @@
    2.24  declare iexec1.intros
    2.25  
    2.26  definition
    2.27 -  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) 
    2.28 +  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
    2.29  where
    2.30    "P \<turnstile> c \<rightarrow> c' = 
    2.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)"
    2.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)"
    2.33  
    2.34  declare exec1_def [simp] 
    2.35  
    2.36  lemma exec1I [intro, code_pred_intro]:
    2.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'"
    2.38 -  by simp
    2.39 +  assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P" 
    2.40 +  shows "P \<turnstile> (i,s,stk) \<rightarrow> c'"
    2.41 +  using assms by simp
    2.42  
    2.43  inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
    2.44  where
    2.45 @@ -245,7 +242,8 @@
    2.46     in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" |
    2.47  "ccomp (WHILE b DO c) =
    2.48   (let cc = ccomp c; cb = bcomp b False (isize cc + 1)
    2.49 -  in cb @ cc @ [JMPB (isize cb + isize cc + 1)])"
    2.50 +  in cb @ cc @ [JMP (-(isize cb + isize cc + 1))])"
    2.51 +
    2.52  
    2.53  value "ccomp
    2.54   (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)