1.1 --- a/src/HOL/IMP/Comp_Rev.thy	Thu Nov 03 15:54:19 2011 +1100
     1.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Thu Nov 03 16:22:29 2011 +1100
     1.3 @@ -18,8 +18,8 @@
     1.4  definition
     1.5    "isuccs i n \<equiv> case i of 
     1.6       JMP j \<Rightarrow> {n + 1 + j}
     1.7 -   | JMPFLESS j \<Rightarrow> {n + 1 + j, n + 1}
     1.8 -   | JMPFGE j \<Rightarrow> {n + 1 + j, n + 1}
     1.9 +   | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1}
    1.10 +   | JMPGE j \<Rightarrow> {n + 1 + j, n + 1}
    1.11     | _ \<Rightarrow> {n +1}"
    1.12  
    1.13  text {* The possible successors pc's of an instruction list *}
    1.14 @@ -88,8 +88,8 @@
    1.15    "succs [LOAD x] n = {n + 1}"
    1.16    "succs [STORE x] n = {n + 1}"
    1.17    "succs [JMP i] n = {n + 1 + i}"
    1.18 -  "succs [JMPFGE i] n = {n + 1 + i, n + 1}"
    1.19 -  "succs [JMPFLESS i] n = {n + 1 + i, n + 1}"
    1.20 +  "succs [JMPGE i] n = {n + 1 + i, n + 1}"
    1.21 +  "succs [JMPLESS i] n = {n + 1 + i, n + 1}"
    1.22    by (auto simp: succs_def isuccs_def)
    1.23  
    1.24  lemma succs_empty [iff]: "succs [] n = {}"
    1.25 @@ -176,8 +176,8 @@
    1.26    "exits [LOAD x] = {1}"
    1.27    "exits [STORE x] = {1}"
    1.28    "i \<noteq> -1 \<Longrightarrow> exits [JMP i] = {1 + i}"
    1.29 -  "i \<noteq> -1 \<Longrightarrow> exits [JMPFGE i] = {1 + i, 1}"
    1.30 -  "i \<noteq> -1 \<Longrightarrow> exits [JMPFLESS i] = {1 + i, 1}"
    1.31 +  "i \<noteq> -1 \<Longrightarrow> exits [JMPGE i] = {1 + i, 1}"
    1.32 +  "i \<noteq> -1 \<Longrightarrow> exits [JMPLESS i] = {1 + i, 1}"
    1.33    by (auto simp: exits_def)
    1.34  
    1.35  lemma acomp_succs [simp]:

     2.1 --- a/src/HOL/IMP/Compiler.thy	Thu Nov 03 15:54:19 2011 +1100
     2.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Nov 03 16:22:29 2011 +1100
     2.3 @@ -37,8 +37,8 @@
     2.4    ADD |
     2.5    STORE string |
     2.6    JMP int |
     2.7 -  JMPFLESS int |
     2.8 -  JMPFGE int
     2.9 +  JMPLESS int |
    2.10 +  JMPGE int
    2.11  
    2.12  type_synonym stack = "val list"
    2.13  type_synonym config = "int\<times>state\<times>stack"
    2.14 @@ -54,8 +54,8 @@
    2.15  "ADD     \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
    2.16  "STORE n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
    2.17  "JMP n   \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
    2.18 -"JMPFLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
    2.19 -"JMPFGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
    2.20 +"JMPLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
    2.21 +"JMPGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
    2.22  
    2.23  code_pred iexec1 .
    2.24  
    2.25 @@ -102,8 +102,8 @@
    2.26    "ADD     \<turnstile>i c \<rightarrow> c'"
    2.27    "STORE n \<turnstile>i c \<rightarrow> c'" 
    2.28    "JMP n   \<turnstile>i c \<rightarrow> c'"
    2.29 -  "JMPFLESS n \<turnstile>i c \<rightarrow> c'"
    2.30 -  "JMPFGE n \<turnstile>i c \<rightarrow> c'"
    2.31 +  "JMPLESS n \<turnstile>i c \<rightarrow> c'"
    2.32 +  "JMPGE n \<turnstile>i c \<rightarrow> c'"
    2.33  
    2.34  text {* Simplification rules for @{const iexec1}. *}
    2.35  lemma iexec1_simps [simp]:
    2.36 @@ -114,10 +114,10 @@
    2.37    "STORE x \<turnstile>i c \<rightarrow> c' = 
    2.38    (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x := hd stk), tl stk))"
    2.39    "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
    2.40 -   "JMPFLESS n \<turnstile>i c \<rightarrow> c' = 
    2.41 +   "JMPLESS n \<turnstile>i c \<rightarrow> c' = 
    2.42    (\<exists>i s stk. c = (i, s, stk) \<and> 
    2.43               c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))"  
    2.44 -  "JMPFGE n \<turnstile>i c \<rightarrow> c' = 
    2.45 +  "JMPGE n \<turnstile>i c \<rightarrow> c' = 
    2.46    (\<exists>i s stk. c = (i, s, stk) \<and> 
    2.47               c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))"
    2.48    by (auto split del: split_if intro!: iexec1.intros)
    2.49 @@ -212,7 +212,7 @@
    2.50        cb1 = bcomp b1 False m
    2.51    in cb1 @ cb2)" |
    2.52  "bcomp (Less a1 a2) c n =
    2.53 - acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
    2.54 + acomp a1 @ acomp a2 @ (if c then [JMPLESS n] else [JMPGE n])"
    2.55  
    2.56  value
    2.57    "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))