equal
deleted
inserted
replaced
1 (*<*)theory Star = Main:(*>*) |
1 (*<*)theory Star = Main:(*>*) |
2 |
2 |
3 section{*The reflexive transitive closure*} |
3 section{*The reflexive transitive closure*} |
4 |
4 |
5 text{*\label{sec:rtc} |
5 text{*\label{sec:rtc} |
|
6 |
6 {\bf Say something about inductive relations as opposed to sets? Or has that |
7 {\bf Say something about inductive relations as opposed to sets? Or has that |
7 been said already? If not, explain induction!} |
8 been said already? If not, explain induction!} |
8 |
9 |
9 A perfect example of an inductive definition is the reflexive transitive |
10 A perfect example of an inductive definition is the reflexive transitive |
10 closure of a relation. This concept was already introduced in |
11 closure of a relation. This concept was already introduced in |
22 |
23 |
23 text{*\noindent |
24 text{*\noindent |
24 The function @{term rtc} is annotated with concrete syntax: instead of |
25 The function @{term rtc} is annotated with concrete syntax: instead of |
25 @{text"rtc r"} we can read and write {term"r*"}. The actual definition |
26 @{text"rtc r"} we can read and write {term"r*"}. The actual definition |
26 consists of two rules. Reflexivity is obvious and is immediately declared an |
27 consists of two rules. Reflexivity is obvious and is immediately declared an |
27 equivalence rule. Thus the automatic tools will apply it automatically. The |
28 equivalence. Thus the automatic tools will apply it automatically. The second |
28 second rule, @{thm[source]rtc_step}, says that we can always add one more |
29 rule, @{thm[source]rtc_step}, says that we can always add one more @{term |
29 @{term r}-step to the left. Although we could make @{thm[source]rtc_step} an |
30 r}-step to the left. Although we could make @{thm[source]rtc_step} an |
30 introduction rule, this is dangerous: the recursion slows down and may |
31 introduction rule, this is dangerous: the recursion slows down and may |
31 even kill the automatic tactics. |
32 even kill the automatic tactics. |
32 |
33 |
33 The above definition of the concept of reflexive transitive closure may |
34 The above definition of the concept of reflexive transitive closure may |
34 be sufficiently intuitive but it is certainly not the only possible one: |
35 be sufficiently intuitive but it is certainly not the only possible one: |