src/HOL/Library/More_List.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45146 5465824c1c8d
child 45973 204f34a99ceb
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 (*  Author:  Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Operations on lists beyond the standard List theory *}
     4 
     5 theory More_List
     6 imports Main Multiset
     7 begin
     8 
     9 hide_const (open) Finite_Set.fold
    10 
    11 text {* Repairing code generator setup *}
    12 
    13 declare (in lattice) Inf_fin_set_fold [code_unfold del]
    14 declare (in lattice) Sup_fin_set_fold [code_unfold del]
    15 declare (in linorder) Min_fin_set_fold [code_unfold del]
    16 declare (in linorder) Max_fin_set_fold [code_unfold del]
    17 declare (in complete_lattice) Inf_set_fold [code_unfold del]
    18 declare (in complete_lattice) Sup_set_fold [code_unfold del]
    19 
    20 
    21 text {* Fold combinator with canonical argument order *}
    22 
    23 primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    24     "fold f [] = id"
    25   | "fold f (x # xs) = fold f xs \<circ> f x"
    26 
    27 lemma foldl_fold:
    28   "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
    29   by (induct xs arbitrary: s) simp_all
    30 
    31 lemma foldr_fold_rev:
    32   "foldr f xs = fold f (rev xs)"
    33   by (simp add: foldr_foldl foldl_fold fun_eq_iff)
    34 
    35 lemma fold_rev_conv [code_unfold]:
    36   "fold f (rev xs) = foldr f xs"
    37   by (simp add: foldr_fold_rev)
    38   
    39 lemma fold_cong [fundef_cong]:
    40   "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
    41     \<Longrightarrow> fold f xs a = fold g ys b"
    42   by (induct ys arbitrary: a b xs) simp_all
    43 
    44 lemma fold_id:
    45   assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
    46   shows "fold f xs = id"
    47   using assms by (induct xs) simp_all
    48 
    49 lemma fold_commute:
    50   assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
    51   shows "h \<circ> fold g xs = fold f xs \<circ> h"
    52   using assms by (induct xs) (simp_all add: fun_eq_iff)
    53 
    54 lemma fold_commute_apply:
    55   assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
    56   shows "h (fold g xs s) = fold f xs (h s)"
    57 proof -
    58   from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
    59   then show ?thesis by (simp add: fun_eq_iff)
    60 qed
    61 
    62 lemma fold_invariant: 
    63   assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
    64     and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
    65   shows "P (fold f xs s)"
    66   using assms by (induct xs arbitrary: s) simp_all
    67 
    68 lemma fold_weak_invariant:
    69   assumes "P s"
    70     and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
    71   shows "P (fold f xs s)"
    72   using assms by (induct xs arbitrary: s) simp_all
    73 
    74 lemma fold_append [simp]:
    75   "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
    76   by (induct xs) simp_all
    77 
    78 lemma fold_map [code_unfold]:
    79   "fold g (map f xs) = fold (g o f) xs"
    80   by (induct xs) simp_all
    81 
    82 lemma fold_remove1_split:
    83   assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
    84     and x: "x \<in> set xs"
    85   shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
    86   using assms by (induct xs) (auto simp add: o_assoc [symmetric])
    87 
    88 lemma fold_multiset_equiv:
    89   assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
    90     and equiv: "multiset_of xs = multiset_of ys"
    91   shows "fold f xs = fold f ys"
    92 using f equiv [symmetric] proof (induct xs arbitrary: ys)
    93   case Nil then show ?case by simp
    94 next
    95   case (Cons x xs)
    96   then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
    97   have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
    98     by (rule Cons.prems(1)) (simp_all add: *)
    99   moreover from * have "x \<in> set ys" by simp
   100   ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
   101   moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps)
   102   ultimately show ?case by simp
   103 qed
   104 
   105 lemma fold_rev:
   106   assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   107   shows "fold f (rev xs) = fold f xs"
   108   by (rule fold_multiset_equiv, rule assms) (simp_all add: in_multiset_in_set)
   109 
   110 lemma foldr_fold:
   111   assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   112   shows "foldr f xs = fold f xs"
   113   using assms unfolding foldr_fold_rev by (rule fold_rev)
   114 
   115 lemma fold_Cons_rev:
   116   "fold Cons xs = append (rev xs)"
   117   by (induct xs) simp_all
   118 
   119 lemma rev_conv_fold [code]:
   120   "rev xs = fold Cons xs []"
   121   by (simp add: fold_Cons_rev)
   122 
   123 lemma fold_append_concat_rev:
   124   "fold append xss = append (concat (rev xss))"
   125   by (induct xss) simp_all
   126 
   127 lemma concat_conv_foldr [code]:
   128   "concat xss = foldr append xss []"
   129   by (simp add: fold_append_concat_rev foldr_fold_rev)
   130 
   131 lemma fold_plus_listsum_rev:
   132   "fold plus xs = plus (listsum (rev xs))"
   133   by (induct xs) (simp_all add: add.assoc)
   134 
   135 lemma (in monoid_add) listsum_conv_fold [code]:
   136   "listsum xs = fold (\<lambda>x y. y + x) xs 0"
   137   by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
   138 
   139 lemma (in linorder) sort_key_conv_fold:
   140   assumes "inj_on f (set xs)"
   141   shows "sort_key f xs = fold (insort_key f) xs []"
   142 proof -
   143   have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
   144   proof (rule fold_rev, rule ext)
   145     fix zs
   146     fix x y
   147     assume "x \<in> set xs" "y \<in> set xs"
   148     with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
   149     have **: "x = y \<longleftrightarrow> y = x" by auto
   150     show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
   151       by (induct zs) (auto intro: * simp add: **)
   152   qed
   153   then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
   154 qed
   155 
   156 lemma (in linorder) sort_conv_fold:
   157   "sort xs = fold insort xs []"
   158   by (rule sort_key_conv_fold) simp
   159 
   160 
   161 text {* @{const Finite_Set.fold} and @{const fold} *}
   162 
   163 lemma (in comp_fun_commute) fold_set_remdups:
   164   "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
   165   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
   166 
   167 lemma (in comp_fun_idem) fold_set:
   168   "Finite_Set.fold f y (set xs) = fold f xs y"
   169   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
   170 
   171 lemma (in ab_semigroup_idem_mult) fold1_set:
   172   assumes "xs \<noteq> []"
   173   shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
   174 proof -
   175   interpret comp_fun_idem times by (fact comp_fun_idem)
   176   from assms obtain y ys where xs: "xs = y # ys"
   177     by (cases xs) auto
   178   show ?thesis
   179   proof (cases "set ys = {}")
   180     case True with xs show ?thesis by simp
   181   next
   182     case False
   183     then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
   184       by (simp only: finite_set fold1_eq_fold_idem)
   185     with xs show ?thesis by (simp add: fold_set mult_commute)
   186   qed
   187 qed
   188 
   189 lemma (in lattice) Inf_fin_set_fold:
   190   "Inf_fin (set (x # xs)) = fold inf xs x"
   191 proof -
   192   interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   193     by (fact ab_semigroup_idem_mult_inf)
   194   show ?thesis
   195     by (simp add: Inf_fin_def fold1_set del: set.simps)
   196 qed
   197 
   198 lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
   199   "Inf_fin (set (x # xs)) = foldr inf xs x"
   200   by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   201 
   202 lemma (in lattice) Sup_fin_set_fold:
   203   "Sup_fin (set (x # xs)) = fold sup xs x"
   204 proof -
   205   interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   206     by (fact ab_semigroup_idem_mult_sup)
   207   show ?thesis
   208     by (simp add: Sup_fin_def fold1_set del: set.simps)
   209 qed
   210 
   211 lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
   212   "Sup_fin (set (x # xs)) = foldr sup xs x"
   213   by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   214 
   215 lemma (in linorder) Min_fin_set_fold:
   216   "Min (set (x # xs)) = fold min xs x"
   217 proof -
   218   interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   219     by (fact ab_semigroup_idem_mult_min)
   220   show ?thesis
   221     by (simp add: Min_def fold1_set del: set.simps)
   222 qed
   223 
   224 lemma (in linorder) Min_fin_set_foldr [code_unfold]:
   225   "Min (set (x # xs)) = foldr min xs x"
   226   by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   227 
   228 lemma (in linorder) Max_fin_set_fold:
   229   "Max (set (x # xs)) = fold max xs x"
   230 proof -
   231   interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   232     by (fact ab_semigroup_idem_mult_max)
   233   show ?thesis
   234     by (simp add: Max_def fold1_set del: set.simps)
   235 qed
   236 
   237 lemma (in linorder) Max_fin_set_foldr [code_unfold]:
   238   "Max (set (x # xs)) = foldr max xs x"
   239   by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
   240 
   241 lemma (in complete_lattice) Inf_set_fold:
   242   "Inf (set xs) = fold inf xs top"
   243 proof -
   244   interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   245     by (fact comp_fun_idem_inf)
   246   show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
   247 qed
   248 
   249 lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
   250   "Inf (set xs) = foldr inf xs top"
   251   by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
   252 
   253 lemma (in complete_lattice) Sup_set_fold:
   254   "Sup (set xs) = fold sup xs bot"
   255 proof -
   256   interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   257     by (fact comp_fun_idem_sup)
   258   show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
   259 qed
   260 
   261 lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
   262   "Sup (set xs) = foldr sup xs bot"
   263   by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
   264 
   265 lemma (in complete_lattice) INFI_set_fold:
   266   "INFI (set xs) f = fold (inf \<circ> f) xs top"
   267   unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
   268 
   269 lemma (in complete_lattice) SUPR_set_fold:
   270   "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
   271   unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
   272 
   273 
   274 text {* @{text nth_map} *}
   275 
   276 definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   277   "nth_map n f xs = (if n < length xs then
   278        take n xs @ [f (xs ! n)] @ drop (Suc n) xs
   279      else xs)"
   280 
   281 lemma nth_map_id:
   282   "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
   283   by (simp add: nth_map_def)
   284 
   285 lemma nth_map_unfold:
   286   "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
   287   by (simp add: nth_map_def)
   288 
   289 lemma nth_map_Nil [simp]:
   290   "nth_map n f [] = []"
   291   by (simp add: nth_map_def)
   292 
   293 lemma nth_map_zero [simp]:
   294   "nth_map 0 f (x # xs) = f x # xs"
   295   by (simp add: nth_map_def)
   296 
   297 lemma nth_map_Suc [simp]:
   298   "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
   299   by (simp add: nth_map_def)
   300 
   301 
   302 text {* Enumeration of all sublists of a list *}
   303 
   304 primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   305   "sublists [] = [[]]"
   306   | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   307 
   308 lemma length_sublists:
   309   "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
   310   by (induct xs) (simp_all add: Let_def)
   311 
   312 lemma sublists_powset:
   313   "set ` set (sublists xs) = Pow (set xs)"
   314 proof -
   315   have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
   316     by (auto simp add: image_def)
   317   have "set (map set (sublists xs)) = Pow (set xs)"
   318     by (induct xs)
   319       (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
   320   then show ?thesis by simp
   321 qed
   322 
   323 lemma distinct_set_sublists:
   324   assumes "distinct xs"
   325   shows "distinct (map set (sublists xs))"
   326 proof (rule card_distinct)
   327   have "finite (set xs)" by rule
   328   then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
   329   with assms distinct_card [of xs]
   330     have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
   331   then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
   332     by (simp add: sublists_powset length_sublists)
   333 qed
   334 
   335 
   336 text {* monad operation *}
   337 
   338 definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   339   "bind xs f = concat (map f xs)"
   340 
   341 lemma bind_simps [simp]:
   342   "bind [] f = []"
   343   "bind (x # xs) f = f x @ bind xs f"
   344   by (simp_all add: bind_def)
   345 
   346 end