src/HOL/List.thy
changeset 15113 fafcd72b9d4b
parent 15110 78b5636eabc7
child 15131 c69542757a4d
     1.1 --- a/src/HOL/List.thy	Wed Aug 04 19:12:15 2004 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Aug 05 10:50:58 2004 +0200
     1.3 @@ -235,13 +235,13 @@
     1.4    by induct blast+
     1.5  
     1.6  lemma lists_Int_eq [simp]: "lists (A \<inter> B) = lists A \<inter> lists B"
     1.7 -apply (rule mono_Int [THEN equalityI])
     1.8 -apply (simp add: mono_def lists_mono)
     1.9 -apply (blast intro!: lists_IntI)
    1.10 -done
    1.11 +proof (rule mono_Int [THEN equalityI])
    1.12 +  show "mono lists" by (simp add: mono_def lists_mono)
    1.13 +  show "lists A \<inter> lists B \<subseteq> lists (A \<inter> B)" by (blast intro: lists_IntI)
    1.14 +qed
    1.15  
    1.16  lemma append_in_lists_conv [iff]:
    1.17 -"(xs @ ys : lists A) = (xs : lists A \<and> ys : lists A)"
    1.18 +     "(xs @ ys : lists A) = (xs : lists A \<and> ys : lists A)"
    1.19  by (induct xs) auto
    1.20  
    1.21  
    1.22 @@ -620,12 +620,21 @@
    1.23  done
    1.24  
    1.25  lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)"
    1.26 -apply (induct xs, simp, simp)
    1.27 -apply (rule iffI)
    1.28 - apply (blast intro: eq_Nil_appendI Cons_eq_appendI)
    1.29 -apply (erule exE)+
    1.30 -apply (case_tac ys, auto)
    1.31 -done
    1.32 +proof (induct xs)
    1.33 +  case Nil show ?case by simp
    1.34 +  case (Cons a xs)
    1.35 +  show ?case
    1.36 +  proof 
    1.37 +    assume "x \<in> set (a # xs)"
    1.38 +    with prems show "\<exists>ys zs. a # xs = ys @ x # zs"
    1.39 +      by (simp, blast intro: Cons_eq_appendI)
    1.40 +  next
    1.41 +    assume "\<exists>ys zs. a # xs = ys @ x # zs"
    1.42 +    then obtain ys zs where eq: "a # xs = ys @ x # zs" by blast
    1.43 +    show "x \<in> set (a # xs)" 
    1.44 +      by (cases ys, auto simp add: eq)
    1.45 +  qed
    1.46 +qed
    1.47  
    1.48  lemma in_lists_conv_set: "(xs : lists A) = (\<forall>x \<in> set xs. x : A)"
    1.49  -- {* eliminate @{text lists} in favour of @{text set} *}