16 "@" :: "'a list => 'a list => 'a list" (infixr 65) |
16 "@" :: "'a list => 'a list => 'a list" (infixr 65) |
17 filter:: "('a => bool) => 'a list => 'a list" |
17 filter:: "('a => bool) => 'a list => 'a list" |
18 concat:: "'a list list => 'a list" |
18 concat:: "'a list list => 'a list" |
19 foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b" |
19 foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b" |
20 foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b" |
20 foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b" |
21 fold_rel :: "('a * 'c * 'a) set => ('a * 'c list * 'a) set" |
|
22 hd:: "'a list => 'a" |
21 hd:: "'a list => 'a" |
23 tl:: "'a list => 'a list" |
22 tl:: "'a list => 'a list" |
24 last:: "'a list => 'a" |
23 last:: "'a list => 'a" |
25 butlast :: "'a list => 'a list" |
24 butlast :: "'a list => 'a list" |
26 set :: "'a list => 'a set" |
25 set :: "'a list => 'a set" |
27 o2l :: "'a option => 'a list" |
|
28 list_all:: "('a => bool) => ('a list => bool)" |
26 list_all:: "('a => bool) => ('a list => bool)" |
29 list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" |
27 list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" |
30 map :: "('a=>'b) => ('a list => 'b list)" |
28 map :: "('a=>'b) => ('a list => 'b list)" |
31 mem :: "'a => 'a list => bool" (infixl 55) |
29 mem :: "'a => 'a list => bool" (infixl 55) |
32 nth :: "'a list => nat => 'a" (infixl "!" 100) |
30 nth :: "'a list => nat => 'a" (infixl "!" 100) |
40 upt :: "nat => nat => nat list" ("(1[_../_'(])") |
38 upt :: "nat => nat => nat list" ("(1[_../_'(])") |
41 remdups :: "'a list => 'a list" |
39 remdups :: "'a list => 'a list" |
42 null:: "'a list => bool" |
40 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 postfix :: "'a list => 'a list => bool" |
|
46 |
|
47 syntax (xsymbols) |
|
48 postfix :: "'a list => 'a list => bool" ("(_/ \<sqsupseteq> _)" [51, 51] 50) |
|
49 |
43 |
50 nonterminals lupdbinds lupdbind |
44 nonterminals lupdbinds lupdbind |
51 |
45 |
52 syntax |
46 syntax |
53 -- {* list Enumeration *} |
47 -- {* list Enumeration *} |
112 "x mem (y#ys) = (if y=x then True else x mem ys)" |
106 "x mem (y#ys) = (if y=x then True else x mem ys)" |
113 primrec |
107 primrec |
114 "set [] = {}" |
108 "set [] = {}" |
115 "set (x#xs) = insert x (set xs)" |
109 "set (x#xs) = insert x (set xs)" |
116 primrec |
110 primrec |
117 "o2l None = []" |
|
118 "o2l (Some x) = [x]" |
|
119 primrec |
|
120 list_all_Nil:"list_all P [] = True" |
111 list_all_Nil:"list_all P [] = True" |
121 list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)" |
112 list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)" |
122 primrec |
113 primrec |
123 "map f [] = []" |
114 "map f [] = []" |
124 "map f (x#xs) = f(x)#map f xs" |
115 "map f (x#xs) = f(x)#map f xs" |
180 "remdups [] = []" |
171 "remdups [] = []" |
181 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" |
172 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" |
182 primrec |
173 primrec |
183 replicate_0: "replicate 0 x = []" |
174 replicate_0: "replicate 0 x = []" |
184 replicate_Suc: "replicate (Suc n) x = x # replicate n x" |
175 replicate_Suc: "replicate (Suc n) x = x # replicate n x" |
185 defs |
|
186 postfix_def: "postfix xs ys == \<exists>zs. xs = zs @ ys" |
|
187 defs |
176 defs |
188 list_all2_def: |
177 list_all2_def: |
189 "list_all2 P xs ys == length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)" |
178 "list_all2 P xs ys == length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)" |
190 |
179 |
191 |
180 |
1237 by (force intro: start_le_sum simp add: in_set_conv_decomp) |
1226 by (force intro: start_le_sum simp add: in_set_conv_decomp) |
1238 |
1227 |
1239 lemma sum_eq_0_conv [iff]: |
1228 lemma sum_eq_0_conv [iff]: |
1240 "!!m::nat. (foldl (op +) m ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))" |
1229 "!!m::nat. (foldl (op +) m ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))" |
1241 by (induct ns) auto |
1230 by (induct ns) auto |
1242 |
|
1243 |
|
1244 subsection {* folding a relation over a list *} |
|
1245 |
|
1246 (*"fold_rel R cs \<equiv> foldl (%r c. r O {(x,y). (c,x,y):R}) Id cs"*) |
|
1247 inductive "fold_rel R" intros |
|
1248 Nil: "(a, [],a) : fold_rel R" |
|
1249 Cons: "[|(a,x,b) : R; (b,xs,c) : fold_rel R|] ==> (a,x#xs,c) : fold_rel R" |
|
1250 inductive_cases fold_rel_elim_case [elim!]: |
|
1251 "(a, [] , b) : fold_rel R" |
|
1252 "(a, x#xs, b) : fold_rel R" |
|
1253 |
|
1254 lemma fold_rel_Nil [intro!]: "a = b ==> (a, [], b) : fold_rel R" |
|
1255 by (simp add: fold_rel.Nil) |
|
1256 declare fold_rel.Cons [intro!] |
|
1257 |
1231 |
1258 |
1232 |
1259 subsection {* @{text upto} *} |
1233 subsection {* @{text upto} *} |
1260 |
1234 |
1261 lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])" |
1235 lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])" |
1442 |
1416 |
1443 lemma in_set_replicateD: "x : set (replicate n y) ==> x = y" |
1417 lemma in_set_replicateD: "x : set (replicate n y) ==> x = y" |
1444 by (simp add: set_replicate_conv_if split: split_if_asm) |
1418 by (simp add: set_replicate_conv_if split: split_if_asm) |
1445 |
1419 |
1446 |
1420 |
1447 subsection {* @{text postfix} *} |
|
1448 |
|
1449 lemma postfix_refl [simp, intro!]: "xs \<sqsupseteq> xs" by (auto simp add: postfix_def) |
|
1450 lemma postfix_trans: "\<lbrakk>xs \<sqsupseteq> ys; ys \<sqsupseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsupseteq> zs" |
|
1451 by (auto simp add: postfix_def) |
|
1452 lemma postfix_antisym: "\<lbrakk>xs \<sqsupseteq> ys; ys \<sqsupseteq> xs\<rbrakk> \<Longrightarrow> xs = ys" |
|
1453 by (auto simp add: postfix_def) |
|
1454 |
|
1455 lemma postfix_emptyI [simp, intro!]: "xs \<sqsupseteq> []" by (auto simp add: postfix_def) |
|
1456 lemma postfix_emptyD [dest!]: "[] \<sqsupseteq> xs \<Longrightarrow> xs = []"by(auto simp add:postfix_def) |
|
1457 lemma postfix_ConsI: "xs \<sqsupseteq> ys \<Longrightarrow> x#xs \<sqsupseteq> ys" by (auto simp add: postfix_def) |
|
1458 lemma postfix_ConsD: "xs \<sqsupseteq> y#ys \<Longrightarrow> xs \<sqsupseteq> ys" by (auto simp add: postfix_def) |
|
1459 lemma postfix_appendI: "xs \<sqsupseteq> ys \<Longrightarrow> zs@xs \<sqsupseteq> ys" by (auto simp add: postfix_def) |
|
1460 lemma postfix_appendD: "xs \<sqsupseteq> zs@ys \<Longrightarrow> xs \<sqsupseteq> ys" by (auto simp add: postfix_def) |
|
1461 |
|
1462 lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs" |
|
1463 by (induct zs, auto) |
|
1464 lemma postfix_is_subset: "xs \<sqsupseteq> ys \<Longrightarrow> set ys \<subseteq> set xs" |
|
1465 by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma) |
|
1466 |
|
1467 lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs \<sqsupseteq> ys" |
|
1468 by (induct zs, auto intro!: postfix_appendI postfix_ConsI) |
|
1469 lemma postfix_ConsD2: "x#xs \<sqsupseteq> y#ys \<Longrightarrow> xs \<sqsupseteq> ys" |
|
1470 by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma) |
|
1471 |
|
1472 subsection {* Lexicographic orderings on lists *} |
1421 subsection {* Lexicographic orderings on lists *} |
1473 |
1422 |
1474 lemma wf_lexn: "wf r ==> wf (lexn r n)" |
1423 lemma wf_lexn: "wf r ==> wf (lexn r n)" |
1475 apply (induct_tac n, simp, simp) |
1424 apply (induct_tac n, simp, simp) |
1476 apply(rule wf_subset) |
1425 apply(rule wf_subset) |