etc/lego/unsaved-goals.l


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

(* 
  Some test cases for closing off unsaved goals, 
  and the setting proof-completed-proof-behaviour.

  David Aspinall, November 1999.

  Things work fairly well in lego with 

       proof-completed-proof-behaviour='closeany

  In that case, undoing/redoing later declarations 
  (E and F) following the completed proof works okay, and
  in the absence of declarations, things work fine.
    
  Declarations in LEGO are global, and forgetting a
  declaration when a proof is still open (even if complete)
  aborts the proof!  So a proper handling would need to
  trigger a *further* retraction when the "Forget D" is
  issued undoing the definition of D.  Never mind.

  With proof-completed-proof-behaviour='closegoal or 'extend,
  undoing the first goal doesn't forget the declarations.

  This file even causes internal errors in LEGO!

     Warning: forgetting a finished proof

     LEGO detects unexpected exception named "InfixInternal"

  Test with undoing and redoing, and various settings
  for proof-completed-proof-behaviour
*)
   

Module unsaved Import lib_logic;

Goal {A,B:Prop}(and A B) -> (and B A);
intros;
Refine H;
intros;
andI;
Immed;
[D = Type];
[E = Type];
[F = Type];

Goal {A,B:Prop}(and A B) -> (and B A);
intros;
Refine H;
intros;
andI;
Immed;