24 hd:: "'a list => 'a" |
24 hd:: "'a list => 'a" |
25 tl:: "'a list => 'a list" |
25 tl:: "'a list => 'a list" |
26 last:: "'a list => 'a" |
26 last:: "'a list => 'a" |
27 butlast :: "'a list => 'a list" |
27 butlast :: "'a list => 'a list" |
28 set :: "'a list => 'a set" |
28 set :: "'a list => 'a set" |
29 list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" |
|
30 map :: "('a=>'b) => ('a list => 'b list)" |
29 map :: "('a=>'b) => ('a list => 'b list)" |
31 nth :: "'a list => nat => 'a" (infixl "!" 100) |
30 nth :: "'a list => nat => 'a" (infixl "!" 100) |
32 list_update :: "'a list => nat => 'a => 'a list" |
31 list_update :: "'a list => nat => 'a => 'a list" |
33 take:: "nat => 'a list => 'a list" |
32 take:: "nat => 'a list => 'a list" |
34 drop:: "nat => 'a list => 'a list" |
33 drop:: "nat => 'a list => 'a list" |
37 rev :: "'a list => 'a list" |
36 rev :: "'a list => 'a list" |
38 zip :: "'a list => 'b list => ('a * 'b) list" |
37 zip :: "'a list => 'b list => ('a * 'b) list" |
39 upt :: "nat => nat => nat list" ("(1[_..</_'])") |
38 upt :: "nat => nat => nat list" ("(1[_..</_'])") |
40 remdups :: "'a list => 'a list" |
39 remdups :: "'a list => 'a list" |
41 remove1 :: "'a => 'a list => 'a list" |
40 remove1 :: "'a => 'a list => 'a list" |
42 null:: "'a list => bool" |
|
43 "distinct":: "'a list => bool" |
41 "distinct":: "'a list => bool" |
44 replicate :: "nat => 'a => 'a list" |
42 replicate :: "nat => 'a => 'a list" |
45 rotate1 :: "'a list \<Rightarrow> 'a list" |
|
46 rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
47 splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
43 splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
48 sublist :: "'a list => nat set => 'a list" |
|
49 (* For efficiency *) |
|
50 mem :: "'a => 'a list => bool" (infixl 55) |
|
51 list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
52 list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" |
|
53 list_all:: "('a => bool) => ('a list => bool)" |
|
54 itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
55 filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" |
|
56 map_filter :: "('a => 'b) => ('a => bool) => 'a list => 'b list" |
|
57 |
44 |
58 abbreviation |
45 abbreviation |
59 upto:: "nat => nat => nat list" ("(1[_../_])") |
46 upto:: "nat => nat => nat list" ("(1[_../_])") |
60 "[i..j] == [i..<(Suc j)]" |
47 "[i..j] == [i..<(Suc j)]" |
61 |
48 |
201 |
184 |
202 primrec |
185 primrec |
203 replicate_0: "replicate 0 x = []" |
186 replicate_0: "replicate 0 x = []" |
204 replicate_Suc: "replicate (Suc n) x = x # replicate n x" |
187 replicate_Suc: "replicate (Suc n) x = x # replicate n x" |
205 |
188 |
206 defs |
189 definition |
207 rotate1_def: "rotate1 xs == (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])" |
190 rotate1 :: "'a list \<Rightarrow> 'a list" |
208 rotate_def: "rotate n == rotate1 ^ n" |
191 rotate1_def: "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])" |
209 |
192 rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
210 list_all2_def: |
193 rotate_def: "rotate n = rotate1 ^ n" |
211 "list_all2 P xs ys == |
194 list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" |
212 length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)" |
195 list_all2_def: "list_all2 P xs ys = |
213 |
196 (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))" |
214 sublist_def: |
197 sublist :: "'a list => nat set => 'a list" |
215 "sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..<size xs]))" |
198 sublist_def: "sublist xs A = |
216 |
199 map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))" |
217 primrec |
200 |
218 "splice [] ys = ys" |
201 primrec |
219 "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))" |
202 "splice [] ys = ys" |
220 -- {*Warning: simpset does not contain the second eqn but a derived one. *} |
203 "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))" |
221 |
204 -- {*Warning: simpset does not contain the second eqn but a derived one. *} |
222 primrec |
205 |
223 "x mem [] = False" |
206 |
224 "x mem (y#ys) = (if y=x then True else x mem ys)" |
207 subsubsection {* @{const Nil} and @{const Cons} *} |
225 |
208 |
226 primrec |
209 lemma not_Cons_self [simp]: |
227 "list_inter [] bs = []" |
210 "xs \<noteq> x # xs" |
228 "list_inter (a#as) bs = |
|
229 (if a \<in> set bs then a#(list_inter as bs) else list_inter as bs)" |
|
230 |
|
231 primrec |
|
232 "list_all P [] = True" |
|
233 "list_all P (x#xs) = (P(x) \<and> list_all P xs)" |
|
234 |
|
235 primrec |
|
236 "list_ex P [] = False" |
|
237 "list_ex P (x#xs) = (P x \<or> list_ex P xs)" |
|
238 |
|
239 primrec |
|
240 "filtermap f [] = []" |
|
241 "filtermap f (x#xs) = |
|
242 (case f x of None \<Rightarrow> filtermap f xs |
|
243 | Some y \<Rightarrow> y # (filtermap f xs))" |
|
244 |
|
245 primrec |
|
246 "map_filter f P [] = []" |
|
247 "map_filter f P (x#xs) = (if P x then f x # map_filter f P xs else |
|
248 map_filter f P xs)" |
|
249 |
|
250 primrec |
|
251 "itrev [] ys = ys" |
|
252 "itrev (x#xs) ys = itrev xs (x#ys)" |
|
253 |
|
254 |
|
255 lemma not_Cons_self [simp]: "xs \<noteq> x # xs" |
|
256 by (induct xs) auto |
211 by (induct xs) auto |
257 |
212 |
258 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric] |
213 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric] |
259 |
214 |
260 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)" |
215 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)" |
261 by (induct xs) auto |
216 by (induct xs) auto |
262 |
217 |
263 lemma length_induct: |
218 lemma length_induct: |
264 "(!!xs. \<forall>ys. length ys < length xs --> P ys ==> P xs) ==> P xs" |
219 "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs" |
265 by (rule measure_induct [of length]) iprover |
220 by (rule measure_induct [of length]) iprover |
266 |
221 |
267 |
222 |
268 subsubsection {* @{text null} *} |
223 subsubsection {* @{const length} *} |
269 |
|
270 lemma null_empty: "null xs = (xs = [])" |
|
271 by (cases xs) simp_all |
|
272 |
|
273 lemma empty_null [code inline]: |
|
274 "(xs = []) = null xs" |
|
275 using null_empty [symmetric] . |
|
276 |
|
277 subsubsection {* @{text length} *} |
|
278 |
224 |
279 text {* |
225 text {* |
280 Needs to come before @{text "@"} because of theorem @{text |
226 Needs to come before @{text "@"} because of theorem @{text |
281 append_eq_append_conv}. |
227 append_eq_append_conv}. |
282 *} |
228 *} |
283 |
229 |
284 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" |
230 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" |
285 by (induct xs) auto |
231 by (induct xs) auto |
286 |
232 |
2232 by (rule in_lists_conv_set [THEN iffD2]) |
2178 by (rule in_lists_conv_set [THEN iffD2]) |
2233 |
2179 |
2234 lemma lists_UNIV [simp]: "lists UNIV = UNIV" |
2180 lemma lists_UNIV [simp]: "lists UNIV = UNIV" |
2235 by auto |
2181 by auto |
2236 |
2182 |
2237 subsubsection {* For efficiency *} |
|
2238 |
|
2239 text{* Only use @{text mem} for generating executable code. Otherwise |
|
2240 use @{prop"x : set xs"} instead --- it is much easier to reason about. |
|
2241 The same is true for @{const list_all} and @{const list_ex}: write |
|
2242 @{text"\<forall>x\<in>set xs"} and @{text"\<exists>x\<in>set xs"} instead because the HOL |
|
2243 quantifiers are aleady known to the automatic provers. In fact, |
|
2244 the declarations in the code subsection make sure that @{text"\<in>"}, @{text"\<forall>x\<in>set xs"} |
|
2245 and @{text"\<exists>x\<in>set xs"} are implemented efficiently. |
|
2246 |
|
2247 The functions @{const itrev}, @{const filtermap} and @{const |
|
2248 map_filter} are just there to generate efficient code. Do not use them |
|
2249 for modelling and proving. *} |
|
2250 |
|
2251 lemma mem_iff: "(x mem xs) = (x : set xs)" |
|
2252 by (induct xs) auto |
|
2253 |
|
2254 lemma list_inter_conv: "set(list_inter xs ys) = set xs \<inter> set ys" |
|
2255 by (induct xs) auto |
|
2256 |
|
2257 lemma list_all_iff: "list_all P xs = (\<forall>x \<in> set xs. P x)" |
|
2258 by (induct xs) auto |
|
2259 |
|
2260 lemma list_all_append [simp]: |
|
2261 "list_all P (xs @ ys) = (list_all P xs \<and> list_all P ys)" |
|
2262 by (induct xs) auto |
|
2263 |
|
2264 lemma list_all_rev [simp]: "list_all P (rev xs) = list_all P xs" |
|
2265 by (simp add: list_all_iff) |
|
2266 |
|
2267 lemma list_ex_iff: "list_ex P xs = (\<exists>x \<in> set xs. P x)" |
|
2268 by (induct xs) simp_all |
|
2269 |
|
2270 lemma itrev[simp]: "ALL ys. itrev xs ys = rev xs @ ys" |
|
2271 by (induct xs) simp_all |
|
2272 |
|
2273 lemma filtermap_conv: |
|
2274 "filtermap f xs = map (%x. the(f x)) (filter (%x. f x \<noteq> None) xs)" |
|
2275 by (induct xs) (simp_all split: option.split) |
|
2276 |
|
2277 lemma map_filter_conv[simp]: "map_filter f P xs = map f (filter P xs)" |
|
2278 by (induct xs) auto |
|
2279 |
|
2280 |
|
2281 subsubsection {* Code generation *} |
|
2282 |
|
2283 text{* Defaults for generating efficient code for some standard functions. *} |
|
2284 |
|
2285 lemmas in_set_code [code unfold] = |
|
2286 mem_iff [symmetric, THEN eq_reflection] |
|
2287 |
|
2288 lemma rev_code[code unfold]: "rev xs == itrev xs []" |
|
2289 by simp |
|
2290 |
|
2291 lemma distinct_Cons_mem[code]: "distinct (x#xs) = (~(x mem xs) \<and> distinct xs)" |
|
2292 by (simp add:mem_iff) |
|
2293 |
|
2294 lemma remdups_Cons_mem[code]: |
|
2295 "remdups (x#xs) = (if x mem xs then remdups xs else x # remdups xs)" |
|
2296 by (simp add:mem_iff) |
|
2297 |
|
2298 lemma list_inter_Cons_mem[code]: "list_inter (a#as) bs = |
|
2299 (if a mem bs then a#(list_inter as bs) else list_inter as bs)" |
|
2300 by(simp add:mem_iff) |
|
2301 |
|
2302 text{* For implementing bounded quantifiers over lists by |
|
2303 @{const list_ex}/@{const list_all}: *} |
|
2304 |
|
2305 lemmas list_bex_code[code unfold] = list_ex_iff[symmetric, THEN eq_reflection] |
|
2306 lemmas list_ball_code[code unfold] = list_all_iff[symmetric, THEN eq_reflection] |
|
2307 |
2183 |
2308 |
2184 |
2309 subsubsection{* Inductive definition for membership *} |
2185 subsubsection{* Inductive definition for membership *} |
2310 |
2186 |
2311 consts ListMem :: "('a \<times> 'a list)set" |
2187 consts ListMem :: "('a \<times> 'a list)set" |
2798 ("List.char.Char", CodegenPackage.appgen_char HOList.dest_char) |
2676 ("List.char.Char", CodegenPackage.appgen_char HOList.dest_char) |
2799 |
2677 |
2800 end; |
2678 end; |
2801 *} |
2679 *} |
2802 |
2680 |
|
2681 |
|
2682 subsubsection {* Generation of efficient code *} |
|
2683 |
|
2684 consts |
|
2685 mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl 55) |
|
2686 null:: "'a list \<Rightarrow> bool" |
|
2687 list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
2688 list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" |
|
2689 list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)" |
|
2690 itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
2691 filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" |
|
2692 map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list" |
|
2693 |
|
2694 primrec |
|
2695 "x mem [] = False" |
|
2696 "x mem (y#ys) = (if y = x then True else x mem ys)" |
|
2697 |
|
2698 primrec |
|
2699 "null [] = True" |
|
2700 "null (x#xs) = False" |
|
2701 |
|
2702 primrec |
|
2703 "list_inter [] bs = []" |
|
2704 "list_inter (a#as) bs = |
|
2705 (if a \<in> set bs then a # list_inter as bs else list_inter as bs)" |
|
2706 |
|
2707 primrec |
|
2708 "list_all P [] = True" |
|
2709 "list_all P (x#xs) = (P x \<and> list_all P xs)" |
|
2710 |
|
2711 primrec |
|
2712 "list_ex P [] = False" |
|
2713 "list_ex P (x#xs) = (P x \<or> list_ex P xs)" |
|
2714 |
|
2715 primrec |
|
2716 "filtermap f [] = []" |
|
2717 "filtermap f (x#xs) = |
|
2718 (case f x of None \<Rightarrow> filtermap f xs |
|
2719 | Some y \<Rightarrow> y # filtermap f xs)" |
|
2720 |
|
2721 primrec |
|
2722 "map_filter f P [] = []" |
|
2723 "map_filter f P (x#xs) = |
|
2724 (if P x then f x # map_filter f P xs else map_filter f P xs)" |
|
2725 |
|
2726 primrec |
|
2727 "itrev [] ys = ys" |
|
2728 "itrev (x#xs) ys = itrev xs (x#ys)" |
|
2729 |
|
2730 text {* |
|
2731 Only use @{text mem} for generating executable code. Otherwise |
|
2732 use @{prop "x : set xs"} instead --- it is much easier to reason about. |
|
2733 The same is true for @{const list_all} and @{const list_ex}: write |
|
2734 @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL |
|
2735 quantifiers are aleady known to the automatic provers. In fact, |
|
2736 the declarations in the code subsection make sure that @{text "\<in>"}, @{text "\<forall>x\<in>set xs"} |
|
2737 and @{text "\<exists>x\<in>set xs"} are implemented efficiently. |
|
2738 |
|
2739 Efficient emptyness check is implemented by @{const null}. |
|
2740 |
|
2741 The functions @{const itrev}, @{const filtermap} and @{const map_filter} |
|
2742 are just there to generate efficient code. Do not use them |
|
2743 for modelling and proving. |
|
2744 *} |
|
2745 |
|
2746 lemma mem_iff [normal post]: |
|
2747 "(x mem xs) = (x \<in> set xs)" |
|
2748 by (induct xs) auto |
|
2749 |
|
2750 lemmas in_set_code [code unfold] = |
|
2751 mem_iff [symmetric, THEN eq_reflection] |
|
2752 |
|
2753 lemma empty_null [code inline]: |
|
2754 "(xs = []) = null xs" |
|
2755 by (cases xs) simp_all |
|
2756 |
|
2757 lemmas null_empty [normal post] = |
|
2758 empty_null [symmetric] |
|
2759 |
|
2760 lemma list_inter_conv: |
|
2761 "set (list_inter xs ys) = set xs \<inter> set ys" |
|
2762 by (induct xs) auto |
|
2763 |
|
2764 lemma list_all_iff [normal post]: |
|
2765 "list_all P xs = (\<forall>x \<in> set xs. P x)" |
|
2766 by (induct xs) auto |
|
2767 |
|
2768 lemmas list_ball_code [code unfold] = |
|
2769 list_all_iff [symmetric, THEN eq_reflection] |
|
2770 |
|
2771 lemma list_all_append [simp]: |
|
2772 "list_all P (xs @ ys) = (list_all P xs \<and> list_all P ys)" |
|
2773 by (induct xs) auto |
|
2774 |
|
2775 lemma list_all_rev [simp]: |
|
2776 "list_all P (rev xs) = list_all P xs" |
|
2777 by (simp add: list_all_iff) |
|
2778 |
|
2779 lemma list_ex_iff [normal post]: |
|
2780 "list_ex P xs = (\<exists>x \<in> set xs. P x)" |
|
2781 by (induct xs) simp_all |
|
2782 |
|
2783 lemmas list_bex_code [code unfold] = |
|
2784 list_ex_iff [symmetric, THEN eq_reflection] |
|
2785 |
|
2786 lemma itrev [simp]: |
|
2787 "itrev xs ys = rev xs @ ys" |
|
2788 by (induct xs arbitrary: ys) simp_all |
|
2789 |
|
2790 lemma filtermap_conv: |
|
2791 "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)" |
|
2792 by (induct xs) (simp_all split: option.split) |
|
2793 |
|
2794 lemma map_filter_conv [simp]: |
|
2795 "map_filter f P xs = map f (filter P xs)" |
|
2796 by (induct xs) auto |
|
2797 |
|
2798 lemma rev_code [code func, code unfold]: |
|
2799 "rev xs == itrev xs []" |
|
2800 by simp |
|
2801 |
|
2802 lemmas itrev_rev [normal post] = |
|
2803 rev_code [symmetric] |
|
2804 |
2803 end |
2805 end |