35 sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) |
35 sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) |
36 constr_sconc :: "'a stream => 'a stream => 'a stream" (* constructive *) |
36 constr_sconc :: "'a stream => 'a stream => 'a stream" (* constructive *) |
37 constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" |
37 constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" |
38 |
38 |
39 defs |
39 defs |
40 i_rt_def: "i_rt == %i s. iterate i rt s" |
40 i_rt_def: "i_rt == %i s. iterate i$rt$s" |
41 i_th_def: "i_th == %i s. ft$(i_rt i s)" |
41 i_th_def: "i_th == %i s. ft$(i_rt i s)" |
42 |
42 |
43 sconc_def: "s1 ooo s2 == case #s1 of |
43 sconc_def: "s1 ooo s2 == case #s1 of |
44 Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2)) |
44 Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2)) |
45 | \<infinity> \<Rightarrow> s1" |
45 | \<infinity> \<Rightarrow> s1" |
134 by auto |
134 by auto |
135 |
135 |
136 lemma surjectiv_scons: "(ft$s)&&(rt$s)=s" |
136 lemma surjectiv_scons: "(ft$s)&&(rt$s)=s" |
137 by (rule stream.casedist [of s], auto) |
137 by (rule stream.casedist [of s], auto) |
138 |
138 |
139 lemma monofun_rt_mult: "x << s ==> iterate i rt x << iterate i rt s" |
139 lemma monofun_rt_mult: "x << s ==> iterate i$rt$x << iterate i$rt$s" |
140 by (insert monofun_iterate2 [of i "rt"], simp add: monofun_def, auto) |
140 by (rule monofun_cfun_arg) |
141 |
141 |
142 |
142 |
143 |
143 |
144 (* ----------------------------------------------------------------------- *) |
144 (* ----------------------------------------------------------------------- *) |
145 (* theorems about stream_take *) |
145 (* theorems about stream_take *) |
150 |
150 |
151 |
151 |
152 lemma stream_reach2: "(LUB i. stream_take i$s) = s" |
152 lemma stream_reach2: "(LUB i. stream_take i$s) = s" |
153 apply (insert stream.reach [of s], erule subst) back |
153 apply (insert stream.reach [of s], erule subst) back |
154 apply (simp add: fix_def2 stream.take_def) |
154 apply (simp add: fix_def2 stream.take_def) |
155 apply (insert contlub_cfun_fun [of "%i. iterate i stream_copy UU" s,THEN sym]) |
155 apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym]) |
156 by (simp add: chain_iterate) |
156 by (simp add: chain_iterate) |
157 |
157 |
158 lemma chain_stream_take: "chain (%i. stream_take i$s)" |
158 lemma chain_stream_take: "chain (%i. stream_take i$s)" |
159 apply (rule chainI) |
159 apply (rule chainI) |
160 apply (rule monofun_cfun_fun) |
160 apply (rule monofun_cfun_fun) |
468 apply (frule stream_finite_less) |
468 apply (frule stream_finite_less) |
469 apply (erule_tac x="s" in allE, simp) |
469 apply (erule_tac x="s" in allE, simp) |
470 apply (drule slen_mono_lemma, auto) |
470 apply (drule slen_mono_lemma, auto) |
471 by (simp add: slen_def) |
471 by (simp add: slen_def) |
472 |
472 |
473 lemma iterate_lemma: "F$(iterate n F x) = iterate n F (F$x)" |
473 lemma iterate_lemma: "F$(iterate n$F$x) = iterate n$F$(F$x)" |
474 by (insert iterate_Suc2 [of n F x], auto) |
474 by (insert iterate_Suc2 [of n F x], auto) |
475 |
475 |
476 lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i rt x)" |
476 lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i$rt$x)" |
477 apply (induct_tac i, auto) |
477 apply (induct_tac i, auto) |
478 apply (case_tac "x=UU", auto) |
478 apply (case_tac "x=UU", auto) |
479 apply (simp add: inat_defs) |
479 apply (simp add: inat_defs) |
480 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
480 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
481 apply (erule_tac x="y" in allE, auto) |
481 apply (erule_tac x="y" in allE, auto) |
968 |
968 |
969 lemma contlub_sconc_lemma: |
969 lemma contlub_sconc_lemma: |
970 "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" |
970 "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" |
971 apply (case_tac "#x=Infty") |
971 apply (case_tac "#x=Infty") |
972 apply (simp add: sconc_def) |
972 apply (simp add: sconc_def) |
973 prefer 2 |
973 apply (drule finite_lub_sconc,auto simp add: slen_infinite) |
974 apply (drule finite_lub_sconc,auto simp add: slen_infinite) |
974 done |
975 apply (simp add: slen_def) |
|
976 apply (insert lub_const [of x] unique_lub [of _ x _]) |
|
977 by (auto simp add: lub) |
|
978 |
975 |
979 lemma contlub_sconc: "contlub (%y. x ooo y)" |
976 lemma contlub_sconc: "contlub (%y. x ooo y)" |
980 by (rule contlubI, insert contlub_sconc_lemma [of _ x], simp) |
977 by (rule contlubI, insert contlub_sconc_lemma [of _ x], simp) |
981 |
978 |
982 lemma monofun_sconc: "monofun (%y. x ooo y)" |
979 lemma monofun_sconc: "monofun (%y. x ooo y)" |