equal
deleted
inserted
replaced
44 \begin{isamarkuptext}% |
44 \begin{isamarkuptext}% |
45 The execution of the stack machine is modelled by a function |
45 The execution of the stack machine is modelled by a function |
46 \isa{exec} that takes a list of instructions, a store (modelled as a |
46 \isa{exec} that takes a list of instructions, a store (modelled as a |
47 function from addresses to values, just like the environment for |
47 function from addresses to values, just like the environment for |
48 evaluating expressions), and a stack (modelled as a list) of values, |
48 evaluating expressions), and a stack (modelled as a list) of values, |
49 and returns the stack at the end of the execution---the store remains |
49 and returns the stack at the end of the execution --- the store remains |
50 unchanged:% |
50 unchanged:% |
51 \end{isamarkuptext}% |
51 \end{isamarkuptext}% |
52 \isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v\ list\ {\isasymRightarrow}\ {\isacharprime}v\ list{\isachardoublequote}\isanewline |
52 \isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v\ list\ {\isasymRightarrow}\ {\isacharprime}v\ list{\isachardoublequote}\isanewline |
53 \isacommand{primrec}\isanewline |
53 \isacommand{primrec}\isanewline |
54 {\isachardoublequote}exec\ {\isacharbrackleft}{\isacharbrackright}\ s\ vs\ {\isacharequal}\ vs{\isachardoublequote}\isanewline |
54 {\isachardoublequote}exec\ {\isacharbrackleft}{\isacharbrackright}\ s\ vs\ {\isacharequal}\ vs{\isachardoublequote}\isanewline |
100 automatic case splitting as well, which finishes the proof:% |
100 automatic case splitting as well, which finishes the proof:% |
101 \end{isamarkuptxt}% |
101 \end{isamarkuptxt}% |
102 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
102 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
103 \begin{isamarkuptext}% |
103 \begin{isamarkuptext}% |
104 \noindent |
104 \noindent |
105 Note that because \isaindex{auto} performs simplification, it can |
105 Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can |
106 also be modified in the same way \isa{simp} can. Thus the proof can be |
106 be modified in the same way \isa{simp} can. Thus the proof can be |
107 rewritten as% |
107 rewritten as% |
108 \end{isamarkuptext}% |
108 \end{isamarkuptext}% |
109 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
109 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
110 \begin{isamarkuptext}% |
110 \begin{isamarkuptext}% |
111 \noindent |
111 \noindent |
112 Although this is more compact, it is less clear for the reader of the proof. |
112 Although this is more compact, it is less clear for the reader of the proof. |
113 |
113 |
114 We could now go back and prove \isa{exec (comp e) s [] = [value e s]} |
114 We could now go back and prove \isa{exec (comp e) s [] = [value e s]} |