# HG changeset patch
# User traytel
# Date 1384353392 -3600
# Node ID 72ec50a85f3bcfb51fd5231e8e018ed3dbc0a797
# Parent  914e2ab723f0d1d550ee6ea9d61fba9080e7ac72
standard relator for list bnf

diff -r 914e2ab723f0 -r 72ec50a85f3b src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Wed Nov 13 11:23:25 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Wed Nov 13 15:36:32 2013 +0100
@@ -104,6 +104,7 @@
   sets: set
   bd: natLeq
   wits: Nil
+  rel: list_all2
 proof -
   show "map id = id" by (rule List.map.id)
 next
@@ -124,6 +125,13 @@
   fix x
   show "|set x| \<le>o natLeq"
     by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
+next
+  fix R
+  show "list_all2 R =
+         (Grp {x. set x \<subseteq> {(x, y). R x y}} (map fst))\<inverse>\<inverse> OO
+         Grp {x. set x \<subseteq> {(x, y). R x y}} (map snd)"
+    unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps
+    by (force simp: zip_map_fst_snd)
 qed (simp add: wpull_map)+
 
 (* Finite sets *)