equal
deleted
inserted
replaced
39 sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) where |
39 sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) where |
40 "s1 ooo s2 = (case #s1 of |
40 "s1 ooo s2 = (case #s1 of |
41 Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2)) |
41 Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2)) |
42 | \<infinity> \<Rightarrow> s1)" |
42 | \<infinity> \<Rightarrow> s1)" |
43 |
43 |
44 consts |
44 primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" |
45 constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" |
45 where |
46 primrec |
|
47 constr_sconc'_0: "constr_sconc' 0 s1 s2 = s2" |
46 constr_sconc'_0: "constr_sconc' 0 s1 s2 = s2" |
48 constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 && |
47 | constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 && |
49 constr_sconc' n (rt$s1) s2" |
48 constr_sconc' n (rt$s1) s2" |
50 |
49 |
51 definition |
50 definition |
52 constr_sconc :: "'a stream => 'a stream => 'a stream" where (* constructive *) |
51 constr_sconc :: "'a stream => 'a stream => 'a stream" where (* constructive *) |
53 "constr_sconc s1 s2 = (case #s1 of |
52 "constr_sconc s1 s2 = (case #s1 of |