221 |
221 |
222 subsection {* @{text lists}: the list-forming operator over sets *} |
222 subsection {* @{text lists}: the list-forming operator over sets *} |
223 |
223 |
224 consts lists :: "'a set => 'a list set" |
224 consts lists :: "'a set => 'a list set" |
225 inductive "lists A" |
225 inductive "lists A" |
226 intros |
226 intros |
227 Nil [intro!]: "[]: lists A" |
227 Nil [intro!]: "[]: lists A" |
228 Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A" |
228 Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A" |
229 |
229 |
230 inductive_cases listsE [elim!]: "x#l : lists A" |
230 inductive_cases listsE [elim!]: "x#l : lists A" |
231 |
231 |
232 lemma lists_mono [mono]: "A \<subseteq> B ==> lists A \<subseteq> lists B" |
232 lemma lists_mono [mono]: "A \<subseteq> B ==> lists A \<subseteq> lists B" |
233 by (unfold lists.defs) (blast intro!: lfp_mono) |
233 by (unfold lists.defs) (blast intro!: lfp_mono) |
646 by (rule in_lists_conv_set [THEN iffD1]) |
646 by (rule in_lists_conv_set [THEN iffD1]) |
647 |
647 |
648 lemma in_listsI [intro!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> lists A" |
648 lemma in_listsI [intro!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> lists A" |
649 by (rule in_lists_conv_set [THEN iffD2]) |
649 by (rule in_lists_conv_set [THEN iffD2]) |
650 |
650 |
|
651 lemma lists_UNIV [simp]: "lists UNIV = UNIV" |
|
652 by auto |
|
653 |
651 lemma finite_list: "finite A ==> EX l. set l = A" |
654 lemma finite_list: "finite A ==> EX l. set l = A" |
652 apply (erule finite_induct, auto) |
655 apply (erule finite_induct, auto) |
653 apply (rule_tac x="x#l" in exI, auto) |
656 apply (rule_tac x="x#l" in exI, auto) |
654 done |
657 done |
655 |
658 |
656 lemma card_length: "card (set xs) \<le> length xs" |
659 lemma card_length: "card (set xs) \<le> length xs" |
657 by (induct xs) (auto simp add: card_insert_if) |
660 by (induct xs) (auto simp add: card_insert_if) |
|
661 |
|
662 |
|
663 subsection{*Sets of Lists*} |
|
664 |
|
665 text{*Resembles a Cartesian product: it denotes the set of lists with head |
|
666 drawn from @{term A} and tail drawn from @{term Xs}.*} |
|
667 constdefs |
|
668 set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" |
|
669 "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}" |
|
670 |
|
671 lemma [simp]: "set_Cons A {[]} = (%x. [x])`A" |
|
672 by (auto simp add: set_Cons_def) |
|
673 |
|
674 text{*Yields the set of lists, all of the same length as the argument and |
|
675 with elements drawn from the corresponding element of the argument.*} |
|
676 consts listset :: "'a set list \<Rightarrow> 'a list set" |
|
677 primrec |
|
678 "listset [] = {[]}" |
|
679 "listset(A#As) = set_Cons A (listset As)" |
|
680 |
658 |
681 |
659 subsection {* @{text mem} *} |
682 subsection {* @{text mem} *} |
660 |
683 |
661 lemma set_mem_eq: "(x mem xs) = (x : set xs)" |
684 lemma set_mem_eq: "(x mem xs) = (x : set xs)" |
662 by (induct xs) auto |
685 by (induct xs) auto |
1554 apply(rule wf_prod_fun_image) |
1577 apply(rule wf_prod_fun_image) |
1555 prefer 2 apply (rule inj_onI, auto) |
1578 prefer 2 apply (rule inj_onI, auto) |
1556 done |
1579 done |
1557 |
1580 |
1558 lemma lexn_length: |
1581 lemma lexn_length: |
1559 "!!xs ys. (xs, ys) : lexn r n ==> length xs = n \<and> length ys = n" |
1582 "!!xs ys. (xs, ys) : lexn r n ==> length xs = n \<and> length ys = n" |
1560 by (induct n) auto |
1583 by (induct n) auto |
1561 |
1584 |
1562 lemma wf_lex [intro!]: "wf r ==> wf (lex r)" |
1585 lemma wf_lex [intro!]: "wf r ==> wf (lex r)" |
1563 apply (unfold lex_def) |
1586 apply (unfold lex_def) |
1564 apply (rule wf_UN) |
1587 apply (rule wf_UN) |
1617 |
1640 |
1618 lemma sublist_nil [simp]: "sublist [] A = []" |
1641 lemma sublist_nil [simp]: "sublist [] A = []" |
1619 by (auto simp add: sublist_def) |
1642 by (auto simp add: sublist_def) |
1620 |
1643 |
1621 lemma sublist_shift_lemma: |
1644 lemma sublist_shift_lemma: |
1622 "map fst [p:zip xs [i..i + length xs(] . snd p : A] = |
1645 "map fst [p:zip xs [i..i + length xs(] . snd p : A] = |
1623 map fst [p:zip xs [0..length xs(] . snd p + i : A]" |
1646 map fst [p:zip xs [0..length xs(] . snd p + i : A]" |
1624 by (induct xs rule: rev_induct) (simp_all add: add_commute) |
1647 by (induct xs rule: rev_induct) (simp_all add: add_commute) |
1625 |
1648 |
1626 lemma sublist_append: |
1649 lemma sublist_append: |
1627 "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}" |
1650 "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}" |
1628 apply (unfold sublist_def) |
1651 apply (unfold sublist_def) |
1629 apply (induct l' rule: rev_induct, simp) |
1652 apply (induct l' rule: rev_induct, simp) |
1630 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma) |
1653 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma) |
1631 apply (simp add: add_commute) |
1654 apply (simp add: add_commute) |
1632 done |
1655 done |
1646 apply (simp split: nat_diff_split add: sublist_append) |
1669 apply (simp split: nat_diff_split add: sublist_append) |
1647 done |
1670 done |
1648 |
1671 |
1649 |
1672 |
1650 lemma take_Cons': |
1673 lemma take_Cons': |
1651 "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)" |
1674 "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)" |
1652 by (cases n) simp_all |
1675 by (cases n) simp_all |
1653 |
1676 |
1654 lemma drop_Cons': |
1677 lemma drop_Cons': |
1655 "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)" |
1678 "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)" |
1656 by (cases n) simp_all |
1679 by (cases n) simp_all |
1657 |
1680 |
1658 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))" |
1681 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))" |
1659 by (cases n) simp_all |
1682 by (cases n) simp_all |
1660 |
1683 |