# HG changeset patch
# User traytel
# Date 1439405193 -7200
# Node ID b0ba7799d05a9ad541ef803ad05bdad749602f8c
# Parent  4ceef1592e8c3645baaf719291ab075548eba30a
use lift_bnf in an example

diff -r 4ceef1592e8c -r b0ba7799d05a src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Wed Aug 12 20:46:33 2015 +0200
+++ b/src/HOL/Library/DAList.thy	Wed Aug 12 20:46:33 2015 +0200
@@ -198,54 +198,8 @@
 
 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)
+lift_bnf (dead 'k, set: 'v) alist [wits: "[] :: ('k \<times> 'v) list"] for map: map rel: rel
+  by auto
 
 hide_const valterm_empty valterm_update random_aux_alist