src/HOL/BNF_Examples/Stream.thy

--- a/src/HOL/BNF_Examples/Stream.thy	Mon Aug 18 17:20:14 2014 +0200
+++ b/src/HOL/BNF_Examples/Stream.thy	Mon Aug 18 18:48:39 2014 +0200
@@ -27,39 +27,14 @@
 
 hide_const (open) smember
 
-(* TODO: Provide by the package*)
-theorem sset_induct:
-  assumes Base: "\<And>s. P (shd s) s" and Step: "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s"
-  shows "\<forall>y \<in> sset s. P y s"
-proof (rule stream.dtor_set_induct)
-  fix a :: 'a and s :: "'a stream"
-  assume "a \<in> set1_pre_stream (dtor_stream s)"
-  then have "a = shd s"
-    by (cases "dtor_stream s")
-      (auto simp: BNF_Comp.id_bnf_comp_def shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def
-        split: stream.splits)
-  with Base show "P a s" by simp
-next
-  fix a :: 'a and s' :: "'a stream"  and s :: "'a stream"
-  assume "s' \<in> set2_pre_stream (dtor_stream s)" and prems: "a \<in> sset s'" "P a s'"
-  then have "s' = stl s"
-    by (cases "dtor_stream s")
-      (auto simp: BNF_Comp.id_bnf_comp_def stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def
-        split: stream.splits)
-  with Step prems show "P a s" by simp
-qed
-
 lemmas smap_simps[simp] = stream.map_sel
 lemmas shd_sset = stream.set_sel(1)
 lemmas stl_sset = stream.set_sel(2)
 
-(* only for the non-mutual case: *)
-theorem sset_induct1[consumes 1, case_names shd stl, induct set: "sset"]:
-  assumes "y \<in> sset s" and "\<And>s. P (shd s) s"
-  and "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s"
+theorem sset_induct[consumes 1, case_names shd stl, induct set: sset]:
+  assumes "y \<in> sset s" and "\<And>s. P (shd s) s" and "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s"
   shows "P y s"
-  using assms sset_induct by blast
-(* end TODO *)
+using assms by induct (metis stream.sel(1), auto)
 
 
 subsection {* prepend list to stream *}
@@ -456,7 +431,7 @@
   thus "x \<in> ?R" by (auto simp: sset_range dest!: nth_mem)
 next
   fix x xs assume "xs \<in> sset s" ?P "x \<in> set xs" thus "x \<in> ?L"
-    by (induct rule: sset_induct1)
+    by (induct rule: sset_induct)
       (metis UnI1 flat_unfold shift.simps(1) sset_shift,
        metis UnI2 flat_unfold shd_sset stl_sset sset_shift)
 qed