equal
deleted
inserted
replaced
44 by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) |
44 by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) |
45 |
45 |
46 lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))" |
46 lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))" |
47 by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) |
47 by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) |
48 |
48 |
49 lemma sum_reflp: |
49 lemma sum_reflp[reflp_preserve]: |
50 "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)" |
50 "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)" |
51 unfolding reflp_def split_sum_all sum_rel.simps by fast |
51 unfolding reflp_def split_sum_all sum_rel.simps by fast |
52 |
52 |
53 lemma sum_symp: |
53 lemma sum_symp: |
54 "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)" |
54 "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)" |