35 intros |
35 intros |
36 r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+" |
36 r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+" |
37 trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+" |
37 trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+" |
38 |
38 |
39 abbreviation |
39 abbreviation |
40 reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999) |
40 reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999) where |
41 "r^= == r \<union> Id" |
41 "r^= == r \<union> Id" |
42 |
42 |
43 notation (xsymbols) |
43 notation (xsymbols) |
44 rtrancl ("(_\<^sup>*)" [1000] 999) |
44 rtrancl ("(_\<^sup>*)" [1000] 999) and |
45 trancl ("(_\<^sup>+)" [1000] 999) |
45 trancl ("(_\<^sup>+)" [1000] 999) and |
46 reflcl ("(_\<^sup>=)" [1000] 999) |
46 reflcl ("(_\<^sup>=)" [1000] 999) |
47 |
47 |
48 notation (HTML output) |
48 notation (HTML output) |
49 rtrancl ("(_\<^sup>*)" [1000] 999) |
49 rtrancl ("(_\<^sup>*)" [1000] 999) and |
50 trancl ("(_\<^sup>+)" [1000] 999) |
50 trancl ("(_\<^sup>+)" [1000] 999) and |
51 reflcl ("(_\<^sup>=)" [1000] 999) |
51 reflcl ("(_\<^sup>=)" [1000] 999) |
52 |
52 |
53 |
53 |
54 subsection {* Reflexive-transitive closure *} |
54 subsection {* Reflexive-transitive closure *} |
55 |
55 |