src/HOL/IMP/ASM.thy
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 44036 d03f9f28d01d
child 45015 fdac1e9880eb
permissions -rw-r--r--
remove lemma stupid_ext
     1 header "Arithmetic Stack Machine and Compilation"
     2 
     3 theory ASM imports AExp begin
     4 
     5 subsection "Arithmetic Stack Machine"
     6 
     7 datatype ainstr = LOADI val | LOAD string | ADD
     8 
     9 type_synonym stack = "val list"
    10 
    11 abbreviation "hd2 xs == hd(tl xs)"
    12 abbreviation "tl2 xs == tl(tl xs)"
    13 
    14 text{* \noindent Abbreviations are transparent: they are unfolded after
    15 parsing and folded back again before printing. Internally, they do not
    16 exist. *}
    17 
    18 fun aexec1 :: "ainstr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
    19 "aexec1 (LOADI n) _ stk  =  n # stk" |
    20 "aexec1 (LOAD n) s stk  =  s(n) # stk" |
    21 "aexec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
    22 
    23 fun aexec :: "ainstr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
    24 "aexec [] _ stk = stk" |
    25 "aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
    26 
    27 value "aexec [LOADI 5, LOAD ''y'', ADD]
    28  <''x'' := 42, ''y'' := 43> [50]"
    29 
    30 lemma aexec_append[simp]:
    31   "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
    32 apply(induct is1 arbitrary: stk)
    33 apply (auto)
    34 done
    35 
    36 
    37 subsection "Compilation"
    38 
    39 fun acomp :: "aexp \<Rightarrow> ainstr list" where
    40 "acomp (N n) = [LOADI n]" |
    41 "acomp (V x) = [LOAD x]" |
    42 "acomp (Plus e1 e2) = acomp e1 @ acomp e2 @ [ADD]"
    43 
    44 value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
    45 
    46 theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
    47 apply(induct a arbitrary: stk)
    48 apply (auto)
    49 done
    50 
    51 end