examples made separate dirs;
authorwenzelm
Fri Feb 05 21:14:17 1999 +0100 (1999-02-05)
changeset 6252935f183bf406
parent 6251 4d89d4f0ab17
child 6253 dbaf79ac2ff9
examples made separate dirs;
src/Sequents/ILL/ILL_kleene_lemmas.ML
src/Sequents/ILL/ILL_predlog.ML
src/Sequents/ILL/ILL_predlog.thy
src/Sequents/ILL/ROOT.ML
src/Sequents/ILL/washing.ML
src/Sequents/ILL/washing.thy
src/Sequents/IsaMakefile
src/Sequents/LK/ROOT.ML
src/Sequents/LK/hardquant.ML
src/Sequents/LK/prop.ML
src/Sequents/LK/quant.ML
src/Sequents/Modal/ROOT.ML
src/Sequents/Modal/S43thms.ML
src/Sequents/Modal/S4thms.ML
src/Sequents/Modal/Tthms.ML
src/Sequents/ex/ILL/ILL_kleene_lemmas.ML
src/Sequents/ex/ILL/ILL_predlog.ML
src/Sequents/ex/ILL/ILL_predlog.thy
src/Sequents/ex/ILL/ROOT.ML
src/Sequents/ex/ILL/washing.ML
src/Sequents/ex/ILL/washing.thy
src/Sequents/ex/LK/ROOT.ML
src/Sequents/ex/LK/hardquant.ML
src/Sequents/ex/LK/prop.ML
src/Sequents/ex/LK/quant.ML
src/Sequents/ex/Modal/ROOT.ML
src/Sequents/ex/Modal/S43thms.ML
src/Sequents/ex/Modal/S4thms.ML
src/Sequents/ex/Modal/Tthms.ML
src/Sequents/ex/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Sequents/ILL/ILL_kleene_lemmas.ML	Fri Feb 05 21:14:17 1999 +0100
     1.3 @@ -0,0 +1,81 @@
     1.4 +
     1.5 +(* from [kleene 52] pp 118,119 *)
     1.6 +
     1.7 +
     1.8 +val k49a = auto1 "|- [* A > ( - ( - A)) *]";
     1.9 +
    1.10 +val k49b = auto1 "|- [*( - ( - ( - A))) = ( - A)*]";
    1.11 +
    1.12 +val k49c = auto1 "|- [* (A | - A) > ( - - A = A) *]";
    1.13 +
    1.14 +val k50a = auto2 "|- [* - (A = - A) *]";
    1.15 +
    1.16 +(*
    1.17 +         [rtac impr_contract 1 THEN REPEAT (rtac conj_lemma 1),
    1.18 +	  res_inst_tac [("A","!((! A) -o 0)")] cut 1
    1.19 +	  THEN rtac context1 1
    1.20 +	  THEN ALLGOALS (best_tac power_cs)]);
    1.21 +*)
    1.22 +
    1.23 +val k51a = auto2 "|- [* - - (A | - A) *]";
    1.24 +    
    1.25 +val k51b = auto2 "|- [* - - (- - A > A) *]";
    1.26 +    
    1.27 +val k56a = auto1 "|- [* (A | B) > - (- A & - B) *]";
    1.28 +
    1.29 +val k56b = auto1 "|- [* (-A | B) > - (A & -B) *]";
    1.30 +    
    1.31 +val k57a = auto1 "|- [* (A & B) > - (-A | -B) *]";
    1.32 +    
    1.33 +val k57b = auto2 "|- [* (A & -B) > -(-A | B) *]";
    1.34 +    
    1.35 +val k58a = auto1 "|- [* (A > B) > - (A & -B) *]";
    1.36 +    
    1.37 +val k58b = auto1 "|- [* (A > -B) = -(A & B) *]";
    1.38 +    
    1.39 +val k58c = auto1 "|- [* - (A & B) = (- - A > - B) *]";
    1.40 +    
    1.41 +val k58d = auto1 "|- [* (- - A > - B) = - - (-A | -B) *]";
    1.42 +    
    1.43 +val k58e = auto1 "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]";
    1.44 +    
    1.45 +val k58f = auto1 "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]";
    1.46 +    
    1.47 +val k58g = auto1 "|- [* (- -A > B) > - (A & -B) *]";
    1.48 +    
    1.49 +val k59a = auto1 "|- [* (-A | B) > (A > B) *]";
    1.50 +
    1.51 +val k59b = auto2 "|- [* (A > B) > - - (-A | B) *]";
    1.52 +    
    1.53 +val k59c = auto2 "|- [* (-A > B) > - -(A | B) *]";
    1.54 +    
    1.55 +val k60a = auto1 "|- [* (A & B) > - (A > -B) *]";
    1.56 +    
    1.57 +val k60b = auto1 "|- [* (A & -B) > - (A > B) *]";
    1.58 +    
    1.59 +val k60c = auto1 "|- [* ( - - A & B) > - (A > -B) *]";
    1.60 +    
    1.61 +val k60d = auto1 "|- [* (- - A & - B) = - (A > B) *]";
    1.62 +    
    1.63 +val k60e = auto1 "|- [* - (A > B) = - (-A | B) *]";
    1.64 +    
    1.65 +val k60f = auto1 "|- [* - (-A | B) = - - (A & -B) *]";
    1.66 +    
    1.67 +val k60g = auto2 "|- [* - - (A > B) = - (A & -B) *]";
    1.68 +    
    1.69 +(*
    1.70 + [step_tac safe_cs 1, best_tac safe_cs 1,
    1.71 + rtac impr 1 THEN rtac impr_contract 1
    1.72 + THEN best_tac safe_cs 1];
    1.73 +*)
    1.74 +
    1.75 +val k60h = auto1 "|- [* - (A & -B) = (A > - -B) *]";
    1.76 +
    1.77 +val k60i = auto1 "|- [* (A > - -B) = (- -A > - -B) *]";
    1.78 +
    1.79 +val k61a = auto1 "|- [* (A | B) > (-A > B) *]";
    1.80 +
    1.81 +val k61b = auto2 "|- [* - (A | B) = - (-A > B) *]";
    1.82 +
    1.83 +val k62a = auto1 "|- [* (-A | -B) > - (A & B) *]";
    1.84 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Sequents/ILL/ILL_predlog.ML	Fri Feb 05 21:14:17 1999 +0100
     2.3 @@ -0,0 +1,9 @@
     2.4 +
     2.5 +open ILL_predlog;
     2.6 +
     2.7 +
     2.8 +fun auto1 x = prove_goal thy x
     2.9 + (fn prems => [best_tac safe_cs 1]) ;
    2.10 +
    2.11 +fun auto2 x = prove_goal thy x
    2.12 + (fn prems => [best_tac power_cs 1]) ;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Sequents/ILL/ILL_predlog.thy	Fri Feb 05 21:14:17 1999 +0100
     3.3 @@ -0,0 +1,42 @@
     3.4 +(* 
     3.5 +    File:	 /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy
     3.6 +    Theory Name: pred_log
     3.7 +    Logic Image: HOL
     3.8 +*)
     3.9 +
    3.10 +ILL_predlog  =  ILL +
    3.11 +
    3.12 +types
    3.13 +
    3.14 +    plf
    3.15 +    
    3.16 +arities
    3.17 +
    3.18 +    plf :: logic
    3.19 +    
    3.20 +consts
    3.21 +
    3.22 +  "&"   :: "[plf,plf] => plf"   (infixr 35)
    3.23 +  "|"   :: "[plf,plf] => plf"   (infixr 35)
    3.24 +  ">"   :: "[plf,plf] => plf"   (infixr 35)
    3.25 +  "="   :: "[plf,plf] => plf"   (infixr 35)
    3.26 +  "@NG" :: "plf => plf"   ("- _ " [50] 55)
    3.27 +  ff    :: "plf"
    3.28 +  
    3.29 +  PL    :: "plf => o"      ("[* / _ / *]" [] 100)
    3.30 +
    3.31 +
    3.32 +translations
    3.33 +
    3.34 +  "[* A & B *]" == "[*A*] && [*B*]" 
    3.35 +  "[* A | B *]" == "![*A*] ++ ![*B*]"
    3.36 +  "[* - A *]"   == "[*A > ff*]"
    3.37 +  "[* ff *]"    == "0"
    3.38 +  "[* A = B *]" => "[* (A > B) & (B > A) *]"
    3.39 +  
    3.40 +  "[* A > B *]" == "![*A*] -o [*B*]"
    3.41 +  
    3.42 +(* another translations for linear implication:
    3.43 +  "[* A > B *]" == "!([*A*] -o [*B*])" *)
    3.44 +
    3.45 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Sequents/ILL/ROOT.ML	Fri Feb 05 21:14:17 1999 +0100
     4.3 @@ -0,0 +1,10 @@
     4.4 +
     4.5 +Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
     4.6 +writeln"Root file for ILL examples";
     4.7 +
     4.8 +set proof_timing;
     4.9 +
    4.10 +time_use_thy "washing";
    4.11 +
    4.12 +time_use_thy "ILL_predlog";
    4.13 +time_use "ILL_kleene_lemmas.ML";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Sequents/ILL/washing.ML	Fri Feb 05 21:14:17 1999 +0100
     5.3 @@ -0,0 +1,33 @@
     5.4 +
     5.5 +open washing;
     5.6 +
     5.7 +(* "activate" definitions for use in proof *)
     5.8 +
     5.9 +val changeI = [context1] RL ([change] RLN (2,[cut]));
    5.10 +val load1I =  [context1] RL ([load1]  RLN (2,[cut]));
    5.11 +val washI =   [context1] RL ([wash]   RLN (2,[cut]));
    5.12 +val dryI =    [context1] RL ([dry]    RLN (2,[cut]));
    5.13 +
    5.14 +
    5.15 +
    5.16 +(* a load of dirty clothes and two dollars gives you clean clothes *)
    5.17 +
    5.18 +Goal "dollar , dollar , dirty |- clean";
    5.19 +
    5.20 +by (best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1);
    5.21 +
    5.22 +
    5.23 +(* order of premises doesn't matter *)
    5.24 +
    5.25 +prove_goal thy "dollar , dirty , dollar |- clean"
    5.26 +(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
    5.27 +
    5.28 +
    5.29 +(* alternative formulation *)
    5.30 +
    5.31 +prove_goal thy "dollar , dollar |- dirty -o clean"
    5.32 +(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
    5.33 +
    5.34 +
    5.35 +
    5.36 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Sequents/ILL/washing.thy	Fri Feb 05 21:14:17 1999 +0100
     6.3 @@ -0,0 +1,33 @@
     6.4 +
     6.5 +
     6.6 +(* code by Sara Kalvala, based on Paulson's LK 
     6.7 +                           and Moore's tisl.ML *)
     6.8 +
     6.9 +washing = ILL +
    6.10 +
    6.11 +consts
    6.12 +
    6.13 +dollar,quarter,loaded,dirty,wet,clean        :: "o"			
    6.14 +
    6.15 +  
    6.16 +rules
    6.17 +
    6.18 +
    6.19 +  change
    6.20 +  "dollar |- (quarter >< quarter >< quarter >< quarter)"
    6.21 +
    6.22 +  load1
    6.23 +  "quarter , quarter , quarter , quarter , quarter |- loaded"
    6.24 +
    6.25 +  load2
    6.26 +  "dollar , quarter |- loaded"
    6.27 +
    6.28 +  wash
    6.29 +  "loaded , dirty |- wet"
    6.30 +
    6.31 +  dry
    6.32 +  "wet, quarter , quarter , quarter |- clean"
    6.33 +
    6.34 +end
    6.35 +
    6.36 +  
    6.37 \ No newline at end of file
     7.1 --- a/src/Sequents/IsaMakefile	Fri Feb 05 21:12:45 1999 +0100
     7.2 +++ b/src/Sequents/IsaMakefile	Fri Feb 05 21:14:17 1999 +0100
     7.3 @@ -8,7 +8,7 @@
     7.4  
     7.5  default: Sequents
     7.6  images: Sequents
     7.7 -test: Sequents-ex
     7.8 +test: Sequents-ILL Sequents-LK Sequents-Modal
     7.9  all: images test
    7.10  
    7.11  
    7.12 @@ -31,19 +31,36 @@
    7.13  	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents
    7.14  
    7.15  
    7.16 -## Sequents-ex
    7.17 +## Sequents-ILL
    7.18 +
    7.19 +Sequents-ILL: Sequents $(LOG)/Sequents-ILL.gz
    7.20  
    7.21 -Sequents-ex: Sequents $(LOG)/Sequents-ex.gz
    7.22 +$(LOG)/Sequents-ILL.gz: $(OUT)/Sequents ILL/ILL_kleene_lemmas.ML \
    7.23 +  ILL/ILL_predlog.ML ILL/ILL_predlog.thy ILL/ROOT.ML ILL/washing.ML \
    7.24 +  ILL/washing.thy
    7.25 +	@$(ISATOOL) usedir $(OUT)/Sequents ILL
    7.26 +
    7.27 +
    7.28 +## Sequents-LK
    7.29  
    7.30 -$(LOG)/Sequents-ex.gz: $(OUT)/Sequents ex/ILL/ILL_kleene_lemmas.ML \
    7.31 -  ex/ILL/ILL_predlog.ML ex/ILL/ILL_predlog.thy ex/ILL/washing.ML \
    7.32 -  ex/ILL/washing.thy ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML \
    7.33 -  ex/LK/quant.ML ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML \
    7.34 -  ex/Modal/Tthms.ML ex/ROOT.ML
    7.35 -	@$(ISATOOL) usedir $(OUT)/Sequents ex
    7.36 +Sequents-LK: Sequents $(LOG)/Sequents-LK.gz
    7.37 +
    7.38 +$(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/hardquant.ML \
    7.39 +  LK/prop.ML LK/quant.ML
    7.40 +	@$(ISATOOL) usedir $(OUT)/Sequents LK
    7.41 +
    7.42 +
    7.43 +## Sequents-Modal
    7.44 +
    7.45 +Sequents-Modal: Sequents $(LOG)/Sequents-Modal.gz
    7.46 +
    7.47 +$(LOG)/Sequents-Modal.gz: $(OUT)/Sequents Modal/ROOT.ML \
    7.48 +  Modal/S43thms.ML Modal/S4thms.ML Modal/Tthms.ML ROOT.ML
    7.49 +	@$(ISATOOL) usedir $(OUT)/Sequents Modal
    7.50  
    7.51  
    7.52  ## clean
    7.53  
    7.54  clean:
    7.55 -	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ex.gz
    7.56 +	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ILL.gz \
    7.57 +	  $(LOG)/Sequents-LK.gz $(LOG)/Sequents-Modal.gz
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Sequents/LK/ROOT.ML	Fri Feb 05 21:14:17 1999 +0100
     8.3 @@ -0,0 +1,16 @@
     8.4 +(*  Title:      LK/ex/ROOT
     8.5 +    ID:         $Id$
     8.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 +    Copyright   1992  University of Cambridge
     8.8 +
     8.9 +Executes all examples for Classical Logic. 
    8.10 +*)
    8.11 +
    8.12 +Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
    8.13 +
    8.14 +writeln"Root file for LK examples";
    8.15 +
    8.16 +set proof_timing;
    8.17 +time_use "prop.ML";
    8.18 +time_use "quant.ML";
    8.19 +time_use "hardquant.ML";
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Sequents/LK/hardquant.ML	Fri Feb 05 21:14:17 1999 +0100
     9.3 @@ -0,0 +1,278 @@
     9.4 +(*  Title:      LK/ex/hard-quant
     9.5 +    ID:         $Id$
     9.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 +    Copyright   1992  University of Cambridge
     9.8 +
     9.9 +Hard examples with quantifiers.  Can be read to test the LK system.
    9.10 +From  F. J. Pelletier,
    9.11 +  Seventy-Five Problems for Testing Automatic Theorem Provers,
    9.12 +  J. Automated Reasoning 2 (1986), 191-216.
    9.13 +  Errata, JAR 4 (1988), 236-236.
    9.14 +
    9.15 +Uses pc_tac rather than fast_tac when the former is significantly faster.
    9.16 +*)
    9.17 +
    9.18 +writeln"File LK/ex/hard-quant.";
    9.19 +
    9.20 +goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
    9.21 +by (fast_tac LK_pack 1);
    9.22 +result(); 
    9.23 +
    9.24 +goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
    9.25 +by (fast_tac LK_pack 1);
    9.26 +result(); 
    9.27 +
    9.28 +goal LK.thy "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
    9.29 +by (fast_tac LK_pack 1);
    9.30 +result(); 
    9.31 +
    9.32 +goal LK.thy "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
    9.33 +by (fast_tac LK_pack 1);
    9.34 +result(); 
    9.35 +
    9.36 +writeln"Problems requiring quantifier duplication";
    9.37 +
    9.38 +(*Not provable by fast_tac LK_pack: needs multiple instantiation of ALL*)
    9.39 +goal LK.thy "|- (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
    9.40 +by (best_tac LK_dup_pack 1);
    9.41 +result();
    9.42 +
    9.43 +(*Needs double instantiation of the quantifier*)
    9.44 +goal LK.thy "|- EX x. P(x) --> P(a) & P(b)";
    9.45 +by (fast_tac LK_dup_pack 1);
    9.46 +result();
    9.47 +
    9.48 +goal LK.thy "|- EX z. P(z) --> (ALL x. P(x))";
    9.49 +by (best_tac LK_dup_pack 1);
    9.50 +result();
    9.51 +
    9.52 +writeln"Hard examples with quantifiers";
    9.53 +
    9.54 +writeln"Problem 18";
    9.55 +goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
    9.56 +by (best_tac LK_dup_pack 1);
    9.57 +result(); 
    9.58 +
    9.59 +writeln"Problem 19";
    9.60 +goal LK.thy "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
    9.61 +by (best_tac LK_dup_pack 1);
    9.62 +result();
    9.63 +
    9.64 +writeln"Problem 20";
    9.65 +goal LK.thy "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
    9.66 +\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
    9.67 +by (fast_tac LK_pack 1); 
    9.68 +result();
    9.69 +
    9.70 +writeln"Problem 21";
    9.71 +goal LK.thy "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
    9.72 +by (best_tac LK_dup_pack 1);
    9.73 +result();
    9.74 +
    9.75 +writeln"Problem 22";
    9.76 +goal LK.thy "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
    9.77 +by (fast_tac LK_pack 1); 
    9.78 +result();
    9.79 +
    9.80 +writeln"Problem 23";
    9.81 +goal LK.thy "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
    9.82 +by (best_tac LK_pack 1);  
    9.83 +result();
    9.84 +
    9.85 +writeln"Problem 24";
    9.86 +goal LK.thy "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
    9.87 +\    ~(EX x. P(x)) --> (EX x. Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
    9.88 +\   --> (EX x. P(x)&R(x))";
    9.89 +by (pc_tac LK_pack 1);
    9.90 +result();
    9.91 +
    9.92 +writeln"Problem 25";
    9.93 +goal LK.thy "|- (EX x. P(x)) &  \
    9.94 +\       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
    9.95 +\       (ALL x. P(x) --> (M(x) & L(x))) &   \
    9.96 +\       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
    9.97 +\   --> (EX x. Q(x)&P(x))";
    9.98 +by (best_tac LK_pack 1);  
    9.99 +result();
   9.100 +
   9.101 +writeln"Problem 26";
   9.102 +goal LK.thy "|- ((EX x. p(x)) <-> (EX x. q(x))) &       \
   9.103 +\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
   9.104 +\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
   9.105 +by (pc_tac LK_pack 1);
   9.106 +result();
   9.107 +
   9.108 +writeln"Problem 27";
   9.109 +goal LK.thy "|- (EX x. P(x) & ~Q(x)) &   \
   9.110 +\             (ALL x. P(x) --> R(x)) &   \
   9.111 +\             (ALL x. M(x) & L(x) --> P(x)) &   \
   9.112 +\             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
   9.113 +\         --> (ALL x. M(x) --> ~L(x))";
   9.114 +by (pc_tac LK_pack 1); 
   9.115 +result();
   9.116 +
   9.117 +writeln"Problem 28.  AMENDED";
   9.118 +goal LK.thy "|- (ALL x. P(x) --> (ALL x. Q(x))) &   \
   9.119 +\       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
   9.120 +\       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
   9.121 +\   --> (ALL x. P(x) & L(x) --> M(x))";
   9.122 +by (pc_tac LK_pack 1);  
   9.123 +result();
   9.124 +
   9.125 +writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
   9.126 +goal LK.thy "|- (EX x. P(x)) & (EX y. Q(y))  \
   9.127 +\   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
   9.128 +\        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
   9.129 +by (pc_tac LK_pack 1); 
   9.130 +result();
   9.131 +
   9.132 +writeln"Problem 30";
   9.133 +goal LK.thy "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
   9.134 +\       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
   9.135 +\   --> (ALL x. S(x))";
   9.136 +by (fast_tac LK_pack 1);  
   9.137 +result();
   9.138 +
   9.139 +writeln"Problem 31";
   9.140 +goal LK.thy "|- ~(EX x. P(x) & (Q(x) | R(x))) & \
   9.141 +\       (EX x. L(x) & P(x)) & \
   9.142 +\       (ALL x. ~ R(x) --> M(x))  \
   9.143 +\   --> (EX x. L(x) & M(x))";
   9.144 +by (fast_tac LK_pack 1);
   9.145 +result();
   9.146 +
   9.147 +writeln"Problem 32";
   9.148 +goal LK.thy "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
   9.149 +\       (ALL x. S(x) & R(x) --> L(x)) & \
   9.150 +\       (ALL x. M(x) --> R(x))  \
   9.151 +\   --> (ALL x. P(x) & M(x) --> L(x))";
   9.152 +by (best_tac LK_pack 1);
   9.153 +result();
   9.154 +
   9.155 +writeln"Problem 33";
   9.156 +goal LK.thy "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
   9.157 +\    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
   9.158 +by (fast_tac LK_pack 1);
   9.159 +result();
   9.160 +
   9.161 +writeln"Problem 34  AMENDED (TWICE!!)  NOT PROVED AUTOMATICALLY";
   9.162 +(*Andrews's challenge*)
   9.163 +goal LK.thy "|- ((EX x. ALL y. p(x) <-> p(y))  <->              \
   9.164 +\              ((EX x. q(x)) <-> (ALL y. p(y))))     <->        \
   9.165 +\             ((EX x. ALL y. q(x) <-> q(y))  <->                \
   9.166 +\              ((EX x. p(x)) <-> (ALL y. q(y))))";
   9.167 +by (safe_goal_tac LK_pack 1);   (*53 secs*) (*13 secs*)
   9.168 +by (TRYALL (fast_tac LK_pack)); (*165 secs*)  (*117 secs*)  (*138 secs*)
   9.169 +(*for some reason, pc_tac leaves 14 subgoals instead of 6*)
   9.170 +by (TRYALL (best_tac LK_dup_pack)); (*55 secs*) (*29 secs*) (*54 secs*)
   9.171 +result();
   9.172 +
   9.173 +
   9.174 +writeln"Problem 35";
   9.175 +goal LK.thy "|- EX x y. P(x,y) -->  (ALL u v. P(u,v))";
   9.176 +by (best_tac LK_dup_pack 1);  (*27 secs??*)
   9.177 +result();
   9.178 +
   9.179 +writeln"Problem 36";
   9.180 +goal LK.thy "|- (ALL x. EX y. J(x,y)) & \
   9.181 +\       (ALL x. EX y. G(x,y)) & \
   9.182 +\       (ALL x y. J(x,y) | G(x,y) -->   \
   9.183 +\       (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
   9.184 +\   --> (ALL x. EX y. H(x,y))";
   9.185 +by (fast_tac LK_pack 1);
   9.186 +result();
   9.187 +
   9.188 +writeln"Problem 37";
   9.189 +goal LK.thy "|- (ALL z. EX w. ALL x. EX y. \
   9.190 +\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
   9.191 +\       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
   9.192 +\       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
   9.193 +\   --> (ALL x. EX y. R(x,y))";
   9.194 +by (pc_tac LK_pack 1);
   9.195 +result();
   9.196 +
   9.197 +writeln"Problem 38";
   9.198 +goal LK.thy
   9.199 + "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
   9.200 +\            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
   9.201 +\    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
   9.202 +\            (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
   9.203 +\             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
   9.204 +by (pc_tac LK_pack 1);
   9.205 +result();
   9.206 +
   9.207 +writeln"Problem 39";
   9.208 +goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
   9.209 +by (fast_tac LK_pack 1);
   9.210 +result();
   9.211 +
   9.212 +writeln"Problem 40.  AMENDED";
   9.213 +goal LK.thy "|- (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
   9.214 +\                    ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
   9.215 +by (fast_tac LK_pack 1);
   9.216 +result();
   9.217 +
   9.218 +writeln"Problem 41";
   9.219 +goal LK.thy "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))      \
   9.220 +\         --> ~ (EX z. ALL x. f(x,z))";
   9.221 +by (fast_tac LK_pack 1);
   9.222 +result();
   9.223 +
   9.224 +writeln"Problem 42";
   9.225 +goal LK.thy "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))";
   9.226 +
   9.227 +writeln"Problem 43  NOT PROVED AUTOMATICALLY";
   9.228 +goal LK.thy "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \
   9.229 +\         --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))";
   9.230 +
   9.231 +writeln"Problem 44";
   9.232 +goal LK.thy "|- (ALL x. f(x) -->                                        \
   9.233 +\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
   9.234 +\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
   9.235 +\             --> (EX x. j(x) & ~f(x))";
   9.236 +by (fast_tac LK_pack 1);
   9.237 +result();
   9.238 +
   9.239 +writeln"Problem 45";
   9.240 +goal LK.thy "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))        \
   9.241 +\                     --> (ALL y. g(y) & h(x,y) --> k(y))) &    \
   9.242 +\     ~ (EX y. l(y) & k(y)) &                                   \
   9.243 +\     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
   9.244 +\                  & (ALL y. g(y) & h(x,y) --> j(x,y)))         \
   9.245 +\     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
   9.246 +by (best_tac LK_pack 1); 
   9.247 +result();
   9.248 +
   9.249 +
   9.250 +writeln"Problem 50";  
   9.251 +goal LK.thy
   9.252 +    "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
   9.253 +by (best_tac LK_dup_pack 1);
   9.254 +result();
   9.255 +
   9.256 +writeln"Problem 57";
   9.257 +goal LK.thy
   9.258 +    "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
   9.259 +\    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
   9.260 +by (fast_tac LK_pack 1);
   9.261 +result();
   9.262 +
   9.263 +writeln"Problem 59";
   9.264 +(*Unification works poorly here -- the abstraction %sobj prevents efficient
   9.265 +  operation of the occurs check*)
   9.266 +Unify.trace_bound := !Unify.search_bound - 1; 
   9.267 +goal LK.thy "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
   9.268 +by (best_tac LK_dup_pack 1);
   9.269 +result();
   9.270 +
   9.271 +writeln"Problem 60";
   9.272 +goal LK.thy
   9.273 +    "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
   9.274 +by (fast_tac LK_pack 1);
   9.275 +result();
   9.276 +
   9.277 +writeln"Reached end of file.";
   9.278 +
   9.279 +(*18 June 92: loaded in 372 secs*)
   9.280 +(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
   9.281 +(*29 June 92: loaded in 370 secs*)
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Sequents/LK/prop.ML	Fri Feb 05 21:14:17 1999 +0100
    10.3 @@ -0,0 +1,194 @@
    10.4 +(*  Title:      LK/ex/prop
    10.5 +    ID:         $Id$
    10.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 +    Copyright   1992  University of Cambridge
    10.8 +
    10.9 +Classical sequent calculus: examples with propositional connectives
   10.10 +Can be read to test the LK system.
   10.11 +*)
   10.12 +
   10.13 +writeln"LK/ex/prop: propositional examples";
   10.14 +
   10.15 +writeln"absorptive laws of & and | ";
   10.16 +
   10.17 +goal LK.thy "|- P & P <-> P";
   10.18 +by (fast_tac prop_pack 1);
   10.19 +result();
   10.20 +
   10.21 +goal LK.thy "|- P | P <-> P";
   10.22 +by (fast_tac prop_pack 1);
   10.23 +result();
   10.24 +
   10.25 +writeln"commutative laws of & and | ";
   10.26 +
   10.27 +goal LK.thy "|- P & Q  <->  Q & P";
   10.28 +by (fast_tac prop_pack 1);
   10.29 +result();
   10.30 +
   10.31 +goal LK.thy "|- P | Q  <->  Q | P";
   10.32 +by (fast_tac prop_pack 1);
   10.33 +result();
   10.34 +
   10.35 +
   10.36 +writeln"associative laws of & and | ";
   10.37 +
   10.38 +goal LK.thy "|- (P & Q) & R  <->  P & (Q & R)";
   10.39 +by (fast_tac prop_pack 1);
   10.40 +result();
   10.41 +
   10.42 +goal LK.thy "|- (P | Q) | R  <->  P | (Q | R)";
   10.43 +by (fast_tac prop_pack 1);
   10.44 +result();
   10.45 +
   10.46 +writeln"distributive laws of & and | ";
   10.47 +goal LK.thy "|- (P & Q) | R  <-> (P | R) & (Q | R)";
   10.48 +by (fast_tac prop_pack 1);
   10.49 +result();
   10.50 +
   10.51 +goal LK.thy "|- (P | Q) & R  <-> (P & R) | (Q & R)";
   10.52 +by (fast_tac prop_pack 1);
   10.53 +result();
   10.54 +
   10.55 +writeln"Laws involving implication";
   10.56 +
   10.57 +goal LK.thy "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
   10.58 +by (fast_tac prop_pack 1);
   10.59 +result(); 
   10.60 +
   10.61 +goal LK.thy "|- (P & Q --> R) <-> (P--> (Q-->R))";
   10.62 +by (fast_tac prop_pack 1);
   10.63 +result(); 
   10.64 +
   10.65 +
   10.66 +goal LK.thy "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
   10.67 +by (fast_tac prop_pack 1);
   10.68 +result();
   10.69 +
   10.70 +
   10.71 +writeln"Classical theorems";
   10.72 +
   10.73 +goal LK.thy "|- P|Q --> P| ~P&Q";
   10.74 +by (fast_tac prop_pack 1);
   10.75 +result();
   10.76 +
   10.77 +
   10.78 +goal LK.thy "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
   10.79 +by (fast_tac prop_pack 1);
   10.80 +result();
   10.81 +
   10.82 +
   10.83 +goal LK.thy "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
   10.84 +by (fast_tac prop_pack 1);
   10.85 +result();
   10.86 +
   10.87 +
   10.88 +goal LK.thy "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
   10.89 +by (fast_tac prop_pack 1);
   10.90 +result();
   10.91 +
   10.92 +
   10.93 +(*If and only if*)
   10.94 +
   10.95 +goal LK.thy "|- (P<->Q) <-> (Q<->P)";
   10.96 +by (fast_tac prop_pack 1);
   10.97 +result();
   10.98 +
   10.99 +goal LK.thy "|- ~ (P <-> ~P)";
  10.100 +by (fast_tac prop_pack 1);
  10.101 +result();
  10.102 +
  10.103 +
  10.104 +(*Sample problems from 
  10.105 +  F. J. Pelletier, 
  10.106 +  Seventy-Five Problems for Testing Automatic Theorem Provers,
  10.107 +  J. Automated Reasoning 2 (1986), 191-216.
  10.108 +  Errata, JAR 4 (1988), 236-236.
  10.109 +*)
  10.110 +
  10.111 +(*1*)
  10.112 +goal LK.thy "|- (P-->Q)  <->  (~Q --> ~P)";
  10.113 +by (fast_tac prop_pack 1);
  10.114 +result();
  10.115 +
  10.116 +(*2*)
  10.117 +goal LK.thy "|- ~ ~ P  <->  P";
  10.118 +by (fast_tac prop_pack 1);
  10.119 +result();
  10.120 +
  10.121 +(*3*)
  10.122 +goal LK.thy "|- ~(P-->Q) --> (Q-->P)";
  10.123 +by (fast_tac prop_pack 1);
  10.124 +result();
  10.125 +
  10.126 +(*4*)
  10.127 +goal LK.thy "|- (~P-->Q)  <->  (~Q --> P)";
  10.128 +by (fast_tac prop_pack 1);
  10.129 +result();
  10.130 +
  10.131 +(*5*)
  10.132 +goal LK.thy "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
  10.133 +by (fast_tac prop_pack 1);
  10.134 +result();
  10.135 +
  10.136 +(*6*)
  10.137 +goal LK.thy "|- P | ~ P";
  10.138 +by (fast_tac prop_pack 1);
  10.139 +result();
  10.140 +
  10.141 +(*7*)
  10.142 +goal LK.thy "|- P | ~ ~ ~ P";
  10.143 +by (fast_tac prop_pack 1);
  10.144 +result();
  10.145 +
  10.146 +(*8.  Peirce's law*)
  10.147 +goal LK.thy "|- ((P-->Q) --> P)  -->  P";
  10.148 +by (fast_tac prop_pack 1);
  10.149 +result();
  10.150 +
  10.151 +(*9*)
  10.152 +goal LK.thy "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
  10.153 +by (fast_tac prop_pack 1);
  10.154 +result();
  10.155 +
  10.156 +(*10*)
  10.157 +goal LK.thy "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
  10.158 +by (fast_tac prop_pack 1);
  10.159 +result();
  10.160 +
  10.161 +(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
  10.162 +goal LK.thy "|- P<->P";
  10.163 +by (fast_tac prop_pack 1);
  10.164 +result();
  10.165 +
  10.166 +(*12.  "Dijkstra's law"*)
  10.167 +goal LK.thy "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
  10.168 +by (fast_tac prop_pack 1);
  10.169 +result();
  10.170 +
  10.171 +(*13.  Distributive law*)
  10.172 +goal LK.thy "|- P | (Q & R)  <-> (P | Q) & (P | R)";
  10.173 +by (fast_tac prop_pack 1);
  10.174 +result();
  10.175 +
  10.176 +(*14*)
  10.177 +goal LK.thy "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
  10.178 +by (fast_tac prop_pack 1);
  10.179 +result();
  10.180 +
  10.181 +
  10.182 +(*15*)
  10.183 +goal LK.thy "|- (P --> Q) <-> (~P | Q)";
  10.184 +by (fast_tac prop_pack 1);
  10.185 +result();
  10.186 +
  10.187 +(*16*)
  10.188 +goal LK.thy "|- (P-->Q) | (Q-->P)";
  10.189 +by (fast_tac prop_pack 1);
  10.190 +result();
  10.191 +
  10.192 +(*17*)
  10.193 +goal LK.thy "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
  10.194 +by (fast_tac prop_pack 1);
  10.195 +result();
  10.196 +
  10.197 +writeln"Reached end of file.";
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Sequents/LK/quant.ML	Fri Feb 05 21:14:17 1999 +0100
    11.3 @@ -0,0 +1,160 @@
    11.4 +(*  Title:      LK/ex/quant
    11.5 +    ID:         $Id$
    11.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 +    Copyright   1992  University of Cambridge
    11.8 +
    11.9 +Classical sequent calculus: examples with quantifiers.
   11.10 +*)
   11.11 +
   11.12 +
   11.13 +writeln"LK/ex/quant: Examples with quantifiers";
   11.14 +
   11.15 +goal LK.thy "|- (ALL x. P)  <->  P";
   11.16 +by (fast_tac LK_pack 1);
   11.17 +result(); 
   11.18 +
   11.19 +goal LK.thy "|- (ALL x y. P(x,y))  <->  (ALL y x. P(x,y))";
   11.20 +by (fast_tac LK_pack 1);
   11.21 +result(); 
   11.22 +
   11.23 +goal LK.thy "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)";
   11.24 +by (fast_tac LK_pack 1);
   11.25 +result(); 
   11.26 +
   11.27 +writeln"Permutation of existential quantifier.";
   11.28 +goal LK.thy "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))";
   11.29 +by (fast_tac LK_pack 1);
   11.30 +result(); 
   11.31 +
   11.32 +goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
   11.33 +by (fast_tac LK_pack 1);
   11.34 +result(); 
   11.35 +
   11.36 +
   11.37 +(*Converse is invalid*)
   11.38 +goal LK.thy "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
   11.39 +by (fast_tac LK_pack 1);
   11.40 +result(); 
   11.41 +
   11.42 +
   11.43 +writeln"Pushing ALL into an implication.";
   11.44 +goal LK.thy "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))";
   11.45 +by (fast_tac LK_pack 1);
   11.46 +result(); 
   11.47 +
   11.48 +
   11.49 +goal LK.thy "|- (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
   11.50 +by (fast_tac LK_pack 1);
   11.51 +result(); 
   11.52 +
   11.53 +
   11.54 +goal LK.thy "|- (EX x. P)  <->  P";
   11.55 +by (fast_tac LK_pack 1);
   11.56 +result(); 
   11.57 +
   11.58 +
   11.59 +writeln"Distribution of EX over disjunction.";
   11.60 +goal LK.thy "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))";
   11.61 +by (fast_tac LK_pack 1);
   11.62 +result(); 
   11.63 +(*5 secs*)
   11.64 +
   11.65 +(*Converse is invalid*)
   11.66 +goal LK.thy "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))";
   11.67 +by (fast_tac LK_pack 1);
   11.68 +result(); 
   11.69 +
   11.70 +
   11.71 +writeln"Harder examples: classical theorems.";
   11.72 +
   11.73 +goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
   11.74 +by (fast_tac LK_pack 1);
   11.75 +result(); 
   11.76 +(*3 secs*)
   11.77 +
   11.78 +
   11.79 +goal LK.thy "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
   11.80 +by (fast_tac LK_pack 1);
   11.81 +result(); 
   11.82 +(*5 secs*)
   11.83 +
   11.84 +
   11.85 +goal LK.thy "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
   11.86 +by (fast_tac LK_pack 1);
   11.87 +result(); 
   11.88 +
   11.89 +
   11.90 +writeln"Basic test of quantifier reasoning";
   11.91 +goal LK.thy
   11.92 +   "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
   11.93 +by (fast_tac LK_pack 1);
   11.94 +result();  
   11.95 +
   11.96 +
   11.97 +goal LK.thy "|- (ALL x. Q(x))  -->  (EX x. Q(x))";
   11.98 +by (fast_tac LK_pack 1);
   11.99 +result();  
  11.100 +
  11.101 +
  11.102 +writeln"The following are invalid!";
  11.103 +
  11.104 +(*INVALID*)
  11.105 +goal LK.thy "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
  11.106 +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; 
  11.107 +(*Check that subgoals remain: proof failed.*)
  11.108 +getgoal 1; 
  11.109 +
  11.110 +(*INVALID*)
  11.111 +goal LK.thy "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
  11.112 +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  11.113 +getgoal 1; 
  11.114 +
  11.115 +goal LK.thy "|- P(?a) --> (ALL x. P(x))";
  11.116 +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  11.117 +(*Check that subgoals remain: proof failed.*)
  11.118 +getgoal 1;  
  11.119 +
  11.120 +goal LK.thy "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
  11.121 +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  11.122 +getgoal 1;  
  11.123 +
  11.124 +
  11.125 +writeln"Back to things that are provable...";
  11.126 +
  11.127 +goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
  11.128 +by (fast_tac LK_pack 1); 
  11.129 +result();  
  11.130 +
  11.131 +(*An example of why exR should be delayed as long as possible*)
  11.132 +goal LK.thy "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))";
  11.133 +by (fast_tac LK_pack 1);
  11.134 +result();  
  11.135 +
  11.136 +writeln"Solving for a Var";
  11.137 +goal LK.thy 
  11.138 +   "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
  11.139 +by (fast_tac LK_pack 1);
  11.140 +result();
  11.141 +
  11.142 +
  11.143 +writeln"Principia Mathematica *11.53";
  11.144 +goal LK.thy 
  11.145 +    "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
  11.146 +by (fast_tac LK_pack 1);
  11.147 +result();
  11.148 +
  11.149 +
  11.150 +writeln"Principia Mathematica *11.55";
  11.151 +goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
  11.152 +by (fast_tac LK_pack 1);
  11.153 +result();
  11.154 +
  11.155 +writeln"Principia Mathematica *11.61";
  11.156 +goal LK.thy
  11.157 +   "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
  11.158 +by (fast_tac LK_pack 1);
  11.159 +result();
  11.160 +
  11.161 +writeln"Reached end of file.";
  11.162 +
  11.163 +(*21 August 88: loaded in 45.7 secs*)
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Sequents/Modal/ROOT.ML	Fri Feb 05 21:14:17 1999 +0100
    12.3 @@ -0,0 +1,26 @@
    12.4 +(*  Title:      Modal/ex/ROOT
    12.5 +    ID:         $Id$
    12.6 +    Author:     Martin Coen
    12.7 +    Copyright   1991  University of Cambridge
    12.8 +*)
    12.9 +
   12.10 +Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
   12.11 +
   12.12 +set proof_timing;
   12.13 +
   12.14 +writeln "\nTheorems of T\n";
   12.15 +fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
   12.16 +time_use "Tthms.ML";
   12.17 +
   12.18 +writeln "\nTheorems of S4\n";
   12.19 +fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2]));
   12.20 +time_use "Tthms.ML";
   12.21 +time_use "S4thms.ML";
   12.22 +
   12.23 +writeln "\nTheorems of S43\n";
   12.24 +fun try s = (writeln s;
   12.25 +             prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE 
   12.26 +                                           S43_Prover.solve_tac 3]));
   12.27 +time_use "Tthms.ML";
   12.28 +time_use "S4thms.ML";
   12.29 +time_use "S43thms.ML";
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Sequents/Modal/S43thms.ML	Fri Feb 05 21:14:17 1999 +0100
    13.3 @@ -0,0 +1,49 @@
    13.4 +(*  Title:      91/Modal/ex/S43thms
    13.5 +    ID:         $Id$
    13.6 +    Author:     Martin Coen
    13.7 +    Copyright   1991  University of Cambridge
    13.8 +*)
    13.9 +
   13.10 +(* Theorems of system S43 *)
   13.11 +
   13.12 +try "|- <>[]P --> []<>P";
   13.13 +try "|- <>[]P --> [][]<>P";
   13.14 +try "|- [](<>P | <>Q) --> []<>P | []<>Q";
   13.15 +try "|- <>[]P & <>[]Q --> <>([]P & []Q)";
   13.16 +try "|- []([]P --> []Q) | []([]Q --> []P)";
   13.17 +try "|- [](<>P --> <>Q) | [](<>Q --> <>P)";
   13.18 +try "|- []([]P --> Q) | []([]Q --> P)";
   13.19 +try "|- [](P --> <>Q) | [](Q --> <>P)";
   13.20 +try "|- [](P --> []Q-->R) | [](P | ([]R --> Q))";
   13.21 +try "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)";
   13.22 +try "|- []([]P | Q) & [](P | []Q) --> []P | []Q";
   13.23 +try "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)";
   13.24 +try "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q";
   13.25 +try "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)";
   13.26 +try "|- <>[]<>P <-> []<>P";
   13.27 +try "|- []<>[]P <-> <>[]P";
   13.28 +
   13.29 +(* These are from Hailpern, LNCS 129 *)
   13.30 +
   13.31 +try "|- [](P & Q) <-> []P & []Q";
   13.32 +try "|- <>(P | Q) <-> <>P | <>Q";
   13.33 +try "|- <>(P --> Q) <-> []P --> <>Q";
   13.34 +
   13.35 +try "|- [](P --> Q) --> <>P --> <>Q";
   13.36 +try "|- []P --> []<>P";
   13.37 +try "|- <>[]P --> <>P";
   13.38 +try "|- []<>[]P --> []<>P";
   13.39 +try "|- <>[]P --> <>[]<>P";
   13.40 +try "|- <>[]P --> []<>P";
   13.41 +try "|- []<>[]P <-> <>[]P";
   13.42 +try "|- <>[]<>P <-> []<>P";
   13.43 +
   13.44 +try "|- []P | []Q --> [](P | Q)";
   13.45 +try "|- <>(P & Q) --> <>P & <>Q";
   13.46 +try "|- [](P | Q) --> []P | <>Q";
   13.47 +try "|- <>P & []Q --> <>(P & Q)";
   13.48 +try "|- [](P | Q) --> <>P | []Q";
   13.49 +try "|- [](P | Q) --> []<>P | []<>Q";
   13.50 +try "|- <>[]P & <>[]Q --> <>(P & Q)";
   13.51 +try "|- <>[](P & Q) <-> <>[]P & <>[]Q";
   13.52 +try "|- []<>(P | Q) <-> []<>P | []<>Q";
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Sequents/Modal/S4thms.ML	Fri Feb 05 21:14:17 1999 +0100
    14.3 @@ -0,0 +1,40 @@
    14.4 +(*  Title:      91/Modal/ex/S4thms
    14.5 +    ID:         $Id$
    14.6 +    Author:     Martin Coen
    14.7 +    Copyright   1991  University of Cambridge
    14.8 +*)
    14.9 +
   14.10 +(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
   14.11 +
   14.12 +try "|- []A --> A";             (* refexivity *)
   14.13 +try "|- []A --> [][]A";         (* transitivity *)
   14.14 +try "|- []A --> <>A";           (* seriality *)
   14.15 +try "|- <>[](<>A --> []<>A)";
   14.16 +try "|- <>[](<>[]A --> []A)";
   14.17 +try "|- []P <-> [][]P";
   14.18 +try "|- <>P <-> <><>P";
   14.19 +try "|- <>[]<>P --> <>P";
   14.20 +try "|- []<>P <-> []<>[]<>P";
   14.21 +try "|- <>[]P <-> <>[]<>[]P";
   14.22 +
   14.23 +(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
   14.24 +
   14.25 +try "|- []P | []Q <-> []([]P | []Q)";
   14.26 +try "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)";
   14.27 +
   14.28 +(* These are from Hailpern, LNCS 129 *)
   14.29 +
   14.30 +try "|- [](P & Q) <-> []P & []Q";
   14.31 +try "|- <>(P | Q) <-> <>P | <>Q";
   14.32 +try "|- <>(P --> Q) <-> ([]P --> <>Q)";
   14.33 +
   14.34 +try "|- [](P --> Q) --> (<>P --> <>Q)";
   14.35 +try "|- []P --> []<>P";
   14.36 +try "|- <>[]P --> <>P";
   14.37 +
   14.38 +try "|- []P | []Q --> [](P | Q)";
   14.39 +try "|- <>(P & Q) --> <>P & <>Q";
   14.40 +try "|- [](P | Q) --> []P | <>Q";
   14.41 +try "|- <>P & []Q --> <>(P & Q)";
   14.42 +try "|- [](P | Q) --> <>P | []Q";
   14.43 +
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/Sequents/Modal/Tthms.ML	Fri Feb 05 21:14:17 1999 +0100
    15.3 @@ -0,0 +1,31 @@
    15.4 +(*  Title:      91/Modal/ex/Tthms
    15.5 +    ID:         $Id$
    15.6 +    Author:     Martin Coen
    15.7 +    Copyright   1991  University of Cambridge
    15.8 +*)
    15.9 +
   15.10 +(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
   15.11 +
   15.12 +try "|- []P --> P";
   15.13 +try "|- [](P-->Q) --> ([]P-->[]Q)";    (* normality*)
   15.14 +try "|- (P--<Q) --> []P --> []Q";
   15.15 +try "|- P --> <>P";
   15.16 +
   15.17 +try "|-  [](P & Q) <-> []P & []Q";
   15.18 +try "|-  <>(P | Q) <-> <>P | <>Q";
   15.19 +try "|-  [](P<->Q) <-> (P>-<Q)";
   15.20 +try "|-  <>(P-->Q) <-> ([]P--><>Q)";
   15.21 +try "|-        []P <-> ~<>(~P)";
   15.22 +try "|-     [](~P) <-> ~<>P";
   15.23 +try "|-       ~[]P <-> <>(~P)";
   15.24 +try "|-      [][]P <-> ~<><>(~P)";
   15.25 +try "|- ~<>(P | Q) <-> ~<>P & ~<>Q";
   15.26 +
   15.27 +try "|- []P | []Q --> [](P | Q)";
   15.28 +try "|- <>(P & Q) --> <>P & <>Q";
   15.29 +try "|- [](P | Q) --> []P | <>Q";
   15.30 +try "|- <>P & []Q --> <>(P & Q)";
   15.31 +try "|- [](P | Q) --> <>P | []Q";
   15.32 +try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)";
   15.33 +try "|- (P--<Q) & (Q--<R) --> (P--<R)";
   15.34 +try "|- []P --> <>Q --> <>(P & Q)";
    16.1 --- a/src/Sequents/ex/ILL/ILL_kleene_lemmas.ML	Fri Feb 05 21:12:45 1999 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,81 +0,0 @@
    16.4 -
    16.5 -(* from [kleene 52] pp 118,119 *)
    16.6 -
    16.7 -
    16.8 -val k49a = auto1 "|- [* A > ( - ( - A)) *]";
    16.9 -
   16.10 -val k49b = auto1 "|- [*( - ( - ( - A))) = ( - A)*]";
   16.11 -
   16.12 -val k49c = auto1 "|- [* (A | - A) > ( - - A = A) *]";
   16.13 -
   16.14 -val k50a = auto2 "|- [* - (A = - A) *]";
   16.15 -
   16.16 -(*
   16.17 -         [rtac impr_contract 1 THEN REPEAT (rtac conj_lemma 1),
   16.18 -	  res_inst_tac [("A","!((! A) -o 0)")] cut 1
   16.19 -	  THEN rtac context1 1
   16.20 -	  THEN ALLGOALS (best_tac power_cs)]);
   16.21 -*)
   16.22 -
   16.23 -val k51a = auto2 "|- [* - - (A | - A) *]";
   16.24 -    
   16.25 -val k51b = auto2 "|- [* - - (- - A > A) *]";
   16.26 -    
   16.27 -val k56a = auto1 "|- [* (A | B) > - (- A & - B) *]";
   16.28 -
   16.29 -val k56b = auto1 "|- [* (-A | B) > - (A & -B) *]";
   16.30 -    
   16.31 -val k57a = auto1 "|- [* (A & B) > - (-A | -B) *]";
   16.32 -    
   16.33 -val k57b = auto2 "|- [* (A & -B) > -(-A | B) *]";
   16.34 -    
   16.35 -val k58a = auto1 "|- [* (A > B) > - (A & -B) *]";
   16.36 -    
   16.37 -val k58b = auto1 "|- [* (A > -B) = -(A & B) *]";
   16.38 -    
   16.39 -val k58c = auto1 "|- [* - (A & B) = (- - A > - B) *]";
   16.40 -    
   16.41 -val k58d = auto1 "|- [* (- - A > - B) = - - (-A | -B) *]";
   16.42 -    
   16.43 -val k58e = auto1 "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]";
   16.44 -    
   16.45 -val k58f = auto1 "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]";
   16.46 -    
   16.47 -val k58g = auto1 "|- [* (- -A > B) > - (A & -B) *]";
   16.48 -    
   16.49 -val k59a = auto1 "|- [* (-A | B) > (A > B) *]";
   16.50 -
   16.51 -val k59b = auto2 "|- [* (A > B) > - - (-A | B) *]";
   16.52 -    
   16.53 -val k59c = auto2 "|- [* (-A > B) > - -(A | B) *]";
   16.54 -    
   16.55 -val k60a = auto1 "|- [* (A & B) > - (A > -B) *]";
   16.56 -    
   16.57 -val k60b = auto1 "|- [* (A & -B) > - (A > B) *]";
   16.58 -    
   16.59 -val k60c = auto1 "|- [* ( - - A & B) > - (A > -B) *]";
   16.60 -    
   16.61 -val k60d = auto1 "|- [* (- - A & - B) = - (A > B) *]";
   16.62 -    
   16.63 -val k60e = auto1 "|- [* - (A > B) = - (-A | B) *]";
   16.64 -    
   16.65 -val k60f = auto1 "|- [* - (-A | B) = - - (A & -B) *]";
   16.66 -    
   16.67 -val k60g = auto2 "|- [* - - (A > B) = - (A & -B) *]";
   16.68 -    
   16.69 -(*
   16.70 - [step_tac safe_cs 1, best_tac safe_cs 1,
   16.71 - rtac impr 1 THEN rtac impr_contract 1
   16.72 - THEN best_tac safe_cs 1];
   16.73 -*)
   16.74 -
   16.75 -val k60h = auto1 "|- [* - (A & -B) = (A > - -B) *]";
   16.76 -
   16.77 -val k60i = auto1 "|- [* (A > - -B) = (- -A > - -B) *]";
   16.78 -
   16.79 -val k61a = auto1 "|- [* (A | B) > (-A > B) *]";
   16.80 -
   16.81 -val k61b = auto2 "|- [* - (A | B) = - (-A > B) *]";
   16.82 -
   16.83 -val k62a = auto1 "|- [* (-A | -B) > - (A & B) *]";
   16.84 -
    17.1 --- a/src/Sequents/ex/ILL/ILL_predlog.ML	Fri Feb 05 21:12:45 1999 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,9 +0,0 @@
    17.4 -
    17.5 -open ILL_predlog;
    17.6 -
    17.7 -
    17.8 -fun auto1 x = prove_goal thy x
    17.9 - (fn prems => [best_tac safe_cs 1]) ;
   17.10 -
   17.11 -fun auto2 x = prove_goal thy x
   17.12 - (fn prems => [best_tac power_cs 1]) ;
    18.1 --- a/src/Sequents/ex/ILL/ILL_predlog.thy	Fri Feb 05 21:12:45 1999 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,42 +0,0 @@
    18.4 -(* 
    18.5 -    File:	 /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy
    18.6 -    Theory Name: pred_log
    18.7 -    Logic Image: HOL
    18.8 -*)
    18.9 -
   18.10 -ILL_predlog  =  ILL +
   18.11 -
   18.12 -types
   18.13 -
   18.14 -    plf
   18.15 -    
   18.16 -arities
   18.17 -
   18.18 -    plf :: logic
   18.19 -    
   18.20 -consts
   18.21 -
   18.22 -  "&"   :: "[plf,plf] => plf"   (infixr 35)
   18.23 -  "|"   :: "[plf,plf] => plf"   (infixr 35)
   18.24 -  ">"   :: "[plf,plf] => plf"   (infixr 35)
   18.25 -  "="   :: "[plf,plf] => plf"   (infixr 35)
   18.26 -  "@NG" :: "plf => plf"   ("- _ " [50] 55)
   18.27 -  ff    :: "plf"
   18.28 -  
   18.29 -  PL    :: "plf => o"      ("[* / _ / *]" [] 100)
   18.30 -
   18.31 -
   18.32 -translations
   18.33 -
   18.34 -  "[* A & B *]" == "[*A*] && [*B*]" 
   18.35 -  "[* A | B *]" == "![*A*] ++ ![*B*]"
   18.36 -  "[* - A *]"   == "[*A > ff*]"
   18.37 -  "[* ff *]"    == "0"
   18.38 -  "[* A = B *]" => "[* (A > B) & (B > A) *]"
   18.39 -  
   18.40 -  "[* A > B *]" == "![*A*] -o [*B*]"
   18.41 -  
   18.42 -(* another translations for linear implication:
   18.43 -  "[* A > B *]" == "!([*A*] -o [*B*])" *)
   18.44 -
   18.45 -end
    19.1 --- a/src/Sequents/ex/ILL/ROOT.ML	Fri Feb 05 21:12:45 1999 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,10 +0,0 @@
    19.4 -
    19.5 -Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
    19.6 -writeln"Root file for ILL examples";
    19.7 -
    19.8 -set proof_timing;
    19.9 -
   19.10 -time_use_thy "ILL/washing";
   19.11 -
   19.12 -time_use_thy "ILL/ILL_predlog";
   19.13 -time_use "ILL/ILL_kleene_lemmas.ML";
    20.1 --- a/src/Sequents/ex/ILL/washing.ML	Fri Feb 05 21:12:45 1999 +0100
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,33 +0,0 @@
    20.4 -
    20.5 -open washing;
    20.6 -
    20.7 -(* "activate" definitions for use in proof *)
    20.8 -
    20.9 -val changeI = [context1] RL ([change] RLN (2,[cut]));
   20.10 -val load1I =  [context1] RL ([load1]  RLN (2,[cut]));
   20.11 -val washI =   [context1] RL ([wash]   RLN (2,[cut]));
   20.12 -val dryI =    [context1] RL ([dry]    RLN (2,[cut]));
   20.13 -
   20.14 -
   20.15 -
   20.16 -(* a load of dirty clothes and two dollars gives you clean clothes *)
   20.17 -
   20.18 -Goal "dollar , dollar , dirty |- clean";
   20.19 -
   20.20 -by (best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1);
   20.21 -
   20.22 -
   20.23 -(* order of premises doesn't matter *)
   20.24 -
   20.25 -prove_goal thy "dollar , dirty , dollar |- clean"
   20.26 -(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
   20.27 -
   20.28 -
   20.29 -(* alternative formulation *)
   20.30 -
   20.31 -prove_goal thy "dollar , dollar |- dirty -o clean"
   20.32 -(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
   20.33 -
   20.34 -
   20.35 -
   20.36 -
    21.1 --- a/src/Sequents/ex/ILL/washing.thy	Fri Feb 05 21:12:45 1999 +0100
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,33 +0,0 @@
    21.4 -
    21.5 -
    21.6 -(* code by Sara Kalvala, based on Paulson's LK 
    21.7 -                           and Moore's tisl.ML *)
    21.8 -
    21.9 -washing = ILL +
   21.10 -
   21.11 -consts
   21.12 -
   21.13 -dollar,quarter,loaded,dirty,wet,clean        :: "o"			
   21.14 -
   21.15 -  
   21.16 -rules
   21.17 -
   21.18 -
   21.19 -  change
   21.20 -  "dollar |- (quarter >< quarter >< quarter >< quarter)"
   21.21 -
   21.22 -  load1
   21.23 -  "quarter , quarter , quarter , quarter , quarter |- loaded"
   21.24 -
   21.25 -  load2
   21.26 -  "dollar , quarter |- loaded"
   21.27 -
   21.28 -  wash
   21.29 -  "loaded , dirty |- wet"
   21.30 -
   21.31 -  dry
   21.32 -  "wet, quarter , quarter , quarter |- clean"
   21.33 -
   21.34 -end
   21.35 -
   21.36 -  
   21.37 \ No newline at end of file
    22.1 --- a/src/Sequents/ex/LK/ROOT.ML	Fri Feb 05 21:12:45 1999 +0100
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,16 +0,0 @@
    22.4 -(*  Title:      LK/ex/ROOT
    22.5 -    ID:         $Id$
    22.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7 -    Copyright   1992  University of Cambridge
    22.8 -
    22.9 -Executes all examples for Classical Logic. 
   22.10 -*)
   22.11 -
   22.12 -Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
   22.13 -
   22.14 -writeln"Root file for LK examples";
   22.15 -
   22.16 -set proof_timing;
   22.17 -time_use "LK/prop.ML";
   22.18 -time_use "LK/quant.ML";
   22.19 -time_use "LK/hardquant.ML";
    23.1 --- a/src/Sequents/ex/LK/hardquant.ML	Fri Feb 05 21:12:45 1999 +0100
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,278 +0,0 @@
    23.4 -(*  Title:      LK/ex/hard-quant
    23.5 -    ID:         $Id$
    23.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.7 -    Copyright   1992  University of Cambridge
    23.8 -
    23.9 -Hard examples with quantifiers.  Can be read to test the LK system.
   23.10 -From  F. J. Pelletier,
   23.11 -  Seventy-Five Problems for Testing Automatic Theorem Provers,
   23.12 -  J. Automated Reasoning 2 (1986), 191-216.
   23.13 -  Errata, JAR 4 (1988), 236-236.
   23.14 -
   23.15 -Uses pc_tac rather than fast_tac when the former is significantly faster.
   23.16 -*)
   23.17 -
   23.18 -writeln"File LK/ex/hard-quant.";
   23.19 -
   23.20 -goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
   23.21 -by (fast_tac LK_pack 1);
   23.22 -result(); 
   23.23 -
   23.24 -goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
   23.25 -by (fast_tac LK_pack 1);
   23.26 -result(); 
   23.27 -
   23.28 -goal LK.thy "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
   23.29 -by (fast_tac LK_pack 1);
   23.30 -result(); 
   23.31 -
   23.32 -goal LK.thy "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
   23.33 -by (fast_tac LK_pack 1);
   23.34 -result(); 
   23.35 -
   23.36 -writeln"Problems requiring quantifier duplication";
   23.37 -
   23.38 -(*Not provable by fast_tac LK_pack: needs multiple instantiation of ALL*)
   23.39 -goal LK.thy "|- (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
   23.40 -by (best_tac LK_dup_pack 1);
   23.41 -result();
   23.42 -
   23.43 -(*Needs double instantiation of the quantifier*)
   23.44 -goal LK.thy "|- EX x. P(x) --> P(a) & P(b)";
   23.45 -by (fast_tac LK_dup_pack 1);
   23.46 -result();
   23.47 -
   23.48 -goal LK.thy "|- EX z. P(z) --> (ALL x. P(x))";
   23.49 -by (best_tac LK_dup_pack 1);
   23.50 -result();
   23.51 -
   23.52 -writeln"Hard examples with quantifiers";
   23.53 -
   23.54 -writeln"Problem 18";
   23.55 -goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
   23.56 -by (best_tac LK_dup_pack 1);
   23.57 -result(); 
   23.58 -
   23.59 -writeln"Problem 19";
   23.60 -goal LK.thy "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
   23.61 -by (best_tac LK_dup_pack 1);
   23.62 -result();
   23.63 -
   23.64 -writeln"Problem 20";
   23.65 -goal LK.thy "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
   23.66 -\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
   23.67 -by (fast_tac LK_pack 1); 
   23.68 -result();
   23.69 -
   23.70 -writeln"Problem 21";
   23.71 -goal LK.thy "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
   23.72 -by (best_tac LK_dup_pack 1);
   23.73 -result();
   23.74 -
   23.75 -writeln"Problem 22";
   23.76 -goal LK.thy "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
   23.77 -by (fast_tac LK_pack 1); 
   23.78 -result();
   23.79 -
   23.80 -writeln"Problem 23";
   23.81 -goal LK.thy "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
   23.82 -by (best_tac LK_pack 1);  
   23.83 -result();
   23.84 -
   23.85 -writeln"Problem 24";
   23.86 -goal LK.thy "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
   23.87 -\    ~(EX x. P(x)) --> (EX x. Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
   23.88 -\   --> (EX x. P(x)&R(x))";
   23.89 -by (pc_tac LK_pack 1);
   23.90 -result();
   23.91 -
   23.92 -writeln"Problem 25";
   23.93 -goal LK.thy "|- (EX x. P(x)) &  \
   23.94 -\       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
   23.95 -\       (ALL x. P(x) --> (M(x) & L(x))) &   \
   23.96 -\       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
   23.97 -\   --> (EX x. Q(x)&P(x))";
   23.98 -by (best_tac LK_pack 1);  
   23.99 -result();
  23.100 -
  23.101 -writeln"Problem 26";
  23.102 -goal LK.thy "|- ((EX x. p(x)) <-> (EX x. q(x))) &       \
  23.103 -\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
  23.104 -\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
  23.105 -by (pc_tac LK_pack 1);
  23.106 -result();
  23.107 -
  23.108 -writeln"Problem 27";
  23.109 -goal LK.thy "|- (EX x. P(x) & ~Q(x)) &   \
  23.110 -\             (ALL x. P(x) --> R(x)) &   \
  23.111 -\             (ALL x. M(x) & L(x) --> P(x)) &   \
  23.112 -\             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
  23.113 -\         --> (ALL x. M(x) --> ~L(x))";
  23.114 -by (pc_tac LK_pack 1); 
  23.115 -result();
  23.116 -
  23.117 -writeln"Problem 28.  AMENDED";
  23.118 -goal LK.thy "|- (ALL x. P(x) --> (ALL x. Q(x))) &   \
  23.119 -\       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
  23.120 -\       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
  23.121 -\   --> (ALL x. P(x) & L(x) --> M(x))";
  23.122 -by (pc_tac LK_pack 1);  
  23.123 -result();
  23.124 -
  23.125 -writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
  23.126 -goal LK.thy "|- (EX x. P(x)) & (EX y. Q(y))  \
  23.127 -\   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
  23.128 -\        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
  23.129 -by (pc_tac LK_pack 1); 
  23.130 -result();
  23.131 -
  23.132 -writeln"Problem 30";
  23.133 -goal LK.thy "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
  23.134 -\       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
  23.135 -\   --> (ALL x. S(x))";
  23.136 -by (fast_tac LK_pack 1);  
  23.137 -result();
  23.138 -
  23.139 -writeln"Problem 31";
  23.140 -goal LK.thy "|- ~(EX x. P(x) & (Q(x) | R(x))) & \
  23.141 -\       (EX x. L(x) & P(x)) & \
  23.142 -\       (ALL x. ~ R(x) --> M(x))  \
  23.143 -\   --> (EX x. L(x) & M(x))";
  23.144 -by (fast_tac LK_pack 1);
  23.145 -result();
  23.146 -
  23.147 -writeln"Problem 32";
  23.148 -goal LK.thy "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
  23.149 -\       (ALL x. S(x) & R(x) --> L(x)) & \
  23.150 -\       (ALL x. M(x) --> R(x))  \
  23.151 -\   --> (ALL x. P(x) & M(x) --> L(x))";
  23.152 -by (best_tac LK_pack 1);
  23.153 -result();
  23.154 -
  23.155 -writeln"Problem 33";
  23.156 -goal LK.thy "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
  23.157 -\    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
  23.158 -by (fast_tac LK_pack 1);
  23.159 -result();
  23.160 -
  23.161 -writeln"Problem 34  AMENDED (TWICE!!)  NOT PROVED AUTOMATICALLY";
  23.162 -(*Andrews's challenge*)
  23.163 -goal LK.thy "|- ((EX x. ALL y. p(x) <-> p(y))  <->              \
  23.164 -\              ((EX x. q(x)) <-> (ALL y. p(y))))     <->        \
  23.165 -\             ((EX x. ALL y. q(x) <-> q(y))  <->                \
  23.166 -\              ((EX x. p(x)) <-> (ALL y. q(y))))";
  23.167 -by (safe_goal_tac LK_pack 1);   (*53 secs*) (*13 secs*)
  23.168 -by (TRYALL (fast_tac LK_pack)); (*165 secs*)  (*117 secs*)  (*138 secs*)
  23.169 -(*for some reason, pc_tac leaves 14 subgoals instead of 6*)
  23.170 -by (TRYALL (best_tac LK_dup_pack)); (*55 secs*) (*29 secs*) (*54 secs*)
  23.171 -result();
  23.172 -
  23.173 -
  23.174 -writeln"Problem 35";
  23.175 -goal LK.thy "|- EX x y. P(x,y) -->  (ALL u v. P(u,v))";
  23.176 -by (best_tac LK_dup_pack 1);  (*27 secs??*)
  23.177 -result();
  23.178 -
  23.179 -writeln"Problem 36";
  23.180 -goal LK.thy "|- (ALL x. EX y. J(x,y)) & \
  23.181 -\       (ALL x. EX y. G(x,y)) & \
  23.182 -\       (ALL x y. J(x,y) | G(x,y) -->   \
  23.183 -\       (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
  23.184 -\   --> (ALL x. EX y. H(x,y))";
  23.185 -by (fast_tac LK_pack 1);
  23.186 -result();
  23.187 -
  23.188 -writeln"Problem 37";
  23.189 -goal LK.thy "|- (ALL z. EX w. ALL x. EX y. \
  23.190 -\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
  23.191 -\       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
  23.192 -\       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
  23.193 -\   --> (ALL x. EX y. R(x,y))";
  23.194 -by (pc_tac LK_pack 1);
  23.195 -result();
  23.196 -
  23.197 -writeln"Problem 38";
  23.198 -goal LK.thy
  23.199 - "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
  23.200 -\            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
  23.201 -\    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
  23.202 -\            (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
  23.203 -\             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
  23.204 -by (pc_tac LK_pack 1);
  23.205 -result();
  23.206 -
  23.207 -writeln"Problem 39";
  23.208 -goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
  23.209 -by (fast_tac LK_pack 1);
  23.210 -result();
  23.211 -
  23.212 -writeln"Problem 40.  AMENDED";
  23.213 -goal LK.thy "|- (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
  23.214 -\                    ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
  23.215 -by (fast_tac LK_pack 1);
  23.216 -result();
  23.217 -
  23.218 -writeln"Problem 41";
  23.219 -goal LK.thy "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))      \
  23.220 -\         --> ~ (EX z. ALL x. f(x,z))";
  23.221 -by (fast_tac LK_pack 1);
  23.222 -result();
  23.223 -
  23.224 -writeln"Problem 42";
  23.225 -goal LK.thy "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))";
  23.226 -
  23.227 -writeln"Problem 43  NOT PROVED AUTOMATICALLY";
  23.228 -goal LK.thy "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \
  23.229 -\         --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))";
  23.230 -
  23.231 -writeln"Problem 44";
  23.232 -goal LK.thy "|- (ALL x. f(x) -->                                        \
  23.233 -\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
  23.234 -\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
  23.235 -\             --> (EX x. j(x) & ~f(x))";
  23.236 -by (fast_tac LK_pack 1);
  23.237 -result();
  23.238 -
  23.239 -writeln"Problem 45";
  23.240 -goal LK.thy "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))        \
  23.241 -\                     --> (ALL y. g(y) & h(x,y) --> k(y))) &    \
  23.242 -\     ~ (EX y. l(y) & k(y)) &                                   \
  23.243 -\     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
  23.244 -\                  & (ALL y. g(y) & h(x,y) --> j(x,y)))         \
  23.245 -\     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
  23.246 -by (best_tac LK_pack 1); 
  23.247 -result();
  23.248 -
  23.249 -
  23.250 -writeln"Problem 50";  
  23.251 -goal LK.thy
  23.252 -    "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
  23.253 -by (best_tac LK_dup_pack 1);
  23.254 -result();
  23.255 -
  23.256 -writeln"Problem 57";
  23.257 -goal LK.thy
  23.258 -    "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
  23.259 -\    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
  23.260 -by (fast_tac LK_pack 1);
  23.261 -result();
  23.262 -
  23.263 -writeln"Problem 59";
  23.264 -(*Unification works poorly here -- the abstraction %sobj prevents efficient
  23.265 -  operation of the occurs check*)
  23.266 -Unify.trace_bound := !Unify.search_bound - 1; 
  23.267 -goal LK.thy "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
  23.268 -by (best_tac LK_dup_pack 1);
  23.269 -result();
  23.270 -
  23.271 -writeln"Problem 60";
  23.272 -goal LK.thy
  23.273 -    "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
  23.274 -by (fast_tac LK_pack 1);
  23.275 -result();
  23.276 -
  23.277 -writeln"Reached end of file.";
  23.278 -
  23.279 -(*18 June 92: loaded in 372 secs*)
  23.280 -(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
  23.281 -(*29 June 92: loaded in 370 secs*)
    24.1 --- a/src/Sequents/ex/LK/prop.ML	Fri Feb 05 21:12:45 1999 +0100
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,194 +0,0 @@
    24.4 -(*  Title:      LK/ex/prop
    24.5 -    ID:         $Id$
    24.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    24.7 -    Copyright   1992  University of Cambridge
    24.8 -
    24.9 -Classical sequent calculus: examples with propositional connectives
   24.10 -Can be read to test the LK system.
   24.11 -*)
   24.12 -
   24.13 -writeln"LK/ex/prop: propositional examples";
   24.14 -
   24.15 -writeln"absorptive laws of & and | ";
   24.16 -
   24.17 -goal LK.thy "|- P & P <-> P";
   24.18 -by (fast_tac prop_pack 1);
   24.19 -result();
   24.20 -
   24.21 -goal LK.thy "|- P | P <-> P";
   24.22 -by (fast_tac prop_pack 1);
   24.23 -result();
   24.24 -
   24.25 -writeln"commutative laws of & and | ";
   24.26 -
   24.27 -goal LK.thy "|- P & Q  <->  Q & P";
   24.28 -by (fast_tac prop_pack 1);
   24.29 -result();
   24.30 -
   24.31 -goal LK.thy "|- P | Q  <->  Q | P";
   24.32 -by (fast_tac prop_pack 1);
   24.33 -result();
   24.34 -
   24.35 -
   24.36 -writeln"associative laws of & and | ";
   24.37 -
   24.38 -goal LK.thy "|- (P & Q) & R  <->  P & (Q & R)";
   24.39 -by (fast_tac prop_pack 1);
   24.40 -result();
   24.41 -
   24.42 -goal LK.thy "|- (P | Q) | R  <->  P | (Q | R)";
   24.43 -by (fast_tac prop_pack 1);
   24.44 -result();
   24.45 -
   24.46 -writeln"distributive laws of & and | ";
   24.47 -goal LK.thy "|- (P & Q) | R  <-> (P | R) & (Q | R)";
   24.48 -by (fast_tac prop_pack 1);
   24.49 -result();
   24.50 -
   24.51 -goal LK.thy "|- (P | Q) & R  <-> (P & R) | (Q & R)";
   24.52 -by (fast_tac prop_pack 1);
   24.53 -result();
   24.54 -
   24.55 -writeln"Laws involving implication";
   24.56 -
   24.57 -goal LK.thy "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
   24.58 -by (fast_tac prop_pack 1);
   24.59 -result(); 
   24.60 -
   24.61 -goal LK.thy "|- (P & Q --> R) <-> (P--> (Q-->R))";
   24.62 -by (fast_tac prop_pack 1);
   24.63 -result(); 
   24.64 -
   24.65 -
   24.66 -goal LK.thy "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
   24.67 -by (fast_tac prop_pack 1);
   24.68 -result();
   24.69 -
   24.70 -
   24.71 -writeln"Classical theorems";
   24.72 -
   24.73 -goal LK.thy "|- P|Q --> P| ~P&Q";
   24.74 -by (fast_tac prop_pack 1);
   24.75 -result();
   24.76 -
   24.77 -
   24.78 -goal LK.thy "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
   24.79 -by (fast_tac prop_pack 1);
   24.80 -result();
   24.81 -
   24.82 -
   24.83 -goal LK.thy "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
   24.84 -by (fast_tac prop_pack 1);
   24.85 -result();
   24.86 -
   24.87 -
   24.88 -goal LK.thy "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
   24.89 -by (fast_tac prop_pack 1);
   24.90 -result();
   24.91 -
   24.92 -
   24.93 -(*If and only if*)
   24.94 -
   24.95 -goal LK.thy "|- (P<->Q) <-> (Q<->P)";
   24.96 -by (fast_tac prop_pack 1);
   24.97 -result();
   24.98 -
   24.99 -goal LK.thy "|- ~ (P <-> ~P)";
  24.100 -by (fast_tac prop_pack 1);
  24.101 -result();
  24.102 -
  24.103 -
  24.104 -(*Sample problems from 
  24.105 -  F. J. Pelletier, 
  24.106 -  Seventy-Five Problems for Testing Automatic Theorem Provers,
  24.107 -  J. Automated Reasoning 2 (1986), 191-216.
  24.108 -  Errata, JAR 4 (1988), 236-236.
  24.109 -*)
  24.110 -
  24.111 -(*1*)
  24.112 -goal LK.thy "|- (P-->Q)  <->  (~Q --> ~P)";
  24.113 -by (fast_tac prop_pack 1);
  24.114 -result();
  24.115 -
  24.116 -(*2*)
  24.117 -goal LK.thy "|- ~ ~ P  <->  P";
  24.118 -by (fast_tac prop_pack 1);
  24.119 -result();
  24.120 -
  24.121 -(*3*)
  24.122 -goal LK.thy "|- ~(P-->Q) --> (Q-->P)";
  24.123 -by (fast_tac prop_pack 1);
  24.124 -result();
  24.125 -
  24.126 -(*4*)
  24.127 -goal LK.thy "|- (~P-->Q)  <->  (~Q --> P)";
  24.128 -by (fast_tac prop_pack 1);
  24.129 -result();
  24.130 -
  24.131 -(*5*)
  24.132 -goal LK.thy "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
  24.133 -by (fast_tac prop_pack 1);
  24.134 -result();
  24.135 -
  24.136 -(*6*)
  24.137 -goal LK.thy "|- P | ~ P";
  24.138 -by (fast_tac prop_pack 1);
  24.139 -result();
  24.140 -
  24.141 -(*7*)
  24.142 -goal LK.thy "|- P | ~ ~ ~ P";
  24.143 -by (fast_tac prop_pack 1);
  24.144 -result();
  24.145 -
  24.146 -(*8.  Peirce's law*)
  24.147 -goal LK.thy "|- ((P-->Q) --> P)  -->  P";
  24.148 -by (fast_tac prop_pack 1);
  24.149 -result();
  24.150 -
  24.151 -(*9*)
  24.152 -goal LK.thy "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
  24.153 -by (fast_tac prop_pack 1);
  24.154 -result();
  24.155 -
  24.156 -(*10*)
  24.157 -goal LK.thy "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
  24.158 -by (fast_tac prop_pack 1);
  24.159 -result();
  24.160 -
  24.161 -(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
  24.162 -goal LK.thy "|- P<->P";
  24.163 -by (fast_tac prop_pack 1);
  24.164 -result();
  24.165 -
  24.166 -(*12.  "Dijkstra's law"*)
  24.167 -goal LK.thy "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
  24.168 -by (fast_tac prop_pack 1);
  24.169 -result();
  24.170 -
  24.171 -(*13.  Distributive law*)
  24.172 -goal LK.thy "|- P | (Q & R)  <-> (P | Q) & (P | R)";
  24.173 -by (fast_tac prop_pack 1);
  24.174 -result();
  24.175 -
  24.176 -(*14*)
  24.177 -goal LK.thy "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
  24.178 -by (fast_tac prop_pack 1);
  24.179 -result();
  24.180 -
  24.181 -
  24.182 -(*15*)
  24.183 -goal LK.thy "|- (P --> Q) <-> (~P | Q)";
  24.184 -by (fast_tac prop_pack 1);
  24.185 -result();
  24.186 -
  24.187 -(*16*)
  24.188 -goal LK.thy "|- (P-->Q) | (Q-->P)";
  24.189 -by (fast_tac prop_pack 1);
  24.190 -result();
  24.191 -
  24.192 -(*17*)
  24.193 -goal LK.thy "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
  24.194 -by (fast_tac prop_pack 1);
  24.195 -result();
  24.196 -
  24.197 -writeln"Reached end of file.";
    25.1 --- a/src/Sequents/ex/LK/quant.ML	Fri Feb 05 21:12:45 1999 +0100
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,160 +0,0 @@
    25.4 -(*  Title:      LK/ex/quant
    25.5 -    ID:         $Id$
    25.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.7 -    Copyright   1992  University of Cambridge
    25.8 -
    25.9 -Classical sequent calculus: examples with quantifiers.
   25.10 -*)
   25.11 -
   25.12 -
   25.13 -writeln"LK/ex/quant: Examples with quantifiers";
   25.14 -
   25.15 -goal LK.thy "|- (ALL x. P)  <->  P";
   25.16 -by (fast_tac LK_pack 1);
   25.17 -result(); 
   25.18 -
   25.19 -goal LK.thy "|- (ALL x y. P(x,y))  <->  (ALL y x. P(x,y))";
   25.20 -by (fast_tac LK_pack 1);
   25.21 -result(); 
   25.22 -
   25.23 -goal LK.thy "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)";
   25.24 -by (fast_tac LK_pack 1);
   25.25 -result(); 
   25.26 -
   25.27 -writeln"Permutation of existential quantifier.";
   25.28 -goal LK.thy "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))";
   25.29 -by (fast_tac LK_pack 1);
   25.30 -result(); 
   25.31 -
   25.32 -goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
   25.33 -by (fast_tac LK_pack 1);
   25.34 -result(); 
   25.35 -
   25.36 -
   25.37 -(*Converse is invalid*)
   25.38 -goal LK.thy "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
   25.39 -by (fast_tac LK_pack 1);
   25.40 -result(); 
   25.41 -
   25.42 -
   25.43 -writeln"Pushing ALL into an implication.";
   25.44 -goal LK.thy "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))";
   25.45 -by (fast_tac LK_pack 1);
   25.46 -result(); 
   25.47 -
   25.48 -
   25.49 -goal LK.thy "|- (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
   25.50 -by (fast_tac LK_pack 1);
   25.51 -result(); 
   25.52 -
   25.53 -
   25.54 -goal LK.thy "|- (EX x. P)  <->  P";
   25.55 -by (fast_tac LK_pack 1);
   25.56 -result(); 
   25.57 -
   25.58 -
   25.59 -writeln"Distribution of EX over disjunction.";
   25.60 -goal LK.thy "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))";
   25.61 -by (fast_tac LK_pack 1);
   25.62 -result(); 
   25.63 -(*5 secs*)
   25.64 -
   25.65 -(*Converse is invalid*)
   25.66 -goal LK.thy "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))";
   25.67 -by (fast_tac LK_pack 1);
   25.68 -result(); 
   25.69 -
   25.70 -
   25.71 -writeln"Harder examples: classical theorems.";
   25.72 -
   25.73 -goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
   25.74 -by (fast_tac LK_pack 1);
   25.75 -result(); 
   25.76 -(*3 secs*)
   25.77 -
   25.78 -
   25.79 -goal LK.thy "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
   25.80 -by (fast_tac LK_pack 1);
   25.81 -result(); 
   25.82 -(*5 secs*)
   25.83 -
   25.84 -
   25.85 -goal LK.thy "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
   25.86 -by (fast_tac LK_pack 1);
   25.87 -result(); 
   25.88 -
   25.89 -
   25.90 -writeln"Basic test of quantifier reasoning";
   25.91 -goal LK.thy
   25.92 -   "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
   25.93 -by (fast_tac LK_pack 1);
   25.94 -result();  
   25.95 -
   25.96 -
   25.97 -goal LK.thy "|- (ALL x. Q(x))  -->  (EX x. Q(x))";
   25.98 -by (fast_tac LK_pack 1);
   25.99 -result();  
  25.100 -
  25.101 -
  25.102 -writeln"The following are invalid!";
  25.103 -
  25.104 -(*INVALID*)
  25.105 -goal LK.thy "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
  25.106 -by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; 
  25.107 -(*Check that subgoals remain: proof failed.*)
  25.108 -getgoal 1; 
  25.109 -
  25.110 -(*INVALID*)
  25.111 -goal LK.thy "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
  25.112 -by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  25.113 -getgoal 1; 
  25.114 -
  25.115 -goal LK.thy "|- P(?a) --> (ALL x. P(x))";
  25.116 -by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  25.117 -(*Check that subgoals remain: proof failed.*)
  25.118 -getgoal 1;  
  25.119 -
  25.120 -goal LK.thy "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
  25.121 -by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  25.122 -getgoal 1;  
  25.123 -
  25.124 -
  25.125 -writeln"Back to things that are provable...";
  25.126 -
  25.127 -goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
  25.128 -by (fast_tac LK_pack 1); 
  25.129 -result();  
  25.130 -
  25.131 -(*An example of why exR should be delayed as long as possible*)
  25.132 -goal LK.thy "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))";
  25.133 -by (fast_tac LK_pack 1);
  25.134 -result();  
  25.135 -
  25.136 -writeln"Solving for a Var";
  25.137 -goal LK.thy 
  25.138 -   "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
  25.139 -by (fast_tac LK_pack 1);
  25.140 -result();
  25.141 -
  25.142 -
  25.143 -writeln"Principia Mathematica *11.53";
  25.144 -goal LK.thy 
  25.145 -    "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
  25.146 -by (fast_tac LK_pack 1);
  25.147 -result();
  25.148 -
  25.149 -
  25.150 -writeln"Principia Mathematica *11.55";
  25.151 -goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
  25.152 -by (fast_tac LK_pack 1);
  25.153 -result();
  25.154 -
  25.155 -writeln"Principia Mathematica *11.61";
  25.156 -goal LK.thy
  25.157 -   "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
  25.158 -by (fast_tac LK_pack 1);
  25.159 -result();
  25.160 -
  25.161 -writeln"Reached end of file.";
  25.162 -
  25.163 -(*21 August 88: loaded in 45.7 secs*)
    26.1 --- a/src/Sequents/ex/Modal/ROOT.ML	Fri Feb 05 21:12:45 1999 +0100
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,26 +0,0 @@
    26.4 -(*  Title:      Modal/ex/ROOT
    26.5 -    ID:         $Id$
    26.6 -    Author:     Martin Coen
    26.7 -    Copyright   1991  University of Cambridge
    26.8 -*)
    26.9 -
   26.10 -Sequents_build_completed;    (*Cause examples to fail if Sequents did*)
   26.11 -
   26.12 -set proof_timing;
   26.13 -
   26.14 -writeln "\nTheorems of T\n";
   26.15 -fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
   26.16 -time_use "Modal/Tthms.ML";
   26.17 -
   26.18 -writeln "\nTheorems of S4\n";
   26.19 -fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2]));
   26.20 -time_use "Modal/Tthms.ML";
   26.21 -time_use "Modal/S4thms.ML";
   26.22 -
   26.23 -writeln "\nTheorems of S43\n";
   26.24 -fun try s = (writeln s;
   26.25 -             prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE 
   26.26 -                                           S43_Prover.solve_tac 3]));
   26.27 -time_use "Modal/Tthms.ML";
   26.28 -time_use "Modal/S4thms.ML";
   26.29 -time_use "Modal/S43thms.ML";
    27.1 --- a/src/Sequents/ex/Modal/S43thms.ML	Fri Feb 05 21:12:45 1999 +0100
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,49 +0,0 @@
    27.4 -(*  Title:      91/Modal/ex/S43thms
    27.5 -    ID:         $Id$
    27.6 -    Author:     Martin Coen
    27.7 -    Copyright   1991  University of Cambridge
    27.8 -*)
    27.9 -
   27.10 -(* Theorems of system S43 *)
   27.11 -
   27.12 -try "|- <>[]P --> []<>P";
   27.13 -try "|- <>[]P --> [][]<>P";
   27.14 -try "|- [](<>P | <>Q) --> []<>P | []<>Q";
   27.15 -try "|- <>[]P & <>[]Q --> <>([]P & []Q)";
   27.16 -try "|- []([]P --> []Q) | []([]Q --> []P)";
   27.17 -try "|- [](<>P --> <>Q) | [](<>Q --> <>P)";
   27.18 -try "|- []([]P --> Q) | []([]Q --> P)";
   27.19 -try "|- [](P --> <>Q) | [](Q --> <>P)";
   27.20 -try "|- [](P --> []Q-->R) | [](P | ([]R --> Q))";
   27.21 -try "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)";
   27.22 -try "|- []([]P | Q) & [](P | []Q) --> []P | []Q";
   27.23 -try "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)";
   27.24 -try "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q";
   27.25 -try "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)";
   27.26 -try "|- <>[]<>P <-> []<>P";
   27.27 -try "|- []<>[]P <-> <>[]P";
   27.28 -
   27.29 -(* These are from Hailpern, LNCS 129 *)
   27.30 -
   27.31 -try "|- [](P & Q) <-> []P & []Q";
   27.32 -try "|- <>(P | Q) <-> <>P | <>Q";
   27.33 -try "|- <>(P --> Q) <-> []P --> <>Q";
   27.34 -
   27.35 -try "|- [](P --> Q) --> <>P --> <>Q";
   27.36 -try "|- []P --> []<>P";
   27.37 -try "|- <>[]P --> <>P";
   27.38 -try "|- []<>[]P --> []<>P";
   27.39 -try "|- <>[]P --> <>[]<>P";
   27.40 -try "|- <>[]P --> []<>P";
   27.41 -try "|- []<>[]P <-> <>[]P";
   27.42 -try "|- <>[]<>P <-> []<>P";
   27.43 -
   27.44 -try "|- []P | []Q --> [](P | Q)";
   27.45 -try "|- <>(P & Q) --> <>P & <>Q";
   27.46 -try "|- [](P | Q) --> []P | <>Q";
   27.47 -try "|- <>P & []Q --> <>(P & Q)";
   27.48 -try "|- [](P | Q) --> <>P | []Q";
   27.49 -try "|- [](P | Q) --> []<>P | []<>Q";
   27.50 -try "|- <>[]P & <>[]Q --> <>(P & Q)";
   27.51 -try "|- <>[](P & Q) <-> <>[]P & <>[]Q";
   27.52 -try "|- []<>(P | Q) <-> []<>P | []<>Q";
    28.1 --- a/src/Sequents/ex/Modal/S4thms.ML	Fri Feb 05 21:12:45 1999 +0100
    28.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.3 @@ -1,40 +0,0 @@
    28.4 -(*  Title:      91/Modal/ex/S4thms
    28.5 -    ID:         $Id$
    28.6 -    Author:     Martin Coen
    28.7 -    Copyright   1991  University of Cambridge
    28.8 -*)
    28.9 -
   28.10 -(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
   28.11 -
   28.12 -try "|- []A --> A";             (* refexivity *)
   28.13 -try "|- []A --> [][]A";         (* transitivity *)
   28.14 -try "|- []A --> <>A";           (* seriality *)
   28.15 -try "|- <>[](<>A --> []<>A)";
   28.16 -try "|- <>[](<>[]A --> []A)";
   28.17 -try "|- []P <-> [][]P";
   28.18 -try "|- <>P <-> <><>P";
   28.19 -try "|- <>[]<>P --> <>P";
   28.20 -try "|- []<>P <-> []<>[]<>P";
   28.21 -try "|- <>[]P <-> <>[]<>[]P";
   28.22 -
   28.23 -(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
   28.24 -
   28.25 -try "|- []P | []Q <-> []([]P | []Q)";
   28.26 -try "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)";
   28.27 -
   28.28 -(* These are from Hailpern, LNCS 129 *)
   28.29 -
   28.30 -try "|- [](P & Q) <-> []P & []Q";
   28.31 -try "|- <>(P | Q) <-> <>P | <>Q";
   28.32 -try "|- <>(P --> Q) <-> ([]P --> <>Q)";
   28.33 -
   28.34 -try "|- [](P --> Q) --> (<>P --> <>Q)";
   28.35 -try "|- []P --> []<>P";
   28.36 -try "|- <>[]P --> <>P";
   28.37 -
   28.38 -try "|- []P | []Q --> [](P | Q)";
   28.39 -try "|- <>(P & Q) --> <>P & <>Q";
   28.40 -try "|- [](P | Q) --> []P | <>Q";
   28.41 -try "|- <>P & []Q --> <>(P & Q)";
   28.42 -try "|- [](P | Q) --> <>P | []Q";
   28.43 -
    29.1 --- a/src/Sequents/ex/Modal/Tthms.ML	Fri Feb 05 21:12:45 1999 +0100
    29.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.3 @@ -1,31 +0,0 @@
    29.4 -(*  Title:      91/Modal/ex/Tthms
    29.5 -    ID:         $Id$
    29.6 -    Author:     Martin Coen
    29.7 -    Copyright   1991  University of Cambridge
    29.8 -*)
    29.9 -
   29.10 -(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
   29.11 -
   29.12 -try "|- []P --> P";
   29.13 -try "|- [](P-->Q) --> ([]P-->[]Q)";    (* normality*)
   29.14 -try "|- (P--<Q) --> []P --> []Q";
   29.15 -try "|- P --> <>P";
   29.16 -
   29.17 -try "|-  [](P & Q) <-> []P & []Q";
   29.18 -try "|-  <>(P | Q) <-> <>P | <>Q";
   29.19 -try "|-  [](P<->Q) <-> (P>-<Q)";
   29.20 -try "|-  <>(P-->Q) <-> ([]P--><>Q)";
   29.21 -try "|-        []P <-> ~<>(~P)";
   29.22 -try "|-     [](~P) <-> ~<>P";
   29.23 -try "|-       ~[]P <-> <>(~P)";
   29.24 -try "|-      [][]P <-> ~<><>(~P)";
   29.25 -try "|- ~<>(P | Q) <-> ~<>P & ~<>Q";
   29.26 -
   29.27 -try "|- []P | []Q --> [](P | Q)";
   29.28 -try "|- <>(P & Q) --> <>P & <>Q";
   29.29 -try "|- [](P | Q) --> []P | <>Q";
   29.30 -try "|- <>P & []Q --> <>(P & Q)";
   29.31 -try "|- [](P | Q) --> <>P | []Q";
   29.32 -try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)";
   29.33 -try "|- (P--<Q) & (Q--<R) --> (P--<R)";
   29.34 -try "|- []P --> <>Q --> <>(P & Q)";
    30.1 --- a/src/Sequents/ex/ROOT.ML	Fri Feb 05 21:12:45 1999 +0100
    30.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.3 @@ -1,7 +0,0 @@
    30.4 -
    30.5 -writeln"Root file for Sequents examples";
    30.6 -Sequents_build_completed;
    30.7 -
    30.8 -use "LK/ROOT.ML";
    30.9 -use "ILL/ROOT.ML";
   30.10 -use "Modal/ROOT.ML";