1.1 --- a/src/HOL/IMP/Compiler.thy	Wed Sep 25 10:53:09 2013 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Wed Sep 25 11:56:33 2013 +0200
     1.3 @@ -21,16 +21,16 @@
     1.4    where @{term i} is an @{typ int}.
     1.5  *}
     1.6  fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
     1.7 -"(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
     1.8 +"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"
     1.9  
    1.10  text {*
    1.11    The only additional lemma we need about this function 
    1.12    is indexing over append:
    1.13  *}
    1.14  lemma inth_append [simp]:
    1.15 -  "0 \<le> n \<Longrightarrow>
    1.16 -  (xs @ ys) !! n = (if n < size xs then xs !! n else ys !! (n - size xs))"
    1.17 -by (induction xs arbitrary: n) (auto simp: algebra_simps)
    1.18 +  "0 \<le> i \<Longrightarrow>
    1.19 +  (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
    1.20 +by (induction xs arbitrary: i) (auto simp: algebra_simps)
    1.21  
    1.22  subsection "Instructions and Stack Machine"
    1.23