diff r a0f257197741 r d654c73e4b12 src/HOL/List.thy
 a/src/HOL/List.thy Fri Apr 06 14:40:00 2012 +0200
+++ b/src/HOL/List.thy Fri Apr 06 18:17:16 2012 +0200
@@ 85,18 +85,20 @@
syntax (HTML output)
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])")
primrec  {* canonical argument order *}
 fold :: "('a \ 'b \ 'b) \ 'a list \ 'b \ 'b" where
 "fold f [] = id"
  "fold f (x # xs) = fold f xs \ f x"

definition
 foldr :: "('a \ 'b \ 'b) \ 'a list \ 'b \ 'b" where
 [code_abbrev]: "foldr f xs = fold f (rev xs)"

definition
 foldl :: "('b \ 'a \ 'b) \ 'b \ 'a list \ 'b" where
 "foldl f s xs = fold (\x s. f s x) xs s"
+primrec fold :: "('a \ 'b \ 'b) \ 'a list \ 'b \ 'b"
+where
+ fold_Nil: "fold f [] = id"
+ fold_Cons: "fold f (x # xs) = fold f xs \ f x"  {* natural argument order *}
+
+primrec foldr :: "('a \ 'b \ 'b) \ 'a list \ 'b \ 'b"
+where
+ foldr_Nil: "foldr f [] = id"
+ foldr_Cons: "foldr f (x # xs) = f x \ foldr f xs"  {* natural argument order *}
+
+primrec foldl :: "('b \ 'a \ 'b) \ 'b \ 'a list \ 'b"
+where
+ foldl_Nil: "foldl f a [] = a"
+ foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
primrec
concat:: "'a list list \ 'a list" where
@@ 250,8 +252,8 @@
@{lemma[source] "filter (\n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
@{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
@{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\
@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by (simp add: foldr_def)}\\
@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by (simp add: foldl_def)}\\
+@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
+@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
@@ 277,7 +279,7 @@
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)}
+@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}
\end{tabular}}
\caption{Characteristic examples}
\label{fig:Characteristic}
@@ 2387,7 +2389,7 @@
by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
subsubsection {* @{const fold} with canonical argument order *}
+subsubsection {* @{const fold} with natural argument order *}
lemma fold_remove1_split:
assumes f: "\x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x"
@@ 2477,7 +2479,7 @@
qed
qed
lemma union_set_fold:
+lemma union_set_fold [code]:
"set xs \ A = fold Set.insert xs A"
proof 
interpret comp_fun_idem Set.insert
@@ 2485,7 +2487,11 @@
show ?thesis by (simp add: union_fold_insert fold_set_fold)
qed
lemma minus_set_fold:
+lemma union_coset_filter [code]:
+ "List.coset xs \ A = List.coset (List.filter (\x. x \ A) xs)"
+ by auto
+
+lemma minus_set_fold [code]:
"A  set xs = fold Set.remove xs A"
proof 
interpret comp_fun_idem Set.remove
@@ 2494,6 +2500,18 @@
by (simp add: minus_fold_remove [of _ A] fold_set_fold)
qed
+lemma minus_coset_filter [code]:
+ "A  List.coset xs = set (List.filter (\x. x \ A) xs)"
+ by auto
+
+lemma inter_set_filter [code]:
+ "A \ set xs = set (List.filter (\x. x \ A) xs)"
+ by auto
+
+lemma inter_coset_fold [code]:
+ "A \ List.coset xs = fold Set.remove xs A"
+ by (simp add: Diff_eq [symmetric] minus_set_fold)
+
lemma (in lattice) Inf_fin_set_fold:
"Inf_fin (set (x # xs)) = fold inf xs x"
proof 
@@ 2503,6 +2521,8 @@
by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
qed
+declare Inf_fin_set_fold [code]
+
lemma (in lattice) Sup_fin_set_fold:
"Sup_fin (set (x # xs)) = fold sup xs x"
proof 
@@ 2512,6 +2532,8 @@
by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
qed
+declare Sup_fin_set_fold [code]
+
lemma (in linorder) Min_fin_set_fold:
"Min (set (x # xs)) = fold min xs x"
proof 
@@ 2521,6 +2543,8 @@
by (simp add: Min_def fold1_set_fold del: set.simps)
qed
+declare Min_fin_set_fold [code]
+
lemma (in linorder) Max_fin_set_fold:
"Max (set (x # xs)) = fold max xs x"
proof 
@@ 2530,6 +2554,8 @@
by (simp add: Max_def fold1_set_fold del: set.simps)
qed
+declare Max_fin_set_fold [code]
+
lemma (in complete_lattice) Inf_set_fold:
"Inf (set xs) = fold inf xs top"
proof 
@@ 2538,6 +2564,8 @@
show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute)
qed
+declare Inf_set_fold [where 'a = "'a set", code]
+
lemma (in complete_lattice) Sup_set_fold:
"Sup (set xs) = fold sup xs bot"
proof 
@@ 2546,73 +2574,74 @@
show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute)
qed
+declare Sup_set_fold [where 'a = "'a set", code]
+
lemma (in complete_lattice) INF_set_fold:
"INFI (set xs) f = fold (inf \ f) xs top"
unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
+declare INF_set_fold [code]
+
lemma (in complete_lattice) SUP_set_fold:
"SUPR (set xs) f = fold (sup \ f) xs bot"
unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
+declare SUP_set_fold [code]
subsubsection {* Fold variants: @{const foldr} and @{const foldl} *}
text {* Correspondence *}
lemma foldr_foldl:  {* The ``Third Duality Theorem'' in Bird \& Wadler: *}
+lemma foldr_conv_fold [code_abbrev]:
+ "foldr f xs = fold f (rev xs)"
+ by (induct xs) simp_all
+
+lemma foldl_conv_fold:
+ "foldl f s xs = fold (\x s. f s x) xs s"
+ by (induct xs arbitrary: s) simp_all
+
+lemma foldr_conv_foldl:  {* The ``Third Duality Theorem'' in Bird \& Wadler: *}
"foldr f xs a = foldl (\x y. f y x) a (rev xs)"
 by (simp add: foldr_def foldl_def)

lemma foldl_foldr:
+ by (simp add: foldr_conv_fold foldl_conv_fold)
+
+lemma foldl_conv_foldr:
"foldl f a xs = foldr (\x y. f y x) (rev xs) a"
 by (simp add: foldr_def foldl_def)
+ by (simp add: foldr_conv_fold foldl_conv_fold)
lemma foldr_fold:
assumes "\x y. x \ set xs \ y \ set xs \ f y \ f x = f x \ f y"
shows "foldr f xs = fold f xs"
 using assms unfolding foldr_def by (rule fold_rev)

lemma
 foldr_Nil [code, simp]: "foldr f [] = id"
 and foldr_Cons [code, simp]: "foldr f (x # xs) = f x \ foldr f xs"
 by (simp_all add: foldr_def)

lemma
 foldl_Nil [simp]: "foldl f a [] = a"
 and foldl_Cons [simp]: "foldl f a (x # xs) = foldl f (f a x) xs"
 by (simp_all add: foldl_def)
+ using assms unfolding foldr_conv_fold by (rule fold_rev)
lemma foldr_cong [fundef_cong]:
"a = b \ l = k \ (\a x. x \ set l \ f x a = g x a) \ foldr f l a = foldr g k b"
 by (auto simp add: foldr_def intro!: fold_cong)
+ by (auto simp add: foldr_conv_fold intro!: fold_cong)
lemma foldl_cong [fundef_cong]:
"a = b \ l = k \ (\a x. x \ set l \ f a x = g a x) \ foldl f a l = foldl g b k"
 by (auto simp add: foldl_def intro!: fold_cong)
+ by (auto simp add: foldl_conv_fold intro!: fold_cong)
lemma foldr_append [simp]:
"foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
 by (simp add: foldr_def)
+ by (simp add: foldr_conv_fold)
lemma foldl_append [simp]:
"foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
 by (simp add: foldl_def)
+ by (simp add: foldl_conv_fold)
lemma foldr_map [code_unfold]:
"foldr g (map f xs) a = foldr (g o f) xs a"
 by (simp add: foldr_def fold_map rev_map)
+ by (simp add: foldr_conv_fold fold_map rev_map)
lemma foldl_map [code_unfold]:
"foldl g a (map f xs) = foldl (\a x. g a (f x)) a xs"
 by (simp add: foldl_def fold_map comp_def)

text {* Executing operations in terms of @{const foldr}  tailrecursive! *}
+ by (simp add: foldl_conv_fold fold_map comp_def)
lemma concat_conv_foldr [code]:
"concat xss = foldr append xss []"
 by (simp add: fold_append_concat_rev foldr_def)

lemma minus_set_foldr [code]:
+ by (simp add: fold_append_concat_rev foldr_conv_fold)
+
+lemma minus_set_foldr:
"A  set xs = foldr Set.remove xs A"
proof 
have "\x y :: 'a. Set.remove y \ Set.remove x = Set.remove x \ Set.remove y"
@@ 2620,11 +2649,7 @@
then show ?thesis by (simp add: minus_set_fold foldr_fold)
qed
lemma subtract_coset_filter [code]:
 "A  List.coset xs = set (List.filter (\x. x \ A) xs)"
 by auto

lemma union_set_foldr [code]:
+lemma union_set_foldr:
"set xs \ A = foldr Set.insert xs A"
proof 
have "\x y :: 'a. insert y \ insert x = insert x \ insert y"
@@ 2632,31 +2657,23 @@
then show ?thesis by (simp add: union_set_fold foldr_fold)
qed
lemma union_coset_foldr [code]:
 "List.coset xs \ A = List.coset (List.filter (\x. x \ A) xs)"
 by auto

lemma inter_set_filer [code]:
 "A \ set xs = set (List.filter (\x. x \ A) xs)"
 by auto

lemma inter_coset_foldr [code]:
+lemma inter_coset_foldr:
"A \ List.coset xs = foldr Set.remove xs A"
by (simp add: Diff_eq [symmetric] minus_set_foldr)
lemma (in lattice) Inf_fin_set_foldr [code]:
+lemma (in lattice) Inf_fin_set_foldr:
"Inf_fin (set (x # xs)) = foldr inf xs x"
by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
lemma (in lattice) Sup_fin_set_foldr [code]:
+lemma (in lattice) Sup_fin_set_foldr:
"Sup_fin (set (x # xs)) = foldr sup xs x"
by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
lemma (in linorder) Min_fin_set_foldr [code]:
+lemma (in linorder) Min_fin_set_foldr:
"Min (set (x # xs)) = foldr min xs x"
by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
lemma (in linorder) Max_fin_set_foldr [code]:
+lemma (in linorder) Max_fin_set_foldr:
"Max (set (x # xs)) = foldr max xs x"
by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
@@ 2668,13 +2685,11 @@
"Sup (set xs) = foldr sup xs bot"
by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code]

lemma (in complete_lattice) INF_set_foldr [code]:
+lemma (in complete_lattice) INF_set_foldr:
"INFI (set xs) f = foldr (inf \ f) xs top"
by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric])
lemma (in complete_lattice) SUP_set_foldr [code]:
+lemma (in complete_lattice) SUP_set_foldr:
"SUPR (set xs) f = foldr (sup \ f) xs bot"
by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
@@ 3108,7 +3123,7 @@
lemma (in comm_monoid_add) listsum_rev [simp]:
"listsum (rev xs) = listsum xs"
 by (simp add: listsum_def foldr_def fold_rev fun_eq_iff add_ac)
+ by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac)
lemma (in monoid_add) fold_plus_listsum_rev:
"fold plus xs = plus (listsum (rev xs))"
@@ 3116,40 +3131,12 @@
fix x
have "fold plus xs x = fold plus xs (x + 0)" by simp
also have "\ = fold plus (x # xs) 0" by simp
 also have "\ = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_def)
+ also have "\ = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_conv_fold)
also have "\ = listsum (rev xs @ [x])" by (simp add: listsum_def)
also have "\ = listsum (rev xs) + listsum [x]" by simp
finally show "fold plus xs x = listsum (rev xs) + x" by simp
qed
lemma (in semigroup_add) foldl_assoc:
 "foldl plus (x + y) zs = x + foldl plus y zs"
 by (simp add: foldl_def fold_commute_apply [symmetric] fun_eq_iff add_assoc)

lemma (in ab_semigroup_add) foldr_conv_foldl:
 "foldr plus xs a = foldl plus a xs"
 by (simp add: foldl_def foldr_fold fun_eq_iff add_ac)

text {*
 Note: @{text "n \ foldl (op +) n ns"} looks simpler, but is more
 difficult to use because it requires an additional transitivity step.
*}

lemma start_le_sum:
 fixes m n :: nat
 shows "m \ n \ m \ foldl plus n ns"
 by (simp add: foldl_def add_commute fold_plus_listsum_rev)

lemma elem_le_sum:
 fixes m n :: nat
 shows "n \ set ns \ n \ foldl plus 0 ns"
 by (force intro: start_le_sum simp add: in_set_conv_decomp)

lemma sum_eq_0_conv [iff]:
 fixes m :: nat
 shows "foldl plus m ns = 0 \ m = 0 \ (\n \ set ns. n = 0)"
 by (induct ns arbitrary: m) auto

text{* Some syntactic sugar for summing a function over a list: *}
syntax
@@ 3186,17 +3173,18 @@
lemma listsum_eq_0_nat_iff_nat [simp]:
"listsum ns = (0::nat) \ (\n \ set ns. n = 0)"
 by (simp add: listsum_def foldr_conv_foldl)
+ by (induct ns) simp_all
+
+lemma member_le_listsum_nat:
+ "(n :: nat) \ set ns \ n \ listsum ns"
+ by (induct ns) auto
lemma elem_le_listsum_nat:
"k < size ns \ ns ! k \ listsum (ns::nat list)"
apply(induct ns arbitrary: k)
 apply simp
apply(fastforce simp add:nth_Cons split: nat.split)
done
+ by (rule member_le_listsum_nat) simp
lemma listsum_update_nat:
 "k listsum (ns[k := (n::nat)]) = listsum ns + n  ns ! k"
+ "k < size ns \ listsum (ns[k := (n::nat)]) = listsum ns + n  ns ! k"
apply(induct ns arbitrary:k)
apply (auto split:nat.split)
apply(drule elem_le_listsum_nat)
@@ 4053,7 +4041,7 @@
show "(insort_key f y \ insort_key f x) zs = (insort_key f x \ insort_key f y) zs"
by (induct zs) (auto intro: * simp add: **)
qed
 then show ?thesis by (simp add: sort_key_def foldr_def)
+ then show ?thesis by (simp add: sort_key_def foldr_conv_fold)
qed
lemma (in linorder) sort_conv_fold:
@@ 4601,7 +4589,7 @@
lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
proof (rule mono_inf [where f=listsp, THEN order_antisym])
show "mono listsp" by (simp add: mono_def listsp_mono)
 show "inf (listsp A) (listsp B) \ listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
+ show "inf (listsp A) (listsp B) \ listsp (inf A B)" by (blast intro!: listsp_infI)
qed
lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def]
@@ 5756,3 +5744,4 @@
by (simp add: wf_iff_acyclic_if_finite)
end
+