equal
deleted
inserted
replaced
233 lemma lists_IntI: |
233 lemma lists_IntI: |
234 assumes l: "l: lists A" shows "l: lists B ==> l: lists (A Int B)" using l |
234 assumes l: "l: lists A" shows "l: lists B ==> l: lists (A Int B)" using l |
235 by induct blast+ |
235 by induct blast+ |
236 |
236 |
237 lemma lists_Int_eq [simp]: "lists (A \<inter> B) = lists A \<inter> lists B" |
237 lemma lists_Int_eq [simp]: "lists (A \<inter> B) = lists A \<inter> lists B" |
238 apply (rule mono_Int [THEN equalityI]) |
238 proof (rule mono_Int [THEN equalityI]) |
239 apply (simp add: mono_def lists_mono) |
239 show "mono lists" by (simp add: mono_def lists_mono) |
240 apply (blast intro!: lists_IntI) |
240 show "lists A \<inter> lists B \<subseteq> lists (A \<inter> B)" by (blast intro: lists_IntI) |
241 done |
241 qed |
242 |
242 |
243 lemma append_in_lists_conv [iff]: |
243 lemma append_in_lists_conv [iff]: |
244 "(xs @ ys : lists A) = (xs : lists A \<and> ys : lists A)" |
244 "(xs @ ys : lists A) = (xs : lists A \<and> ys : lists A)" |
245 by (induct xs) auto |
245 by (induct xs) auto |
246 |
246 |
247 |
247 |
248 subsection {* @{text length} *} |
248 subsection {* @{text length} *} |
249 |
249 |
618 apply (induct j, simp_all) |
618 apply (induct j, simp_all) |
619 apply (erule ssubst, auto) |
619 apply (erule ssubst, auto) |
620 done |
620 done |
621 |
621 |
622 lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)" |
622 lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)" |
623 apply (induct xs, simp, simp) |
623 proof (induct xs) |
624 apply (rule iffI) |
624 case Nil show ?case by simp |
625 apply (blast intro: eq_Nil_appendI Cons_eq_appendI) |
625 case (Cons a xs) |
626 apply (erule exE)+ |
626 show ?case |
627 apply (case_tac ys, auto) |
627 proof |
628 done |
628 assume "x \<in> set (a # xs)" |
|
629 with prems show "\<exists>ys zs. a # xs = ys @ x # zs" |
|
630 by (simp, blast intro: Cons_eq_appendI) |
|
631 next |
|
632 assume "\<exists>ys zs. a # xs = ys @ x # zs" |
|
633 then obtain ys zs where eq: "a # xs = ys @ x # zs" by blast |
|
634 show "x \<in> set (a # xs)" |
|
635 by (cases ys, auto simp add: eq) |
|
636 qed |
|
637 qed |
629 |
638 |
630 lemma in_lists_conv_set: "(xs : lists A) = (\<forall>x \<in> set xs. x : A)" |
639 lemma in_lists_conv_set: "(xs : lists A) = (\<forall>x \<in> set xs. x : A)" |
631 -- {* eliminate @{text lists} in favour of @{text set} *} |
640 -- {* eliminate @{text lists} in favour of @{text set} *} |
632 by (induct xs) auto |
641 by (induct xs) auto |
633 |
642 |