# HG changeset patch
# User traytel
# Date 1347437911 -7200
# Node ID a1b0654e7c90cbf5e8d6afaaecabab00e1a17e3e
# Parent  e5b84afa73540c2af1de7b35241529943e108a70
option_pred characterization

diff -r e5b84afa7354 -r a1b0654e7c90 src/HOL/Codatatype/More_BNFs.thy
--- a/src/HOL/Codatatype/More_BNFs.thy	Wed Sep 12 09:39:41 2012 +0200
+++ b/src/HOL/Codatatype/More_BNFs.thy	Wed Sep 12 10:18:31 2012 +0200
@@ -83,6 +83,15 @@
   thus False by simp
 qed
 
+lemma option_pred[simp]: "option_pred R x_opt y_opt =
+  (case (x_opt, y_opt) of
+    (None, None) \<Rightarrow> True
+  | (Some x, Some y) \<Rightarrow> R x y
+  | _ \<Rightarrow> False)"
+unfolding option_pred_def option_rel_def Gr_def relcomp_unfold converse_unfold
+by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
+  split: option.splits)
+
 lemma card_of_list_in:
   "|{xs. set xs \<subseteq> A}| \<le>o |Pfunc (UNIV :: nat set) A|" (is "|?LHS| \<le>o |?RHS|")
 proof -