29 \end{itemize} |
29 \end{itemize} |
30 In Isabelle this becomes% |
30 In Isabelle this becomes% |
31 \end{isamarkuptext}% |
31 \end{isamarkuptext}% |
32 \isamarkuptrue% |
32 \isamarkuptrue% |
33 \isacommand{datatype}\isamarkupfalse% |
33 \isacommand{datatype}\isamarkupfalse% |
34 \ {\isacharprime}a\ aexp\ {\isacharequal}\ IF\ \ \ {\isachardoublequoteopen}{\isacharprime}a\ bexp{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ aexp{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ aexp{\isachardoublequoteclose}\isanewline |
34 \ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{3D}{\isacharequal}}\ IF\ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
35 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Sum\ \ {\isachardoublequoteopen}{\isacharprime}a\ aexp{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ aexp{\isachardoublequoteclose}\isanewline |
35 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Sum\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
36 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Diff\ {\isachardoublequoteopen}{\isacharprime}a\ aexp{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ aexp{\isachardoublequoteclose}\isanewline |
36 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Diff\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
37 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Var\ {\isacharprime}a\isanewline |
37 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Var\ {\isaliteral{27}{\isacharprime}}a\isanewline |
38 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Num\ nat\isanewline |
38 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Num\ nat\isanewline |
39 \isakeyword{and}\ \ \ \ \ \ {\isacharprime}a\ bexp\ {\isacharequal}\ Less\ {\isachardoublequoteopen}{\isacharprime}a\ aexp{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ aexp{\isachardoublequoteclose}\isanewline |
39 \isakeyword{and}\ \ \ \ \ \ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{3D}{\isacharequal}}\ Less\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
40 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ \ {\isachardoublequoteopen}{\isacharprime}a\ bexp{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ bexp{\isachardoublequoteclose}\isanewline |
40 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ And\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
41 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ \ {\isachardoublequoteopen}{\isacharprime}a\ bexp{\isachardoublequoteclose}% |
41 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Neg\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}% |
42 \begin{isamarkuptext}% |
42 \begin{isamarkuptext}% |
43 \noindent |
43 \noindent |
44 Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler}, |
44 Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler}, |
45 except that we have added an \isa{IF} constructor, |
45 except that we have added an \isa{IF} constructor, |
46 fixed the values to be of type \isa{nat} and declared the two binary |
46 fixed the values to be of type \isa{nat} and declared the two binary |
48 expressions can be arithmetic comparisons, conjunctions and negations. |
48 expressions can be arithmetic comparisons, conjunctions and negations. |
49 The semantics is given by two evaluation functions:% |
49 The semantics is given by two evaluation functions:% |
50 \end{isamarkuptext}% |
50 \end{isamarkuptext}% |
51 \isamarkuptrue% |
51 \isamarkuptrue% |
52 \isacommand{primrec}\isamarkupfalse% |
52 \isacommand{primrec}\isamarkupfalse% |
53 \ evala\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
53 \ evala\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline |
54 \ \ \ \ \ \ \ \ \ evalb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
54 \ \ \ \ \ \ \ \ \ evalb\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
55 {\isachardoublequoteopen}evala\ {\isacharparenleft}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\isanewline |
55 {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\isanewline |
56 \ \ \ {\isacharparenleft}if\ evalb\ b\ env\ then\ evala\ a{\isadigit{1}}\ env\ else\ evala\ a{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
56 \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ evalb\ b\ env\ then\ evala\ a{\isadigit{1}}\ env\ else\ evala\ a{\isadigit{2}}\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
57 {\isachardoublequoteopen}evala\ {\isacharparenleft}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a{\isadigit{1}}\ env\ {\isacharplus}\ evala\ a{\isadigit{2}}\ env{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
57 {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ evala\ a{\isadigit{1}}\ env\ {\isaliteral{2B}{\isacharplus}}\ evala\ a{\isadigit{2}}\ env{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
58 {\isachardoublequoteopen}evala\ {\isacharparenleft}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a{\isadigit{1}}\ env\ {\isacharminus}\ evala\ a{\isadigit{2}}\ env{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
58 {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ evala\ a{\isadigit{1}}\ env\ {\isaliteral{2D}{\isacharminus}}\ evala\ a{\isadigit{2}}\ env{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
59 {\isachardoublequoteopen}evala\ {\isacharparenleft}Var\ v{\isacharparenright}\ env\ {\isacharequal}\ env\ v{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
59 {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}Var\ v{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ env\ v{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
60 {\isachardoublequoteopen}evala\ {\isacharparenleft}Num\ n{\isacharparenright}\ env\ {\isacharequal}\ n{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
60 {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
61 \isanewline |
61 \isanewline |
62 {\isachardoublequoteopen}evalb\ {\isacharparenleft}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evala\ a{\isadigit{1}}\ env\ {\isacharless}\ evala\ a{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
62 {\isaliteral{22}{\isachardoublequoteopen}}evalb\ {\isaliteral{28}{\isacharparenleft}}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}evala\ a{\isadigit{1}}\ env\ {\isaliteral{3C}{\isacharless}}\ evala\ a{\isadigit{2}}\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
63 {\isachardoublequoteopen}evalb\ {\isacharparenleft}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evalb\ b{\isadigit{1}}\ env\ {\isasymand}\ evalb\ b{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
63 {\isaliteral{22}{\isachardoublequoteopen}}evalb\ {\isaliteral{28}{\isacharparenleft}}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}evalb\ b{\isadigit{1}}\ env\ {\isaliteral{5C3C616E643E}{\isasymand}}\ evalb\ b{\isadigit{2}}\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
64 {\isachardoublequoteopen}evalb\ {\isacharparenleft}Neg\ b{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ evalb\ b\ env{\isacharparenright}{\isachardoublequoteclose}% |
64 {\isaliteral{22}{\isachardoublequoteopen}}evalb\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ evalb\ b\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
65 \begin{isamarkuptext}% |
65 \begin{isamarkuptext}% |
66 \noindent |
66 \noindent |
67 |
67 |
68 Both take an expression and an environment (a mapping from variables |
68 Both take an expression and an environment (a mapping from variables |
69 \isa{{\isacharprime}a} to values \isa{nat}) and return its arithmetic/boolean |
69 \isa{{\isaliteral{27}{\isacharprime}}a} to values \isa{nat}) and return its arithmetic/boolean |
70 value. Since the datatypes are mutually recursive, so are functions |
70 value. Since the datatypes are mutually recursive, so are functions |
71 that operate on them. Hence they need to be defined in a single |
71 that operate on them. Hence they need to be defined in a single |
72 \isacommand{primrec} section. Notice the \isakeyword{and} separating |
72 \isacommand{primrec} section. Notice the \isakeyword{and} separating |
73 the declarations of \isa{evala} and \isa{evalb}. Their defining |
73 the declarations of \isa{evala} and \isa{evalb}. Their defining |
74 equations need not be split into two groups; |
74 equations need not be split into two groups; |
76 |
76 |
77 In the same fashion we also define two functions that perform substitution:% |
77 In the same fashion we also define two functions that perform substitution:% |
78 \end{isamarkuptext}% |
78 \end{isamarkuptext}% |
79 \isamarkuptrue% |
79 \isamarkuptrue% |
80 \isacommand{primrec}\isamarkupfalse% |
80 \isacommand{primrec}\isamarkupfalse% |
81 \ substa\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
81 \ substa\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline |
82 \ \ \ \ \ \ \ \ \ substb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharprime}b\ bexp{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
82 \ \ \ \ \ \ \ \ \ substb\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
83 {\isachardoublequoteopen}substa\ s\ {\isacharparenleft}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline |
83 {\isaliteral{22}{\isachardoublequoteopen}}substa\ s\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
84 \ \ \ IF\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
84 \ \ \ IF\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
85 {\isachardoublequoteopen}substa\ s\ {\isacharparenleft}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ Sum\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
85 {\isaliteral{22}{\isachardoublequoteopen}}substa\ s\ {\isaliteral{28}{\isacharparenleft}}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Sum\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
86 {\isachardoublequoteopen}substa\ s\ {\isacharparenleft}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ Diff\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
86 {\isaliteral{22}{\isachardoublequoteopen}}substa\ s\ {\isaliteral{28}{\isacharparenleft}}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Diff\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
87 {\isachardoublequoteopen}substa\ s\ {\isacharparenleft}Var\ v{\isacharparenright}\ {\isacharequal}\ s\ v{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
87 {\isaliteral{22}{\isachardoublequoteopen}}substa\ s\ {\isaliteral{28}{\isacharparenleft}}Var\ v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ s\ v{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
88 {\isachardoublequoteopen}substa\ s\ {\isacharparenleft}Num\ n{\isacharparenright}\ {\isacharequal}\ Num\ n{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
88 {\isaliteral{22}{\isachardoublequoteopen}}substa\ s\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Num\ n{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
89 \isanewline |
89 \isanewline |
90 {\isachardoublequoteopen}substb\ s\ {\isacharparenleft}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ Less\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
90 {\isaliteral{22}{\isachardoublequoteopen}}substb\ s\ {\isaliteral{28}{\isacharparenleft}}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Less\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
91 {\isachardoublequoteopen}substb\ s\ {\isacharparenleft}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ And\ {\isacharparenleft}substb\ s\ b{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substb\ s\ b{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
91 {\isaliteral{22}{\isachardoublequoteopen}}substb\ s\ {\isaliteral{28}{\isacharparenleft}}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ And\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
92 {\isachardoublequoteopen}substb\ s\ {\isacharparenleft}Neg\ b{\isacharparenright}\ {\isacharequal}\ Neg\ {\isacharparenleft}substb\ s\ b{\isacharparenright}{\isachardoublequoteclose}% |
92 {\isaliteral{22}{\isachardoublequoteopen}}substb\ s\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Neg\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
93 \begin{isamarkuptext}% |
93 \begin{isamarkuptext}% |
94 \noindent |
94 \noindent |
95 Their first argument is a function mapping variables to expressions, the |
95 Their first argument is a function mapping variables to expressions, the |
96 substitution. It is applied to all variables in the second argument. As a |
96 substitution. It is applied to all variables in the second argument. As a |
97 result, the type of variables in the expression may change from \isa{{\isacharprime}a} |
97 result, the type of variables in the expression may change from \isa{{\isaliteral{27}{\isacharprime}}a} |
98 to \isa{{\isacharprime}b}. Note that there are only arithmetic and no boolean variables. |
98 to \isa{{\isaliteral{27}{\isacharprime}}b}. Note that there are only arithmetic and no boolean variables. |
99 |
99 |
100 Now we can prove a fundamental theorem about the interaction between |
100 Now we can prove a fundamental theorem about the interaction between |
101 evaluation and substitution: applying a substitution $s$ to an expression $a$ |
101 evaluation and substitution: applying a substitution $s$ to an expression $a$ |
102 and evaluating the result in an environment $env$ yields the same result as |
102 and evaluating the result in an environment $env$ yields the same result as |
103 evaluation $a$ in the environment that maps every variable $x$ to the value |
103 evaluation $a$ in the environment that maps every variable $x$ to the value |
106 theorem in the induction step. Therefore you need to state and prove both |
106 theorem in the induction step. Therefore you need to state and prove both |
107 theorems simultaneously:% |
107 theorems simultaneously:% |
108 \end{isamarkuptext}% |
108 \end{isamarkuptext}% |
109 \isamarkuptrue% |
109 \isamarkuptrue% |
110 \isacommand{lemma}\isamarkupfalse% |
110 \isacommand{lemma}\isamarkupfalse% |
111 \ {\isachardoublequoteopen}evala\ {\isacharparenleft}substa\ s\ a{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}\ {\isasymand}\isanewline |
111 \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ evala\ a\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ evala\ {\isaliteral{28}{\isacharparenleft}}s\ x{\isaliteral{29}{\isacharparenright}}\ env{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline |
112 \ \ \ \ \ \ \ \ evalb\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ env\ {\isacharequal}\ evalb\ b\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}{\isachardoublequoteclose}\isanewline |
112 \ \ \ \ \ \ \ \ evalb\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ evalb\ b\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ evala\ {\isaliteral{28}{\isacharparenleft}}s\ x{\isaliteral{29}{\isacharparenright}}\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
113 % |
113 % |
114 \isadelimproof |
114 \isadelimproof |
115 % |
115 % |
116 \endisadelimproof |
116 \endisadelimproof |
117 % |
117 % |
118 \isatagproof |
118 \isatagproof |
119 \isacommand{apply}\isamarkupfalse% |
119 \isacommand{apply}\isamarkupfalse% |
120 {\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}% |
120 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ a\ \isakeyword{and}\ b{\isaliteral{29}{\isacharparenright}}% |
121 \begin{isamarkuptxt}% |
121 \begin{isamarkuptxt}% |
122 \noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:% |
122 \noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:% |
123 \end{isamarkuptxt}% |
123 \end{isamarkuptxt}% |
124 \isamarkuptrue% |
124 \isamarkuptrue% |
125 \isacommand{apply}\isamarkupfalse% |
125 \isacommand{apply}\isamarkupfalse% |
126 \ simp{\isacharunderscore}all% |
126 \ simp{\isaliteral{5F}{\isacharunderscore}}all% |
127 \endisatagproof |
127 \endisatagproof |
128 {\isafoldproof}% |
128 {\isafoldproof}% |
129 % |
129 % |
130 \isadelimproof |
130 \isadelimproof |
131 % |
131 % |
135 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
135 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
136 an inductive proof expects a goal of the form |
136 an inductive proof expects a goal of the form |
137 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
137 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
138 where each variable $x@i$ is of type $\tau@i$. Induction is started by |
138 where each variable $x@i$ is of type $\tau@i$. Induction is started by |
139 \begin{isabelle} |
139 \begin{isabelle} |
140 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$\isa{{\isacharparenright}} |
140 \isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$\isa{{\isaliteral{29}{\isacharparenright}}} |
141 \end{isabelle} |
141 \end{isabelle} |
142 |
142 |
143 \begin{exercise} |
143 \begin{exercise} |
144 Define a function \isa{norma} of type \isa{{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharprime}a\ aexp} that |
144 Define a function \isa{norma} of type \isa{{\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp} that |
145 replaces \isa{IF}s with complex boolean conditions by nested |
145 replaces \isa{IF}s with complex boolean conditions by nested |
146 \isa{IF}s; it should eliminate the constructors |
146 \isa{IF}s; it should eliminate the constructors |
147 \isa{And} and \isa{Neg}, leaving only \isa{Less}. |
147 \isa{And} and \isa{Neg}, leaving only \isa{Less}. |
148 Prove that \isa{norma} |
148 Prove that \isa{norma} |
149 preserves the value of an expression and that the result of \isa{norma} |
149 preserves the value of an expression and that the result of \isa{norma} |
150 is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in |
150 is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in |
151 it. ({\em Hint:} proceed as in \S\ref{sec:boolex} and read the discussion |
151 it. ({\em Hint:} proceed as in \S\ref{sec:boolex} and read the discussion |
152 of type annotations following lemma \isa{subst{\isacharunderscore}id} below). |
152 of type annotations following lemma \isa{subst{\isaliteral{5F}{\isacharunderscore}}id} below). |
153 \end{exercise}% |
153 \end{exercise}% |
154 \end{isamarkuptext}% |
154 \end{isamarkuptext}% |
155 \isamarkuptrue% |
155 \isamarkuptrue% |
156 % |
156 % |
157 \isadelimproof |
157 \isadelimproof |