15 defaultsort type |
15 defaultsort type |
16 |
16 |
17 types 'a fstream = "'a lift stream" |
17 types 'a fstream = "'a lift stream" |
18 |
18 |
19 definition |
19 definition |
20 fscons :: "'a \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" |
20 fscons :: "'a \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where |
21 "fscons a = (\<Lambda> s. Def a && s)" |
21 "fscons a = (\<Lambda> s. Def a && s)" |
22 |
22 |
23 fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" |
23 definition |
|
24 fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where |
24 "fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))" |
25 "fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))" |
25 |
26 |
26 abbreviation |
27 abbreviation |
27 emptystream :: "'a fstream" ("<>") |
28 emptystream :: "'a fstream" ("<>") where |
28 "<> == \<bottom>" |
29 "<> == \<bottom>" |
29 |
30 |
30 fscons' :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_~>_)" [66,65] 65) |
31 abbreviation |
|
32 fscons' :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_~>_)" [66,65] 65) where |
31 "a~>s == fscons a\<cdot>s" |
33 "a~>s == fscons a\<cdot>s" |
32 |
34 |
33 fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63) |
35 abbreviation |
|
36 fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63) where |
34 "A(C)s == fsfilter A\<cdot>s" |
37 "A(C)s == fsfilter A\<cdot>s" |
35 |
38 |
36 notation (xsymbols) |
39 notation (xsymbols) |
37 fscons' ("(_\<leadsto>_)" [66,65] 65) |
40 fscons' ("(_\<leadsto>_)" [66,65] 65) and |
38 fsfilter' ("(_\<copyright>_)" [64,63] 63) |
41 fsfilter' ("(_\<copyright>_)" [64,63] 63) |
39 |
42 |
40 |
43 |
41 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d" |
44 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d" |
42 apply (rule flat_eq [THEN iffD1, symmetric]) |
45 apply (rule flat_eq [THEN iffD1, symmetric]) |