equal
deleted
inserted
replaced
43 lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))" |
43 lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))" |
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 |
|
49 lemma option_rel_mono[relator_mono]: |
|
50 assumes "A \<le> B" |
|
51 shows "(option_rel A) \<le> (option_rel B)" |
|
52 using assms by (auto simp: option_rel_unfold split: option.splits) |
|
53 |
|
54 lemma option_rel_OO[relator_distr]: |
|
55 "(option_rel A) OO (option_rel B) = option_rel (A OO B)" |
|
56 by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split) |
48 |
57 |
49 lemma option_reflp[reflexivity_rule]: |
58 lemma option_reflp[reflexivity_rule]: |
50 "reflp R \<Longrightarrow> reflp (option_rel R)" |
59 "reflp R \<Longrightarrow> reflp (option_rel R)" |
51 unfolding reflp_def split_option_all by simp |
60 unfolding reflp_def split_option_all by simp |
52 |
61 |