66 by (case_tac [!] s) (auto simp: Stream_def stream.dtor_ctor) |
66 by (case_tac [!] s) (auto simp: Stream_def stream.dtor_ctor) |
67 |
67 |
68 declare stream.map[code] |
68 declare stream.map[code] |
69 |
69 |
70 theorem shd_sset: "shd s \<in> sset s" |
70 theorem shd_sset: "shd s \<in> sset s" |
|
71 sorry |
|
72 (* |
71 by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) |
73 by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) |
72 (metis UnCI fsts_def insertI1 stream.dtor_set) |
74 (metis UnCI fsts_def insertI1 stream.dtor_set) |
|
75 *) |
73 |
76 |
74 theorem stl_sset: "y \<in> sset (stl s) \<Longrightarrow> y \<in> sset s" |
77 theorem stl_sset: "y \<in> sset (stl s) \<Longrightarrow> y \<in> sset s" |
|
78 sorry |
|
79 (* |
75 by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) |
80 by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) |
76 (metis insertI1 set_mp snds_def stream.dtor_set_set_incl) |
81 (metis insertI1 set_mp snds_def stream.dtor_set_set_incl) |
|
82 *) |
77 |
83 |
78 (* only for the non-mutual case: *) |
84 (* only for the non-mutual case: *) |
79 theorem sset_induct1[consumes 1, case_names shd stl, induct set: "sset"]: |
85 theorem sset_induct1[consumes 1, case_names shd stl, induct set: "sset"]: |
80 assumes "y \<in> sset s" and "\<And>s. P (shd s) s" |
86 assumes "y \<in> sset s" and "\<And>s. P (shd s) s" |
81 and "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s" |
87 and "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s" |