# HG changeset patch
# User paulson
# Date 1091695858 -7200
# Node ID fafcd72b9d4b9fb7bce8811ca1e7cab02007a88b
# Parent  6f0772a942993170fc453730be66c475b95fc531
some structured proofs

diff -r 6f0772a94299 -r fafcd72b9d4b src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 04 19:12:15 2004 +0200
+++ b/src/HOL/List.thy	Thu Aug 05 10:50:58 2004 +0200
@@ -235,13 +235,13 @@
   by induct blast+
 
 lemma lists_Int_eq [simp]: "lists (A \<inter> B) = lists A \<inter> lists B"
-apply (rule mono_Int [THEN equalityI])
-apply (simp add: mono_def lists_mono)
-apply (blast intro!: lists_IntI)
-done
+proof (rule mono_Int [THEN equalityI])
+  show "mono lists" by (simp add: mono_def lists_mono)
+  show "lists A \<inter> lists B \<subseteq> lists (A \<inter> B)" by (blast intro: lists_IntI)
+qed
 
 lemma append_in_lists_conv [iff]:
-"(xs @ ys : lists A) = (xs : lists A \<and> ys : lists A)"
+     "(xs @ ys : lists A) = (xs : lists A \<and> ys : lists A)"
 by (induct xs) auto
 
 
@@ -620,12 +620,21 @@
 done
 
 lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)"
-apply (induct xs, simp, simp)
-apply (rule iffI)
- apply (blast intro: eq_Nil_appendI Cons_eq_appendI)
-apply (erule exE)+
-apply (case_tac ys, auto)
-done
+proof (induct xs)
+  case Nil show ?case by simp
+  case (Cons a xs)
+  show ?case
+  proof 
+    assume "x \<in> set (a # xs)"
+    with prems show "\<exists>ys zs. a # xs = ys @ x # zs"
+      by (simp, blast intro: Cons_eq_appendI)
+  next
+    assume "\<exists>ys zs. a # xs = ys @ x # zs"
+    then obtain ys zs where eq: "a # xs = ys @ x # zs" by blast
+    show "x \<in> set (a # xs)" 
+      by (cases ys, auto simp add: eq)
+  qed
+qed
 
 lemma in_lists_conv_set: "(xs : lists A) = (\<forall>x \<in> set xs. x : A)"
 -- {* eliminate @{text lists} in favour of @{text set} *}