src/HOL/BNF_Examples/Stream.thy
changeset 57986 0d60b9e58487
parent 57983 6edc3529bb4e
     1.1 --- a/src/HOL/BNF_Examples/Stream.thy	Mon Aug 18 17:20:14 2014 +0200
     1.2 +++ b/src/HOL/BNF_Examples/Stream.thy	Mon Aug 18 18:48:39 2014 +0200
     1.3 @@ -27,39 +27,14 @@
     1.4  
     1.5  hide_const (open) smember
     1.6  
     1.7 -(* TODO: Provide by the package*)
     1.8 -theorem sset_induct:
     1.9 -  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"
    1.10 -  shows "\<forall>y \<in> sset s. P y s"
    1.11 -proof (rule stream.dtor_set_induct)
    1.12 -  fix a :: 'a and s :: "'a stream"
    1.13 -  assume "a \<in> set1_pre_stream (dtor_stream s)"
    1.14 -  then have "a = shd s"
    1.15 -    by (cases "dtor_stream s")
    1.16 -      (auto simp: BNF_Comp.id_bnf_comp_def shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def
    1.17 -        split: stream.splits)
    1.18 -  with Base show "P a s" by simp
    1.19 -next
    1.20 -  fix a :: 'a and s' :: "'a stream"  and s :: "'a stream"
    1.21 -  assume "s' \<in> set2_pre_stream (dtor_stream s)" and prems: "a \<in> sset s'" "P a s'"
    1.22 -  then have "s' = stl s"
    1.23 -    by (cases "dtor_stream s")
    1.24 -      (auto simp: BNF_Comp.id_bnf_comp_def stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def
    1.25 -        split: stream.splits)
    1.26 -  with Step prems show "P a s" by simp
    1.27 -qed
    1.28 -
    1.29  lemmas smap_simps[simp] = stream.map_sel
    1.30  lemmas shd_sset = stream.set_sel(1)
    1.31  lemmas stl_sset = stream.set_sel(2)
    1.32  
    1.33 -(* only for the non-mutual case: *)
    1.34 -theorem sset_induct1[consumes 1, case_names shd stl, induct set: "sset"]:
    1.35 -  assumes "y \<in> sset s" and "\<And>s. P (shd s) s"
    1.36 -  and "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s"
    1.37 +theorem sset_induct[consumes 1, case_names shd stl, induct set: sset]:
    1.38 +  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"
    1.39    shows "P y s"
    1.40 -  using assms sset_induct by blast
    1.41 -(* end TODO *)
    1.42 +using assms by induct (metis stream.sel(1), auto)
    1.43  
    1.44  
    1.45  subsection {* prepend list to stream *}
    1.46 @@ -456,7 +431,7 @@
    1.47    thus "x \<in> ?R" by (auto simp: sset_range dest!: nth_mem)
    1.48  next
    1.49    fix x xs assume "xs \<in> sset s" ?P "x \<in> set xs" thus "x \<in> ?L"
    1.50 -    by (induct rule: sset_induct1)
    1.51 +    by (induct rule: sset_induct)
    1.52        (metis UnI1 flat_unfold shift.simps(1) sset_shift,
    1.53         metis UnI2 flat_unfold shd_sset stl_sset sset_shift)
    1.54  qed