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[reflp_preserve]: |
49 lemma option_reflp[reflexivity_rule]: |
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 |
|
53 lemma option_left_total[reflexivity_rule]: |
|
54 "left_total R \<Longrightarrow> left_total (option_rel R)" |
|
55 apply (intro left_totalI) |
|
56 unfolding split_option_ex |
|
57 by (case_tac x) (auto elim: left_totalE) |
52 |
58 |
53 lemma option_symp: |
59 lemma option_symp: |
54 "symp R \<Longrightarrow> symp (option_rel R)" |
60 "symp R \<Longrightarrow> symp (option_rel R)" |
55 unfolding symp_def split_option_all option_rel.simps by fast |
61 unfolding symp_def split_option_all option_rel.simps by fast |
56 |
62 |