equal
deleted
inserted
replaced
32 done |
32 done |
33 |
33 |
34 lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)" |
34 lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)" |
35 unfolding set_rel_def fun_eq_iff by auto |
35 unfolding set_rel_def fun_eq_iff by auto |
36 |
36 |
37 lemma reflp_set_rel[reflp_preserve]: "reflp R \<Longrightarrow> reflp (set_rel R)" |
37 lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)" |
38 unfolding reflp_def set_rel_def by fast |
38 unfolding reflp_def set_rel_def by fast |
|
39 |
|
40 lemma left_total_set_rel[reflexivity_rule]: |
|
41 assumes lt_R: "left_total R" |
|
42 shows "left_total (set_rel R)" |
|
43 proof - |
|
44 { |
|
45 fix A |
|
46 let ?B = "{y. \<exists>x \<in> A. R x y}" |
|
47 have "(\<forall>x\<in>A. \<exists>y\<in>?B. R x y) \<and> (\<forall>y\<in>?B. \<exists>x\<in>A. R x y)" using lt_R by(elim left_totalE) blast |
|
48 } |
|
49 then have "\<And>A. \<exists>B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y)" by blast |
|
50 then show ?thesis by (auto simp: set_rel_def intro: left_totalI) |
|
51 qed |
39 |
52 |
40 lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)" |
53 lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)" |
41 unfolding symp_def set_rel_def by fast |
54 unfolding symp_def set_rel_def by fast |
42 |
55 |
43 lemma transp_set_rel: "transp R \<Longrightarrow> transp (set_rel R)" |
56 lemma transp_set_rel: "transp R \<Longrightarrow> transp (set_rel R)" |