40 datatype \isa{gterm} for the type of ground terms. It is a type constructor |
40 datatype \isa{gterm} for the type of ground terms. It is a type constructor |
41 whose argument is a type of function symbols.% |
41 whose argument is a type of function symbols.% |
42 \end{isamarkuptext}% |
42 \end{isamarkuptext}% |
43 \isamarkuptrue% |
43 \isamarkuptrue% |
44 \isacommand{datatype}\isamarkupfalse% |
44 \isacommand{datatype}\isamarkupfalse% |
45 \ {\isacharprime}f\ gterm\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequoteopen}{\isacharprime}f\ gterm\ list{\isachardoublequoteclose}% |
45 \ {\isaliteral{27}{\isacharprime}}f\ gterm\ {\isaliteral{3D}{\isacharequal}}\ Apply\ {\isaliteral{27}{\isacharprime}}f\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ gterm\ list{\isaliteral{22}{\isachardoublequoteclose}}% |
46 \begin{isamarkuptext}% |
46 \begin{isamarkuptext}% |
47 To try it out, we declare a datatype of some integer operations: |
47 To try it out, we declare a datatype of some integer operations: |
48 integer constants, the unary minus operator and the addition |
48 integer constants, the unary minus operator and the addition |
49 operator.% |
49 operator.% |
50 \end{isamarkuptext}% |
50 \end{isamarkuptext}% |
51 \isamarkuptrue% |
51 \isamarkuptrue% |
52 \isacommand{datatype}\isamarkupfalse% |
52 \isacommand{datatype}\isamarkupfalse% |
53 \ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus% |
53 \ integer{\isaliteral{5F}{\isacharunderscore}}op\ {\isaliteral{3D}{\isacharequal}}\ Number\ int\ {\isaliteral{7C}{\isacharbar}}\ UnaryMinus\ {\isaliteral{7C}{\isacharbar}}\ Plus% |
54 \begin{isamarkuptext}% |
54 \begin{isamarkuptext}% |
55 Now the type \isa{integer{\isacharunderscore}op\ gterm} denotes the ground |
55 Now the type \isa{integer{\isaliteral{5F}{\isacharunderscore}}op\ gterm} denotes the ground |
56 terms built over those symbols. |
56 terms built over those symbols. |
57 |
57 |
58 The type constructor \isa{gterm} can be generalized to a function |
58 The type constructor \isa{gterm} can be generalized to a function |
59 over sets. It returns |
59 over sets. It returns |
60 the set of ground terms that can be formed over a set \isa{F} of function symbols. For |
60 the set of ground terms that can be formed over a set \isa{F} of function symbols. For |
61 example, we could consider the set of ground terms formed from the finite |
61 example, we could consider the set of ground terms formed from the finite |
62 set \isa{{\isacharbraceleft}Number\ {\isadigit{2}}{\isacharcomma}\ UnaryMinus{\isacharcomma}\ Plus{\isacharbraceright}}. |
62 set \isa{{\isaliteral{7B}{\isacharbraceleft}}Number\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ UnaryMinus{\isaliteral{2C}{\isacharcomma}}\ Plus{\isaliteral{7D}{\isacharbraceright}}}. |
63 |
63 |
64 This concept is inductive. If we have a list \isa{args} of ground terms |
64 This concept is inductive. If we have a list \isa{args} of ground terms |
65 over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we |
65 over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we |
66 can apply \isa{f} to \isa{args} to obtain another ground term. |
66 can apply \isa{f} to \isa{args} to obtain another ground term. |
67 The only difficulty is that the argument list may be of any length. Hitherto, |
67 The only difficulty is that the argument list may be of any length. Hitherto, |
72 to our inductively defined set: is a ground term |
72 to our inductively defined set: is a ground term |
73 over~\isa{F}. The function \isa{set} denotes the set of elements in a given |
73 over~\isa{F}. The function \isa{set} denotes the set of elements in a given |
74 list.% |
74 list.% |
75 \end{isamarkuptext}% |
75 \end{isamarkuptext}% |
76 \isamarkuptrue% |
76 \isamarkuptrue% |
77 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% |
77 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
78 \isanewline |
78 \isanewline |
79 \ \ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline |
79 \ \ gterms\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}f\ gterm\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
80 \ \ \isakeyword{for}\ F\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ set{\isachardoublequoteclose}\isanewline |
80 \ \ \isakeyword{for}\ F\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
81 \isakeyword{where}\isanewline |
81 \isakeyword{where}\isanewline |
82 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline |
82 step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{3B}{\isacharsemicolon}}\ \ f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
83 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequoteclose}% |
83 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Apply\ f\ args{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{22}{\isachardoublequoteclose}}% |
84 \begin{isamarkuptext}% |
84 \begin{isamarkuptext}% |
85 To demonstrate a proof from this definition, let us |
85 To demonstrate a proof from this definition, let us |
86 show that the function \isa{gterms} |
86 show that the function \isa{gterms} |
87 is \textbf{monotone}. We shall need this concept shortly.% |
87 is \textbf{monotone}. We shall need this concept shortly.% |
88 \end{isamarkuptext}% |
88 \end{isamarkuptext}% |
89 \isamarkuptrue% |
89 \isamarkuptrue% |
90 \isacommand{lemma}\isamarkupfalse% |
90 \isacommand{lemma}\isamarkupfalse% |
91 \ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequoteopen}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequoteclose}\isanewline |
91 \ gterms{\isaliteral{5F}{\isacharunderscore}}mono{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}F{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}G\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ gterms\ F\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ gterms\ G{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
92 % |
92 % |
93 \isadelimproof |
93 \isadelimproof |
94 % |
94 % |
95 \endisadelimproof |
95 \endisadelimproof |
96 % |
96 % |
97 \isatagproof |
97 \isatagproof |
98 \isacommand{apply}\isamarkupfalse% |
98 \isacommand{apply}\isamarkupfalse% |
99 \ clarify\isanewline |
99 \ clarify\isanewline |
100 \isacommand{apply}\isamarkupfalse% |
100 \isacommand{apply}\isamarkupfalse% |
101 \ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isanewline |
101 \ {\isaliteral{28}{\isacharparenleft}}erule\ gterms{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
102 \isacommand{apply}\isamarkupfalse% |
102 \isacommand{apply}\isamarkupfalse% |
103 \ blast\isanewline |
103 \ blast\isanewline |
104 \isacommand{done}\isamarkupfalse% |
104 \isacommand{done}\isamarkupfalse% |
105 % |
105 % |
106 \endisatagproof |
106 \endisatagproof |
122 terms. The proof is a trivial rule induction. |
122 terms. The proof is a trivial rule induction. |
123 First we use the \isa{clarify} method to assume the existence of an element of |
123 First we use the \isa{clarify} method to assume the existence of an element of |
124 \isa{gterms\ F}. (We could have used \isa{intro\ subsetI}.) We then |
124 \isa{gterms\ F}. (We could have used \isa{intro\ subsetI}.) We then |
125 apply rule induction. Here is the resulting subgoal: |
125 apply rule induction. Here is the resulting subgoal: |
126 \begin{isabelle}% |
126 \begin{isabelle}% |
127 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline |
127 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ args\ f{\isaliteral{2E}{\isachardot}}\isanewline |
128 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline |
128 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}F\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ G{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G{\isaliteral{3B}{\isacharsemicolon}}\ f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
129 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G% |
129 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G% |
130 \end{isabelle} |
130 \end{isabelle} |
131 The assumptions state that \isa{f} belongs |
131 The assumptions state that \isa{f} belongs |
132 to~\isa{F}, which is included in~\isa{G}, and that every element of the list \isa{args} is |
132 to~\isa{F}, which is included in~\isa{G}, and that every element of the list \isa{args} is |
133 a ground term over~\isa{G}. The \isa{blast} method finds this chain of reasoning easily.% |
133 a ground term over~\isa{G}. The \isa{blast} method finds this chain of reasoning easily.% |
134 \end{isamarkuptxt}% |
134 \end{isamarkuptxt}% |
160 terms and a function symbol~\isa{f}. If the length of the list matches the |
160 terms and a function symbol~\isa{f}. If the length of the list matches the |
161 function's arity then applying \isa{f} to \isa{args} yields a well-formed |
161 function's arity then applying \isa{f} to \isa{args} yields a well-formed |
162 term.% |
162 term.% |
163 \end{isamarkuptext}% |
163 \end{isamarkuptext}% |
164 \isamarkuptrue% |
164 \isamarkuptrue% |
165 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% |
165 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
166 \isanewline |
166 \isanewline |
167 \ \ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline |
167 \ \ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}f\ gterm\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
168 \ \ \isakeyword{for}\ arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline |
168 \ \ \isakeyword{for}\ arity\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
169 \isakeyword{where}\isanewline |
169 \isakeyword{where}\isanewline |
170 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline |
170 step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{3B}{\isacharsemicolon}}\ \ \isanewline |
171 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline |
171 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
172 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequoteclose}% |
172 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Apply\ f\ args{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{22}{\isachardoublequoteclose}}% |
173 \begin{isamarkuptext}% |
173 \begin{isamarkuptext}% |
174 The inductive definition neatly captures the reasoning above. |
174 The inductive definition neatly captures the reasoning above. |
175 The universal quantification over the |
175 The universal quantification over the |
176 \isa{set} of arguments expresses that all of them are well-formed.% |
176 \isa{set} of arguments expresses that all of them are well-formed.% |
177 \index{quantifiers!and inductive definitions|)}% |
177 \index{quantifiers!and inductive definitions|)}% |
198 introduction rule. The first premise states that \isa{args} belongs to |
198 introduction rule. The first premise states that \isa{args} belongs to |
199 the \isa{lists} of well-formed terms. This formulation is more |
199 the \isa{lists} of well-formed terms. This formulation is more |
200 direct, if more obscure, than using a universal quantifier.% |
200 direct, if more obscure, than using a universal quantifier.% |
201 \end{isamarkuptext}% |
201 \end{isamarkuptext}% |
202 \isamarkuptrue% |
202 \isamarkuptrue% |
203 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% |
203 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
204 \isanewline |
204 \isanewline |
205 \ \ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline |
205 \ \ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}f\ gterm\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
206 \ \ \isakeyword{for}\ arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline |
206 \ \ \isakeyword{for}\ arity\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
207 \isakeyword{where}\isanewline |
207 \isakeyword{where}\isanewline |
208 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline |
208 step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \isanewline |
209 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline |
209 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
210 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequoteclose}\isanewline |
210 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Apply\ f\ args{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
211 \isakeyword{monos}\ lists{\isacharunderscore}mono% |
211 \isakeyword{monos}\ lists{\isaliteral{5F}{\isacharunderscore}}mono% |
212 \begin{isamarkuptext}% |
212 \begin{isamarkuptext}% |
213 We cite the theorem \isa{lists{\isacharunderscore}mono} to justify |
213 We cite the theorem \isa{lists{\isaliteral{5F}{\isacharunderscore}}mono} to justify |
214 using the function \isa{lists}.% |
214 using the function \isa{lists}.% |
215 \footnote{This particular theorem is installed by default already, but we |
215 \footnote{This particular theorem is installed by default already, but we |
216 include the \isakeyword{monos} declaration in order to illustrate its syntax.} |
216 include the \isakeyword{monos} declaration in order to illustrate its syntax.} |
217 \begin{isabelle}% |
217 \begin{isabelle}% |
218 A\ {\isasymsubseteq}\ B\ {\isasymLongrightarrow}\ lists\ A\ {\isasymsubseteq}\ lists\ B\rulename{lists{\isacharunderscore}mono}% |
218 A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lists\ A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ lists\ B\rulename{lists{\isaliteral{5F}{\isacharunderscore}}mono}% |
219 \end{isabelle} |
219 \end{isabelle} |
220 Why must the function be monotone? An inductive definition describes |
220 Why must the function be monotone? An inductive definition describes |
221 an iterative construction: each element of the set is constructed by a |
221 an iterative construction: each element of the set is constructed by a |
222 finite number of introduction rule applications. For example, the |
222 finite number of introduction rule applications. For example, the |
223 elements of \isa{even} are constructed by finitely many applications of |
223 elements of \isa{even} are constructed by finitely many applications of |
224 the rules |
224 the rules |
225 \begin{isabelle}% |
225 \begin{isabelle}% |
226 {\isadigit{0}}\ {\isasymin}\ even\isasep\isanewline% |
226 {\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isasep\isanewline% |
227 n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even% |
227 n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even% |
228 \end{isabelle} |
228 \end{isabelle} |
229 All references to a set in its |
229 All references to a set in its |
230 inductive definition must be positive. Applications of an |
230 inductive definition must be positive. Applications of an |
231 introduction rule cannot invalidate previous applications, allowing the |
231 introduction rule cannot invalidate previous applications, allowing the |
232 construction process to converge. |
232 construction process to converge. |
233 The following pair of rules do not constitute an inductive definition: |
233 The following pair of rules do not constitute an inductive definition: |
234 \begin{trivlist} |
234 \begin{trivlist} |
235 \item \isa{{\isadigit{0}}\ {\isasymin}\ even} |
235 \item \isa{{\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even} |
236 \item \isa{n\ {\isasymnotin}\ even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ even} |
236 \item \isa{n\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even} |
237 \end{trivlist} |
237 \end{trivlist} |
238 Showing that 4 is even using these rules requires showing that 3 is not |
238 Showing that 4 is even using these rules requires showing that 3 is not |
239 even. It is far from trivial to show that this set of rules |
239 even. It is far from trivial to show that this set of rules |
240 characterizes the even numbers. |
240 characterizes the even numbers. |
241 |
241 |
242 Even with its use of the function \isa{lists}, the premise of our |
242 Even with its use of the function \isa{lists}, the premise of our |
243 introduction rule is positive: |
243 introduction rule is positive: |
244 \begin{isabelle}% |
244 \begin{isabelle}% |
245 args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}% |
245 args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{29}{\isacharparenright}}% |
246 \end{isabelle} |
246 \end{isabelle} |
247 To apply the rule we construct a list \isa{args} of previously |
247 To apply the rule we construct a list \isa{args} of previously |
248 constructed well-formed terms. We obtain a |
248 constructed well-formed terms. We obtain a |
249 new term, \isa{Apply\ f\ args}. Because \isa{lists} is monotone, |
249 new term, \isa{Apply\ f\ args}. Because \isa{lists} is monotone, |
250 applications of the rule remain valid as new terms are constructed. |
250 applications of the rule remain valid as new terms are constructed. |
293 % |
293 % |
294 \isatagproof |
294 \isatagproof |
295 % |
295 % |
296 \begin{isamarkuptxt}% |
296 \begin{isamarkuptxt}% |
297 The \isa{clarify} method gives |
297 The \isa{clarify} method gives |
298 us an element of \isa{well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity} on which to perform |
298 us an element of \isa{well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity} on which to perform |
299 induction. The resulting subgoal can be proved automatically: |
299 induction. The resulting subgoal can be proved automatically: |
300 \begin{isabelle}% |
300 \begin{isabelle}% |
301 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline |
301 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ args\ f{\isaliteral{2E}{\isachardot}}\isanewline |
302 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline |
302 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\isanewline |
303 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline |
303 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ \ \ }t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
304 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline |
304 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
305 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% |
305 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity% |
306 \end{isabelle} |
306 \end{isabelle} |
307 This proof resembles the one given in |
307 This proof resembles the one given in |
308 {\S}\ref{sec:gterm-datatype} above, especially in the form of the |
308 {\S}\ref{sec:gterm-datatype} above, especially in the form of the |
309 induction hypothesis. Next, we consider the opposite inclusion:% |
309 induction hypothesis. Next, we consider the opposite inclusion:% |
310 \end{isamarkuptxt}% |
310 \end{isamarkuptxt}% |
347 % |
347 % |
348 \begin{isamarkuptxt}% |
348 \begin{isamarkuptxt}% |
349 The proof script is virtually identical, |
349 The proof script is virtually identical, |
350 but the subgoal after applying induction may be surprising: |
350 but the subgoal after applying induction may be surprising: |
351 \begin{isabelle}% |
351 \begin{isabelle}% |
352 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline |
352 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ args\ f{\isaliteral{2E}{\isachardot}}\isanewline |
353 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline |
353 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}args\isanewline |
354 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline |
354 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}}{\isaliteral{5C3C696E3E}{\isasymin}}\ lists\isanewline |
355 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline |
355 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C696E3E}{\isasymin}}\ \ }{\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\isanewline |
356 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}a{\isachardot}\ a\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline |
356 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C696E3E}{\isasymin}}\ \ {\isaliteral{28}{\isacharparenleft}}}{\isaliteral{7B}{\isacharbraceleft}}a{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
357 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline |
357 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
358 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% |
358 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity% |
359 \end{isabelle} |
359 \end{isabelle} |
360 The induction hypothesis contains an application of \isa{lists}. Using a |
360 The induction hypothesis contains an application of \isa{lists}. Using a |
361 monotone function in the inductive definition always has this effect. The |
361 monotone function in the inductive definition always has this effect. The |
362 subgoal may look uninviting, but fortunately |
362 subgoal may look uninviting, but fortunately |
363 \isa{lists} distributes over intersection: |
363 \isa{lists} distributes over intersection: |
364 \begin{isabelle}% |
364 \begin{isabelle}% |
365 listsp\ {\isacharparenleft}{\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ A{\isacharparenright}\ {\isasyminter}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ B{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ lists\ A{\isacharparenright}\ {\isasyminter}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ lists\ B{\isacharparenright}\rulename{lists{\isacharunderscore}Int{\isacharunderscore}eq}% |
365 listsp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ B{\isaliteral{29}{\isacharparenright}}\rulename{lists{\isaliteral{5F}{\isacharunderscore}}Int{\isaliteral{5F}{\isacharunderscore}}eq}% |
366 \end{isabelle} |
366 \end{isabelle} |
367 Thanks to this default simplification rule, the induction hypothesis |
367 Thanks to this default simplification rule, the induction hypothesis |
368 is quickly replaced by its two parts: |
368 is quickly replaced by its two parts: |
369 \begin{trivlist} |
369 \begin{trivlist} |
370 \item \isa{args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}} |
370 \item \isa{args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{29}{\isacharparenright}}} |
371 \item \isa{args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharparenright}} |
371 \item \isa{args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{29}{\isacharparenright}}} |
372 \end{trivlist} |
372 \end{trivlist} |
373 Invoking the rule \isa{well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}step} completes the proof. The |
373 Invoking the rule \isa{well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{2E}{\isachardot}}step} completes the proof. The |
374 call to \isa{auto} does all this work. |
374 call to \isa{auto} does all this work. |
375 |
375 |
376 This example is typical of how monotone functions |
376 This example is typical of how monotone functions |
377 \index{monotone functions} can be used. In particular, many of them |
377 \index{monotone functions} can be used. In particular, many of them |
378 distribute over intersection. Monotonicity implies one direction of |
378 distribute over intersection. Monotonicity implies one direction of |
379 this set equality; we have this theorem: |
379 this set equality; we have this theorem: |
380 \begin{isabelle}% |
380 \begin{isabelle}% |
381 mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B\rulename{mono{\isacharunderscore}Int}% |
381 mono\ f\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ f\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ f\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ f\ B\rulename{mono{\isaliteral{5F}{\isacharunderscore}}Int}% |
382 \end{isabelle}% |
382 \end{isabelle}% |
383 \end{isamarkuptxt}% |
383 \end{isamarkuptxt}% |
384 \isamarkuptrue% |
384 \isamarkuptrue% |
385 % |
385 % |
386 \endisatagproof |
386 \endisatagproof |
395 \isamarkuptrue% |
395 \isamarkuptrue% |
396 % |
396 % |
397 \begin{isamarkuptext}% |
397 \begin{isamarkuptext}% |
398 \index{rule inversion|(}% |
398 \index{rule inversion|(}% |
399 Does \isa{gterms} distribute over intersection? We have proved that this |
399 Does \isa{gterms} distribute over intersection? We have proved that this |
400 function is monotone, so \isa{mono{\isacharunderscore}Int} gives one of the inclusions. The |
400 function is monotone, so \isa{mono{\isaliteral{5F}{\isacharunderscore}}Int} gives one of the inclusions. The |
401 opposite inclusion asserts that if \isa{t} is a ground term over both of the |
401 opposite inclusion asserts that if \isa{t} is a ground term over both of the |
402 sets |
402 sets |
403 \isa{F} and~\isa{G} then it is also a ground term over their intersection, |
403 \isa{F} and~\isa{G} then it is also a ground term over their intersection, |
404 \isa{F\ {\isasyminter}\ G}.% |
404 \isa{F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G}.% |
405 \end{isamarkuptext}% |
405 \end{isamarkuptext}% |
406 \isamarkuptrue% |
406 \isamarkuptrue% |
407 \isacommand{lemma}\isamarkupfalse% |
407 \isacommand{lemma}\isamarkupfalse% |
408 \ gterms{\isacharunderscore}IntI{\isacharcolon}\isanewline |
408 \ gterms{\isaliteral{5F}{\isacharunderscore}}IntI{\isaliteral{3A}{\isacharcolon}}\isanewline |
409 \ \ \ \ \ {\isachardoublequoteopen}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequoteclose}% |
409 \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F{\isaliteral{5C3C696E7465723E}{\isasyminter}}G{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
410 \isadelimproof |
410 \isadelimproof |
411 % |
411 % |
412 \endisadelimproof |
412 \endisadelimproof |
413 % |
413 % |
414 \isatagproof |
414 \isatagproof |
420 % |
420 % |
421 \endisadelimproof |
421 \endisadelimproof |
422 % |
422 % |
423 \begin{isamarkuptext}% |
423 \begin{isamarkuptext}% |
424 Attempting this proof, we get the assumption |
424 Attempting this proof, we get the assumption |
425 \isa{Apply\ f\ args\ {\isasymin}\ gterms\ G}, which cannot be broken down. |
425 \isa{Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G}, which cannot be broken down. |
426 It looks like a job for rule inversion:\cmmdx{inductive\protect\_cases}% |
426 It looks like a job for rule inversion:\cmmdx{inductive\protect\_cases}% |
427 \end{isamarkuptext}% |
427 \end{isamarkuptext}% |
428 \isamarkuptrue% |
428 \isamarkuptrue% |
429 \isacommand{inductive{\isacharunderscore}cases}\isamarkupfalse% |
429 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}\isamarkupfalse% |
430 \ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequoteclose}% |
430 \ gterm{\isaliteral{5F}{\isacharunderscore}}Apply{\isaliteral{5F}{\isacharunderscore}}elim\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{22}{\isachardoublequoteclose}}% |
431 \begin{isamarkuptext}% |
431 \begin{isamarkuptext}% |
432 Here is the result. |
432 Here is the result. |
433 \begin{isabelle}% |
433 \begin{isabelle}% |
434 {\isasymlbrakk}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isacharsemicolon}\isanewline |
434 {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
435 \isaindent{\ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\isanewline |
435 \isaindent{\ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{3B}{\isacharsemicolon}}\ f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
436 {\isasymLongrightarrow}\ P\rulename{gterm{\isacharunderscore}Apply{\isacharunderscore}elim}% |
436 {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\rulename{gterm{\isaliteral{5F}{\isacharunderscore}}Apply{\isaliteral{5F}{\isacharunderscore}}elim}% |
437 \end{isabelle} |
437 \end{isabelle} |
438 This rule replaces an assumption about \isa{Apply\ f\ args} by |
438 This rule replaces an assumption about \isa{Apply\ f\ args} by |
439 assumptions about \isa{f} and~\isa{args}. |
439 assumptions about \isa{f} and~\isa{args}. |
440 No cases are discarded (there was only one to begin |
440 No cases are discarded (there was only one to begin |
441 with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}. |
441 with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}. |
442 It can be applied repeatedly as an elimination rule without looping, so we |
442 It can be applied repeatedly as an elimination rule without looping, so we |
443 have given the \isa{elim{\isacharbang}} attribute. |
443 have given the \isa{elim{\isaliteral{21}{\isacharbang}}} attribute. |
444 |
444 |
445 Now we can prove the other half of that distributive law.% |
445 Now we can prove the other half of that distributive law.% |
446 \end{isamarkuptext}% |
446 \end{isamarkuptext}% |
447 \isamarkuptrue% |
447 \isamarkuptrue% |
448 \isacommand{lemma}\isamarkupfalse% |
448 \isacommand{lemma}\isamarkupfalse% |
449 \ gterms{\isacharunderscore}IntI\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline |
449 \ gterms{\isaliteral{5F}{\isacharunderscore}}IntI\ {\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{2C}{\isacharcomma}}\ intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
450 \ \ \ \ \ {\isachardoublequoteopen}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequoteclose}\isanewline |
450 \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F{\isaliteral{5C3C696E7465723E}{\isasyminter}}G{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
451 % |
451 % |
452 \isadelimproof |
452 \isadelimproof |
453 % |
453 % |
454 \endisadelimproof |
454 \endisadelimproof |
455 % |
455 % |
456 \isatagproof |
456 \isatagproof |
457 \isacommand{apply}\isamarkupfalse% |
457 \isacommand{apply}\isamarkupfalse% |
458 \ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isanewline |
458 \ {\isaliteral{28}{\isacharparenleft}}erule\ gterms{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
459 \isacommand{apply}\isamarkupfalse% |
459 \isacommand{apply}\isamarkupfalse% |
460 \ blast\isanewline |
460 \ blast\isanewline |
461 \isacommand{done}\isamarkupfalse% |
461 \isacommand{done}\isamarkupfalse% |
462 % |
462 % |
463 \endisatagproof |
463 \endisatagproof |
475 % |
475 % |
476 \begin{isamarkuptxt}% |
476 \begin{isamarkuptxt}% |
477 The proof begins with rule induction over the definition of |
477 The proof begins with rule induction over the definition of |
478 \isa{gterms}, which leaves a single subgoal: |
478 \isa{gterms}, which leaves a single subgoal: |
479 \begin{isabelle}% |
479 \begin{isabelle}% |
480 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline |
480 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}args\ f{\isaliteral{2E}{\isachardot}}\isanewline |
481 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline |
481 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\isanewline |
482 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
482 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ \ \ }t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
483 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline |
483 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
484 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline |
484 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline |
485 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}% |
485 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}% |
486 \end{isabelle} |
486 \end{isabelle} |
487 To prove this, we assume \isa{Apply\ f\ args\ {\isasymin}\ gterms\ G}. Rule inversion, |
487 To prove this, we assume \isa{Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G}. Rule inversion, |
488 in the form of \isa{gterm{\isacharunderscore}Apply{\isacharunderscore}elim}, infers |
488 in the form of \isa{gterm{\isaliteral{5F}{\isacharunderscore}}Apply{\isaliteral{5F}{\isacharunderscore}}elim}, infers |
489 that every element of \isa{args} belongs to |
489 that every element of \isa{args} belongs to |
490 \isa{gterms\ G}; hence (by the induction hypothesis) it belongs |
490 \isa{gterms\ G}; hence (by the induction hypothesis) it belongs |
491 to \isa{gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}}. Rule inversion also yields |
491 to \isa{gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}}. Rule inversion also yields |
492 \isa{f\ {\isasymin}\ G} and hence \isa{f\ {\isasymin}\ F\ {\isasyminter}\ G}. |
492 \isa{f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ G} and hence \isa{f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G}. |
493 All of this reasoning is done by \isa{blast}. |
493 All of this reasoning is done by \isa{blast}. |
494 |
494 |
495 \smallskip |
495 \smallskip |
496 Our distributive law is a trivial consequence of previously-proved results:% |
496 Our distributive law is a trivial consequence of previously-proved results:% |
497 \end{isamarkuptxt}% |
497 \end{isamarkuptxt}% |