17 cpair, spair, sinl, sinr, up, ONE, TT, FF. |
16 cpair, spair, sinl, sinr, up, ONE, TT, FF. |
18 *} |
17 *} |
19 |
18 |
20 text {* typical usage is with lazy constructors *} |
19 text {* typical usage is with lazy constructors *} |
21 |
20 |
22 consts down :: "'a u \<rightarrow> 'a" |
21 fixrec down :: "'a u \<rightarrow> 'a" |
23 fixrec "down\<cdot>(up\<cdot>x) = x" |
22 where "down\<cdot>(up\<cdot>x) = x" |
24 |
23 |
25 text {* with strict constructors, rewrite rules may require side conditions *} |
24 text {* with strict constructors, rewrite rules may require side conditions *} |
26 |
25 |
27 consts from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a" |
26 fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a" |
28 fixrec "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x" |
27 where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x" |
29 |
28 |
30 text {* lifting can turn a strict constructor into a lazy one *} |
29 text {* lifting can turn a strict constructor into a lazy one *} |
31 |
30 |
32 consts from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a" |
31 fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a" |
33 fixrec "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x" |
32 where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x" |
34 |
33 |
35 |
34 |
36 subsection {* fixpat examples *} |
35 subsection {* fixpat examples *} |
37 |
36 |
38 text {* a type of lazy lists *} |
37 text {* a type of lazy lists *} |
39 |
38 |
40 domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist") |
39 domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist") |
41 |
40 |
42 text {* zip function for lazy lists *} |
41 text {* zip function for lazy lists *} |
43 |
42 |
44 consts lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist" |
|
45 |
|
46 text {* notice that the patterns are not exhaustive *} |
43 text {* notice that the patterns are not exhaustive *} |
47 |
44 |
48 fixrec |
45 fixrec |
|
46 lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist" |
|
47 where |
49 "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)" |
48 "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)" |
50 "lzip\<cdot>lNil\<cdot>lNil = lNil" |
49 | "lzip\<cdot>lNil\<cdot>lNil = lNil" |
51 |
50 |
52 text {* fixpat is useful for producing strictness theorems *} |
51 text {* fixpat is useful for producing strictness theorems *} |
53 text {* note that pattern matching is done in left-to-right order *} |
52 text {* note that pattern matching is done in left-to-right order *} |
54 |
53 |
55 fixpat lzip_stricts [simp]: |
54 fixpat lzip_stricts [simp]: |
66 |
65 |
67 subsection {* skipping proofs of rewrite rules *} |
66 subsection {* skipping proofs of rewrite rules *} |
68 |
67 |
69 text {* another zip function for lazy lists *} |
68 text {* another zip function for lazy lists *} |
70 |
69 |
71 consts lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist" |
|
72 |
|
73 text {* |
70 text {* |
74 Notice that this version has overlapping patterns. |
71 Notice that this version has overlapping patterns. |
75 The second equation cannot be proved as a theorem |
72 The second equation cannot be proved as a theorem |
76 because it only applies when the first pattern fails. |
73 because it only applies when the first pattern fails. |
77 *} |
74 *} |
78 |
75 |
79 fixrec (permissive) |
76 fixrec (permissive) |
|
77 lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist" |
|
78 where |
80 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)" |
79 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)" |
81 "lzip2\<cdot>xs\<cdot>ys = lNil" |
80 | "lzip2\<cdot>xs\<cdot>ys = lNil" |
82 |
81 |
83 text {* |
82 text {* |
84 Usually fixrec tries to prove all equations as theorems. |
83 Usually fixrec tries to prove all equations as theorems. |
85 The "permissive" option overrides this behavior, so fixrec |
84 The "permissive" option overrides this behavior, so fixrec |
86 does not produce any simp rules. |
85 does not produce any simp rules. |
103 text {* tree and forest types *} |
102 text {* tree and forest types *} |
104 |
103 |
105 domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest") |
104 domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest") |
106 and 'a forest = Empty | Trees (lazy "'a tree") "'a forest" |
105 and 'a forest = Empty | Trees (lazy "'a tree") "'a forest" |
107 |
106 |
108 consts |
|
109 map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)" |
|
110 map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)" |
|
111 |
|
112 text {* |
107 text {* |
113 To define mutually recursive functions, separate the equations |
108 To define mutually recursive functions, separate the equations |
114 for each function using the keyword "and". |
109 for each function using the keyword "and". |
115 *} |
110 *} |
116 |
111 |
117 fixrec |
112 fixrec |
|
113 map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)" |
|
114 and |
|
115 map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)" |
|
116 where |
118 "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)" |
117 "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)" |
119 "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)" |
118 | "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)" |
120 and |
119 | "map_forest\<cdot>f\<cdot>Empty = Empty" |
121 "map_forest\<cdot>f\<cdot>Empty = Empty" |
120 | "ts \<noteq> \<bottom> \<Longrightarrow> |
122 "ts \<noteq> \<bottom> \<Longrightarrow> |
|
123 map_forest\<cdot>f\<cdot>(Trees\<cdot>t\<cdot>ts) = Trees\<cdot>(map_tree\<cdot>f\<cdot>t)\<cdot>(map_forest\<cdot>f\<cdot>ts)" |
121 map_forest\<cdot>f\<cdot>(Trees\<cdot>t\<cdot>ts) = Trees\<cdot>(map_tree\<cdot>f\<cdot>t)\<cdot>(map_forest\<cdot>f\<cdot>ts)" |
124 |
122 |
125 fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>" |
123 fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>" |
126 fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>" |
124 fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>" |
127 |
125 |