# Theory Compiler

section "Compiler for IMP"
theory Compiler imports Big_Step Star
begin
subsection "List setup"
text ‹
In the following, we use the length of lists as integers
instead of natural numbers. Instead of converting \<^typ>‹nat›
to \<^typ>‹int› explicitly, we tell Isabelle to coerce \<^typ>‹nat›
automatically when necessary.
›
declare [[coercion_enabled]]
declare [[coercion "int :: nat ⇒ int"]]
text ‹
Similarly, we will want to access the ith element of a list,
where \<^term>‹i› is an \<^typ>‹int›.
›
fun inth :: "'a list ⇒ int ⇒ 'a" (infixl "!!" 100) where
"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"
text ‹
The only additional lemma we need about this function
is indexing over append:
›
lemma inth_append [simp]:
"0 ≤ i ⟹
(xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
by (induction xs arbitrary: i) (auto simp: algebra_simps)
text‹We hide coercion \<^const>‹int› applied to \<^const>‹length›:›
abbreviation (output)
"isize xs == int (length xs)"
notation isize ("size")
subsection "Instructions and Stack Machine"
text_raw‹\snip{instrdef}{0}{1}{%›