25 An inductive definition may accept parameters, so it can express |
25 An inductive definition may accept parameters, so it can express |
26 functions that yield sets. |
26 functions that yield sets. |
27 Relations too can be defined inductively, since they are just sets of pairs. |
27 Relations too can be defined inductively, since they are just sets of pairs. |
28 A perfect example is the function that maps a relation to its |
28 A perfect example is the function that maps a relation to its |
29 reflexive transitive closure. This concept was already |
29 reflexive transitive closure. This concept was already |
30 introduced in \S\ref{sec:Relations}, where the operator \isa{\isactrlsup {\isacharasterisk}} was |
30 introduced in \S\ref{sec:Relations}, where the operator \isa{\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} was |
31 defined as a least fixed point because inductive definitions were not yet |
31 defined as a least fixed point because inductive definitions were not yet |
32 available. But now they are:% |
32 available. But now they are:% |
33 \end{isamarkuptext}% |
33 \end{isamarkuptext}% |
34 \isamarkuptrue% |
34 \isamarkuptrue% |
35 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% |
35 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
36 \isanewline |
36 \isanewline |
37 \ \ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
37 \ \ rtc\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{29}{\isacharparenright}}\isanewline |
38 \ \ \isakeyword{for}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline |
38 \ \ \isakeyword{for}\ r\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
39 \isakeyword{where}\isanewline |
39 \isakeyword{where}\isanewline |
40 \ \ rtc{\isacharunderscore}refl{\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline |
40 \ \ rtc{\isaliteral{5F}{\isacharunderscore}}refl{\isaliteral{5B}{\isacharbrackleft}}iff{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
41 {\isacharbar}\ rtc{\isacharunderscore}step{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}% |
41 {\isaliteral{7C}{\isacharbar}}\ rtc{\isaliteral{5F}{\isacharunderscore}}step{\isaliteral{3A}{\isacharcolon}}\ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}% |
42 \begin{isamarkuptext}% |
42 \begin{isamarkuptext}% |
43 \noindent |
43 \noindent |
44 The function \isa{rtc} is annotated with concrete syntax: instead of |
44 The function \isa{rtc} is annotated with concrete syntax: instead of |
45 \isa{rtc\ r} we can write \isa{r{\isacharasterisk}}. The actual definition |
45 \isa{rtc\ r} we can write \isa{r{\isaliteral{2A}{\isacharasterisk}}}. The actual definition |
46 consists of two rules. Reflexivity is obvious and is immediately given the |
46 consists of two rules. Reflexivity is obvious and is immediately given the |
47 \isa{iff} attribute to increase automation. The |
47 \isa{iff} attribute to increase automation. The |
48 second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more |
48 second rule, \isa{rtc{\isaliteral{5F}{\isacharunderscore}}step}, says that we can always add one more |
49 \isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an |
49 \isa{r}-step to the left. Although we could make \isa{rtc{\isaliteral{5F}{\isacharunderscore}}step} an |
50 introduction rule, this is dangerous: the recursion in the second premise |
50 introduction rule, this is dangerous: the recursion in the second premise |
51 slows down and may even kill the automatic tactics. |
51 slows down and may even kill the automatic tactics. |
52 |
52 |
53 The above definition of the concept of reflexive transitive closure may |
53 The above definition of the concept of reflexive transitive closure may |
54 be sufficiently intuitive but it is certainly not the only possible one: |
54 be sufficiently intuitive but it is certainly not the only possible one: |
76 % |
76 % |
77 \begin{isamarkuptext}% |
77 \begin{isamarkuptext}% |
78 \noindent |
78 \noindent |
79 Although the lemma itself is an unremarkable consequence of the basic rules, |
79 Although the lemma itself is an unremarkable consequence of the basic rules, |
80 it has the advantage that it can be declared an introduction rule without the |
80 it has the advantage that it can be declared an introduction rule without the |
81 danger of killing the automatic tactics because \isa{r{\isacharasterisk}} occurs only in |
81 danger of killing the automatic tactics because \isa{r{\isaliteral{2A}{\isacharasterisk}}} occurs only in |
82 the conclusion and not in the premise. Thus some proofs that would otherwise |
82 the conclusion and not in the premise. Thus some proofs that would otherwise |
83 need \isa{rtc{\isacharunderscore}step} can now be found automatically. The proof also |
83 need \isa{rtc{\isaliteral{5F}{\isacharunderscore}}step} can now be found automatically. The proof also |
84 shows that \isa{blast} is able to handle \isa{rtc{\isacharunderscore}step}. But |
84 shows that \isa{blast} is able to handle \isa{rtc{\isaliteral{5F}{\isacharunderscore}}step}. But |
85 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. |
85 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. |
86 |
86 |
87 To prove transitivity, we need rule induction, i.e.\ theorem |
87 To prove transitivity, we need rule induction, i.e.\ theorem |
88 \isa{rtc{\isachardot}induct}: |
88 \isa{rtc{\isaliteral{2E}{\isachardot}}induct}: |
89 \begin{isabelle}% |
89 \begin{isabelle}% |
90 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline |
90 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}x{\isadigit{1}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}x{\isadigit{2}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
91 \isaindent{\ \ \ \ \ \ }{\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 |
91 \isaindent{\ \ \ \ \ \ }{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}r{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}P\ y\ z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
92 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}% |
92 \isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3F}{\isacharquery}}x{\isadigit{1}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}\ {\isaliteral{3F}{\isacharquery}}x{\isadigit{2}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}% |
93 \end{isabelle} |
93 \end{isabelle} |
94 It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} |
94 It says that \isa{{\isaliteral{3F}{\isacharquery}}P} holds for an arbitrary pair \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}x{\isadigit{1}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}x{\isadigit{2}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}r{\isaliteral{2A}{\isacharasterisk}}} |
95 if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition, |
95 if \isa{{\isaliteral{3F}{\isacharquery}}P} is preserved by all rules of the inductive definition, |
96 i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the |
96 i.e.\ if \isa{{\isaliteral{3F}{\isacharquery}}P} holds for the conclusion provided it holds for the |
97 premises. In general, rule induction for an $n$-ary inductive relation $R$ |
97 premises. In general, rule induction for an $n$-ary inductive relation $R$ |
98 expects a premise of the form $(x@1,\dots,x@n) \in R$. |
98 expects a premise of the form $(x@1,\dots,x@n) \in R$. |
99 |
99 |
100 Now we turn to the inductive proof of transitivity:% |
100 Now we turn to the inductive proof of transitivity:% |
101 \end{isamarkuptext}% |
101 \end{isamarkuptext}% |
102 \isamarkuptrue% |
102 \isamarkuptrue% |
103 \isacommand{lemma}\isamarkupfalse% |
103 \isacommand{lemma}\isamarkupfalse% |
104 \ rtc{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline |
104 \ rtc{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
105 % |
105 % |
106 \isadelimproof |
106 \isadelimproof |
107 % |
107 % |
108 \endisadelimproof |
108 \endisadelimproof |
109 % |
109 % |
110 \isatagproof |
110 \isatagproof |
111 \isacommand{apply}\isamarkupfalse% |
111 \isacommand{apply}\isamarkupfalse% |
112 {\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}% |
112 {\isaliteral{28}{\isacharparenleft}}erule\ rtc{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}% |
113 \begin{isamarkuptxt}% |
113 \begin{isamarkuptxt}% |
114 \noindent |
114 \noindent |
115 Unfortunately, even the base case is a problem: |
115 Unfortunately, even the base case is a problem: |
116 \begin{isabelle}% |
116 \begin{isabelle}% |
117 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% |
117 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}% |
118 \end{isabelle} |
118 \end{isabelle} |
119 We have to abandon this proof attempt. |
119 We have to abandon this proof attempt. |
120 To understand what is going on, let us look again at \isa{rtc{\isachardot}induct}. |
120 To understand what is going on, let us look again at \isa{rtc{\isaliteral{2E}{\isachardot}}induct}. |
121 In the above application of \isa{erule}, the first premise of |
121 In the above application of \isa{erule}, the first premise of |
122 \isa{rtc{\isachardot}induct} is unified with the first suitable assumption, which |
122 \isa{rtc{\isaliteral{2E}{\isachardot}}induct} is unified with the first suitable assumption, which |
123 is \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} rather than \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}. Although that |
123 is \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}} rather than \isa{{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}}. Although that |
124 is what we want, it is merely due to the order in which the assumptions occur |
124 is what we want, it is merely due to the order in which the assumptions occur |
125 in the subgoal, which it is not good practice to rely on. As a result, |
125 in the subgoal, which it is not good practice to rely on. As a result, |
126 \isa{{\isacharquery}xb} becomes \isa{x}, \isa{{\isacharquery}xa} becomes |
126 \isa{{\isaliteral{3F}{\isacharquery}}xb} becomes \isa{x}, \isa{{\isaliteral{3F}{\isacharquery}}xa} becomes |
127 \isa{y} and \isa{{\isacharquery}P} becomes \isa{{\isasymlambda}u\ v{\isachardot}\ {\isacharparenleft}u{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus |
127 \isa{y} and \isa{{\isaliteral{3F}{\isacharquery}}P} becomes \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}u\ v{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}u{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}}, thus |
128 yielding the above subgoal. So what went wrong? |
128 yielding the above subgoal. So what went wrong? |
129 |
129 |
130 When looking at the instantiation of \isa{{\isacharquery}P} we see that it does not |
130 When looking at the instantiation of \isa{{\isaliteral{3F}{\isacharquery}}P} we see that it does not |
131 depend on its second parameter at all. The reason is that in our original |
131 depend on its second parameter at all. The reason is that in our original |
132 goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only \isa{x} appears also in the |
132 goal, of the pair \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}} only \isa{x} appears also in the |
133 conclusion, but not \isa{y}. Thus our induction statement is too |
133 conclusion, but not \isa{y}. Thus our induction statement is too |
134 general. Fortunately, it can easily be specialized: |
134 general. Fortunately, it can easily be specialized: |
135 transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:% |
135 transfer the additional premise \isa{{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}} into the conclusion:% |
136 \end{isamarkuptxt}% |
136 \end{isamarkuptxt}% |
137 \isamarkuptrue% |
137 \isamarkuptrue% |
138 % |
138 % |
139 \endisatagproof |
139 \endisatagproof |
140 {\isafoldproof}% |
140 {\isafoldproof}% |
141 % |
141 % |
142 \isadelimproof |
142 \isadelimproof |
143 % |
143 % |
144 \endisadelimproof |
144 \endisadelimproof |
145 \isacommand{lemma}\isamarkupfalse% |
145 \isacommand{lemma}\isamarkupfalse% |
146 \ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline |
146 \ rtc{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
147 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}% |
147 \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}% |
148 \isadelimproof |
148 \isadelimproof |
149 % |
149 % |
150 \endisadelimproof |
150 \endisadelimproof |
151 % |
151 % |
152 \isatagproof |
152 \isatagproof |
158 When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$, |
158 When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$, |
159 pull all other premises containing any of the $x@i$ into the conclusion |
159 pull all other premises containing any of the $x@i$ into the conclusion |
160 using $\longrightarrow$. |
160 using $\longrightarrow$. |
161 \end{quote} |
161 \end{quote} |
162 A similar heuristic for other kinds of inductions is formulated in |
162 A similar heuristic for other kinds of inductions is formulated in |
163 \S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns |
163 \S\ref{sec:ind-var-in-prems}. The \isa{rule{\isaliteral{5F}{\isacharunderscore}}format} directive turns |
164 \isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}: in the end we obtain the original |
164 \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} back into \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}: in the end we obtain the original |
165 statement of our lemma.% |
165 statement of our lemma.% |
166 \end{isamarkuptxt}% |
166 \end{isamarkuptxt}% |
167 \isamarkuptrue% |
167 \isamarkuptrue% |
168 \isacommand{apply}\isamarkupfalse% |
168 \isacommand{apply}\isamarkupfalse% |
169 {\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}% |
169 {\isaliteral{28}{\isacharparenleft}}erule\ rtc{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}% |
170 \begin{isamarkuptxt}% |
170 \begin{isamarkuptxt}% |
171 \noindent |
171 \noindent |
172 Now induction produces two subgoals which are both proved automatically: |
172 Now induction produces two subgoals which are both proved automatically: |
173 \begin{isabelle}% |
173 \begin{isabelle}% |
174 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline |
174 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\isanewline |
175 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline |
175 \ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ za{\isaliteral{2E}{\isachardot}}\isanewline |
176 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\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 |
176 \isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ za{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}za{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
177 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% |
177 \isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}za{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}% |
178 \end{isabelle}% |
178 \end{isabelle}% |
179 \end{isamarkuptxt}% |
179 \end{isamarkuptxt}% |
180 \isamarkuptrue% |
180 \isamarkuptrue% |
181 \ \isacommand{apply}\isamarkupfalse% |
181 \ \isacommand{apply}\isamarkupfalse% |
182 {\isacharparenleft}blast{\isacharparenright}\isanewline |
182 {\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline |
183 \isacommand{apply}\isamarkupfalse% |
183 \isacommand{apply}\isamarkupfalse% |
184 {\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline |
184 {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ rtc{\isaliteral{5F}{\isacharunderscore}}step{\isaliteral{29}{\isacharparenright}}\isanewline |
185 \isacommand{done}\isamarkupfalse% |
185 \isacommand{done}\isamarkupfalse% |
186 % |
186 % |
187 \endisatagproof |
187 \endisatagproof |
188 {\isafoldproof}% |
188 {\isafoldproof}% |
189 % |
189 % |
190 \isadelimproof |
190 \isadelimproof |
191 % |
191 % |
192 \endisadelimproof |
192 \endisadelimproof |
193 % |
193 % |
194 \begin{isamarkuptext}% |
194 \begin{isamarkuptext}% |
195 Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure |
195 Let us now prove that \isa{r{\isaliteral{2A}{\isacharasterisk}}} is really the reflexive transitive closure |
196 of \isa{r}, i.e.\ the least reflexive and transitive |
196 of \isa{r}, i.e.\ the least reflexive and transitive |
197 relation containing \isa{r}. The latter is easily formalized% |
197 relation containing \isa{r}. The latter is easily formalized% |
198 \end{isamarkuptext}% |
198 \end{isamarkuptext}% |
199 \isamarkuptrue% |
199 \isamarkuptrue% |
200 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% |
200 \isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
201 \isanewline |
201 \isanewline |
202 \ \ rtc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline |
202 \ \ rtc{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
203 \ \ \isakeyword{for}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline |
203 \ \ \isakeyword{for}\ r\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
204 \isakeyword{where}\isanewline |
204 \isakeyword{where}\isanewline |
205 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}\isanewline |
205 \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ rtc{\isadigit{2}}\ r{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
206 {\isacharbar}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}\isanewline |
206 {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ rtc{\isadigit{2}}\ r{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
207 {\isacharbar}\ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}% |
207 {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ rtc{\isadigit{2}}\ r{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ rtc{\isadigit{2}}\ r\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ rtc{\isadigit{2}}\ r{\isaliteral{22}{\isachardoublequoteclose}}% |
208 \begin{isamarkuptext}% |
208 \begin{isamarkuptext}% |
209 \noindent |
209 \noindent |
210 and the equivalence of the two definitions is easily shown by the obvious rule |
210 and the equivalence of the two definitions is easily shown by the obvious rule |
211 inductions:% |
211 inductions:% |
212 \end{isamarkuptext}% |
212 \end{isamarkuptext}% |
213 \isamarkuptrue% |
213 \isamarkuptrue% |
214 \isacommand{lemma}\isamarkupfalse% |
214 \isacommand{lemma}\isamarkupfalse% |
215 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline |
215 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ rtc{\isadigit{2}}\ r\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
216 % |
216 % |
217 \isadelimproof |
217 \isadelimproof |
218 % |
218 % |
219 \endisadelimproof |
219 \endisadelimproof |
220 % |
220 % |
221 \isatagproof |
221 \isatagproof |
222 \isacommand{apply}\isamarkupfalse% |
222 \isacommand{apply}\isamarkupfalse% |
223 {\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline |
223 {\isaliteral{28}{\isacharparenleft}}erule\ rtc{\isadigit{2}}{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
224 \ \ \isacommand{apply}\isamarkupfalse% |
224 \ \ \isacommand{apply}\isamarkupfalse% |
225 {\isacharparenleft}blast{\isacharparenright}\isanewline |
225 {\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline |
226 \ \isacommand{apply}\isamarkupfalse% |
226 \ \isacommand{apply}\isamarkupfalse% |
227 {\isacharparenleft}blast{\isacharparenright}\isanewline |
227 {\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline |
228 \isacommand{apply}\isamarkupfalse% |
228 \isacommand{apply}\isamarkupfalse% |
229 {\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline |
229 {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ rtc{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{29}{\isacharparenright}}\isanewline |
230 \isacommand{done}\isamarkupfalse% |
230 \isacommand{done}\isamarkupfalse% |
231 % |
231 % |
232 \endisatagproof |
232 \endisatagproof |
233 {\isafoldproof}% |
233 {\isafoldproof}% |
234 % |
234 % |
261 \endisadelimproof |
261 \endisadelimproof |
262 % |
262 % |
263 \begin{isamarkuptext}% |
263 \begin{isamarkuptext}% |
264 So why did we start with the first definition? Because it is simpler. It |
264 So why did we start with the first definition? Because it is simpler. It |
265 contains only two rules, and the single step rule is simpler than |
265 contains only two rules, and the single step rule is simpler than |
266 transitivity. As a consequence, \isa{rtc{\isachardot}induct} is simpler than |
266 transitivity. As a consequence, \isa{rtc{\isaliteral{2E}{\isachardot}}induct} is simpler than |
267 \isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough |
267 \isa{rtc{\isadigit{2}}{\isaliteral{2E}{\isachardot}}induct}. Since inductive proofs are hard enough |
268 anyway, we should always pick the simplest induction schema available. |
268 anyway, we should always pick the simplest induction schema available. |
269 Hence \isa{rtc} is the definition of choice. |
269 Hence \isa{rtc} is the definition of choice. |
270 \index{reflexive transitive closure!defining inductively|)} |
270 \index{reflexive transitive closure!defining inductively|)} |
271 |
271 |
272 \begin{exercise}\label{ex:converse-rtc-step} |
272 \begin{exercise}\label{ex:converse-rtc-step} |
273 Show that the converse of \isa{rtc{\isacharunderscore}step} also holds: |
273 Show that the converse of \isa{rtc{\isaliteral{5F}{\isacharunderscore}}step} also holds: |
274 \begin{isabelle}% |
274 \begin{isabelle}% |
275 \ \ \ \ \ {\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}% |
275 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}% |
276 \end{isabelle} |
276 \end{isabelle} |
277 \end{exercise} |
277 \end{exercise} |
278 \begin{exercise} |
278 \begin{exercise} |
279 Repeat the development of this section, but starting with a definition of |
279 Repeat the development of this section, but starting with a definition of |
280 \isa{rtc} where \isa{rtc{\isacharunderscore}step} is replaced by its converse as shown |
280 \isa{rtc} where \isa{rtc{\isaliteral{5F}{\isacharunderscore}}step} is replaced by its converse as shown |
281 in exercise~\ref{ex:converse-rtc-step}. |
281 in exercise~\ref{ex:converse-rtc-step}. |
282 \end{exercise}% |
282 \end{exercise}% |
283 \end{isamarkuptext}% |
283 \end{isamarkuptext}% |
284 \isamarkuptrue% |
284 \isamarkuptrue% |
285 % |
285 % |