src/HOL/List.thy
changeset 55129 26bd1cba3ab5
parent 54890 cb892d835803
child 55147 bce3dbc11f95
--- a/src/HOL/List.thy	Thu Jan 23 19:02:22 2014 +0100
+++ b/src/HOL/List.thy	Fri Jan 24 11:51:45 2014 +0100
@@ -5936,7 +5936,6 @@
 
 subsection {* Code generation *}
 
-
 text{* Optional tail recursive version of @{const map}. Can avoid
 stack overflow in some target languages. *}
 
@@ -6531,6 +6530,7 @@
   "wf (set xs) = acyclic (set xs)"
   by (simp add: wf_iff_acyclic_if_finite)
 
+
 subsection {* Setup for Lifting/Transfer *}
 
 subsubsection {* Relator and predicator properties *}
@@ -6879,4 +6879,46 @@
 
 end
 
+
+subsection {* BNF setup *}
+
+bnf "'a list"
+  map: map
+  sets: set
+  bd: natLeq
+  wits: Nil
+  rel: list_all2
+proof -
+  show "map id = id" by (rule List.map.id)
+next
+  fix f g
+  show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
+next
+  fix x f g
+  assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
+  thus "map f x = map g x" by simp
+next
+  fix f
+  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
+next
+  show "card_order natLeq" by (rule natLeq_card_order)
+next
+  show "cinfinite natLeq" by (rule natLeq_cinfinite)
+next
+  fix x
+  show "|set x| \<le>o natLeq"
+    by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
+next
+  fix R S
+  show "list_all2 R OO list_all2 S \<le> list_all2 (R OO S)"
+    by (metis list_all2_OO order_refl)
+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
+
 end