Re: [isabelle] blast works incretable slow at tty mode



Li, Chanjuan wrote:
> hi,all:
>    I use isabelle in tty mode instead of emacs for my gentoo machine
> update the emacs to 23, isabelle can not work well with emacs 23.
> today I duplicate a simple example of tutorial of isabelle as follows:
> $ isabelle tty -l HOL 
> 
>> lemma "(x,y) : (-r)^* ==> (y,x) : r^*";

Your problem is that this is not a theorem. You mistyped it: instead of
-r it should be r^-1.

If you were using Isabelle2009-1 via emacs I would recommend to switch
on Auto Nitpick (under Isabelle > Settings). It would have found a
counterexample right away, automatically.

Tobias

> proof (prove): step 0
> 
> goal (1 subgoal):
>  1. (x, y) : (- r)^* ==> (y, x) : r^*
> 
>> apply(erule rtrancl_induct);
> 
> proof (prove): step 1
> 
> goal (2 subgoals):
>  1. (x, x) : r^*
>  2. !!y z.
>        [| (x, y) : (- r)^*; (y, z) : - r; (y, x) : r^* |] ==> (z, x) :
> r^*
> 
>> apply(rule rtrancl_refl);
> proof (prove): step 2
> 
> goal (1 subgoal):
>  1. !!y z.
>        [| (x, y) : (- r)^*; (y, z) : - r; (y, x) : r^* |] ==> (z, x) :
> r^*
>> apply(blast intro: rtrancl_trans);
> Search depth = 0
> Search depth = 1
> Search depth = 2
> Search depth = 3
> Search depth = 4
> Search depth = 5
> 
> it seems the proof procedure stalled. I wait for about 20 minutes, there
> is nothing happened. I use isabelle2009  and polyml-5.2.1.
> Is anyone know the reason blast stalled? thanks for helping me.
> 
> 
> lily
> 
> 
> 
> 






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