Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 14:25):

From: "Li, Chanjuan" <lichanjuan04@gmail.com>
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^*";
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

Email Gateway (Aug 18 2022 at 14:25):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Last updated: Apr 27 2024 at 01:05 UTC