src/HOL/IMP/ASM.thy
changeset 45257 12063e071d92
parent 45222 6eab55bab82f
child 45266 13b5fb92b9f5
equal deleted inserted replaced
45256:62b025f434e9 45257:12063e071d92
     2 
     2 
     3 theory ASM imports AExp begin
     3 theory ASM imports AExp begin
     4 
     4 
     5 subsection "Arithmetic Stack Machine"
     5 subsection "Arithmetic Stack Machine"
     6 
     6 
     7 datatype ainstr = LOADI val | LOAD vname | ADD
     7 text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMinstrdef}{% *}
       
     8 datatype instr = LOADI val | LOAD vname | ADD
       
     9 text_raw{*}\end{isaverbatimwrite}*}
     8 
    10 
       
    11 text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMstackdef}{% *}
     9 type_synonym stack = "val list"
    12 type_synonym stack = "val list"
       
    13 text_raw{*}\end{isaverbatimwrite}*}
    10 
    14 
    11 abbreviation "hd2 xs == hd(tl xs)"
    15 abbreviation "hd2 xs == hd(tl xs)"
    12 abbreviation "tl2 xs == tl(tl xs)"
    16 abbreviation "tl2 xs == tl(tl xs)"
    13 
    17 
    14 text{* \noindent Abbreviations are transparent: they are unfolded after
    18 text{* \noindent Abbreviations are transparent: they are unfolded after
    15 parsing and folded back again before printing. Internally, they do not
    19 parsing and folded back again before printing. Internally, they do not
    16 exist. *}
    20 exist. *}
    17 
    21 
    18 fun aexec1 :: "ainstr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
    22 text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMexeconedef}{% *}
    19 "aexec1 (LOADI n) _ stk  =  n # stk" |
    23 fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
    20 "aexec1 (LOAD n) s stk  =  s(n) # stk" |
    24 "exec1 (LOADI n) _ stk  =  n # stk" |
    21 "aexec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
    25 "exec1 (LOAD x) s stk  =  s(x) # stk" |
       
    26 "exec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
       
    27 text_raw{*}\end{isaverbatimwrite}*}
    22 
    28 
    23 fun aexec :: "ainstr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
    29 text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMexecdef}{% *}
    24 "aexec [] _ stk = stk" |
    30 fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
    25 "aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
    31 "exec [] _ stk = stk" |
       
    32 "exec (i#is) s stk = exec is s (exec1 i s stk)"
       
    33 text_raw{*}\end{isaverbatimwrite}*}
    26 
    34 
    27 value "aexec [LOADI 5, LOAD ''y'', ADD]
    35 value "exec [LOADI 5, LOAD ''y'', ADD]
    28  <''x'' := 42, ''y'' := 43> [50]"
    36  <''x'' := 42, ''y'' := 43> [50]"
    29 
    37 
    30 lemma aexec_append[simp]:
    38 lemma exec_append[simp]:
    31   "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
    39   "exec (is1@is2) s stk = exec is2 s (exec is1 s stk)"
    32 apply(induction is1 arbitrary: stk)
    40 apply(induction is1 arbitrary: stk)
    33 apply (auto)
    41 apply (auto)
    34 done
    42 done
    35 
    43 
    36 
    44 
    37 subsection "Compilation"
    45 subsection "Compilation"
    38 
    46 
    39 fun acomp :: "aexp \<Rightarrow> ainstr list" where
    47 text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMcompdef}{% *}
    40 "acomp (N n) = [LOADI n]" |
    48 fun comp :: "aexp \<Rightarrow> instr list" where
    41 "acomp (V x) = [LOAD x]" |
    49 "comp (N n) = [LOADI n]" |
    42 "acomp (Plus e1 e2) = acomp e1 @ acomp e2 @ [ADD]"
    50 "comp (V x) = [LOAD x]" |
       
    51 "comp (Plus e1 e2) = comp e1 @ comp e2 @ [ADD]"
       
    52 text_raw{*}\end{isaverbatimwrite}*}
    43 
    53 
    44 value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
    54 value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
    45 
    55 
    46 theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
    56 theorem exec_comp: "exec (comp a) s stk = aval a s # stk"
    47 apply(induction a arbitrary: stk)
    57 apply(induction a arbitrary: stk)
    48 apply (auto)
    58 apply (auto)
    49 done
    59 done
    50 
    60 
    51 end
    61 end