src/HOL/IMP/Comp_Rev.thy

 
 text {* The possible successor pc's of an instruction at position @{term n} *}
 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 *}
 definition
   "succs P n = {s. \<exists>i. 0 \<le> i \<and> i < isize P \<and> s \<in> isuccs (P!!i) (n+i)}" 

   "succs [ADD] n = {n + 1}"
   "succs [LOADI v] n = {n + 1}"
   "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 = {}"
   by (simp add: succs_def)
 

   "exits [ADD] = {1}"
   "exits [LOADI v] = {1}"
   "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]:
   "succs (acomp a) n = {n + 1 .. n + isize (acomp a)}"
   by (induct a arbitrary: n) auto