src/HOL/Library/Quotient_Option.thy
changeset 51956 a4d81cdebf8b
parent 51377 7da251a6c16e
child 51994 82cc2aeb7d13
--- a/src/HOL/Library/Quotient_Option.thy	Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Mon May 13 13:59:04 2013 +0200
@@ -24,6 +24,16 @@
     | _ \<Rightarrow> False)"
   by (cases x) (cases y, simp_all)+
 
+fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
+where
+  "option_pred R None = True"
+| "option_pred R (Some x) = R x"
+
+lemma option_pred_unfold:
+  "option_pred P x = (case x of None \<Rightarrow> True
+    | Some x \<Rightarrow> P x)"
+by (cases x) simp_all
+
 lemma option_rel_map1:
   "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
   by (simp add: option_rel_unfold split: option.split)
@@ -55,6 +65,12 @@
   "(option_rel A) OO (option_rel B) = option_rel (A OO B)"
 by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split)
 
+lemma Domainp_option[relator_domain]:
+  assumes "Domainp A = P"
+  shows "Domainp (option_rel A) = (option_pred P)"
+using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def]
+by (auto iff: fun_eq_iff split: option.split)
+
 lemma option_reflp[reflexivity_rule]:
   "reflp R \<Longrightarrow> reflp (option_rel R)"
   unfolding reflp_def split_option_all by simp
@@ -123,11 +139,6 @@
   using assms unfolding Quotient_alt_def option_rel_unfold
   by (simp split: option.split)
 
-fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
-where
-  "option_pred R None = True"
-| "option_pred R (Some x) = R x"
-
 lemma option_invariant_commute [invariant_commute]:
   "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)"
   apply (simp add: fun_eq_iff Lifting.invariant_def)