src/HOL/List.thy
changeset 55129 26bd1cba3ab5
parent 54890 cb892d835803
child 55147 bce3dbc11f95
     1.1 --- a/src/HOL/List.thy	Thu Jan 23 19:02:22 2014 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Jan 24 11:51:45 2014 +0100
     1.3 @@ -5936,7 +5936,6 @@
     1.4  
     1.5  subsection {* Code generation *}
     1.6  
     1.7 -
     1.8  text{* Optional tail recursive version of @{const map}. Can avoid
     1.9  stack overflow in some target languages. *}
    1.10  
    1.11 @@ -6531,6 +6530,7 @@
    1.12    "wf (set xs) = acyclic (set xs)"
    1.13    by (simp add: wf_iff_acyclic_if_finite)
    1.14  
    1.15 +
    1.16  subsection {* Setup for Lifting/Transfer *}
    1.17  
    1.18  subsubsection {* Relator and predicator properties *}
    1.19 @@ -6879,4 +6879,46 @@
    1.20  
    1.21  end
    1.22  
    1.23 +
    1.24 +subsection {* BNF setup *}
    1.25 +
    1.26 +bnf "'a list"
    1.27 +  map: map
    1.28 +  sets: set
    1.29 +  bd: natLeq
    1.30 +  wits: Nil
    1.31 +  rel: list_all2
    1.32 +proof -
    1.33 +  show "map id = id" by (rule List.map.id)
    1.34 +next
    1.35 +  fix f g
    1.36 +  show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
    1.37 +next
    1.38 +  fix x f g
    1.39 +  assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
    1.40 +  thus "map f x = map g x" by simp
    1.41 +next
    1.42 +  fix f
    1.43 +  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
    1.44 +next
    1.45 +  show "card_order natLeq" by (rule natLeq_card_order)
    1.46 +next
    1.47 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
    1.48 +next
    1.49 +  fix x
    1.50 +  show "|set x| \<le>o natLeq"
    1.51 +    by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
    1.52 +next
    1.53 +  fix R S
    1.54 +  show "list_all2 R OO list_all2 S \<le> list_all2 (R OO S)"
    1.55 +    by (metis list_all2_OO order_refl)
    1.56 +next
    1.57 +  fix R
    1.58 +  show "list_all2 R =
    1.59 +         (Grp {x. set x \<subseteq> {(x, y). R x y}} (map fst))\<inverse>\<inverse> OO
    1.60 +         Grp {x. set x \<subseteq> {(x, y). R x y}} (map snd)"
    1.61 +    unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps
    1.62 +    by (force simp: zip_map_fst_snd)
    1.63 +qed simp
    1.64 +
    1.65  end