96 This requires induction on \isa{xs} and ordinary simplification for the |
96 This requires induction on \isa{xs} and ordinary simplification for the |
97 base cases. In the induction step, simplification leaves us with a formula |
97 base cases. In the induction step, simplification leaves us with a formula |
98 that contains two \isa{case}-expressions over instructions. Thus we add |
98 that contains two \isa{case}-expressions over instructions. Thus we add |
99 automatic case splitting as well, which finishes the proof:% |
99 automatic case splitting as well, which finishes the proof:% |
100 \end{isamarkuptxt}% |
100 \end{isamarkuptxt}% |
101 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
101 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
102 \begin{isamarkuptext}% |
102 \begin{isamarkuptext}% |
103 \noindent |
103 \noindent |
104 Note that because \isaindex{auto} performs simplification, it can |
104 Note that because \isaindex{auto} performs simplification, it can |
105 also be modified in the same way \isa{simp} can. Thus the proof can be |
105 also be modified in the same way \isa{simp} can. Thus the proof can be |
106 rewritten as% |
106 rewritten as% |
107 \end{isamarkuptext}% |
107 \end{isamarkuptext}% |
108 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
108 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
109 \begin{isamarkuptext}% |
109 \begin{isamarkuptext}% |
110 \noindent |
110 \noindent |
111 Although this is more compact, it is less clear for the reader of the proof. |
111 Although this is more compact, it is less clear for the reader of the proof. |
112 |
112 |
113 We could now go back and prove \isa{exec (comp e) s [] = [value e s]} |
113 We could now go back and prove \isa{exec (comp e) s [] = [value e s]} |