49 some of the other automatic tactics are more sensitive, and even \isa{blast} can be lead astray in the presence of large numbers of rules. |
49 some of the other automatic tactics are more sensitive, and even \isa{blast} can be lead astray in the presence of large numbers of rules. |
50 |
50 |
51 To prove transitivity, we need rule induction, i.e.\ theorem |
51 To prove transitivity, we need rule induction, i.e.\ theorem |
52 \isa{rtc{\isachardot}induct}: |
52 \isa{rtc{\isachardot}induct}: |
53 \begin{isabelle}% |
53 \begin{isabelle}% |
54 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline |
54 \ \ \ \ \ {\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}\ {\isasymLongrightarrow}\isanewline |
55 \ \ \ \ \ \ \ \ {\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isacharquery}P\ y\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isasymrbrakk}\isanewline |
55 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharparenright}\ {\isasymLongrightarrow}\isanewline |
56 \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa% |
56 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}x\ y\ z{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ y\ z\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa% |
57 \end{isabelle} |
57 \end{isabelle} |
58 It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}xb{\isacharcomma}{\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition, |
58 It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}xb{\isacharcomma}{\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition, |
59 i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the |
59 i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the |
60 premises. In general, rule induction for an $n$-ary inductive relation $R$ |
60 premises. In general, rule induction for an $n$-ary inductive relation $R$ |
61 expects a premise of the form $(x@1,\dots,x@n) \in R$. |
61 expects a premise of the form $(x@1,\dots,x@n) \in R$. |
108 \noindent |
108 \noindent |
109 Now induction produces two subgoals which are both proved automatically: |
109 Now induction produces two subgoals which are both proved automatically: |
110 \begin{isabelle}% |
110 \begin{isabelle}% |
111 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline |
111 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline |
112 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline |
112 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline |
113 \ \ \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isasymrbrakk}\isanewline |
113 \ \ \ \ \ \ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\isanewline |
114 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% |
114 \ \ \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\isanewline |
|
115 \ \ \ \ \ \ \ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% |
115 \end{isabelle}% |
116 \end{isabelle}% |
116 \end{isamarkuptxt}% |
117 \end{isamarkuptxt}% |
117 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
118 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline |
118 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline |
119 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline |
119 \isacommand{done}% |
120 \isacommand{done}% |
154 Hence \isa{rtc} is the definition of choice. |
155 Hence \isa{rtc} is the definition of choice. |
155 |
156 |
156 \begin{exercise}\label{ex:converse-rtc-step} |
157 \begin{exercise}\label{ex:converse-rtc-step} |
157 Show that the converse of \isa{rtc{\isacharunderscore}step} also holds: |
158 Show that the converse of \isa{rtc{\isacharunderscore}step} also holds: |
158 \begin{isabelle}% |
159 \begin{isabelle}% |
159 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% |
160 \ \ \ \ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% |
160 \end{isabelle} |
161 \end{isabelle} |
161 \end{exercise} |
162 \end{exercise} |
162 \begin{exercise} |
163 \begin{exercise} |
163 Repeat the development of this section, but starting with a definition of |
164 Repeat the development of this section, but starting with a definition of |
164 \isa{rtc} where \isa{rtc{\isacharunderscore}step} is replaced by its converse as shown |
165 \isa{rtc} where \isa{rtc{\isacharunderscore}step} is replaced by its converse as shown |