# HG changeset patch
# User kleing
# Date 1320297749 -39600
# Node ID 654cc47f6115032028ac415049809dbab1bb99c1
# Parent  b227989b6ee6a2778bd3fe7cbd821f1ad378c1d9
JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.

diff -r b227989b6ee6 -r 654cc47f6115 src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Thu Nov 03 15:54:19 2011 +1100
+++ b/src/HOL/IMP/Comp_Rev.thy	Thu Nov 03 16:22:29 2011 +1100
@@ -18,8 +18,8 @@
 definition
   "isuccs i n \<equiv> case i of 
      JMP j \<Rightarrow> {n + 1 + j}
-   | JMPFLESS j \<Rightarrow> {n + 1 + j, n + 1}
-   | JMPFGE j \<Rightarrow> {n + 1 + j, n + 1}
+   | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1}
+   | JMPGE j \<Rightarrow> {n + 1 + j, n + 1}
    | _ \<Rightarrow> {n +1}"
 
 text {* The possible successors pc's of an instruction list *}
@@ -88,8 +88,8 @@
   "succs [LOAD x] n = {n + 1}"
   "succs [STORE x] n = {n + 1}"
   "succs [JMP i] n = {n + 1 + i}"
-  "succs [JMPFGE i] n = {n + 1 + i, n + 1}"
-  "succs [JMPFLESS i] n = {n + 1 + i, n + 1}"
+  "succs [JMPGE i] n = {n + 1 + i, n + 1}"
+  "succs [JMPLESS i] n = {n + 1 + i, n + 1}"
   by (auto simp: succs_def isuccs_def)
 
 lemma succs_empty [iff]: "succs [] n = {}"
@@ -176,8 +176,8 @@
   "exits [LOAD x] = {1}"
   "exits [STORE x] = {1}"
   "i \<noteq> -1 \<Longrightarrow> exits [JMP i] = {1 + i}"
-  "i \<noteq> -1 \<Longrightarrow> exits [JMPFGE i] = {1 + i, 1}"
-  "i \<noteq> -1 \<Longrightarrow> exits [JMPFLESS i] = {1 + i, 1}"
+  "i \<noteq> -1 \<Longrightarrow> exits [JMPGE i] = {1 + i, 1}"
+  "i \<noteq> -1 \<Longrightarrow> exits [JMPLESS i] = {1 + i, 1}"
   by (auto simp: exits_def)
 
 lemma acomp_succs [simp]:
diff -r b227989b6ee6 -r 654cc47f6115 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Nov 03 15:54:19 2011 +1100
+++ b/src/HOL/IMP/Compiler.thy	Thu Nov 03 16:22:29 2011 +1100
@@ -37,8 +37,8 @@
   ADD |
   STORE string |
   JMP int |
-  JMPFLESS int |
-  JMPFGE int
+  JMPLESS int |
+  JMPGE int
 
 type_synonym stack = "val list"
 type_synonym config = "int\<times>state\<times>stack"
@@ -54,8 +54,8 @@
 "ADD     \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
 "STORE n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(n := hd stk),tl stk)" |
 "JMP n   \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
-"JMPFLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
-"JMPFGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
+"JMPLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
+"JMPGE n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)"
 
 code_pred iexec1 .
 
@@ -102,8 +102,8 @@
   "ADD     \<turnstile>i c \<rightarrow> c'"
   "STORE n \<turnstile>i c \<rightarrow> c'" 
   "JMP n   \<turnstile>i c \<rightarrow> c'"
-  "JMPFLESS n \<turnstile>i c \<rightarrow> c'"
-  "JMPFGE n \<turnstile>i c \<rightarrow> c'"
+  "JMPLESS n \<turnstile>i c \<rightarrow> c'"
+  "JMPGE n \<turnstile>i c \<rightarrow> c'"
 
 text {* Simplification rules for @{const iexec1}. *}
 lemma iexec1_simps [simp]:
@@ -114,10 +114,10 @@
   "STORE x \<turnstile>i c \<rightarrow> c' = 
   (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x := hd stk), tl stk))"
   "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
-   "JMPFLESS n \<turnstile>i c \<rightarrow> c' = 
+   "JMPLESS n \<turnstile>i c \<rightarrow> c' = 
   (\<exists>i s stk. c = (i, s, stk) \<and> 
              c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))"  
-  "JMPFGE n \<turnstile>i c \<rightarrow> c' = 
+  "JMPGE n \<turnstile>i c \<rightarrow> c' = 
   (\<exists>i s stk. c = (i, s, stk) \<and> 
              c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))"
   by (auto split del: split_if intro!: iexec1.intros)
@@ -212,7 +212,7 @@
       cb1 = bcomp b1 False m
   in cb1 @ cb2)" |
 "bcomp (Less a1 a2) c n =
- acomp a1 @ acomp a2 @ (if c then [JMPFLESS n] else [JMPFGE n])"
+ acomp a1 @ acomp a2 @ (if c then [JMPLESS n] else [JMPGE n])"
 
 value
   "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))