Re: [isabelle] Non terminating function proven terminating



There is no bug here. "(% _ .  ()) (f ()) = ()", and "f x = ()" is
exactly what Isabelle defines. You can see that when you look at the thm
f.simps. You may complain that Isabelle beta-reduced the rhs of your
input string before it made the definition. You can hide the beta redex
by an explicit apply function, and then fun will no longer accept your
input.

The point is that your input string is transformed into a definition and
on the way it may get modified, and this is unavoidable. Beta-reduction
is one of the possible modifications. Disambiguation on pattern matching
is another.

Tobias


Am 21/10/2011 15:52, schrieb gallais @ ensl.org:
> Hi everyone,
> 
> I did not find Isabelle's bug tracker so I hope that this is the place where
> I'm supposed to report this.
> 
> Pierre Boutillier's trick (which breaks Coq's SN) seems to work in Isabelle.
> As in Agda, we do not lose SN but we do accept a function that is not
> well-defined.
> 
> ================================
> theory test
> imports Main
> 
> begin
> 
> fun f :: "unit \<Rightarrow> unit" where
>   "f x = (\<lambda> _ .  ()) (f ())"
> 
> lemma fail : "f () \<equiv> ()"
> by simp
> 
> end
> ================================
> 
> Cheers,
> 
> --
> gallais





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