author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42151  4da4fc77664b 
child 58880  0baae4311a9f 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Tutorial/Fixrec_ex.thy 
16554  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: 

35925  16 
Pair, spair, sinl, sinr, up, ONE, TT, FF. 
16554  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 

33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
31008
diff
changeset

34 
text {* Fixrec also works with the HOL pair constructor. *} 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
31008
diff
changeset

35 

fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
31008
diff
changeset

36 
fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b" 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
31008
diff
changeset

37 
where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)" 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
31008
diff
changeset

38 

16554  39 

33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

40 
subsection {* Examples using @{text fixrec_simp} *} 
16554  41 

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

42 
text {* A type of lazy lists. *} 
16554  43 

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

45 

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

46 
text {* A zip function for lazy lists. *} 
16554  47 

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

48 
text {* Notice that the patterns are not exhaustive. *} 
16554  49 

50 
fixrec 

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

51 
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

52 
where 
35925  53 
"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

54 
 "lzip\<cdot>lNil\<cdot>lNil = lNil" 
16554  55 

33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

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

57 
text {* Note that pattern matching is done in lefttoright order. *} 
16554  58 

33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

59 
lemma lzip_stricts [simp]: 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

60 
"lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

61 
"lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

62 
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

63 
by fixrec_simp+ 
16554  64 

33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

65 
text {* @{text fixrec_simp} can also produce rules for missing cases. *} 
16554  66 

33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

67 
lemma lzip_undefs [simp]: 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

68 
"lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

69 
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

70 
by fixrec_simp+ 
16554  71 

72 

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

73 
subsection {* Pattern matching with bottoms *} 
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 
text {* 
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

76 
As an alternative to using @{text fixrec_simp}, it is also possible 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

77 
to use bottom as a constructor pattern. When using a bottom 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

78 
pattern, the righthandside must also be bottom; otherwise, @{text 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

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

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

81 

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

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

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

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

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

86 
 "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x" 
16554  87 

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

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

89 
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

90 
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

91 
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

92 
actually redundant, and could have been proven separately by 
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

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

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

95 

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

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

97 
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

98 
certain argument, similar to a bangpattern in Haskell. 
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 
fixrec 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30158
diff
changeset

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

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

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

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

106 

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

107 

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

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

109 

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

110 
text {* Another zip function for lazy lists. *} 
16554  111 

112 
text {* 

113 
Notice that this version has overlapping patterns. 

114 
The second equation cannot be proved as a theorem 

115 
because it only applies when the first pattern fails. 

116 
*} 

117 

40041
1f09b4c7b85e
replace fixrec 'permissive' mode with perequation 'unchecked' option
huffman
parents:
37000
diff
changeset

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

119 
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

120 
where 
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with perequation 'unchecked' option
huffman
parents:
37000
diff
changeset

121 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip2\<cdot>xs\<cdot>ys)" 
1f09b4c7b85e
replace fixrec 'permissive' mode with perequation 'unchecked' option
huffman
parents:
37000
diff
changeset

122 
 (unchecked) "lzip2\<cdot>xs\<cdot>ys = lNil" 
16554  123 

124 
text {* 

125 
Usually fixrec tries to prove all equations as theorems. 

40041
1f09b4c7b85e
replace fixrec 'permissive' mode with perequation 'unchecked' option
huffman
parents:
37000
diff
changeset

126 
The "unchecked" option overrides this behavior, so fixrec 
1f09b4c7b85e
replace fixrec 'permissive' mode with perequation 'unchecked' option
huffman
parents:
37000
diff
changeset

127 
does not attempt to prove that particular equation. 
16554  128 
*} 
129 

33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

130 
text {* Simp rules can be generated later using @{text fixrec_simp}. *} 
16554  131 

33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

132 
lemma lzip2_simps [simp]: 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

133 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

134 
"lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

135 
"lzip2\<cdot>lNil\<cdot>lNil = lNil" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

136 
by fixrec_simp+ 
16554  137 

33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

138 
lemma lzip2_stricts [simp]: 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

139 
"lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

140 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

141 
by fixrec_simp+ 
16554  142 

143 

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

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

145 

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

146 
text {* Tree and forest types. *} 
16554  147 

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

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

150 

151 
text {* 

35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

152 
To define mutually recursive functions, give multiple type signatures 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

153 
separated by the keyword @{text "and"}. 
16554  154 
*} 
155 

156 
fixrec 

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

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

159 
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

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

161 
"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

162 
 "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

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

164 
 "ts \<noteq> \<bottom> \<Longrightarrow> 
16554  165 
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)" 
166 

33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

167 
lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

168 
by fixrec_simp 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

169 

70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

170 
lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>" 
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset

171 
by fixrec_simp 
16554  172 

37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36997
diff
changeset

173 
(* 
16554  174 
Theorems generated: 
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

175 
@{text map_tree_def} @{thm map_tree_def} 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

176 
@{text map_forest_def} @{thm map_forest_def} 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

177 
@{text map_tree.unfold} @{thm map_tree.unfold} 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

178 
@{text map_forest.unfold} @{thm map_forest.unfold} 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

179 
@{text map_tree.simps} @{thm map_tree.simps} 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

180 
@{text map_forest.simps} @{thm map_forest.simps} 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

181 
@{text map_tree_map_forest.induct} @{thm map_tree_map_forest.induct} 
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36997
diff
changeset

182 
*) 
16554  183 

35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

184 

36997
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

185 
subsection {* Looping simp rules *} 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

186 

ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

187 
text {* 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

188 
The defining equations of a fixrec definition are declared as simp 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

189 
rules by default. In some cases, especially for constants with no 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

190 
arguments or functions with variable patterns, the defining 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

191 
equations may cause the simplifier to loop. In these cases it will 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

192 
be necessary to use a @{text "[simp del]"} declaration. 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

193 
*} 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

194 

ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

195 
fixrec 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

196 
repeat :: "'a \<rightarrow> 'a llist" 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

197 
where 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

198 
[simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)" 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

199 

ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

200 
text {* 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

201 
We can derive other nonlooping simp rules for @{const repeat} by 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

202 
using the @{text subst} method with the @{text repeat.simps} rule. 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

203 
*} 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

204 

ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

205 
lemma repeat_simps [simp]: 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

206 
"repeat\<cdot>x \<noteq> \<bottom>" 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

207 
"repeat\<cdot>x \<noteq> lNil" 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

208 
"repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys" 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

209 
by (subst repeat.simps, simp)+ 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

210 

40213
b63e966564da
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents:
40041
diff
changeset

211 
lemma llist_case_repeat [simp]: 
b63e966564da
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents:
40041
diff
changeset

212 
"llist_case\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)" 
36997
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

213 
by (subst repeat.simps, simp) 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

214 

ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

215 
text {* 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

216 
For mutuallyrecursive constants, looping might only occur if all 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

217 
equations are in the simpset at the same time. In such cases it may 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

218 
only be necessary to declare @{text "[simp del]"} on one equation. 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

219 
*} 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

220 

ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

221 
fixrec 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

222 
inf_tree :: "'a tree" and inf_forest :: "'a forest" 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

223 
where 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

224 
[simp del]: "inf_tree = Branch\<cdot>inf_forest" 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

225 
 "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)" 
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

226 

ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset

227 

35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

228 
subsection {* Using @{text fixrec} inside locales *} 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

229 

a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

230 
locale test = 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

231 
fixes foo :: "'a \<rightarrow> 'a" 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

232 
assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>" 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

233 
begin 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

234 

a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

235 
fixrec 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

236 
bar :: "'a u \<rightarrow> 'a" 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

237 
where 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

238 
"bar\<cdot>(up\<cdot>x) = foo\<cdot>x" 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

239 

a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

240 
lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>" 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

241 
by fixrec_simp 
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

242 

16554  243 
end 
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

244 

a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset

245 
end 