--- a/src/HOLCF/ex/Fixrec_ex.thy Wed May 19 13:07:15 2010 -0700
+++ b/src/HOLCF/ex/Fixrec_ex.thy Wed May 19 14:38:25 2010 -0700
@@ -183,6 +183,49 @@
*}
+subsection {* Looping simp rules *}
+
+text {*
+ The defining equations of a fixrec definition are declared as simp
+ rules by default. In some cases, especially for constants with no
+ arguments or functions with variable patterns, the defining
+ equations may cause the simplifier to loop. In these cases it will
+ be necessary to use a @{text "[simp del]"} declaration.
+*}
+
+fixrec
+ repeat :: "'a \<rightarrow> 'a llist"
+where
+ [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
+
+text {*
+ We can derive other non-looping simp rules for @{const repeat} by
+ using the @{text subst} method with the @{text repeat.simps} rule.
+*}
+
+lemma repeat_simps [simp]:
+ "repeat\<cdot>x \<noteq> \<bottom>"
+ "repeat\<cdot>x \<noteq> lNil"
+ "repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
+by (subst repeat.simps, simp)+
+
+lemma llist_when_repeat [simp]:
+ "llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
+by (subst repeat.simps, simp)
+
+text {*
+ For mutually-recursive constants, looping might only occur if all
+ equations are in the simpset at the same time. In such cases it may
+ only be necessary to declare @{text "[simp del]"} on one equation.
+*}
+
+fixrec
+ inf_tree :: "'a tree" and inf_forest :: "'a forest"
+where
+ [simp del]: "inf_tree = Branch\<cdot>inf_forest"
+| "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
+
+
subsection {* Using @{text fixrec} inside locales *}
locale test =