equal
deleted
inserted
replaced
23 |
23 |
24 definition trancl :: "i set \<Rightarrow> i set" ("(_^+)" [100] 100) |
24 definition trancl :: "i set \<Rightarrow> i set" ("(_^+)" [100] 100) |
25 where "r^+ == r O rtrancl(r)" |
25 where "r^+ == r O rtrancl(r)" |
26 |
26 |
27 |
27 |
28 subsection \<open>Natural deduction for @{text "trans(r)"}\<close> |
28 subsection \<open>Natural deduction for \<open>trans(r)\<close>\<close> |
29 |
29 |
30 lemma transI: "(\<And>x y z. \<lbrakk><x,y>:r; <y,z>:r\<rbrakk> \<Longrightarrow> <x,z>:r) \<Longrightarrow> trans(r)" |
30 lemma transI: "(\<And>x y z. \<lbrakk><x,y>:r; <y,z>:r\<rbrakk> \<Longrightarrow> <x,z>:r) \<Longrightarrow> trans(r)" |
31 unfolding trans_def by blast |
31 unfolding trans_def by blast |
32 |
32 |
33 lemma transD: "\<lbrakk>trans(r); <a,b>:r; <b,c>:r\<rbrakk> \<Longrightarrow> <a,c>:r" |
33 lemma transD: "\<lbrakk>trans(r); <a,b>:r; <b,c>:r\<rbrakk> \<Longrightarrow> <a,c>:r" |