equal
deleted
inserted
replaced
21 acc :: "('a \<times> 'a) set => 'a set" |
21 acc :: "('a \<times> 'a) set => 'a set" |
22 inductive "acc r" |
22 inductive "acc r" |
23 intros |
23 intros |
24 accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r" |
24 accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r" |
25 |
25 |
26 syntax |
26 abbreviation (output) |
27 termi :: "('a \<times> 'a) set => 'a set" |
27 termi :: "('a \<times> 'a) set => 'a set" |
28 translations |
28 "termi r == acc (r\<inverse>)" |
29 "termi r" == "acc (r\<inverse>)" |
|
30 |
29 |
31 |
30 |
32 subsection {* Induction rules *} |
31 subsection {* Induction rules *} |
33 |
32 |
34 theorem acc_induct: |
33 theorem acc_induct: |