Re: [isabelle] Type annotations



lemma works:
"[| ALL n1 n2. k n1 = k n2 --> n1 = n2;
     k x1 = k x2 |] ==> x1 = x2"

It works because k is inferred to have type 'a => 'b.

lemma fails:
"[| ALL n1 n2. (k :: obj => obj) n1 = (k :: obj => obj) n2 --> n1 = n2;
     k (x1::obj) = k (x2::obj) |] ==> (x1::obj) = (x2::obj)"

It fails because - by restricting the type - you have given the simplifier
the chance for an infinite recursive invocation of the conditional rewrite rule
k n1 = k n2 --> (n1 = n2) = True
This is simply stopped once simp_depth_limit is reached.

Tobias





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