34 } |
34 } |
35 \isamarkuptrue% |
35 \isamarkuptrue% |
36 % |
36 % |
37 \begin{isamarkuptext}% |
37 \begin{isamarkuptext}% |
38 Tuples may be used as patterns in $\lambda$-abstractions, |
38 Tuples may be used as patterns in $\lambda$-abstractions, |
39 for example \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}x{\isacharplus}y{\isacharplus}z} and \isa{{\isasymlambda}{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isacharcomma}z{\isacharparenright}{\isachardot}x{\isacharplus}y{\isacharplus}z}. In fact, |
39 for example \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}x{\isaliteral{2B}{\isacharplus}}y{\isaliteral{2B}{\isacharplus}}z} and \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}x{\isaliteral{2B}{\isacharplus}}y{\isaliteral{2B}{\isacharplus}}z}. In fact, |
40 tuple patterns can be used in most variable binding constructs, |
40 tuple patterns can be used in most variable binding constructs, |
41 and they can be nested. Here are |
41 and they can be nested. Here are |
42 some typical examples: |
42 some typical examples: |
43 \begin{quote} |
43 \begin{quote} |
44 \isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\ |
44 \isa{let\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ z\ in\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}}\\ |
45 \isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}\\ |
45 \isa{case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ zs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ x\ {\isaliteral{2B}{\isacharplus}}\ y}\\ |
46 \isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}A{\isachardot}\ x{\isacharequal}y}\\ |
46 \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}y}\\ |
47 \isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}\ x{\isacharequal}z{\isacharbraceright}}\\ |
47 \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}z{\isaliteral{7D}{\isacharbraceright}}}\\ |
48 \isa{{\isasymUnion}\isactrlbsub {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A\isactrlesub \ {\isacharbraceleft}x\ {\isacharplus}\ y{\isacharbraceright}} |
48 \isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}\isaliteral{5C3C5E627375623E}{}\isactrlbsub {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E3E}{\isasymin}}A\isaliteral{5C3C5E657375623E}{}\isactrlesub \ {\isaliteral{7B}{\isacharbraceleft}}x\ {\isaliteral{2B}{\isacharplus}}\ y{\isaliteral{7D}{\isacharbraceright}}} |
49 \end{quote} |
49 \end{quote} |
50 The intuitive meanings of these expressions should be obvious. |
50 The intuitive meanings of these expressions should be obvious. |
51 Unfortunately, we need to know in more detail what the notation really stands |
51 Unfortunately, we need to know in more detail what the notation really stands |
52 for once we have to reason about it. Abstraction |
52 for once we have to reason about it. Abstraction |
53 over pairs and tuples is merely a convenient shorthand for a more complex |
53 over pairs and tuples is merely a convenient shorthand for a more complex |
54 internal representation. Thus the internal and external form of a term may |
54 internal representation. Thus the internal and external form of a term may |
55 differ, which can affect proofs. If you want to avoid this complication, |
55 differ, which can affect proofs. If you want to avoid this complication, |
56 stick to \isa{fst} and \isa{snd} and write \isa{{\isasymlambda}p{\isachardot}\ fst\ p\ {\isacharplus}\ snd\ p} |
56 stick to \isa{fst} and \isa{snd} and write \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}p{\isaliteral{2E}{\isachardot}}\ fst\ p\ {\isaliteral{2B}{\isacharplus}}\ snd\ p} |
57 instead of \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharplus}y}. These terms are distinct even though they |
57 instead of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{2B}{\isacharplus}}y}. These terms are distinct even though they |
58 denote the same function. |
58 denote the same function. |
59 |
59 |
60 Internally, \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} becomes \isa{split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}}, where |
60 Internally, \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ t} becomes \isa{split\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}}, where |
61 \cdx{split} is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as |
61 \cdx{split} is the uncurrying function of type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c} defined as |
62 \begin{center} |
62 \begin{center} |
63 \isa{prod{\isacharunderscore}case\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}} |
63 \isa{prod{\isaliteral{5F}{\isacharunderscore}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}c\ p{\isaliteral{2E}{\isachardot}}\ c\ {\isaliteral{28}{\isacharparenleft}}fst\ p{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}snd\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} |
64 \hfill(\isa{split{\isacharunderscore}def}) |
64 \hfill(\isa{split{\isaliteral{5F}{\isacharunderscore}}def}) |
65 \end{center} |
65 \end{center} |
66 Pattern matching in |
66 Pattern matching in |
67 other variable binding constructs is translated similarly. Thus we need to |
67 other variable binding constructs is translated similarly. Thus we need to |
68 understand how to reason about such constructs.% |
68 understand how to reason about such constructs.% |
69 \end{isamarkuptext}% |
69 \end{isamarkuptext}% |
72 \isamarkupsubsection{Theorem Proving% |
72 \isamarkupsubsection{Theorem Proving% |
73 } |
73 } |
74 \isamarkuptrue% |
74 \isamarkuptrue% |
75 % |
75 % |
76 \begin{isamarkuptext}% |
76 \begin{isamarkuptext}% |
77 The most obvious approach is the brute force expansion of \isa{prod{\isacharunderscore}case}:% |
77 The most obvious approach is the brute force expansion of \isa{prod{\isaliteral{5F}{\isacharunderscore}}case}:% |
78 \end{isamarkuptext}% |
78 \end{isamarkuptext}% |
79 \isamarkuptrue% |
79 \isamarkuptrue% |
80 \isacommand{lemma}\isamarkupfalse% |
80 \isacommand{lemma}\isamarkupfalse% |
81 \ {\isachardoublequoteopen}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}x{\isacharparenright}\ p\ {\isacharequal}\ fst\ p{\isachardoublequoteclose}\isanewline |
81 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}x{\isaliteral{29}{\isacharparenright}}\ p\ {\isaliteral{3D}{\isacharequal}}\ fst\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
82 % |
82 % |
83 \isadelimproof |
83 \isadelimproof |
84 % |
84 % |
85 \endisadelimproof |
85 \endisadelimproof |
86 % |
86 % |
87 \isatagproof |
87 \isatagproof |
88 \isacommand{by}\isamarkupfalse% |
88 \isacommand{by}\isamarkupfalse% |
89 {\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}def{\isacharparenright}% |
89 {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ split{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% |
90 \endisatagproof |
90 \endisatagproof |
91 {\isafoldproof}% |
91 {\isafoldproof}% |
92 % |
92 % |
93 \isadelimproof |
93 \isadelimproof |
94 % |
94 % |
95 \endisadelimproof |
95 \endisadelimproof |
96 % |
96 % |
97 \begin{isamarkuptext}% |
97 \begin{isamarkuptext}% |
98 \noindent |
98 \noindent |
99 This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the |
99 This works well if rewriting with \isa{split{\isaliteral{5F}{\isacharunderscore}}def} finishes the |
100 proof, as it does above. But if it does not, you end up with exactly what |
100 proof, as it does above. But if it does not, you end up with exactly what |
101 we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this |
101 we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this |
102 approach is neither elegant nor very practical in large examples, although it |
102 approach is neither elegant nor very practical in large examples, although it |
103 can be effective in small ones. |
103 can be effective in small ones. |
104 |
104 |
105 If we consider why this lemma presents a problem, |
105 If we consider why this lemma presents a problem, |
106 we realize that we need to replace variable~\isa{p} by some pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}. Then both sides of the |
106 we realize that we need to replace variable~\isa{p} by some pair \isa{{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}}. Then both sides of the |
107 equation would simplify to \isa{a} by the simplification rules |
107 equation would simplify to \isa{a} by the simplification rules |
108 \isa{prod{\isacharunderscore}case\ f\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ f\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}. |
108 \isa{prod{\isaliteral{5F}{\isacharunderscore}}case\ f\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ a\ b} and \isa{fst\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a}. |
109 To reason about tuple patterns requires some way of |
109 To reason about tuple patterns requires some way of |
110 converting a variable of product type into a pair. |
110 converting a variable of product type into a pair. |
111 In case of a subterm of the form \isa{prod{\isacharunderscore}case\ f\ p} this is easy: the split |
111 In case of a subterm of the form \isa{prod{\isaliteral{5F}{\isacharunderscore}}case\ f\ p} this is easy: the split |
112 rule \isa{split{\isacharunderscore}split} replaces \isa{p} by a pair:% |
112 rule \isa{split{\isaliteral{5F}{\isacharunderscore}}split} replaces \isa{p} by a pair:% |
113 \index{*split (method)}% |
113 \index{*split (method)}% |
114 \end{isamarkuptext}% |
114 \end{isamarkuptext}% |
115 \isamarkuptrue% |
115 \isamarkuptrue% |
116 \isacommand{lemma}\isamarkupfalse% |
116 \isacommand{lemma}\isamarkupfalse% |
117 \ {\isachardoublequoteopen}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}y{\isacharparenright}\ p\ {\isacharequal}\ snd\ p{\isachardoublequoteclose}\isanewline |
117 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}y{\isaliteral{29}{\isacharparenright}}\ p\ {\isaliteral{3D}{\isacharequal}}\ snd\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
118 % |
118 % |
119 \isadelimproof |
119 \isadelimproof |
120 % |
120 % |
121 \endisadelimproof |
121 \endisadelimproof |
122 % |
122 % |
123 \isatagproof |
123 \isatagproof |
124 \isacommand{apply}\isamarkupfalse% |
124 \isacommand{apply}\isamarkupfalse% |
125 {\isacharparenleft}split\ split{\isacharunderscore}split{\isacharparenright}% |
125 {\isaliteral{28}{\isacharparenleft}}split\ split{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{29}{\isacharparenright}}% |
126 \begin{isamarkuptxt}% |
126 \begin{isamarkuptxt}% |
127 \begin{isabelle}% |
127 \begin{isabelle}% |
128 \ {\isadigit{1}}{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymlongrightarrow}\ y\ {\isacharequal}\ snd\ p% |
128 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ p\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ snd\ p% |
129 \end{isabelle} |
129 \end{isabelle} |
130 This subgoal is easily proved by simplification. Thus we could have combined |
130 This subgoal is easily proved by simplification. Thus we could have combined |
131 simplification and splitting in one command that proves the goal outright:% |
131 simplification and splitting in one command that proves the goal outright:% |
132 \end{isamarkuptxt}% |
132 \end{isamarkuptxt}% |
133 \isamarkuptrue% |
133 \isamarkuptrue% |
156 \begin{isamarkuptext}% |
156 \begin{isamarkuptext}% |
157 Let us look at a second example:% |
157 Let us look at a second example:% |
158 \end{isamarkuptext}% |
158 \end{isamarkuptext}% |
159 \isamarkuptrue% |
159 \isamarkuptrue% |
160 \isacommand{lemma}\isamarkupfalse% |
160 \isacommand{lemma}\isamarkupfalse% |
161 \ {\isachardoublequoteopen}let\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ p\ in\ fst\ p\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
161 \ {\isaliteral{22}{\isachardoublequoteopen}}let\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ p\ in\ fst\ p\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
162 % |
162 % |
163 \isadelimproof |
163 \isadelimproof |
164 % |
164 % |
165 \endisadelimproof |
165 \endisadelimproof |
166 % |
166 % |
167 \isatagproof |
167 \isatagproof |
168 \isacommand{apply}\isamarkupfalse% |
168 \isacommand{apply}\isamarkupfalse% |
169 {\isacharparenleft}simp\ only{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% |
169 {\isaliteral{28}{\isacharparenleft}}simp\ only{\isaliteral{3A}{\isacharcolon}}\ Let{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% |
170 \begin{isamarkuptxt}% |
170 \begin{isamarkuptxt}% |
171 \begin{isabelle}% |
171 \begin{isabelle}% |
172 \ {\isadigit{1}}{\isachardot}\ case\ p\ of\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymRightarrow}\ fst\ p\ {\isacharequal}\ x% |
172 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ case\ p\ of\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ fst\ p\ {\isaliteral{3D}{\isacharequal}}\ x% |
173 \end{isabelle} |
173 \end{isabelle} |
174 A paired \isa{let} reduces to a paired $\lambda$-abstraction, which |
174 A paired \isa{let} reduces to a paired $\lambda$-abstraction, which |
175 can be split as above. The same is true for paired set comprehension:% |
175 can be split as above. The same is true for paired set comprehension:% |
176 \end{isamarkuptxt}% |
176 \end{isamarkuptxt}% |
177 \isamarkuptrue% |
177 \isamarkuptrue% |
181 % |
181 % |
182 \isadelimproof |
182 \isadelimproof |
183 % |
183 % |
184 \endisadelimproof |
184 \endisadelimproof |
185 \isacommand{lemma}\isamarkupfalse% |
185 \isacommand{lemma}\isamarkupfalse% |
186 \ {\isachardoublequoteopen}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequoteclose}\isanewline |
186 \ {\isaliteral{22}{\isachardoublequoteopen}}p\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}y{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ fst\ p\ {\isaliteral{3D}{\isacharequal}}\ snd\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
187 % |
187 % |
188 \isadelimproof |
188 \isadelimproof |
189 % |
189 % |
190 \endisadelimproof |
190 \endisadelimproof |
191 % |
191 % |
192 \isatagproof |
192 \isatagproof |
193 \isacommand{apply}\isamarkupfalse% |
193 \isacommand{apply}\isamarkupfalse% |
194 \ simp% |
194 \ simp% |
195 \begin{isamarkuptxt}% |
195 \begin{isamarkuptxt}% |
196 \begin{isabelle}% |
196 \begin{isabelle}% |
197 \ {\isadigit{1}}{\isachardot}\ prod{\isacharunderscore}case\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p% |
197 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ prod{\isaliteral{5F}{\isacharunderscore}}case\ op\ {\isaliteral{3D}{\isacharequal}}\ p\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ fst\ p\ {\isaliteral{3D}{\isacharequal}}\ snd\ p% |
198 \end{isabelle} |
198 \end{isabelle} |
199 Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split} |
199 Again, simplification produces a term suitable for \isa{split{\isaliteral{5F}{\isacharunderscore}}split} |
200 as above. If you are worried about the strange form of the premise: |
200 as above. If you are worried about the strange form of the premise: |
201 \isa{split\ {\isacharparenleft}op\ {\isacharequal}{\isacharparenright}} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y}. |
201 \isa{split\ {\isaliteral{28}{\isacharparenleft}}op\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}} is short for \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ y}. |
202 The same proof procedure works for% |
202 The same proof procedure works for% |
203 \end{isamarkuptxt}% |
203 \end{isamarkuptxt}% |
204 \isamarkuptrue% |
204 \isamarkuptrue% |
205 % |
205 % |
206 \endisatagproof |
206 \endisatagproof |
208 % |
208 % |
209 \isadelimproof |
209 \isadelimproof |
210 % |
210 % |
211 \endisadelimproof |
211 \endisadelimproof |
212 \isacommand{lemma}\isamarkupfalse% |
212 \isacommand{lemma}\isamarkupfalse% |
213 \ {\isachardoublequoteopen}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequoteclose}% |
213 \ {\isaliteral{22}{\isachardoublequoteopen}}p\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{3D}{\isacharequal}}y{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ fst\ p\ {\isaliteral{3D}{\isacharequal}}\ snd\ p{\isaliteral{22}{\isachardoublequoteclose}}% |
214 \isadelimproof |
214 \isadelimproof |
215 % |
215 % |
216 \endisadelimproof |
216 \endisadelimproof |
217 % |
217 % |
218 \isatagproof |
218 \isatagproof |
219 % |
219 % |
220 \begin{isamarkuptxt}% |
220 \begin{isamarkuptxt}% |
221 \noindent |
221 \noindent |
222 except that we now have to use \isa{split{\isacharunderscore}split{\isacharunderscore}asm}, because |
222 except that we now have to use \isa{split{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{5F}{\isacharunderscore}}asm}, because |
223 \isa{prod{\isacharunderscore}case} occurs in the assumptions. |
223 \isa{prod{\isaliteral{5F}{\isacharunderscore}}case} occurs in the assumptions. |
224 |
224 |
225 However, splitting \isa{prod{\isacharunderscore}case} is not always a solution, as no \isa{prod{\isacharunderscore}case} |
225 However, splitting \isa{prod{\isaliteral{5F}{\isacharunderscore}}case} is not always a solution, as no \isa{prod{\isaliteral{5F}{\isacharunderscore}}case} |
226 may be present in the goal. Consider the following function:% |
226 may be present in the goal. Consider the following function:% |
227 \end{isamarkuptxt}% |
227 \end{isamarkuptxt}% |
228 \isamarkuptrue% |
228 \isamarkuptrue% |
229 % |
229 % |
230 \endisatagproof |
230 \endisatagproof |
232 % |
232 % |
233 \isadelimproof |
233 \isadelimproof |
234 % |
234 % |
235 \endisadelimproof |
235 \endisadelimproof |
236 \isacommand{primrec}\isamarkupfalse% |
236 \isacommand{primrec}\isamarkupfalse% |
237 \ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}swap\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardoublequoteclose}% |
237 \ swap\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}swap\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
238 \begin{isamarkuptext}% |
238 \begin{isamarkuptext}% |
239 \noindent |
239 \noindent |
240 Note that the above \isacommand{primrec} definition is admissible |
240 Note that the above \isacommand{primrec} definition is admissible |
241 because \isa{{\isasymtimes}} is a datatype. When we now try to prove% |
241 because \isa{{\isaliteral{5C3C74696D65733E}{\isasymtimes}}} is a datatype. When we now try to prove% |
242 \end{isamarkuptext}% |
242 \end{isamarkuptext}% |
243 \isamarkuptrue% |
243 \isamarkuptrue% |
244 \isacommand{lemma}\isamarkupfalse% |
244 \isacommand{lemma}\isamarkupfalse% |
245 \ {\isachardoublequoteopen}swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p{\isachardoublequoteclose}% |
245 \ {\isaliteral{22}{\isachardoublequoteopen}}swap{\isaliteral{28}{\isacharparenleft}}swap\ p{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}% |
246 \isadelimproof |
246 \isadelimproof |
247 % |
247 % |
248 \endisadelimproof |
248 \endisadelimproof |
249 % |
249 % |
250 \isatagproof |
250 \isatagproof |
251 % |
251 % |
252 \begin{isamarkuptxt}% |
252 \begin{isamarkuptxt}% |
253 \noindent |
253 \noindent |
254 simplification will do nothing, because the defining equation for |
254 simplification will do nothing, because the defining equation for |
255 \isa{swap} expects a pair. Again, we need to turn \isa{p} |
255 \isa{swap} expects a pair. Again, we need to turn \isa{p} |
256 into a pair first, but this time there is no \isa{prod{\isacharunderscore}case} in sight. |
256 into a pair first, but this time there is no \isa{prod{\isaliteral{5F}{\isacharunderscore}}case} in sight. |
257 The only thing we can do is to split the term by hand:% |
257 The only thing we can do is to split the term by hand:% |
258 \end{isamarkuptxt}% |
258 \end{isamarkuptxt}% |
259 \isamarkuptrue% |
259 \isamarkuptrue% |
260 \isacommand{apply}\isamarkupfalse% |
260 \isacommand{apply}\isamarkupfalse% |
261 {\isacharparenleft}case{\isacharunderscore}tac\ p{\isacharparenright}% |
261 {\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ p{\isaliteral{29}{\isacharparenright}}% |
262 \begin{isamarkuptxt}% |
262 \begin{isamarkuptxt}% |
263 \noindent |
263 \noindent |
264 \begin{isabelle}% |
264 \begin{isabelle}% |
265 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ swap\ {\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p% |
265 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ b{\isaliteral{2E}{\isachardot}}\ p\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ swap\ {\isaliteral{28}{\isacharparenleft}}swap\ p{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ p% |
266 \end{isabelle} |
266 \end{isabelle} |
267 Again, \methdx{case_tac} is applicable because \isa{{\isasymtimes}} is a datatype. |
267 Again, \methdx{case_tac} is applicable because \isa{{\isaliteral{5C3C74696D65733E}{\isasymtimes}}} is a datatype. |
268 The subgoal is easily proved by \isa{simp}. |
268 The subgoal is easily proved by \isa{simp}. |
269 |
269 |
270 Splitting by \isa{case{\isacharunderscore}tac} also solves the previous examples and may thus |
270 Splitting by \isa{case{\isaliteral{5F}{\isacharunderscore}}tac} also solves the previous examples and may thus |
271 appear preferable to the more arcane methods introduced first. However, see |
271 appear preferable to the more arcane methods introduced first. However, see |
272 the warning about \isa{case{\isacharunderscore}tac} in \S\ref{sec:struct-ind-case}. |
272 the warning about \isa{case{\isaliteral{5F}{\isacharunderscore}}tac} in \S\ref{sec:struct-ind-case}. |
273 |
273 |
274 Alternatively, you can split \emph{all} \isa{{\isasymAnd}}-quantified variables |
274 Alternatively, you can split \emph{all} \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}-quantified variables |
275 in a goal with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:% |
275 in a goal with the rewrite rule \isa{split{\isaliteral{5F}{\isacharunderscore}}paired{\isaliteral{5F}{\isacharunderscore}}all}:% |
276 \end{isamarkuptxt}% |
276 \end{isamarkuptxt}% |
277 \isamarkuptrue% |
277 \isamarkuptrue% |
278 % |
278 % |
279 \endisatagproof |
279 \endisatagproof |
280 {\isafoldproof}% |
280 {\isafoldproof}% |
281 % |
281 % |
282 \isadelimproof |
282 \isadelimproof |
283 % |
283 % |
284 \endisadelimproof |
284 \endisadelimproof |
285 \isacommand{lemma}\isamarkupfalse% |
285 \isacommand{lemma}\isamarkupfalse% |
286 \ {\isachardoublequoteopen}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequoteclose}\isanewline |
286 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}p\ q{\isaliteral{2E}{\isachardot}}\ swap{\isaliteral{28}{\isacharparenleft}}swap\ p{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ q\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ p\ {\isaliteral{3D}{\isacharequal}}\ q{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
287 % |
287 % |
288 \isadelimproof |
288 \isadelimproof |
289 % |
289 % |
290 \endisadelimproof |
290 \endisadelimproof |
291 % |
291 % |
292 \isatagproof |
292 \isatagproof |
293 \isacommand{apply}\isamarkupfalse% |
293 \isacommand{apply}\isamarkupfalse% |
294 {\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}% |
294 {\isaliteral{28}{\isacharparenleft}}simp\ only{\isaliteral{3A}{\isacharcolon}}\ split{\isaliteral{5F}{\isacharunderscore}}paired{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}% |
295 \begin{isamarkuptxt}% |
295 \begin{isamarkuptxt}% |
296 \noindent |
296 \noindent |
297 \begin{isabelle}% |
297 \begin{isabelle}% |
298 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\ swap\ {\isacharparenleft}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}% |
298 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ b\ aa\ ba{\isaliteral{2E}{\isachardot}}\ swap\ {\isaliteral{28}{\isacharparenleft}}swap\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}aa{\isaliteral{2C}{\isacharcomma}}\ ba{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}aa{\isaliteral{2C}{\isacharcomma}}\ ba{\isaliteral{29}{\isacharparenright}}% |
299 \end{isabelle}% |
299 \end{isabelle}% |
300 \end{isamarkuptxt}% |
300 \end{isamarkuptxt}% |
301 \isamarkuptrue% |
301 \isamarkuptrue% |
302 \isacommand{apply}\isamarkupfalse% |
302 \isacommand{apply}\isamarkupfalse% |
303 \ simp\isanewline |
303 \ simp\isanewline |
327 % |
327 % |
328 \endisadelimproof |
328 \endisadelimproof |
329 % |
329 % |
330 \isatagproof |
330 \isatagproof |
331 \isacommand{apply}\isamarkupfalse% |
331 \isacommand{apply}\isamarkupfalse% |
332 {\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}% |
332 {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ split{\isaliteral{5F}{\isacharunderscore}}paired{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}% |
333 \endisatagproof |
333 \endisatagproof |
334 {\isafoldproof}% |
334 {\isafoldproof}% |
335 % |
335 % |
336 \isadelimproof |
336 \isadelimproof |
337 % |
337 % |
338 \endisadelimproof |
338 \endisadelimproof |
339 % |
339 % |
340 \begin{isamarkuptext}% |
340 \begin{isamarkuptext}% |
341 \noindent |
341 \noindent |
342 Finally, the simplifier automatically splits all \isa{{\isasymforall}} and |
342 Finally, the simplifier automatically splits all \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}} and |
343 \isa{{\isasymexists}}-quantified variables:% |
343 \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}}-quantified variables:% |
344 \end{isamarkuptext}% |
344 \end{isamarkuptext}% |
345 \isamarkuptrue% |
345 \isamarkuptrue% |
346 \isacommand{lemma}\isamarkupfalse% |
346 \isacommand{lemma}\isamarkupfalse% |
347 \ {\isachardoublequoteopen}{\isasymforall}p{\isachardot}\ {\isasymexists}q{\isachardot}\ swap\ p\ {\isacharequal}\ swap\ q{\isachardoublequoteclose}\isanewline |
347 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}p{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}q{\isaliteral{2E}{\isachardot}}\ swap\ p\ {\isaliteral{3D}{\isacharequal}}\ swap\ q{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
348 % |
348 % |
349 \isadelimproof |
349 \isadelimproof |
350 % |
350 % |
351 \endisadelimproof |
351 \endisadelimproof |
352 % |
352 % |
363 \begin{isamarkuptext}% |
363 \begin{isamarkuptext}% |
364 \noindent |
364 \noindent |
365 To turn off this automatic splitting, disable the |
365 To turn off this automatic splitting, disable the |
366 responsible simplification rules: |
366 responsible simplification rules: |
367 \begin{center} |
367 \begin{center} |
368 \isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}} |
368 \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}a\ b{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} |
369 \hfill |
369 \hfill |
370 (\isa{split{\isacharunderscore}paired{\isacharunderscore}All})\\ |
370 (\isa{split{\isaliteral{5F}{\isacharunderscore}}paired{\isaliteral{5F}{\isacharunderscore}}All})\\ |
371 \isa{{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}} |
371 \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ b{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} |
372 \hfill |
372 \hfill |
373 (\isa{split{\isacharunderscore}paired{\isacharunderscore}Ex}) |
373 (\isa{split{\isaliteral{5F}{\isacharunderscore}}paired{\isaliteral{5F}{\isacharunderscore}}Ex}) |
374 \end{center}% |
374 \end{center}% |
375 \end{isamarkuptext}% |
375 \end{isamarkuptext}% |
376 \isamarkuptrue% |
376 \isamarkuptrue% |
377 % |
377 % |
378 \isadelimtheory |
378 \isadelimtheory |