equal
deleted
inserted
replaced
61 |
61 |
62 To prove transitivity, we need rule induction, i.e.\ theorem |
62 To prove transitivity, we need rule induction, i.e.\ theorem |
63 \isa{rtc{\isachardot}induct}: |
63 \isa{rtc{\isachardot}induct}: |
64 \begin{isabelle}% |
64 \begin{isabelle}% |
65 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline |
65 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline |
66 \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 |
66 \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 |
67 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa% |
67 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa% |
68 \end{isabelle} |
68 \end{isabelle} |
69 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, |
69 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, |
70 i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the |
70 i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the |
71 premises. In general, rule induction for an $n$-ary inductive relation $R$ |
71 premises. In general, rule induction for an $n$-ary inductive relation $R$ |