src/HOL/Library/Quotient_Option.thy
changeset 47634 091bcd569441
parent 47624 16d433895d2e
child 47635 ebb79474262c
--- a/src/HOL/Library/Quotient_Option.thy	Fri Apr 20 15:49:45 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Fri Apr 20 18:29:21 2012 +0200
@@ -110,6 +110,22 @@
 
 declare [[map option = (option_rel, Quotient_option)]]
 
+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)
+  apply (intro allI) 
+  apply (case_tac x rule: option.exhaust)
+  apply (case_tac xa rule: option.exhaust)
+  apply auto[2]
+  apply (case_tac xa rule: option.exhaust)
+  apply auto
+done
+
 subsection {* Rules for quotient package *}
 
 lemma option_quotient [quot_thm]: