equal
deleted
inserted
replaced
74 unfolding trans_def by blast |
74 unfolding trans_def by blast |
75 |
75 |
76 |
76 |
77 subsection {* Reflexive-transitive closure *} |
77 subsection {* Reflexive-transitive closure *} |
78 |
78 |
79 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r Un Id)" |
79 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)" |
80 by (simp add: expand_fun_eq sup2_iff) |
80 by (simp add: mem_def pair_in_Id_conv [simplified mem_def] sup_fun_eq sup_bool_eq) |
81 |
81 |
82 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*" |
82 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*" |
83 -- {* @{text rtrancl} of @{text r} contains @{text r} *} |
83 -- {* @{text rtrancl} of @{text r} contains @{text r} *} |
84 apply (simp only: split_tupled_all) |
84 apply (simp only: split_tupled_all) |
85 apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) |
85 apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) |