# HG changeset patch
# User wenzelm
# Date 1425496599 -3600
# Node ID 3c94c44dfc0f4ae712d993e822332f670bd6ca00
# Parent  0fbed69ff081ce0111a17e0024902acf3f9b974d# Parent  09722854b8f4ef7627206f01418df9938a87801f
merged;

diff -r 0fbed69ff081 -r 3c94c44dfc0f src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Wed Mar 04 19:53:18 2015 +0100
+++ b/src/HOL/Library/DAList.thy	Wed Mar 04 20:16:39 2015 +0100
@@ -195,9 +195,61 @@
 
 end
 
+
+section \<open>alist is a BNF\<close>
+
+lift_definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('k, 'a) alist \<Rightarrow> ('k, 'b) alist"
+  is "\<lambda>f xs. List.map (map_prod id f) xs" by simp
+
+lift_definition set :: "('k, 'v) alist => 'v set"
+  is "\<lambda>xs. snd ` List.set xs" .
+
+lift_definition rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('k, 'a) alist \<Rightarrow> ('k, 'b) alist \<Rightarrow> bool"
+  is "\<lambda>R xs ys. list_all2 (rel_prod op = R) xs ys" .
+
+bnf "('k, 'v) alist"
+  map: map
+  sets: set
+  bd: natLeq
+  wits: empty
+  rel: rel
+proof (unfold OO_Grp_alt)
+  show "map id = id" by (rule ext, transfer) (simp add: prod.map_id0)
+next
+  fix f g
+  show "map (g \<circ> f) = map g \<circ> map f"
+    by (rule ext, transfer) (simp add: prod.map_comp)
+next
+  fix x f g
+  assume "(\<And>z. z \<in> set x \<Longrightarrow> f z = g z)"
+  then show "map f x = map g x" by transfer force
+next
+  fix f
+  show "set \<circ> map f = op ` f \<circ> set"
+    by (rule ext, transfer) (simp add: image_image)
+next
+  fix x
+  show "ordLeq3 (card_of (set x)) natLeq"
+    by transfer (auto simp: finite_iff_ordLess_natLeq[symmetric] intro: ordLess_imp_ordLeq)
+next
+  fix R S
+  show "rel R OO rel S \<le> rel (R OO S)"
+    by (rule predicate2I, transfer)
+      (auto simp: list.rel_compp prod.rel_compp[of "op =", unfolded eq_OO])
+next
+  fix R
+  show "rel R = (\<lambda>x y. \<exists>z. z \<in> {x. set x \<subseteq> {(x, y). R x y}} \<and> map fst z = x \<and> map snd z = y)"
+   unfolding fun_eq_iff by transfer (fastforce simp: list.in_rel o_def intro:
+     exI[of _ "List.map (\<lambda>p. ((fst p, fst (snd p)), (fst p, snd (snd p)))) z" for z]
+     exI[of _ "List.map (\<lambda>p. (fst (fst p), snd (fst p), snd (snd p))) z" for z])
+next
+  fix z assume "z \<in> set empty"
+  then show False by transfer simp
+qed (simp_all add: natLeq_cinfinite natLeq_card_order)
+
 hide_const valterm_empty valterm_update random_aux_alist
 
 hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
-hide_const (open) impl_of lookup empty update delete map_entry filter map_default
+hide_const (open) impl_of lookup empty update delete map_entry filter map_default map set rel
 
 end