equal
deleted
inserted
replaced
49 |
49 |
50 abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999) |
50 abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999) |
51 where "r\<^sup>= \<equiv> r \<union> Id" |
51 where "r\<^sup>= \<equiv> r \<union> Id" |
52 |
52 |
53 abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_\<^sup>=\<^sup>=)" [1000] 1000) |
53 abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_\<^sup>=\<^sup>=)" [1000] 1000) |
54 where "r\<^sup>=\<^sup>= \<equiv> sup r op =" |
54 where "r\<^sup>=\<^sup>= \<equiv> sup r (=)" |
55 |
55 |
56 notation (ASCII) |
56 notation (ASCII) |
57 rtrancl ("(_^*)" [1000] 999) and |
57 rtrancl ("(_^*)" [1000] 999) and |
58 trancl ("(_^+)" [1000] 999) and |
58 trancl ("(_^+)" [1000] 999) and |
59 reflcl ("(_^=)" [1000] 999) and |
59 reflcl ("(_^=)" [1000] 999) and |
77 by blast |
77 by blast |
78 |
78 |
79 |
79 |
80 subsection \<open>Reflexive-transitive closure\<close> |
80 subsection \<open>Reflexive-transitive closure\<close> |
81 |
81 |
82 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)" |
82 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) (=)) = (\<lambda>x y. (x, y) \<in> r \<union> Id)" |
83 by (auto simp add: fun_eq_iff) |
83 by (auto simp add: fun_eq_iff) |
84 |
84 |
85 lemma r_into_rtrancl [intro]: "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>*" |
85 lemma r_into_rtrancl [intro]: "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>*" |
86 \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close> |
86 \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close> |
87 apply (simp only: split_tupled_all) |
87 apply (simp only: split_tupled_all) |
221 apply (case_tac "a = b") |
221 apply (case_tac "a = b") |
222 apply blast |
222 apply blast |
223 apply blast |
223 apply blast |
224 done |
224 done |
225 |
225 |
226 lemma rtranclp_r_diff_Id: "(inf r op \<noteq>)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" |
226 lemma rtranclp_r_diff_Id: "(inf r (\<noteq>))\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" |
227 apply (rule sym) |
227 apply (rule sym) |
228 apply (rule rtranclp_subset) |
228 apply (rule rtranclp_subset) |
229 apply blast+ |
229 apply blast+ |
230 done |
230 done |
231 |
231 |