Re: [isabelle] query about the isabelle tutorial slides



I received a query about conditional rewriting that may be of general
interest. Why does it "work" to make the lemma

lemma test1 [simp]: "Suc n < m ==> (n < m) = True"

a simp rule, despite the fact that the condition is bigger than the rhs, and
hence the simplifier should loop once it starts to use that lemmma?

There is a limit to the number of recursive invocations of the simplifier
(Isabedlle -> Settings -> Trace Simplifier Depth in ProofGeneral) with the
new (2005) default of 100. Hence the potential nontermination of test1 above
is simply aborted quite quickly.

By playing around with this limit (eg by including ML"simp_depth_limit := 10"
in your proof) you can use this feature in a controlled manner. However, it
is not recommended to make such nonterminating lemmas global simp rules as it
can greatly increase the search space for the simplifier.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.