author  huffman 
Mon, 27 Apr 2009 19:44:30 0700  
changeset 31008  b8f4e351b5bf 
parent 30158  83c50c62cf23 
child 33401  fc43fa403a69 
permissions  rwrr 
16554  1 
(* Title: HOLCF/ex/Fixrec_ex.thy 
2 
Author: Brian Huffman 

3 
*) 

4 

5 
header {* Fixrec package examples *} 

6 

7 
theory Fixrec_ex 

8 
imports HOLCF 

9 
begin 

10 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

11 
subsection {* Basic @{text fixrec} examples *} 
16554  12 

13 
text {* 

14 
Fixrec patterns can mention any constructor defined by the domain 

15 
package, as well as any of the following builtin constructors: 

16 
cpair, spair, sinl, sinr, up, ONE, TT, FF. 

17 
*} 

18 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

19 
text {* Typical usage is with lazy constructors. *} 
16554  20 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

21 
fixrec down :: "'a u \<rightarrow> 'a" 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

22 
where "down\<cdot>(up\<cdot>x) = x" 
16554  23 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

24 
text {* With strict constructors, rewrite rules may require side conditions. *} 
16554  25 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

26 
fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a" 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

27 
where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x" 
16554  28 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

29 
text {* Lifting can turn a strict constructor into a lazy one. *} 
16554  30 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

31 
fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a" 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

32 
where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x" 
16554  33 

34 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

35 
subsection {* Examples using @{text fixpat} *} 
16554  36 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

37 
text {* A type of lazy lists. *} 
16554  38 

39 
domain 'a llist = lNil  lCons (lazy 'a) (lazy "'a llist") 

40 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

41 
text {* A zip function for lazy lists. *} 
16554  42 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

43 
text {* Notice that the patterns are not exhaustive. *} 
16554  44 

45 
fixrec 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

46 
lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist" 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

47 
where 
16554  48 
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)" 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

49 
 "lzip\<cdot>lNil\<cdot>lNil = lNil" 
16554  50 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

51 
text {* @{text fixpat} is useful for producing strictness theorems. *} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

52 
text {* Note that pattern matching is done in lefttoright order. *} 
16554  53 

54 
fixpat lzip_stricts [simp]: 

55 
"lzip\<cdot>\<bottom>\<cdot>ys" 

56 
"lzip\<cdot>lNil\<cdot>\<bottom>" 

57 
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>" 

58 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

59 
text {* @{text fixpat} can also produce rules for missing cases. *} 
16554  60 

61 
fixpat lzip_undefs [simp]: 

62 
"lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)" 

63 
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil" 

64 

65 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

66 
subsection {* Pattern matching with bottoms *} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

67 

b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

68 
text {* 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

69 
As an alternative to using @{text fixpat}, it is also possible to 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

70 
use bottom as a constructor pattern. When using a bottom pattern, 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

71 
the righthandside must also be bottom; otherwise, @{text fixrec} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

72 
will not be able to prove the equation. 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

73 
*} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

74 

b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

75 
fixrec 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

76 
from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b" 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

77 
where 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

78 
"from_sinr_up\<cdot>\<bottom> = \<bottom>" 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

79 
 "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x" 
16554  80 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

81 
text {* 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

82 
If the function is already strict in that argument, then the bottom 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

83 
pattern does not change the meaning of the function. For example, 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

84 
in the definition of @{term from_sinr_up}, the first equation is 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

85 
actually redundant, and could have been proven separately by 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

86 
@{text fixpat}. 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

87 
*} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

88 

b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

89 
text {* 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

90 
A bottom pattern can also be used to make a function strict in a 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

91 
certain argument, similar to a bangpattern in Haskell. 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

92 
*} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

93 

b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

94 
fixrec 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

95 
seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

96 
where 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

97 
"seq\<cdot>\<bottom>\<cdot>y = \<bottom>" 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

98 
 "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y" 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

99 

b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

100 

b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

101 
subsection {* Skipping proofs of rewrite rules *} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

102 

b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

103 
text {* Another zip function for lazy lists. *} 
16554  104 

105 
text {* 

106 
Notice that this version has overlapping patterns. 

107 
The second equation cannot be proved as a theorem 

108 
because it only applies when the first pattern fails. 

109 
*} 

110 

111 
fixrec (permissive) 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

112 
lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist" 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

113 
where 
16554  114 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)" 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

115 
 "lzip2\<cdot>xs\<cdot>ys = lNil" 
16554  116 

117 
text {* 

118 
Usually fixrec tries to prove all equations as theorems. 

119 
The "permissive" option overrides this behavior, so fixrec 

120 
does not produce any simp rules. 

121 
*} 

122 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

123 
text {* Simp rules can be generated later using @{text fixpat}. *} 
16554  124 

125 
fixpat lzip2_simps [simp]: 

126 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)" 

127 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil" 

128 
"lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)" 

129 
"lzip2\<cdot>lNil\<cdot>lNil" 

130 

131 
fixpat lzip2_stricts [simp]: 

132 
"lzip2\<cdot>\<bottom>\<cdot>ys" 

133 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>" 

134 

135 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

136 
subsection {* Mutual recursion with @{text fixrec} *} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

137 

b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

138 
text {* Tree and forest types. *} 
16554  139 

140 
domain 'a tree = Leaf (lazy 'a)  Branch (lazy "'a forest") 

141 
and 'a forest = Empty  Trees (lazy "'a tree") "'a forest" 

142 

143 
text {* 

144 
To define mutually recursive functions, separate the equations 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

145 
for each function using the keyword @{text "and"}. 
16554  146 
*} 
147 

148 
fixrec 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

149 
map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)" 
16554  150 
and 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

151 
map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)" 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

152 
where 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

153 
"map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)" 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

154 
 "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)" 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

155 
 "map_forest\<cdot>f\<cdot>Empty = Empty" 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
16554
diff
changeset

156 
 "ts \<noteq> \<bottom> \<Longrightarrow> 
16554  157 
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)" 
158 

159 
fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>" 

160 
fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>" 

161 

162 
text {* 

163 
Theorems generated: 

31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

164 
@{text map_tree_def} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

165 
@{text map_forest_def} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

166 
@{text map_tree_unfold} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

167 
@{text map_forest_unfold} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

168 
@{text map_tree_simps} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

169 
@{text map_forest_simps} 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

170 
@{text map_tree_map_forest_induct} 
16554  171 
*} 
172 

173 
end 