equal
deleted
inserted
replaced
52 blast} can be lead astray in the presence of large numbers of rules. |
52 blast} can be lead astray in the presence of large numbers of rules. |
53 |
53 |
54 To prove transitivity, we need rule induction, i.e.\ theorem |
54 To prove transitivity, we need rule induction, i.e.\ theorem |
55 @{thm[source]rtc.induct}: |
55 @{thm[source]rtc.induct}: |
56 @{thm[display]rtc.induct} |
56 @{thm[display]rtc.induct} |
57 It says that @{text"?P"} holds for an arbitrary pair @{thm_style prem1 rtc.induct} |
57 It says that @{text"?P"} holds for an arbitrary pair @{thm (prem 1) rtc.induct} |
58 if @{text"?P"} is preserved by all rules of the inductive definition, |
58 if @{text"?P"} is preserved by all rules of the inductive definition, |
59 i.e.\ if @{text"?P"} holds for the conclusion provided it holds for the |
59 i.e.\ if @{text"?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$. |
62 |
62 |