1.1 --- a/src/HOLCF/ex/Fixrec_ex.thy	Wed May 19 13:07:15 2010 -0700
     1.2 +++ b/src/HOLCF/ex/Fixrec_ex.thy	Wed May 19 14:38:25 2010 -0700
     1.3 @@ -183,6 +183,49 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsection {* Looping simp rules *}
     1.8 +
     1.9 +text {*
    1.10 +  The defining equations of a fixrec definition are declared as simp
    1.11 +  rules by default.  In some cases, especially for constants with no
    1.12 +  arguments or functions with variable patterns, the defining
    1.13 +  equations may cause the simplifier to loop.  In these cases it will
    1.14 +  be necessary to use a @{text "[simp del]"} declaration.
    1.15 +*}
    1.16 +
    1.17 +fixrec
    1.18 +  repeat :: "'a \<rightarrow> 'a llist"
    1.19 +where
    1.20 +  [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
    1.21 +
    1.22 +text {*
    1.23 +  We can derive other non-looping simp rules for @{const repeat} by
    1.24 +  using the @{text subst} method with the @{text repeat.simps} rule.
    1.25 +*}
    1.26 +
    1.27 +lemma repeat_simps [simp]:
    1.28 +  "repeat\<cdot>x \<noteq> \<bottom>"
    1.29 +  "repeat\<cdot>x \<noteq> lNil"
    1.30 +  "repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
    1.31 +by (subst repeat.simps, simp)+
    1.32 +
    1.33 +lemma llist_when_repeat [simp]:
    1.34 +  "llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
    1.35 +by (subst repeat.simps, simp)
    1.36 +
    1.37 +text {*
    1.38 +  For mutually-recursive constants, looping might only occur if all
    1.39 +  equations are in the simpset at the same time.  In such cases it may
    1.40 +  only be necessary to declare @{text "[simp del]"} on one equation.
    1.41 +*}
    1.42 +
    1.43 +fixrec
    1.44 +  inf_tree :: "'a tree" and inf_forest :: "'a forest"
    1.45 +where
    1.46 +  [simp del]: "inf_tree = Branch\<cdot>inf_forest"
    1.47 +| "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
    1.48 +
    1.49 +
    1.50  subsection {* Using @{text fixrec} inside locales *}
    1.51  
    1.52  locale test =