# HG changeset patch
# User kleing
# Date 1311864974 -7200
# Node ID a9fcbafdf208f3f6b32a9823abb20d12c8f11b27
# Parent  0a0ee31ec20ae4dbcc9fe3497447b92b6daaf589
compiler proof cleanup

diff -r 0a0ee31ec20a -r a9fcbafdf208 src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Thu Jul 28 16:32:49 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy	Thu Jul 28 16:56:14 2011 +0200
@@ -22,7 +22,6 @@
    | JMPFGE j \<Rightarrow> {n + 1 + j, n + 1}
    | _ \<Rightarrow> {n +1}"
 
-(* FIXME: _Collect? *)
 text {* The possible successors pc's of an instruction list *}
 definition
   "succs P n = {s. \<exists>i. 0 \<le> i \<and> i < isize P \<and> s \<in> isuccs (P!!i) (n+i)}" 
@@ -36,7 +35,7 @@
 
 lemma exec_n_exec:
   "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'"
-  by (induct n arbitrary: c)  (auto intro: exec.step)
+  by (induct n arbitrary: c) auto
 
 lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
 
@@ -56,7 +55,7 @@
   "[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)"
   by (induct k) auto
 
-lemma exec1_exec_n [elim,intro!]:
+lemma exec1_exec_n [intro!]:
   "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'"
   by (cases c') simp
 
@@ -133,8 +132,9 @@
 qed
 
 lemma succs_iexec1:
-  "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> fst c' \<in> succs P 0"
-  by (auto elim!: iexec1.cases simp: succs_def isuccs_def)
+  assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P"
+  shows "fst c' \<in> succs P 0"
+  using assms by (auto elim!: iexec1.cases simp: succs_def isuccs_def)
 
 lemma succs_shift:
   "(p - n \<in> succs P 0) = (p \<in> succs P n)" 
@@ -256,14 +256,15 @@
   by (auto elim!: iexec1.cases)
 
 lemma exec_n_split:
-  shows "\<lbrakk> P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow>^n (j, s');
-           0 \<le> i; i < isize c; j \<notin> {isize P ..< isize P + isize c} \<rbrakk> \<Longrightarrow>
-         \<exists>s'' i' k m. 
+  assumes "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow>^n (j, s')"
+          "0 \<le> i" "i < isize c" 
+          "j \<notin> {isize P ..< isize P + isize c}"
+  shows "\<exists>s'' i' k m. 
                    c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and>
                    i' \<in> exits c \<and> 
                    P @ c @ P' \<turnstile> (isize P + i', s'') \<rightarrow>^m (j, s') \<and>
                    n = k + m" 
-proof (induct n arbitrary: i j s)
+using assms proof (induct n arbitrary: i j s)
   case 0
   thus ?case by simp
 next
@@ -304,14 +305,14 @@
 qed
 
 lemma exec_n_drop_right:
-  shows "\<lbrakk> c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s'); j \<notin> {0..<isize c} \<rbrakk> \<Longrightarrow>
-         \<exists>s'' i' k m. 
-                   (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
-                   else
-                   c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
-                   i' \<in> exits c) \<and> 
-                   c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and>
-                   n = k + m"
+  assumes "c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s')" "j \<notin> {0..<isize c}"
+  shows "\<exists>s'' i' k m. 
+          (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
+           else c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
+           i' \<in> exits c) \<and> 
+           c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and>
+           n = k + m"
+  using assms
   by (cases "c = []")
      (auto dest: exec_n_split [where P="[]", simplified])
   
@@ -334,10 +335,10 @@
 qed
 
 lemma exec_n_drop_left:
-  "\<lbrakk> P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk'); 
-     isize P \<le> i; exits P' \<subseteq> {0..} \<rbrakk> \<Longrightarrow>
-     P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')"
-proof (induct k arbitrary: i s stk)
+  assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
+          "isize P \<le> i" "exits P' \<subseteq> {0..}"
+  shows "P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')"
+using assms proof (induct k arbitrary: i s stk)
   case 0 thus ?case by simp
 next
   case (Suc k)
@@ -427,22 +428,21 @@
 qed (auto simp: exec_n_simps)
 
 lemma bcomp_split:
-  shows "\<lbrakk> bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk'); 
-           j \<notin> {0..<isize (bcomp b c i)}; 0 \<le> i \<rbrakk> \<Longrightarrow>
-         \<exists>s'' stk'' i' k m. 
+  assumes "bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')" 
+          "j \<notin> {0..<isize (bcomp b c i)}" "0 \<le> i"
+  shows "\<exists>s'' stk'' i' k m. 
            bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and>
            (i' = isize (bcomp b c i) \<or> i' = i + isize (bcomp b c i)) \<and>
            bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and>
            n = k + m"
-  by (cases "bcomp b c i = []")
-     (fastsimp dest!: exec_n_drop_right)+
+  using assms by (cases "bcomp b c i = []") (fastsimp dest!: exec_n_drop_right)+
 
 lemma bcomp_exec_n [dest]:
-  "\<lbrakk> bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk');
-     isize (bcomp b c j) \<le> i; 0 \<le> j \<rbrakk> \<Longrightarrow>
-  i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
-  s' = s \<and> stk' = stk"
-proof (induct b arbitrary: c j i n s' stk')
+  assumes "bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')"
+          "isize (bcomp b c j) \<le> i" "0 \<le> j"
+  shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
+         s' = s \<and> stk' = stk"
+using assms proof (induct b arbitrary: c j i n s' stk')
   case B thus ?case 
     by (simp split: split_if_asm add: exec_n_simps)
 next
@@ -554,7 +554,7 @@
       let ?c0 = "WHILE b DO c"
       let ?cs = "ccomp ?c0"
       let ?bs = "bcomp b False (isize (ccomp c) + 1)"
-      let ?jmp = "[JMPB (isize ?bs + isize (ccomp c) + 1)]"
+      let ?jmp = "[JMP (-((isize ?bs + isize (ccomp c) + 1)))]"
       
       from "1.prems" b
       obtain k where
diff -r 0a0ee31ec20a -r a9fcbafdf208 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Jul 28 16:32:49 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy	Thu Jul 28 16:56:14 2011 +0200
@@ -40,10 +40,6 @@
   JMPFLESS int |
   JMPFGE int
 
-(* reads slightly nicer *)
-abbreviation
-  "JMPB i == JMP (-i)"
-
 type_synonym stack = "val list"
 type_synonym config = "int\<times>state\<times>stack"
 
@@ -51,7 +47,7 @@
 abbreviation "tl2 xs == tl(tl xs)"
 
 inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
-    ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [50,0,0] 50)
+    ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [59,0,59] 60)
 where
 "LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
 "LOAD x  \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
@@ -66,16 +62,17 @@
 declare iexec1.intros
 
 definition
-  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) 
+  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
 where
   "P \<turnstile> c \<rightarrow> c' = 
-   (\<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)"
+  (\<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)"
 
 declare exec1_def [simp] 
 
 lemma exec1I [intro, code_pred_intro]:
-  "\<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'"
-  by simp
+  assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P" 
+  shows "P \<turnstile> (i,s,stk) \<rightarrow> c'"
+  using assms by simp
 
 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
 where
@@ -245,7 +242,8 @@
    in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" |
 "ccomp (WHILE b DO c) =
  (let cc = ccomp c; cb = bcomp b False (isize cc + 1)
-  in cb @ cc @ [JMPB (isize cb + isize cc + 1)])"
+  in cb @ cc @ [JMP (-(isize cb + isize cc + 1))])"
+
 
 value "ccomp
  (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)