equal
deleted
inserted
replaced
44 by (metis option.exhaust) (* TODO: move to Option.thy *) |
44 by (metis option.exhaust) (* TODO: move to Option.thy *) |
45 |
45 |
46 lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))" |
46 lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))" |
47 by (metis option.exhaust) (* TODO: move to Option.thy *) |
47 by (metis option.exhaust) (* TODO: move to Option.thy *) |
48 |
48 |
49 lemma option_reflp: |
49 lemma option_reflp[reflp_preserve]: |
50 "reflp R \<Longrightarrow> reflp (option_rel R)" |
50 "reflp R \<Longrightarrow> reflp (option_rel R)" |
51 unfolding reflp_def split_option_all by simp |
51 unfolding reflp_def split_option_all by simp |
52 |
52 |
53 lemma option_symp: |
53 lemma option_symp: |
54 "symp R \<Longrightarrow> symp (option_rel R)" |
54 "symp R \<Longrightarrow> symp (option_rel R)" |