summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Mon, 21 May 2007 19:11:39 +0200 | |

changeset 23060 | 0c0b03d0ec7e |

parent 23059 | e7cd9719dbc2 |

child 23061 | fd89206652dd |

improved code for rev

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Mon May 21 19:11:38 2007 +0200 +++ b/src/HOL/List.thy Mon May 21 19:11:39 2007 +0200 @@ -2728,7 +2728,6 @@ list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)" - itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list" @@ -2764,10 +2763,6 @@ "map_filter f P (x#xs) = (if P x then f x # map_filter f P xs else map_filter f P xs)" -primrec - "itrev [] ys = ys" - "itrev (x#xs) ys = itrev xs (x#ys)" - text {* Only use @{text mem} for generating executable code. Otherwise use @{prop "x : set xs"} instead --- it is much easier to reason about. @@ -2780,11 +2775,27 @@ Efficient emptyness check is implemented by @{const null}. - The functions @{const itrev}, @{const filtermap} and @{const - map_filter} are just there to generate efficient code. Do not use + The functions @{const filtermap} and @{const map_filter} are just + there to generate efficient code. Do not use them for modelling and proving. *} +lemma rev_foldl_cons [code]: + "rev xs = foldl (\<lambda>xs x. x # xs) [] xs" +proof (induct xs) + case Nil then show ?case by simp +next + case Cons + { + fix x xs ys + have "foldl (\<lambda>xs x. x # xs) ys xs @ [x] + = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs" + by (induct xs arbitrary: ys) auto + } + note aux = this + show ?case by (induct xs) (auto simp add: Cons aux) +qed + lemma mem_iff [normal post]: "x mem xs \<longleftrightarrow> x \<in> set xs" by (induct xs) auto @@ -2831,10 +2842,6 @@ "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))" unfolding list_ex_iff set_conv_nth by auto -lemma itrev [simp]: - "itrev xs ys = rev xs @ ys" - by (induct xs arbitrary: ys) simp_all - lemma filtermap_conv: "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)" by (induct xs) (simp_all split: option.split) @@ -2843,10 +2850,6 @@ "map_filter f P xs = map f (filter P xs)" by (induct xs) auto -lemma rev_code [code func]: - "rev xs = itrev xs []" - by simp - text {* code for bounded quantification over nats *}