converted legacy ML scripts;
authorwenzelm
Mon Nov 20 23:47:10 2006 +0100 (2006-11-20)
changeset 2142687ac12bed1ab
parent 21425 c11ab38b78a7
child 21427 7c8f4a331f9b
converted legacy ML scripts;
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/ILL_predlog.thy
src/Sequents/IsaMakefile
src/Sequents/LK/Hard_Quantifiers.thy
src/Sequents/LK/Nat.ML
src/Sequents/LK/Nat.thy
src/Sequents/LK/Propositional.thy
src/Sequents/LK/Quantifiers.thy
src/Sequents/LK/ROOT.ML
src/Sequents/LK/hardquant.ML
src/Sequents/LK/prop.ML
src/Sequents/LK/quant.ML
src/Sequents/LK0.ML
src/Sequents/LK0.thy
src/Sequents/Modal/ROOT.ML
src/Sequents/Modal/S43thms.ML
src/Sequents/Modal/S4thms.ML
src/Sequents/Modal/Tthms.ML
src/Sequents/Modal0.ML
src/Sequents/Modal0.thy
src/Sequents/ROOT.ML
src/Sequents/S4.ML
src/Sequents/S4.thy
src/Sequents/S43.ML
src/Sequents/S43.thy
src/Sequents/T.ML
src/Sequents/T.thy
src/Sequents/Washing.thy
src/Sequents/simpdata.ML
     1.1 --- a/src/Sequents/ILL/ILL_kleene_lemmas.ML	Mon Nov 20 21:23:12 2006 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,81 +0,0 @@
     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 --- a/src/Sequents/ILL/ILL_predlog.ML	Mon Nov 20 21:23:12 2006 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,6 +0,0 @@
     2.4 -
     2.5 -fun auto1 x = prove_goal (the_context ()) x
     2.6 - (fn prems => [best_tac safe_cs 1]) ;
     2.7 -
     2.8 -fun auto2 x = prove_goal (the_context ()) x
     2.9 - (fn prems => [best_tac power_cs 1]) ;
     3.1 --- a/src/Sequents/ILL/ILL_predlog.thy	Mon Nov 20 21:23:12 2006 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,33 +0,0 @@
     3.4 -(* $Id$ *)
     3.5 -
     3.6 -theory ILL_predlog
     3.7 -imports ILL
     3.8 -begin
     3.9 -
    3.10 -typedecl plf
    3.11 -
    3.12 -consts
    3.13 -  "&"   :: "[plf,plf] => plf"   (infixr 35)
    3.14 -  "|"   :: "[plf,plf] => plf"   (infixr 35)
    3.15 -  ">"   :: "[plf,plf] => plf"   (infixr 35)
    3.16 -  "="   :: "[plf,plf] => plf"   (infixr 35)
    3.17 -  "@NG" :: "plf => plf"   ("- _ " [50] 55)
    3.18 -  ff    :: "plf"
    3.19 -
    3.20 -  PL    :: "plf => o"      ("[* / _ / *]" [] 100)
    3.21 -
    3.22 -
    3.23 -translations
    3.24 -
    3.25 -  "[* A & B *]" == "[*A*] && [*B*]"
    3.26 -  "[* A | B *]" == "![*A*] ++ ![*B*]"
    3.27 -  "[* - A *]"   == "[*A > ff*]"
    3.28 -  "[* ff *]"    == "0"
    3.29 -  "[* A = B *]" => "[* (A > B) & (B > A) *]"
    3.30 -
    3.31 -  "[* A > B *]" == "![*A*] -o [*B*]"
    3.32 -
    3.33 -(* another translations for linear implication:
    3.34 -  "[* A > B *]" == "!([*A*] -o [*B*])" *)
    3.35 -
    3.36 -end
     4.1 --- a/src/Sequents/ILL/ROOT.ML	Mon Nov 20 21:23:12 2006 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,5 +0,0 @@
     4.4 -(* $Id$ *)
     4.5 -
     4.6 -time_use_thy "washing";
     4.7 -time_use_thy "ILL_predlog";
     4.8 -time_use "ILL_kleene_lemmas.ML";
     5.1 --- a/src/Sequents/ILL/washing.ML	Mon Nov 20 21:23:12 2006 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,28 +0,0 @@
     5.4 -(* $Id$ *)
     5.5 -
     5.6 -(* "activate" definitions for use in proof *)
     5.7 -
     5.8 -val changeI = [context1] RL ([change] RLN (2,[cut]));
     5.9 -val load1I =  [context1] RL ([load1]  RLN (2,[cut]));
    5.10 -val washI =   [context1] RL ([wash]   RLN (2,[cut]));
    5.11 -val dryI =    [context1] RL ([dry]    RLN (2,[cut]));
    5.12 -
    5.13 -
    5.14 -
    5.15 -(* a load of dirty clothes and two dollars gives you clean clothes *)
    5.16 -
    5.17 -Goal "dollar , dollar , dirty |- clean";
    5.18 -
    5.19 -by (best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1);
    5.20 -
    5.21 -
    5.22 -(* order of premises doesn't matter *)
    5.23 -
    5.24 -prove_goal (the_context ()) "dollar , dirty , dollar |- clean"
    5.25 -(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
    5.26 -
    5.27 -
    5.28 -(* alternative formulation *)
    5.29 -
    5.30 -prove_goal (the_context ()) "dollar , dollar |- dirty -o clean"
    5.31 -(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
     6.1 --- a/src/Sequents/ILL/washing.thy	Mon Nov 20 21:23:12 2006 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,38 +0,0 @@
     6.4 -
     6.5 -(* $Id$ *)
     6.6 -
     6.7 -(* code by Sara Kalvala, based on Paulson's LK
     6.8 -                           and Moore's tisl.ML *)
     6.9 -
    6.10 -theory washing
    6.11 -imports ILL
    6.12 -begin
    6.13 -
    6.14 -consts
    6.15 -  dollar :: o
    6.16 -  quarter :: o
    6.17 -  loaded :: o
    6.18 -  dirty :: o
    6.19 -  wet :: o
    6.20 -  clean :: o
    6.21 -
    6.22 -axioms
    6.23 -  change:
    6.24 -  "dollar |- (quarter >< quarter >< quarter >< quarter)"
    6.25 -
    6.26 -  load1:
    6.27 -  "quarter , quarter , quarter , quarter , quarter |- loaded"
    6.28 -
    6.29 -  load2:
    6.30 -  "dollar , quarter |- loaded"
    6.31 -
    6.32 -  wash:
    6.33 -  "loaded , dirty |- wet"
    6.34 -
    6.35 -  dry:
    6.36 -  "wet, quarter , quarter , quarter |- clean"
    6.37 -
    6.38 -ML {* use_legacy_bindings (the_context ()) *}
    6.39 -
    6.40 -end
    6.41 -
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Sequents/ILL_predlog.thy	Mon Nov 20 23:47:10 2006 +0100
     7.3 @@ -0,0 +1,135 @@
     7.4 +(* $Id$ *)
     7.5 +
     7.6 +theory ILL_predlog
     7.7 +imports ILL
     7.8 +begin
     7.9 +
    7.10 +typedecl plf
    7.11 +
    7.12 +consts
    7.13 +  conj :: "[plf,plf] => plf"   (infixr "&" 35)
    7.14 +  disj :: "[plf,plf] => plf"   (infixr "|" 35)
    7.15 +  impl :: "[plf,plf] => plf"   (infixr ">" 35)
    7.16 +  eq :: "[plf,plf] => plf"   (infixr "=" 35)
    7.17 +  "@NG" :: "plf => plf"   ("- _ " [50] 55)
    7.18 +  ff    :: "plf"
    7.19 +
    7.20 +  PL    :: "plf => o"      ("[* / _ / *]" [] 100)
    7.21 +
    7.22 +translations
    7.23 +
    7.24 +  "[* A & B *]" == "[*A*] && [*B*]"
    7.25 +  "[* A | B *]" == "![*A*] ++ ![*B*]"
    7.26 +  "[* - A *]"   == "[*A > ff*]"
    7.27 +  "[* ff *]"    == "0"
    7.28 +  "[* A = B *]" => "[* (A > B) & (B > A) *]"
    7.29 +
    7.30 +  "[* A > B *]" == "![*A*] -o [*B*]"
    7.31 +
    7.32 +(* another translations for linear implication:
    7.33 +  "[* A > B *]" == "!([*A*] -o [*B*])" *)
    7.34 +
    7.35 +method_setup auto1 =
    7.36 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} ""
    7.37 +method_setup auto2 =
    7.38 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} ""
    7.39 +
    7.40 +(* from [kleene 52] pp 118,119 *)
    7.41 +
    7.42 +lemma k49a: "|- [* A > ( - ( - A)) *]"
    7.43 +  by auto1
    7.44 +
    7.45 +lemma k49b: "|- [*( - ( - ( - A))) = ( - A)*]"
    7.46 +  by auto1
    7.47 +
    7.48 +lemma k49c: "|- [* (A | - A) > ( - - A = A) *]"
    7.49 +  by auto1
    7.50 +
    7.51 +lemma k50a: "|- [* - (A = - A) *]"
    7.52 +  by auto2
    7.53 +
    7.54 +lemma k51a: "|- [* - - (A | - A) *]"
    7.55 +  by auto1
    7.56 +
    7.57 +lemma k51b: "|- [* - - (- - A > A) *]"
    7.58 +  by auto2
    7.59 +
    7.60 +lemma k56a: "|- [* (A | B) > - (- A & - B) *]"
    7.61 +  by auto1
    7.62 +
    7.63 +lemma k56b: "|- [* (-A | B) > - (A & -B) *]"
    7.64 +  by auto1
    7.65 +
    7.66 +lemma k57a: "|- [* (A & B) > - (-A | -B) *]"
    7.67 +  by auto1
    7.68 +
    7.69 +lemma k57b: "|- [* (A & -B) > -(-A | B) *]"
    7.70 +  by auto2
    7.71 +
    7.72 +lemma k58a: "|- [* (A > B) > - (A & -B) *]"
    7.73 +  by auto1
    7.74 +
    7.75 +lemma k58b: "|- [* (A > -B) = -(A & B) *]"
    7.76 +  by auto1
    7.77 +
    7.78 +lemma k58c: "|- [* - (A & B) = (- - A > - B) *]"
    7.79 +  by auto1
    7.80 +
    7.81 +lemma k58d: "|- [* (- - A > - B) = - - (-A | -B) *]"
    7.82 +  by auto1
    7.83 +
    7.84 +lemma k58e: "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]"
    7.85 +  by auto1
    7.86 +
    7.87 +lemma k58f: "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]"
    7.88 +  by auto1
    7.89 +
    7.90 +lemma k58g: "|- [* (- -A > B) > - (A & -B) *]"
    7.91 +  by auto1
    7.92 +
    7.93 +lemma k59a: "|- [* (-A | B) > (A > B) *]"
    7.94 +  by auto1
    7.95 +
    7.96 +lemma k59b: "|- [* (A > B) > - - (-A | B) *]"
    7.97 +  by auto2
    7.98 +
    7.99 +lemma k59c: "|- [* (-A > B) > - -(A | B) *]"
   7.100 +  by auto2
   7.101 +
   7.102 +lemma k60a: "|- [* (A & B) > - (A > -B) *]"
   7.103 +  by auto1
   7.104 +
   7.105 +lemma k60b: "|- [* (A & -B) > - (A > B) *]"
   7.106 +  by auto1
   7.107 +
   7.108 +lemma k60c: "|- [* ( - - A & B) > - (A > -B) *]"
   7.109 +  by auto1
   7.110 +
   7.111 +lemma k60d: "|- [* (- - A & - B) = - (A > B) *]"
   7.112 +  by auto1
   7.113 +
   7.114 +lemma k60e: "|- [* - (A > B) = - (-A | B) *]"
   7.115 +  by auto1
   7.116 +
   7.117 +lemma k60f: "|- [* - (-A | B) = - - (A & -B) *]"
   7.118 +  by auto1
   7.119 +
   7.120 +lemma k60g: "|- [* - - (A > B) = - (A & -B) *]"
   7.121 +  by auto2
   7.122 +
   7.123 +lemma k60h: "|- [* - (A & -B) = (A > - -B) *]"
   7.124 +  by auto1
   7.125 +
   7.126 +lemma k60i: "|- [* (A > - -B) = (- -A > - -B) *]"
   7.127 +  by auto1
   7.128 +
   7.129 +lemma k61a: "|- [* (A | B) > (-A > B) *]"
   7.130 +  by auto1
   7.131 +
   7.132 +lemma k61b: "|- [* - (A | B) = - (-A > B) *]"
   7.133 +  by auto2
   7.134 +
   7.135 +lemma k62a: "|- [* (-A | -B) > - (A & B) *]"
   7.136 +  by auto1
   7.137 +
   7.138 +end
     8.1 --- a/src/Sequents/IsaMakefile	Mon Nov 20 21:23:12 2006 +0100
     8.2 +++ b/src/Sequents/IsaMakefile	Mon Nov 20 23:47:10 2006 +0100
     8.3 @@ -8,7 +8,7 @@
     8.4  
     8.5  default: Sequents
     8.6  images: Sequents
     8.7 -test: Sequents-ILL Sequents-LK Sequents-Modal
     8.8 +test: Sequents-LK
     8.9  all: images test
    8.10  
    8.11  
    8.12 @@ -26,42 +26,22 @@
    8.13  Pure:
    8.14  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    8.15  
    8.16 -$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK0.ML LK0.thy LK.thy \
    8.17 -  modal.ML ROOT.ML simpdata.ML S4.ML \
    8.18 -  S4.thy S43.ML S43.thy Sequents.thy T.ML T.thy prover.ML
    8.19 +$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK0.thy LK.thy \
    8.20 +  modal.ML ROOT.ML simpdata.ML S4.thy S43.thy Sequents.thy T.thy prover.ML \
    8.21 +  ILL_predlog.thy Washing.thy
    8.22  	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents
    8.23  
    8.24  
    8.25 -## Sequents-ILL
    8.26 -
    8.27 -Sequents-ILL: Sequents $(LOG)/Sequents-ILL.gz
    8.28 -
    8.29 -$(LOG)/Sequents-ILL.gz: $(OUT)/Sequents ILL/ILL_kleene_lemmas.ML \
    8.30 -  ILL/ILL_predlog.ML ILL/ILL_predlog.thy ILL/ROOT.ML ILL/washing.ML \
    8.31 -  ILL/washing.thy
    8.32 -	@$(ISATOOL) usedir $(OUT)/Sequents ILL
    8.33 -
    8.34 -
    8.35  ## Sequents-LK
    8.36  
    8.37  Sequents-LK: Sequents $(LOG)/Sequents-LK.gz
    8.38  
    8.39 -$(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/hardquant.ML \
    8.40 -  LK/prop.ML LK/quant.ML LK/Nat.thy LK/Nat.ML
    8.41 +$(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/Hard_Quantifiers.thy \
    8.42 +  LK/Propositional.thy LK/Quantifiers.thy LK/Nat.thy
    8.43  	@$(ISATOOL) usedir $(OUT)/Sequents LK
    8.44  
    8.45  
    8.46 -## Sequents-Modal
    8.47 -
    8.48 -Sequents-Modal: Sequents $(LOG)/Sequents-Modal.gz
    8.49 -
    8.50 -$(LOG)/Sequents-Modal.gz: $(OUT)/Sequents Modal/ROOT.ML \
    8.51 -  Modal/S43thms.ML Modal/S4thms.ML Modal/Tthms.ML ROOT.ML
    8.52 -	@$(ISATOOL) usedir $(OUT)/Sequents Modal
    8.53 -
    8.54 -
    8.55  ## clean
    8.56  
    8.57  clean:
    8.58 -	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ILL.gz \
    8.59 -	  $(LOG)/Sequents-LK.gz $(LOG)/Sequents-Modal.gz
    8.60 +	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-LK.gz
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Sequents/LK/Hard_Quantifiers.thy	Mon Nov 20 23:47:10 2006 +0100
     9.3 @@ -0,0 +1,271 @@
     9.4 +(*  Title:      LK/Hard_Quantifiers.thy
     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 +theory Hard_Quantifiers
    9.19 +imports LK
    9.20 +begin
    9.21 +
    9.22 +lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
    9.23 +  by fast
    9.24 +
    9.25 +lemma "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
    9.26 +  by fast
    9.27 +
    9.28 +lemma "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
    9.29 +  by fast
    9.30 +
    9.31 +lemma "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
    9.32 +  by fast
    9.33 +
    9.34 +
    9.35 +text "Problems requiring quantifier duplication"
    9.36 +
    9.37 +(*Not provable by fast: needs multiple instantiation of ALL*)
    9.38 +lemma "|- (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
    9.39 +  by best_dup
    9.40 +
    9.41 +(*Needs double instantiation of the quantifier*)
    9.42 +lemma "|- EX x. P(x) --> P(a) & P(b)"
    9.43 +  by fast_dup
    9.44 +
    9.45 +lemma "|- EX z. P(z) --> (ALL x. P(x))"
    9.46 +  by best_dup
    9.47 +
    9.48 +
    9.49 +text "Hard examples with quantifiers"
    9.50 +
    9.51 +text "Problem 18"
    9.52 +lemma "|- EX y. ALL x. P(y)-->P(x)"
    9.53 +  by best_dup
    9.54 +
    9.55 +text "Problem 19"
    9.56 +lemma "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
    9.57 +  by best_dup
    9.58 +
    9.59 +text "Problem 20"
    9.60 +lemma "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
    9.61 +    --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
    9.62 +  by fast
    9.63 +
    9.64 +text "Problem 21"
    9.65 +lemma "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
    9.66 +  by best_dup
    9.67 +
    9.68 +text "Problem 22"
    9.69 +lemma "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
    9.70 +  by fast
    9.71 +
    9.72 +text "Problem 23"
    9.73 +lemma "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))"
    9.74 +  by best
    9.75 +
    9.76 +text "Problem 24"
    9.77 +lemma "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
    9.78 +     ~(EX x. P(x)) --> (EX x. Q(x)) & (ALL x. Q(x)|R(x) --> S(x))   
    9.79 +    --> (EX x. P(x)&R(x))"
    9.80 +  by (tactic "pc_tac LK_pack 1")
    9.81 +
    9.82 +text "Problem 25"
    9.83 +lemma "|- (EX x. P(x)) &   
    9.84 +        (ALL x. L(x) --> ~ (M(x) & R(x))) &   
    9.85 +        (ALL x. P(x) --> (M(x) & L(x))) &    
    9.86 +        ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))   
    9.87 +    --> (EX x. Q(x)&P(x))"
    9.88 +  by best
    9.89 +
    9.90 +text "Problem 26"
    9.91 +lemma "|- ((EX x. p(x)) <-> (EX x. q(x))) &        
    9.92 +      (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))    
    9.93 +  --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
    9.94 +  by (tactic "pc_tac LK_pack 1")
    9.95 +
    9.96 +text "Problem 27"
    9.97 +lemma "|- (EX x. P(x) & ~Q(x)) &    
    9.98 +              (ALL x. P(x) --> R(x)) &    
    9.99 +              (ALL x. M(x) & L(x) --> P(x)) &    
   9.100 +              ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))   
   9.101 +          --> (ALL x. M(x) --> ~L(x))"
   9.102 +  by (tactic "pc_tac LK_pack 1")
   9.103 +
   9.104 +text "Problem 28.  AMENDED"
   9.105 +lemma "|- (ALL x. P(x) --> (ALL x. Q(x))) &    
   9.106 +        ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &   
   9.107 +        ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))   
   9.108 +    --> (ALL x. P(x) & L(x) --> M(x))"
   9.109 +  by (tactic "pc_tac LK_pack 1")
   9.110 +
   9.111 +text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
   9.112 +lemma "|- (EX x. P(x)) & (EX y. Q(y))   
   9.113 +    --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
   9.114 +         (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
   9.115 +  by (tactic "pc_tac LK_pack 1")
   9.116 +
   9.117 +text "Problem 30"
   9.118 +lemma "|- (ALL x. P(x) | Q(x) --> ~ R(x)) &  
   9.119 +        (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
   9.120 +    --> (ALL x. S(x))"
   9.121 +  by fast
   9.122 +
   9.123 +text "Problem 31"
   9.124 +lemma "|- ~(EX x. P(x) & (Q(x) | R(x))) &  
   9.125 +        (EX x. L(x) & P(x)) &  
   9.126 +        (ALL x. ~ R(x) --> M(x))   
   9.127 +    --> (EX x. L(x) & M(x))"
   9.128 +  by fast
   9.129 +
   9.130 +text "Problem 32"
   9.131 +lemma "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
   9.132 +        (ALL x. S(x) & R(x) --> L(x)) &  
   9.133 +        (ALL x. M(x) --> R(x))   
   9.134 +    --> (ALL x. P(x) & M(x) --> L(x))"
   9.135 +  by best
   9.136 +
   9.137 +text "Problem 33"
   9.138 +lemma "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->     
   9.139 +     (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
   9.140 +  by fast
   9.141 +
   9.142 +text "Problem 34  AMENDED (TWICE!!)"
   9.143 +(*Andrews's challenge*)
   9.144 +lemma "|- ((EX x. ALL y. p(x) <-> p(y))  <->               
   9.145 +               ((EX x. q(x)) <-> (ALL y. p(y))))     <->         
   9.146 +              ((EX x. ALL y. q(x) <-> q(y))  <->                 
   9.147 +               ((EX x. p(x)) <-> (ALL y. q(y))))"
   9.148 +  by best_dup
   9.149 +
   9.150 +text "Problem 35"
   9.151 +lemma "|- EX x y. P(x,y) -->  (ALL u v. P(u,v))"
   9.152 +  by best_dup
   9.153 +
   9.154 +text "Problem 36"
   9.155 +lemma "|- (ALL x. EX y. J(x,y)) &  
   9.156 +         (ALL x. EX y. G(x,y)) &  
   9.157 +         (ALL x y. J(x,y) | G(x,y) -->    
   9.158 +         (ALL z. J(y,z) | G(y,z) --> H(x,z)))    
   9.159 +         --> (ALL x. EX y. H(x,y))"
   9.160 +  by fast
   9.161 +
   9.162 +text "Problem 37"
   9.163 +lemma "|- (ALL z. EX w. ALL x. EX y.  
   9.164 +           (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) &  
   9.165 +        (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &  
   9.166 +        ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))   
   9.167 +    --> (ALL x. EX y. R(x,y))"
   9.168 +  by (tactic "pc_tac LK_pack 1")
   9.169 +
   9.170 +text "Problem 38"
   9.171 +lemma "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->         
   9.172 +                 (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->          
   9.173 +         (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &     
   9.174 +                 (~p(a) | ~(EX y. p(y) & r(x,y)) |                           
   9.175 +                 (EX z. EX w. p(z) & r(x,w) & r(w,z))))"
   9.176 +  by (tactic "pc_tac LK_pack 1")
   9.177 +
   9.178 +text "Problem 39"
   9.179 +lemma "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
   9.180 +  by fast
   9.181 +
   9.182 +text "Problem 40.  AMENDED"
   9.183 +lemma "|- (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
   9.184 +         ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
   9.185 +  by fast
   9.186 +
   9.187 +text "Problem 41"
   9.188 +lemma "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))       
   9.189 +         --> ~ (EX z. ALL x. f(x,z))"
   9.190 +  by fast
   9.191 +
   9.192 +text "Problem 42"
   9.193 +lemma "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))"
   9.194 +  oops
   9.195 +
   9.196 +text "Problem 43"
   9.197 +lemma "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y)))  
   9.198 +          --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))"
   9.199 +  oops
   9.200 +
   9.201 +text "Problem 44"
   9.202 +lemma "|- (ALL x. f(x) -->                                         
   9.203 +                 (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
   9.204 +         (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
   9.205 +         --> (EX x. j(x) & ~f(x))"
   9.206 +  by fast
   9.207 +
   9.208 +text "Problem 45"
   9.209 +lemma "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))         
   9.210 +                      --> (ALL y. g(y) & h(x,y) --> k(y))) &     
   9.211 +      ~ (EX y. l(y) & k(y)) &                                    
   9.212 +      (EX x. f(x) & (ALL y. h(x,y) --> l(y))                     
   9.213 +                   & (ALL y. g(y) & h(x,y) --> j(x,y)))          
   9.214 +      --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))"
   9.215 +  by best
   9.216 +
   9.217 +
   9.218 +text "Problems (mainly) involving equality or functions"
   9.219 +
   9.220 +text "Problem 48"
   9.221 +lemma "|- (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
   9.222 +  by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *})
   9.223 +
   9.224 +text "Problem 50"
   9.225 +lemma "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
   9.226 +  by best_dup
   9.227 +
   9.228 +text "Problem 51"
   9.229 +lemma "|- (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->   
   9.230 +         (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
   9.231 +  by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *})
   9.232 +
   9.233 +text "Problem 52"  (*Almost the same as 51. *)
   9.234 +lemma "|- (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->
   9.235 +         (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"
   9.236 +  by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *})
   9.237 +
   9.238 +text "Problem 56"
   9.239 +lemma "|- (ALL x.(EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
   9.240 +  by (tactic {* best_tac (LK_pack add_unsafes [thm "symL", thm "subst"]) 1 *})
   9.241 +  (*requires tricker to orient the equality properly*)
   9.242 +
   9.243 +text "Problem 57"
   9.244 +lemma "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
   9.245 +         (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
   9.246 +  by fast
   9.247 +
   9.248 +text "Problem 58!"
   9.249 +lemma "|- (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
   9.250 +  by (tactic {* fast_tac (LK_pack add_safes [thm "subst"]) 1 *})
   9.251 +
   9.252 +text "Problem 59"
   9.253 +(*Unification works poorly here -- the abstraction %sobj prevents efficient
   9.254 +  operation of the occurs check*)
   9.255 +ML {* Unify.trace_bound := !Unify.search_bound - 1 *}
   9.256 +lemma "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
   9.257 +  by best_dup
   9.258 +
   9.259 +text "Problem 60"
   9.260 +lemma "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
   9.261 +  by fast
   9.262 +
   9.263 +text "Problem 62 as corrected in JAR 18 (1997), page 135"
   9.264 +lemma "|- (ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->
   9.265 +      (ALL x. (~p(a) | p(x) | p(f(f(x)))) &                       
   9.266 +              (~p(a) | ~p(f(x)) | p(f(f(x)))))"
   9.267 +  by fast
   9.268 +
   9.269 +(*18 June 92: loaded in 372 secs*)
   9.270 +(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
   9.271 +(*29 June 92: loaded in 370 secs*)
   9.272 +(*18 September 2005: loaded in 1.809 secs*)
   9.273 +
   9.274 +end
    10.1 --- a/src/Sequents/LK/Nat.ML	Mon Nov 20 21:23:12 2006 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,49 +0,0 @@
    10.4 -(*  Title:      Sequents/LK/Nat.ML
    10.5 -    ID:         $Id$
    10.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 -    Copyright   1999  University of Cambridge
    10.8 -*)
    10.9 -
   10.10 -Addsimps [Suc_neq_0];
   10.11 -
   10.12 -Add_safes [Suc_inject RS L_of_imp];
   10.13 -
   10.14 -Goal "|- Suc(k) ~= k";
   10.15 -by (res_inst_tac [("n","k")] induct 1);
   10.16 -by (Simp_tac 1);
   10.17 -by (Fast_tac 1);
   10.18 -qed "Suc_n_not_n";
   10.19 -
   10.20 -Goalw [add_def] "|- 0+n = n";
   10.21 -by (rtac rec_0 1);
   10.22 -qed "add_0";
   10.23 -
   10.24 -Goalw [add_def] "|- Suc(m)+n = Suc(m+n)";
   10.25 -by (rtac rec_Suc 1);
   10.26 -qed "add_Suc";
   10.27 -
   10.28 -Addsimps [add_0, add_Suc];
   10.29 -
   10.30 -Goal "|- (k+m)+n = k+(m+n)";
   10.31 -by (res_inst_tac [("n","k")] induct 1);
   10.32 -by (Simp_tac 1);
   10.33 -by (Asm_simp_tac 1);
   10.34 -qed "add_assoc";
   10.35 -
   10.36 -Goal "|- m+0 = m";
   10.37 -by (res_inst_tac [("n","m")] induct 1);
   10.38 -by (Simp_tac 1);
   10.39 -by (Asm_simp_tac 1);
   10.40 -qed "add_0_right";
   10.41 -
   10.42 -Goal "|- m+Suc(n) = Suc(m+n)";
   10.43 -by (res_inst_tac [("n","m")] induct 1);
   10.44 -by (ALLGOALS (Asm_simp_tac));
   10.45 -qed "add_Suc_right";
   10.46 -
   10.47 -(*Example used in Reference Manual, Doc/Ref/simplifier.tex*)
   10.48 -val [prem] = Goal "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)";
   10.49 -by (res_inst_tac [("n","i")] induct 1);
   10.50 -by (Simp_tac 1);
   10.51 -by (simp_tac (simpset() addsimps [prem]) 1);
   10.52 -result();
    11.1 --- a/src/Sequents/LK/Nat.thy	Mon Nov 20 21:23:12 2006 +0100
    11.2 +++ b/src/Sequents/LK/Nat.thy	Mon Nov 20 23:47:10 2006 +0100
    11.3 @@ -27,6 +27,52 @@
    11.4    rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
    11.5    add_def:     "m+n == rec(m, n, %x y. Suc(y))"
    11.6  
    11.7 -ML {* use_legacy_bindings (the_context ()) *}
    11.8 +
    11.9 +declare Suc_neq_0 [simp]
   11.10 +
   11.11 +lemma Suc_inject_rule: "$H, $G, m = n |- $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G |- $E"
   11.12 +  by (rule L_of_imp [OF Suc_inject])
   11.13 +
   11.14 +lemma Suc_n_not_n: "|- Suc(k) ~= k"
   11.15 +  apply (rule_tac n = k in induct)
   11.16 +  apply (tactic {* simp_tac (LK_ss addsimps [thm "Suc_neq_0"]) 1 *})
   11.17 +  apply (tactic {* fast_tac (LK_pack add_safes [thm "Suc_inject_rule"]) 1 *})
   11.18 +  done
   11.19 +
   11.20 +lemma add_0: "|- 0+n = n"
   11.21 +  apply (unfold add_def)
   11.22 +  apply (rule rec_0)
   11.23 +  done
   11.24 +
   11.25 +lemma add_Suc: "|- Suc(m)+n = Suc(m+n)"
   11.26 +  apply (unfold add_def)
   11.27 +  apply (rule rec_Suc)
   11.28 +  done
   11.29 +
   11.30 +declare add_0 [simp] add_Suc [simp]
   11.31 +
   11.32 +lemma add_assoc: "|- (k+m)+n = k+(m+n)"
   11.33 +  apply (rule_tac n = "k" in induct)
   11.34 +  apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *})
   11.35 +  apply (tactic {* simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *})
   11.36 +  done
   11.37 +
   11.38 +lemma add_0_right: "|- m+0 = m"
   11.39 +  apply (rule_tac n = "m" in induct)
   11.40 +  apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *})
   11.41 +  apply (tactic {* simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *})
   11.42 +  done
   11.43 +
   11.44 +lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)"
   11.45 +  apply (rule_tac n = "m" in induct)
   11.46 +  apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *})
   11.47 +  apply (tactic {* simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *})
   11.48 +  done
   11.49 +
   11.50 +lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)"
   11.51 +  apply (rule_tac n = "i" in induct)
   11.52 +  apply (tactic {* simp_tac (LK_ss addsimps [thm "add_0"]) 1 *})
   11.53 +  apply (tactic {* asm_simp_tac (LK_ss addsimps [thm "add_Suc"]) 1 *})
   11.54 +  done
   11.55  
   11.56  end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Sequents/LK/Propositional.thy	Mon Nov 20 23:47:10 2006 +0100
    12.3 @@ -0,0 +1,160 @@
    12.4 +(*  Title:      LK/Propositional.thy
    12.5 +    ID:         $Id$
    12.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7 +    Copyright   1992  University of Cambridge
    12.8 +*)
    12.9 +
   12.10 +header {* Classical sequent calculus: examples with propositional connectives *}
   12.11 +
   12.12 +theory Propositional
   12.13 +imports LK
   12.14 +begin
   12.15 +
   12.16 +text "absorptive laws of & and | "
   12.17 +
   12.18 +lemma "|- P & P <-> P"
   12.19 +  by fast_prop
   12.20 +
   12.21 +lemma "|- P | P <-> P"
   12.22 +  by fast_prop
   12.23 +
   12.24 +
   12.25 +text "commutative laws of & and | "
   12.26 +
   12.27 +lemma "|- P & Q  <->  Q & P"
   12.28 +  by fast_prop
   12.29 +
   12.30 +lemma "|- P | Q  <->  Q | P"
   12.31 +  by fast_prop
   12.32 +
   12.33 +
   12.34 +text "associative laws of & and | "
   12.35 +
   12.36 +lemma "|- (P & Q) & R  <->  P & (Q & R)"
   12.37 +  by fast_prop
   12.38 +
   12.39 +lemma "|- (P | Q) | R  <->  P | (Q | R)"
   12.40 +  by fast_prop
   12.41 +
   12.42 +
   12.43 +text "distributive laws of & and | "
   12.44 +
   12.45 +lemma "|- (P & Q) | R  <-> (P | R) & (Q | R)"
   12.46 +  by fast_prop
   12.47 +
   12.48 +lemma "|- (P | Q) & R  <-> (P & R) | (Q & R)"
   12.49 +  by fast_prop
   12.50 +
   12.51 +
   12.52 +text "Laws involving implication"
   12.53 +
   12.54 +lemma "|- (P|Q --> R) <-> (P-->R) & (Q-->R)"
   12.55 +  by fast_prop
   12.56 +
   12.57 +lemma "|- (P & Q --> R) <-> (P--> (Q-->R))"
   12.58 +  by fast_prop
   12.59 +
   12.60 +lemma "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   12.61 +  by fast_prop
   12.62 +
   12.63 +
   12.64 +text "Classical theorems"
   12.65 +
   12.66 +lemma "|- P|Q --> P| ~P&Q"
   12.67 +  by fast_prop
   12.68 +
   12.69 +lemma "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)"
   12.70 +  by fast_prop
   12.71 +
   12.72 +lemma "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)"
   12.73 +  by fast_prop
   12.74 +
   12.75 +lemma "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)"
   12.76 +  by fast_prop
   12.77 +
   12.78 +
   12.79 +(*If and only if*)
   12.80 +
   12.81 +lemma "|- (P<->Q) <-> (Q<->P)"
   12.82 +  by fast_prop
   12.83 +
   12.84 +lemma "|- ~ (P <-> ~P)"
   12.85 +  by fast_prop
   12.86 +
   12.87 +
   12.88 +(*Sample problems from 
   12.89 +  F. J. Pelletier, 
   12.90 +  Seventy-Five Problems for Testing Automatic Theorem Provers,
   12.91 +  J. Automated Reasoning 2 (1986), 191-216.
   12.92 +  Errata, JAR 4 (1988), 236-236.
   12.93 +*)
   12.94 +
   12.95 +(*1*)
   12.96 +lemma "|- (P-->Q)  <->  (~Q --> ~P)"
   12.97 +  by fast_prop
   12.98 +
   12.99 +(*2*)
  12.100 +lemma "|- ~ ~ P  <->  P"
  12.101 +  by fast_prop
  12.102 +
  12.103 +(*3*)
  12.104 +lemma "|- ~(P-->Q) --> (Q-->P)"
  12.105 +  by fast_prop
  12.106 +
  12.107 +(*4*)
  12.108 +lemma "|- (~P-->Q)  <->  (~Q --> P)"
  12.109 +  by fast_prop
  12.110 +
  12.111 +(*5*)
  12.112 +lemma "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))"
  12.113 +  by fast_prop
  12.114 +
  12.115 +(*6*)
  12.116 +lemma "|- P | ~ P"
  12.117 +  by fast_prop
  12.118 +
  12.119 +(*7*)
  12.120 +lemma "|- P | ~ ~ ~ P"
  12.121 +  by fast_prop
  12.122 +
  12.123 +(*8.  Peirce's law*)
  12.124 +lemma "|- ((P-->Q) --> P)  -->  P"
  12.125 +  by fast_prop
  12.126 +
  12.127 +(*9*)
  12.128 +lemma "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
  12.129 +  by fast_prop
  12.130 +
  12.131 +(*10*)
  12.132 +lemma "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q"
  12.133 +  by fast_prop
  12.134 +
  12.135 +(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
  12.136 +lemma "|- P<->P"
  12.137 +  by fast_prop
  12.138 +
  12.139 +(*12.  "Dijkstra's law"*)
  12.140 +lemma "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
  12.141 +  by fast_prop
  12.142 +
  12.143 +(*13.  Distributive law*)
  12.144 +lemma "|- P | (Q & R)  <-> (P | Q) & (P | R)"
  12.145 +  by fast_prop
  12.146 +
  12.147 +(*14*)
  12.148 +lemma "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
  12.149 +  by fast_prop
  12.150 +
  12.151 +(*15*)
  12.152 +lemma "|- (P --> Q) <-> (~P | Q)"
  12.153 +  by fast_prop
  12.154 +
  12.155 +(*16*)
  12.156 +lemma "|- (P-->Q) | (Q-->P)"
  12.157 +  by fast_prop
  12.158 +
  12.159 +(*17*)
  12.160 +lemma "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
  12.161 +  by fast_prop
  12.162 +
  12.163 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Sequents/LK/Quantifiers.thy	Mon Nov 20 23:47:10 2006 +0100
    13.3 @@ -0,0 +1,143 @@
    13.4 +(*  Title:      LK/Quantifiers.ML
    13.5 +    ID:         $Id$
    13.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 +    Copyright   1992  University of Cambridge
    13.8 +
    13.9 +Classical sequent calculus: examples with quantifiers.
   13.10 +*)
   13.11 +
   13.12 +theory Quantifiers
   13.13 +imports LK
   13.14 +begin
   13.15 +
   13.16 +lemma "|- (ALL x. P)  <->  P"
   13.17 +  by fast
   13.18 +
   13.19 +lemma "|- (ALL x y. P(x,y))  <->  (ALL y x. P(x,y))"
   13.20 +  by fast
   13.21 +
   13.22 +lemma "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)"
   13.23 +  by fast
   13.24 +
   13.25 +
   13.26 +text "Permutation of existential quantifier."
   13.27 +
   13.28 +lemma "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))"
   13.29 +  by fast
   13.30 +
   13.31 +lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
   13.32 +  by fast
   13.33 +
   13.34 +(*Converse is invalid*)
   13.35 +lemma "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))"
   13.36 +  by fast
   13.37 +
   13.38 +
   13.39 +text "Pushing ALL into an implication."
   13.40 +
   13.41 +lemma "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))"
   13.42 +  by fast
   13.43 +
   13.44 +lemma "|- (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   13.45 +  by fast
   13.46 +
   13.47 +lemma "|- (EX x. P)  <->  P"
   13.48 +  by fast
   13.49 +
   13.50 +
   13.51 +text "Distribution of EX over disjunction."
   13.52 +
   13.53 +lemma "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))"
   13.54 +  by fast
   13.55 +
   13.56 +(*Converse is invalid*)
   13.57 +lemma "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))"
   13.58 +  by fast
   13.59 +
   13.60 +
   13.61 +text "Harder examples: classical theorems."
   13.62 +
   13.63 +lemma "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
   13.64 +  by fast
   13.65 +
   13.66 +lemma "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
   13.67 +  by fast
   13.68 +
   13.69 +lemma "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
   13.70 +  by fast
   13.71 +
   13.72 +
   13.73 +text "Basic test of quantifier reasoning"
   13.74 +
   13.75 +lemma "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
   13.76 +  by fast
   13.77 +
   13.78 +lemma "|- (ALL x. Q(x))  -->  (EX x. Q(x))"
   13.79 +  by fast
   13.80 +
   13.81 +
   13.82 +text "The following are invalid!"
   13.83 +
   13.84 +(*INVALID*)
   13.85 +lemma "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   13.86 +  apply fast?
   13.87 +  apply (rule _)
   13.88 +  oops
   13.89 +
   13.90 +(*INVALID*)
   13.91 +lemma "|- (EX x. Q(x))  -->  (ALL x. Q(x))"
   13.92 +  apply fast?
   13.93 +  apply (rule _)
   13.94 +  oops
   13.95 +
   13.96 +(*INVALID*)
   13.97 +lemma "|- P(?a) --> (ALL x. P(x))"
   13.98 +  apply fast?
   13.99 +  apply (rule _)
  13.100 +  oops
  13.101 +
  13.102 +(*INVALID*)
  13.103 +lemma "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
  13.104 +  apply fast?
  13.105 +  apply (rule _)
  13.106 +  oops
  13.107 +
  13.108 +
  13.109 +text "Back to things that are provable..."
  13.110 +
  13.111 +lemma "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
  13.112 +  by fast
  13.113 +
  13.114 +(*An example of why exR should be delayed as long as possible*)
  13.115 +lemma "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))"
  13.116 +  by fast
  13.117 +
  13.118 +
  13.119 +text "Solving for a Var"
  13.120 +
  13.121 +lemma "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
  13.122 +  by fast
  13.123 +
  13.124 +
  13.125 +text "Principia Mathematica *11.53"
  13.126 +
  13.127 +lemma "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  13.128 +  by fast
  13.129 +
  13.130 +
  13.131 +text "Principia Mathematica *11.55"
  13.132 +
  13.133 +lemma "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  13.134 +  by fast
  13.135 +
  13.136 +
  13.137 +text "Principia Mathematica *11.61"
  13.138 +
  13.139 +lemma "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  13.140 +  by fast
  13.141 +
  13.142 +
  13.143 +(*21 August 88: loaded in 45.7 secs*)
  13.144 +(*18 September 2005: loaded in 0.114 secs*)
  13.145 +
  13.146 +end
    14.1 --- a/src/Sequents/LK/ROOT.ML	Mon Nov 20 21:23:12 2006 +0100
    14.2 +++ b/src/Sequents/LK/ROOT.ML	Mon Nov 20 23:47:10 2006 +0100
    14.3 @@ -6,7 +6,7 @@
    14.4  Examples for Classical Logic.
    14.5  *)
    14.6  
    14.7 -time_use "prop.ML";
    14.8 -time_use "quant.ML";
    14.9 -time_use "hardquant.ML";
   14.10 -time_use_thy "Nat";
   14.11 +use_thy "Propositional";
   14.12 +use_thy "Quantifiers";
   14.13 +use_thy "Hard_Quantifiers";
   14.14 +use_thy "Nat";
    15.1 --- a/src/Sequents/LK/hardquant.ML	Mon Nov 20 21:23:12 2006 +0100
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,308 +0,0 @@
    15.4 -(*  Title:      LK/ex/hard-quant
    15.5 -    ID:         $Id$
    15.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7 -    Copyright   1992  University of Cambridge
    15.8 -
    15.9 -Hard examples with quantifiers.  Can be read to test the LK system.
   15.10 -From  F. J. Pelletier,
   15.11 -  Seventy-Five Problems for Testing Automatic Theorem Provers,
   15.12 -  J. Automated Reasoning 2 (1986), 191-216.
   15.13 -  Errata, JAR 4 (1988), 236-236.
   15.14 -
   15.15 -Uses pc_tac rather than fast_tac when the former is significantly faster.
   15.16 -*)
   15.17 -
   15.18 -context (theory "LK");
   15.19 -
   15.20 -Goal "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
   15.21 -by (Fast_tac 1);
   15.22 -result();
   15.23 -
   15.24 -Goal "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
   15.25 -by (Fast_tac 1);
   15.26 -result();
   15.27 -
   15.28 -Goal "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
   15.29 -by (Fast_tac 1);
   15.30 -result();
   15.31 -
   15.32 -Goal "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
   15.33 -by (Fast_tac 1);
   15.34 -result();
   15.35 -
   15.36 -writeln"Problems requiring quantifier duplication";
   15.37 -
   15.38 -(*Not provable by Fast_tac: needs multiple instantiation of ALL*)
   15.39 -Goal "|- (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
   15.40 -by (best_tac LK_dup_pack 1);
   15.41 -result();
   15.42 -
   15.43 -(*Needs double instantiation of the quantifier*)
   15.44 -Goal "|- EX x. P(x) --> P(a) & P(b)";
   15.45 -by (fast_tac LK_dup_pack 1);
   15.46 -result();
   15.47 -
   15.48 -Goal "|- EX z. P(z) --> (ALL x. P(x))";
   15.49 -by (best_tac LK_dup_pack 1);
   15.50 -result();
   15.51 -
   15.52 -writeln"Hard examples with quantifiers";
   15.53 -
   15.54 -writeln"Problem 18";
   15.55 -Goal "|- EX y. ALL x. P(y)-->P(x)";
   15.56 -by (best_tac LK_dup_pack 1);
   15.57 -result();
   15.58 -
   15.59 -writeln"Problem 19";
   15.60 -Goal "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
   15.61 -by (best_tac LK_dup_pack 1);
   15.62 -result();
   15.63 -
   15.64 -writeln"Problem 20";
   15.65 -Goal "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
   15.66 -\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
   15.67 -by (Fast_tac 1);
   15.68 -result();
   15.69 -
   15.70 -writeln"Problem 21";
   15.71 -Goal "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
   15.72 -by (best_tac LK_dup_pack 1);
   15.73 -result();
   15.74 -
   15.75 -writeln"Problem 22";
   15.76 -Goal "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
   15.77 -by (Fast_tac 1);
   15.78 -result();
   15.79 -
   15.80 -writeln"Problem 23";
   15.81 -Goal "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
   15.82 -by (best_tac LK_pack 1);
   15.83 -result();
   15.84 -
   15.85 -writeln"Problem 24";
   15.86 -Goal "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
   15.87 -\    ~(EX x. P(x)) --> (EX x. Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
   15.88 -\   --> (EX x. P(x)&R(x))";
   15.89 -by (pc_tac LK_pack 1);
   15.90 -result();
   15.91 -
   15.92 -writeln"Problem 25";
   15.93 -Goal "|- (EX x. P(x)) &  \
   15.94 -\       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
   15.95 -\       (ALL x. P(x) --> (M(x) & L(x))) &   \
   15.96 -\       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
   15.97 -\   --> (EX x. Q(x)&P(x))";
   15.98 -by (best_tac LK_pack 1);
   15.99 -result();
  15.100 -
  15.101 -writeln"Problem 26";
  15.102 -Goal "|- ((EX x. p(x)) <-> (EX x. q(x))) &       \
  15.103 -\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
  15.104 -\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
  15.105 -by (pc_tac LK_pack 1);
  15.106 -result();
  15.107 -
  15.108 -writeln"Problem 27";
  15.109 -Goal "|- (EX x. P(x) & ~Q(x)) &   \
  15.110 -\             (ALL x. P(x) --> R(x)) &   \
  15.111 -\             (ALL x. M(x) & L(x) --> P(x)) &   \
  15.112 -\             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
  15.113 -\         --> (ALL x. M(x) --> ~L(x))";
  15.114 -by (pc_tac LK_pack 1);
  15.115 -result();
  15.116 -
  15.117 -writeln"Problem 28.  AMENDED";
  15.118 -Goal "|- (ALL x. P(x) --> (ALL x. Q(x))) &   \
  15.119 -\       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
  15.120 -\       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
  15.121 -\   --> (ALL x. P(x) & L(x) --> M(x))";
  15.122 -by (pc_tac LK_pack 1);
  15.123 -result();
  15.124 -
  15.125 -writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
  15.126 -Goal "|- (EX x. P(x)) & (EX y. Q(y))  \
  15.127 -\   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
  15.128 -\        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
  15.129 -by (pc_tac LK_pack 1);
  15.130 -result();
  15.131 -
  15.132 -writeln"Problem 30";
  15.133 -Goal "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
  15.134 -\       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
  15.135 -\   --> (ALL x. S(x))";
  15.136 -by (Fast_tac 1);
  15.137 -result();
  15.138 -
  15.139 -writeln"Problem 31";
  15.140 -Goal "|- ~(EX x. P(x) & (Q(x) | R(x))) & \
  15.141 -\       (EX x. L(x) & P(x)) & \
  15.142 -\       (ALL x. ~ R(x) --> M(x))  \
  15.143 -\   --> (EX x. L(x) & M(x))";
  15.144 -by (Fast_tac 1);
  15.145 -result();
  15.146 -
  15.147 -writeln"Problem 32";
  15.148 -Goal "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
  15.149 -\       (ALL x. S(x) & R(x) --> L(x)) & \
  15.150 -\       (ALL x. M(x) --> R(x))  \
  15.151 -\   --> (ALL x. P(x) & M(x) --> L(x))";
  15.152 -by (best_tac LK_pack 1);
  15.153 -result();
  15.154 -
  15.155 -writeln"Problem 33";
  15.156 -Goal "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
  15.157 -\    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
  15.158 -by (Fast_tac 1);
  15.159 -result();
  15.160 -
  15.161 -writeln"Problem 34  AMENDED (TWICE!!)";
  15.162 -(*Andrews's challenge*)
  15.163 -Goal "|- ((EX x. ALL y. p(x) <-> p(y))  <->              \
  15.164 -\              ((EX x. q(x)) <-> (ALL y. p(y))))     <->        \
  15.165 -\             ((EX x. ALL y. q(x) <-> q(y))  <->                \
  15.166 -\              ((EX x. p(x)) <-> (ALL y. q(y))))";
  15.167 -by (best_tac LK_dup_pack 1); (*10 secs!*)
  15.168 -result();
  15.169 -
  15.170 -
  15.171 -writeln"Problem 35";
  15.172 -Goal "|- EX x y. P(x,y) -->  (ALL u v. P(u,v))";
  15.173 -by (best_tac LK_dup_pack 1);
  15.174 -result();
  15.175 -
  15.176 -writeln"Problem 36";
  15.177 -Goal "|- (ALL x. EX y. J(x,y)) & \
  15.178 -\        (ALL x. EX y. G(x,y)) & \
  15.179 -\        (ALL x y. J(x,y) | G(x,y) -->   \
  15.180 -\        (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
  15.181 -\        --> (ALL x. EX y. H(x,y))";
  15.182 -by (Fast_tac 1);
  15.183 -result();
  15.184 -
  15.185 -writeln"Problem 37";
  15.186 -Goal "|- (ALL z. EX w. ALL x. EX y. \
  15.187 -\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
  15.188 -\       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
  15.189 -\       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
  15.190 -\   --> (ALL x. EX y. R(x,y))";
  15.191 -by (pc_tac LK_pack 1);
  15.192 -result();
  15.193 -
  15.194 -writeln"Problem 38";
  15.195 -Goal "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
  15.196 -\                (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
  15.197 -\        (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
  15.198 -\                (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
  15.199 -\                (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
  15.200 -by (pc_tac LK_pack 1);
  15.201 -result();
  15.202 -
  15.203 -writeln"Problem 39";
  15.204 -Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
  15.205 -by (Fast_tac 1);
  15.206 -result();
  15.207 -
  15.208 -writeln"Problem 40.  AMENDED";
  15.209 -Goal "|- (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
  15.210 -\        ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
  15.211 -by (Fast_tac 1);
  15.212 -result();
  15.213 -
  15.214 -writeln"Problem 41";
  15.215 -Goal "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))      \
  15.216 -\        --> ~ (EX z. ALL x. f(x,z))";
  15.217 -by (Fast_tac 1);
  15.218 -result();
  15.219 -
  15.220 -writeln"Problem 42";
  15.221 -Goal "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))";
  15.222 -
  15.223 -writeln"Problem 43  NOT PROVED AUTOMATICALLY";
  15.224 -Goal "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \
  15.225 -\         --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))";
  15.226 -
  15.227 -writeln"Problem 44";
  15.228 -Goal "|- (ALL x. f(x) -->                                        \
  15.229 -\                (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
  15.230 -\        (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
  15.231 -\        --> (EX x. j(x) & ~f(x))";
  15.232 -by (Fast_tac 1);
  15.233 -result();
  15.234 -
  15.235 -writeln"Problem 45";
  15.236 -Goal "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))        \
  15.237 -\                     --> (ALL y. g(y) & h(x,y) --> k(y))) &    \
  15.238 -\     ~ (EX y. l(y) & k(y)) &                                   \
  15.239 -\     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
  15.240 -\                  & (ALL y. g(y) & h(x,y) --> j(x,y)))         \
  15.241 -\     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
  15.242 -by (best_tac LK_pack 1);
  15.243 -result();
  15.244 -
  15.245 -
  15.246 -writeln"Problems (mainly) involving equality or functions";
  15.247 -
  15.248 -writeln"Problem 48";
  15.249 -Goal "|- (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
  15.250 -by (fast_tac (pack() add_safes [subst]) 1);
  15.251 -result();
  15.252 -
  15.253 -writeln"Problem 50";
  15.254 -Goal "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
  15.255 -by (best_tac LK_dup_pack 1);
  15.256 -result();
  15.257 -
  15.258 -writeln"Problem 51";
  15.259 -Goal "|- (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
  15.260 -\        (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
  15.261 -by (fast_tac (pack() add_safes [subst]) 1);
  15.262 -result();
  15.263 -
  15.264 -writeln"Problem 52";
  15.265 -(*Almost the same as 51. *)
  15.266 -Goal "|- (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
  15.267 -\        (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)";
  15.268 -by (fast_tac (pack() add_safes [subst]) 1);
  15.269 -result();
  15.270 -
  15.271 -writeln"Problem 56";
  15.272 -Goal "|- (ALL x.(EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
  15.273 -by (best_tac (pack() add_unsafes [symL, subst]) 1);
  15.274 -(*requires tricker to orient the equality properly*)
  15.275 -result();
  15.276 -
  15.277 -writeln"Problem 57";
  15.278 -Goal "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
  15.279 -\        (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
  15.280 -by (Fast_tac 1);
  15.281 -result();
  15.282 -
  15.283 -writeln"Problem 58!";
  15.284 -Goal "|- (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
  15.285 -by (fast_tac (pack() add_safes [subst]) 1);
  15.286 -result();
  15.287 -
  15.288 -writeln"Problem 59";
  15.289 -(*Unification works poorly here -- the abstraction %sobj prevents efficient
  15.290 -  operation of the occurs check*)
  15.291 -Unify.trace_bound := !Unify.search_bound - 1;
  15.292 -Goal "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
  15.293 -by (best_tac LK_dup_pack 1);
  15.294 -result();
  15.295 -
  15.296 -writeln"Problem 60";
  15.297 -Goal "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
  15.298 -by (Fast_tac 1);
  15.299 -result();
  15.300 -
  15.301 -writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
  15.302 -Goal "|- (ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->     \
  15.303 -\     (ALL x. (~p(a) | p(x) | p(f(f(x)))) &                      \
  15.304 -\             (~p(a) | ~p(f(x)) | p(f(f(x)))))";
  15.305 -by (Fast_tac 1);
  15.306 -result();
  15.307 -
  15.308 -(*18 June 92: loaded in 372 secs*)
  15.309 -(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
  15.310 -(*29 June 92: loaded in 370 secs*)
  15.311 -(*18 September 2005: loaded in 1.809 secs*)
    16.1 --- a/src/Sequents/LK/prop.ML	Mon Nov 20 21:23:12 2006 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,190 +0,0 @@
    16.4 -(*  Title:      LK/ex/prop
    16.5 -    ID:         $Id$
    16.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.7 -    Copyright   1992  University of Cambridge
    16.8 -
    16.9 -Classical sequent calculus: examples with propositional connectives
   16.10 -Can be read to test the LK system.
   16.11 -*)
   16.12 -
   16.13 -writeln"absorptive laws of & and | ";
   16.14 -
   16.15 -goal (theory "LK") "|- P & P <-> P";
   16.16 -by (fast_tac prop_pack 1);
   16.17 -result();
   16.18 -
   16.19 -goal (theory "LK") "|- P | P <-> P";
   16.20 -by (fast_tac prop_pack 1);
   16.21 -result();
   16.22 -
   16.23 -writeln"commutative laws of & and | ";
   16.24 -
   16.25 -goal (theory "LK") "|- P & Q  <->  Q & P";
   16.26 -by (fast_tac prop_pack 1);
   16.27 -result();
   16.28 -
   16.29 -goal (theory "LK") "|- P | Q  <->  Q | P";
   16.30 -by (fast_tac prop_pack 1);
   16.31 -result();
   16.32 -
   16.33 -
   16.34 -writeln"associative laws of & and | ";
   16.35 -
   16.36 -goal (theory "LK") "|- (P & Q) & R  <->  P & (Q & R)";
   16.37 -by (fast_tac prop_pack 1);
   16.38 -result();
   16.39 -
   16.40 -goal (theory "LK") "|- (P | Q) | R  <->  P | (Q | R)";
   16.41 -by (fast_tac prop_pack 1);
   16.42 -result();
   16.43 -
   16.44 -writeln"distributive laws of & and | ";
   16.45 -goal (theory "LK") "|- (P & Q) | R  <-> (P | R) & (Q | R)";
   16.46 -by (fast_tac prop_pack 1);
   16.47 -result();
   16.48 -
   16.49 -goal (theory "LK") "|- (P | Q) & R  <-> (P & R) | (Q & R)";
   16.50 -by (fast_tac prop_pack 1);
   16.51 -result();
   16.52 -
   16.53 -writeln"Laws involving implication";
   16.54 -
   16.55 -goal (theory "LK") "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
   16.56 -by (fast_tac prop_pack 1);
   16.57 -result(); 
   16.58 -
   16.59 -goal (theory "LK") "|- (P & Q --> R) <-> (P--> (Q-->R))";
   16.60 -by (fast_tac prop_pack 1);
   16.61 -result(); 
   16.62 -
   16.63 -
   16.64 -goal (theory "LK") "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
   16.65 -by (fast_tac prop_pack 1);
   16.66 -result();
   16.67 -
   16.68 -
   16.69 -writeln"Classical theorems";
   16.70 -
   16.71 -goal (theory "LK") "|- P|Q --> P| ~P&Q";
   16.72 -by (fast_tac prop_pack 1);
   16.73 -result();
   16.74 -
   16.75 -
   16.76 -goal (theory "LK") "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
   16.77 -by (fast_tac prop_pack 1);
   16.78 -result();
   16.79 -
   16.80 -
   16.81 -goal (theory "LK") "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
   16.82 -by (fast_tac prop_pack 1);
   16.83 -result();
   16.84 -
   16.85 -
   16.86 -goal (theory "LK") "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
   16.87 -by (fast_tac prop_pack 1);
   16.88 -result();
   16.89 -
   16.90 -
   16.91 -(*If and only if*)
   16.92 -
   16.93 -goal (theory "LK") "|- (P<->Q) <-> (Q<->P)";
   16.94 -by (fast_tac prop_pack 1);
   16.95 -result();
   16.96 -
   16.97 -goal (theory "LK") "|- ~ (P <-> ~P)";
   16.98 -by (fast_tac prop_pack 1);
   16.99 -result();
  16.100 -
  16.101 -
  16.102 -(*Sample problems from 
  16.103 -  F. J. Pelletier, 
  16.104 -  Seventy-Five Problems for Testing Automatic Theorem Provers,
  16.105 -  J. Automated Reasoning 2 (1986), 191-216.
  16.106 -  Errata, JAR 4 (1988), 236-236.
  16.107 -*)
  16.108 -
  16.109 -(*1*)
  16.110 -goal (theory "LK") "|- (P-->Q)  <->  (~Q --> ~P)";
  16.111 -by (fast_tac prop_pack 1);
  16.112 -result();
  16.113 -
  16.114 -(*2*)
  16.115 -goal (theory "LK") "|- ~ ~ P  <->  P";
  16.116 -by (fast_tac prop_pack 1);
  16.117 -result();
  16.118 -
  16.119 -(*3*)
  16.120 -goal (theory "LK") "|- ~(P-->Q) --> (Q-->P)";
  16.121 -by (fast_tac prop_pack 1);
  16.122 -result();
  16.123 -
  16.124 -(*4*)
  16.125 -goal (theory "LK") "|- (~P-->Q)  <->  (~Q --> P)";
  16.126 -by (fast_tac prop_pack 1);
  16.127 -result();
  16.128 -
  16.129 -(*5*)
  16.130 -goal (theory "LK") "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
  16.131 -by (fast_tac prop_pack 1);
  16.132 -result();
  16.133 -
  16.134 -(*6*)
  16.135 -goal (theory "LK") "|- P | ~ P";
  16.136 -by (fast_tac prop_pack 1);
  16.137 -result();
  16.138 -
  16.139 -(*7*)
  16.140 -goal (theory "LK") "|- P | ~ ~ ~ P";
  16.141 -by (fast_tac prop_pack 1);
  16.142 -result();
  16.143 -
  16.144 -(*8.  Peirce's law*)
  16.145 -goal (theory "LK") "|- ((P-->Q) --> P)  -->  P";
  16.146 -by (fast_tac prop_pack 1);
  16.147 -result();
  16.148 -
  16.149 -(*9*)
  16.150 -goal (theory "LK") "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
  16.151 -by (fast_tac prop_pack 1);
  16.152 -result();
  16.153 -
  16.154 -(*10*)
  16.155 -goal (theory "LK") "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
  16.156 -by (fast_tac prop_pack 1);
  16.157 -result();
  16.158 -
  16.159 -(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
  16.160 -goal (theory "LK") "|- P<->P";
  16.161 -by (fast_tac prop_pack 1);
  16.162 -result();
  16.163 -
  16.164 -(*12.  "Dijkstra's law"*)
  16.165 -goal (theory "LK") "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
  16.166 -by (fast_tac prop_pack 1);
  16.167 -result();
  16.168 -
  16.169 -(*13.  Distributive law*)
  16.170 -goal (theory "LK") "|- P | (Q & R)  <-> (P | Q) & (P | R)";
  16.171 -by (fast_tac prop_pack 1);
  16.172 -result();
  16.173 -
  16.174 -(*14*)
  16.175 -goal (theory "LK") "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
  16.176 -by (fast_tac prop_pack 1);
  16.177 -result();
  16.178 -
  16.179 -
  16.180 -(*15*)
  16.181 -goal (theory "LK") "|- (P --> Q) <-> (~P | Q)";
  16.182 -by (fast_tac prop_pack 1);
  16.183 -result();
  16.184 -
  16.185 -(*16*)
  16.186 -goal (theory "LK") "|- (P-->Q) | (Q-->P)";
  16.187 -by (fast_tac prop_pack 1);
  16.188 -result();
  16.189 -
  16.190 -(*17*)
  16.191 -goal (theory "LK") "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
  16.192 -by (fast_tac prop_pack 1);
  16.193 -result();
    17.1 --- a/src/Sequents/LK/quant.ML	Mon Nov 20 21:23:12 2006 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,156 +0,0 @@
    17.4 -(*  Title:      LK/ex/quant.ML
    17.5 -    ID:         $Id$
    17.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.7 -    Copyright   1992  University of Cambridge
    17.8 -
    17.9 -Classical sequent calculus: examples with quantifiers.
   17.10 -*)
   17.11 -
   17.12 -goal (theory "LK") "|- (ALL x. P)  <->  P";
   17.13 -by (fast_tac LK_pack 1);
   17.14 -result();
   17.15 -
   17.16 -goal (theory "LK") "|- (ALL x y. P(x,y))  <->  (ALL y x. P(x,y))";
   17.17 -by (fast_tac LK_pack 1);
   17.18 -result();
   17.19 -
   17.20 -goal (theory "LK") "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)";
   17.21 -by (fast_tac LK_pack 1);
   17.22 -result();
   17.23 -
   17.24 -writeln"Permutation of existential quantifier.";
   17.25 -goal (theory "LK") "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))";
   17.26 -by (fast_tac LK_pack 1);
   17.27 -result();
   17.28 -
   17.29 -goal (theory "LK") "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
   17.30 -by (fast_tac LK_pack 1);
   17.31 -result();
   17.32 -
   17.33 -
   17.34 -(*Converse is invalid*)
   17.35 -goal (theory "LK") "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
   17.36 -by (fast_tac LK_pack 1);
   17.37 -result();
   17.38 -
   17.39 -
   17.40 -writeln"Pushing ALL into an implication.";
   17.41 -goal (theory "LK") "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))";
   17.42 -by (fast_tac LK_pack 1);
   17.43 -result();
   17.44 -
   17.45 -
   17.46 -goal (theory "LK") "|- (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
   17.47 -by (fast_tac LK_pack 1);
   17.48 -result();
   17.49 -
   17.50 -
   17.51 -goal (theory "LK") "|- (EX x. P)  <->  P";
   17.52 -by (fast_tac LK_pack 1);
   17.53 -result();
   17.54 -
   17.55 -
   17.56 -writeln"Distribution of EX over disjunction.";
   17.57 -goal (theory "LK") "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))";
   17.58 -by (fast_tac LK_pack 1);
   17.59 -result();
   17.60 -(*5 secs*)
   17.61 -
   17.62 -(*Converse is invalid*)
   17.63 -goal (theory "LK") "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))";
   17.64 -by (fast_tac LK_pack 1);
   17.65 -result();
   17.66 -
   17.67 -
   17.68 -writeln"Harder examples: classical theorems.";
   17.69 -
   17.70 -goal (theory "LK") "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
   17.71 -by (fast_tac LK_pack 1);
   17.72 -result();
   17.73 -(*3 secs*)
   17.74 -
   17.75 -
   17.76 -goal (theory "LK") "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
   17.77 -by (fast_tac LK_pack 1);
   17.78 -result();
   17.79 -(*5 secs*)
   17.80 -
   17.81 -
   17.82 -goal (theory "LK") "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
   17.83 -by (fast_tac LK_pack 1);
   17.84 -result();
   17.85 -
   17.86 -
   17.87 -writeln"Basic test of quantifier reasoning";
   17.88 -goal (theory "LK")
   17.89 -   "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
   17.90 -by (fast_tac LK_pack 1);
   17.91 -result();
   17.92 -
   17.93 -
   17.94 -goal (theory "LK") "|- (ALL x. Q(x))  -->  (EX x. Q(x))";
   17.95 -by (fast_tac LK_pack 1);
   17.96 -result();
   17.97 -
   17.98 -
   17.99 -writeln"The following are invalid!";
  17.100 -
  17.101 -(*INVALID*)
  17.102 -goal (theory "LK") "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
  17.103 -by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
  17.104 -(*Check that subgoals remain: proof failed.*)
  17.105 -getgoal 1;
  17.106 -
  17.107 -(*INVALID*)
  17.108 -goal (theory "LK") "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
  17.109 -by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
  17.110 -getgoal 1;
  17.111 -
  17.112 -goal (theory "LK") "|- P(?a) --> (ALL x. P(x))";
  17.113 -by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
  17.114 -(*Check that subgoals remain: proof failed.*)
  17.115 -getgoal 1;
  17.116 -
  17.117 -goal (theory "LK") "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
  17.118 -by (fast_tac LK_pack 1) handle ERROR _ => writeln"Failed, as expected";
  17.119 -getgoal 1;
  17.120 -
  17.121 -
  17.122 -writeln"Back to things that are provable...";
  17.123 -
  17.124 -goal (theory "LK") "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
  17.125 -by (fast_tac LK_pack 1);
  17.126 -result();
  17.127 -
  17.128 -(*An example of why exR should be delayed as long as possible*)
  17.129 -goal (theory "LK") "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))";
  17.130 -by (fast_tac LK_pack 1);
  17.131 -result();
  17.132 -
  17.133 -writeln"Solving for a Var";
  17.134 -goal (theory "LK")
  17.135 -   "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
  17.136 -by (fast_tac LK_pack 1);
  17.137 -result();
  17.138 -
  17.139 -
  17.140 -writeln"Principia Mathematica *11.53";
  17.141 -goal (theory "LK")
  17.142 -    "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
  17.143 -by (fast_tac LK_pack 1);
  17.144 -result();
  17.145 -
  17.146 -
  17.147 -writeln"Principia Mathematica *11.55";
  17.148 -goal (theory "LK") "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
  17.149 -by (fast_tac LK_pack 1);
  17.150 -result();
  17.151 -
  17.152 -writeln"Principia Mathematica *11.61";
  17.153 -goal (theory "LK")
  17.154 -   "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
  17.155 -by (fast_tac LK_pack 1);
  17.156 -result();
  17.157 -
  17.158 -(*21 August 88: loaded in 45.7 secs*)
  17.159 -(*18 September 2005: loaded in 0.114 secs*)
    18.1 --- a/src/Sequents/LK0.ML	Mon Nov 20 21:23:12 2006 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,200 +0,0 @@
    18.4 -(*  Title:      LK/LK0.ML
    18.5 -    ID:         $Id$
    18.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.7 -    Copyright   1992  University of Cambridge
    18.8 -
    18.9 -Tactics and lemmas for LK (thanks also to Philippe de Groote)
   18.10 -
   18.11 -Structural rules by Soren Heilmann
   18.12 -*)
   18.13 -
   18.14 -(** Structural Rules on formulas **)
   18.15 -
   18.16 -(*contraction*)
   18.17 -
   18.18 -Goal "$H |- $E, P, P, $F ==> $H |- $E, P, $F";
   18.19 -by (etac contRS 1);
   18.20 -qed "contR";
   18.21 -
   18.22 -Goal "$H, P, P, $G |- $E ==> $H, P, $G |- $E";
   18.23 -by (etac contLS 1);
   18.24 -qed "contL";
   18.25 -
   18.26 -(*thinning*)
   18.27 -
   18.28 -Goal "$H |- $E, $F ==> $H |- $E, P, $F";
   18.29 -by (etac thinRS 1);
   18.30 -qed "thinR";
   18.31 -
   18.32 -Goal "$H, $G |- $E ==> $H, P, $G |- $E";
   18.33 -by (etac thinLS 1);
   18.34 -qed "thinL";
   18.35 -
   18.36 -(*exchange*)
   18.37 -
   18.38 -Goal "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F";
   18.39 -by (etac exchRS 1);
   18.40 -qed "exchR";
   18.41 -
   18.42 -Goal "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E";
   18.43 -by (etac exchLS 1);
   18.44 -qed "exchL";
   18.45 -
   18.46 -(*Cut and thin, replacing the right-side formula*)
   18.47 -fun cutR_tac (sP: string) i =
   18.48 -    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
   18.49 -
   18.50 -(*Cut and thin, replacing the left-side formula*)
   18.51 -fun cutL_tac (sP: string) i =
   18.52 -    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
   18.53 -
   18.54 -
   18.55 -(** If-and-only-if rules **)
   18.56 -Goalw [iff_def]
   18.57 -    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F";
   18.58 -by (REPEAT (ares_tac [conjR,impR] 1));
   18.59 -qed "iffR";
   18.60 -
   18.61 -Goalw [iff_def]
   18.62 -    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E";
   18.63 -by (REPEAT (ares_tac [conjL,impL,basic] 1));
   18.64 -qed "iffL";
   18.65 -
   18.66 -Goal "$H |- $E, (P <-> P), $F";
   18.67 -by (REPEAT (resolve_tac [iffR,basic] 1));
   18.68 -qed "iff_refl";
   18.69 -
   18.70 -Goalw [True_def] "$H |- $E, True, $F";
   18.71 -by (rtac impR 1);
   18.72 -by (rtac basic 1);
   18.73 -qed "TrueR";
   18.74 -
   18.75 -(*Descriptions*)
   18.76 -val [p1,p2] = Goal
   18.77 -    "[| $H |- $E, P(a), $F;  !!x. $H, P(x) |- $E, x=a, $F |] \
   18.78 -\    ==> $H |- $E, (THE x. P(x)) = a, $F";
   18.79 -by (rtac cut 1);
   18.80 -by (rtac p2 2);
   18.81 -by (rtac The 1 THEN rtac thinR 1 THEN rtac exchRS 1 THEN rtac p1 1);
   18.82 -by (rtac thinR 1 THEN rtac exchRS 1 THEN rtac p2 1);
   18.83 -qed "the_equality";
   18.84 -
   18.85 -(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
   18.86 -
   18.87 -Goal "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E";
   18.88 -by (rtac allL 1);
   18.89 -by (etac thinL 1);
   18.90 -qed "allL_thin";
   18.91 -
   18.92 -Goal "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F";
   18.93 -by (rtac exR 1);
   18.94 -by (etac thinR 1);
   18.95 -qed "exR_thin";
   18.96 -
   18.97 -
   18.98 -(*The rules of LK*)
   18.99 -val prop_pack = empty_pack add_safes
  18.100 -                [basic, refl, TrueR, FalseL,
  18.101 -                 conjL, conjR, disjL, disjR, impL, impR,
  18.102 -                 notL, notR, iffL, iffR];
  18.103 -
  18.104 -val LK_pack = prop_pack add_safes   [allR, exL]
  18.105 -                        add_unsafes [allL_thin, exR_thin, the_equality];
  18.106 -
  18.107 -val LK_dup_pack = prop_pack add_safes   [allR, exL]
  18.108 -                            add_unsafes [allL, exR, the_equality];
  18.109 -
  18.110 -
  18.111 -pack_ref() := LK_pack;
  18.112 -
  18.113 -fun lemma_tac th i =
  18.114 -    rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
  18.115 -
  18.116 -val [major,minor] = goal (the_context ())
  18.117 -    "[| $H |- $E, $F, P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
  18.118 -by (rtac (thinRS RS cut) 1 THEN rtac major 1);
  18.119 -by (Step_tac 1);
  18.120 -by (rtac thinR 1 THEN rtac minor 1);
  18.121 -qed "mp_R";
  18.122 -
  18.123 -val [major,minor] = goal (the_context ())
  18.124 -    "[| $H, $G |- $E, P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
  18.125 -by (rtac (thinL RS cut) 1 THEN rtac major 1);
  18.126 -by (Step_tac 1);
  18.127 -by (rtac thinL 1 THEN rtac minor 1);
  18.128 -qed "mp_L";
  18.129 -
  18.130 -
  18.131 -(** Two rules to generate left- and right- rules from implications **)
  18.132 -
  18.133 -val [major,minor] = goal (the_context ())
  18.134 -    "[| |- P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
  18.135 -by (rtac mp_R 1);
  18.136 -by (rtac minor 2);
  18.137 -by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
  18.138 -qed "R_of_imp";
  18.139 -
  18.140 -val [major,minor] = goal (the_context ())
  18.141 -    "[| |- P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
  18.142 -by (rtac mp_L 1);
  18.143 -by (rtac minor 2);
  18.144 -by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
  18.145 -qed "L_of_imp";
  18.146 -
  18.147 -(*Can be used to create implications in a subgoal*)
  18.148 -val [prem] = goal (the_context ())
  18.149 -    "[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F";
  18.150 -by (rtac mp_L 1);
  18.151 -by (rtac basic 2);
  18.152 -by (rtac thinR 1 THEN rtac prem 1);
  18.153 -qed "backwards_impR";
  18.154 -
  18.155 -Goal "|-P&Q ==> |-P";
  18.156 -by (etac (thinR RS cut) 1);
  18.157 -by (Fast_tac 1);
  18.158 -qed "conjunct1";
  18.159 -
  18.160 -Goal "|-P&Q ==> |-Q";
  18.161 -by (etac (thinR RS cut) 1);
  18.162 -by (Fast_tac 1);
  18.163 -qed "conjunct2";
  18.164 -
  18.165 -Goal "|- (ALL x. P(x)) ==> |- P(x)";
  18.166 -by (etac (thinR RS cut) 1);
  18.167 -by (Fast_tac 1);
  18.168 -qed "spec";
  18.169 -
  18.170 -(** Equality **)
  18.171 -
  18.172 -Goal "|- a=b --> b=a";
  18.173 -by (safe_tac (LK_pack add_safes [subst]) 1);
  18.174 -qed "sym";
  18.175 -
  18.176 -Goal "|- a=b --> b=c --> a=c";
  18.177 -by (safe_tac (LK_pack add_safes [subst]) 1);
  18.178 -qed "trans";
  18.179 -
  18.180 -(* Symmetry of equality in hypotheses *)
  18.181 -bind_thm ("symL", sym RS L_of_imp);
  18.182 -
  18.183 -(* Symmetry of equality in hypotheses *)
  18.184 -bind_thm ("symR", sym RS R_of_imp);
  18.185 -
  18.186 -Goal "[| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F";
  18.187 -by (rtac (trans RS R_of_imp RS mp_R) 1);
  18.188 -by (ALLGOALS assume_tac);
  18.189 -qed "transR";
  18.190 -
  18.191 -
  18.192 -(* Two theorms for rewriting only one instance of a definition:
  18.193 -   the first for definitions of formulae and the second for terms *)
  18.194 -
  18.195 -val prems = goal (the_context ()) "(A == B) ==> |- A <-> B";
  18.196 -by (rewrite_goals_tac prems);
  18.197 -by (rtac iff_refl 1);
  18.198 -qed "def_imp_iff";
  18.199 -
  18.200 -val prems = goal (the_context ()) "(A == B) ==> |- A = B";
  18.201 -by (rewrite_goals_tac prems);
  18.202 -by (rtac refl 1);
  18.203 -qed "meta_eq_to_obj_eq";
    19.1 --- a/src/Sequents/LK0.thy	Mon Nov 20 21:23:12 2006 +0100
    19.2 +++ b/src/Sequents/LK0.thy	Mon Nov 20 23:47:10 2006 +0100
    19.3 @@ -132,8 +132,262 @@
    19.4  setup
    19.5    prover_setup
    19.6  
    19.7 -ML {* use_legacy_bindings (the_context ()) *}
    19.8 +
    19.9 +(** Structural Rules on formulas **)
   19.10 +
   19.11 +(*contraction*)
   19.12 +
   19.13 +lemma contR: "$H |- $E, P, P, $F ==> $H |- $E, P, $F"
   19.14 +  by (rule contRS)
   19.15 +
   19.16 +lemma contL: "$H, P, P, $G |- $E ==> $H, P, $G |- $E"
   19.17 +  by (rule contLS)
   19.18 +
   19.19 +(*thinning*)
   19.20 +
   19.21 +lemma thinR: "$H |- $E, $F ==> $H |- $E, P, $F"
   19.22 +  by (rule thinRS)
   19.23 +
   19.24 +lemma thinL: "$H, $G |- $E ==> $H, P, $G |- $E"
   19.25 +  by (rule thinLS)
   19.26 +
   19.27 +(*exchange*)
   19.28 +
   19.29 +lemma exchR: "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F"
   19.30 +  by (rule exchRS)
   19.31 +
   19.32 +lemma exchL: "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E"
   19.33 +  by (rule exchLS)
   19.34 +
   19.35 +ML {*
   19.36 +local
   19.37 +  val thinR = thm "thinR"
   19.38 +  val thinL = thm "thinL"
   19.39 +  val cut = thm "cut"
   19.40 +in
   19.41 +
   19.42 +(*Cut and thin, replacing the right-side formula*)
   19.43 +fun cutR_tac s i =
   19.44 +  res_inst_tac [ ("P", s) ] cut i  THEN  rtac thinR i
   19.45 +
   19.46 +(*Cut and thin, replacing the left-side formula*)
   19.47 +fun cutL_tac s i =
   19.48 +  res_inst_tac [("P", s)] cut i  THEN  rtac thinL (i+1)
   19.49  
   19.50  end
   19.51 +*}
   19.52 +
   19.53 +
   19.54 +(** If-and-only-if rules **)
   19.55 +lemma iffR: 
   19.56 +    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
   19.57 +  apply (unfold iff_def)
   19.58 +  apply (assumption | rule conjR impR)+
   19.59 +  done
   19.60 +
   19.61 +lemma iffL: 
   19.62 +    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
   19.63 +  apply (unfold iff_def)
   19.64 +  apply (assumption | rule conjL impL basic)+
   19.65 +  done
   19.66 +
   19.67 +lemma iff_refl: "$H |- $E, (P <-> P), $F"
   19.68 +  apply (rule iffR basic)+
   19.69 +  done
   19.70 +
   19.71 +lemma TrueR: "$H |- $E, True, $F"
   19.72 +  apply (unfold True_def)
   19.73 +  apply (rule impR)
   19.74 +  apply (rule basic)
   19.75 +  done
   19.76 +
   19.77 +(*Descriptions*)
   19.78 +lemma the_equality:
   19.79 +  assumes p1: "$H |- $E, P(a), $F"
   19.80 +    and p2: "!!x. $H, P(x) |- $E, x=a, $F"
   19.81 +  shows "$H |- $E, (THE x. P(x)) = a, $F"
   19.82 +  apply (rule cut)
   19.83 +   apply (rule_tac [2] p2)
   19.84 +  apply (rule The, rule thinR, rule exchRS, rule p1)
   19.85 +  apply (rule thinR, rule exchRS, rule p2)
   19.86 +  done
   19.87 +
   19.88 +
   19.89 +(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
   19.90 +
   19.91 +lemma allL_thin: "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"
   19.92 +  apply (rule allL)
   19.93 +  apply (erule thinL)
   19.94 +  done
   19.95 +
   19.96 +lemma exR_thin: "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F"
   19.97 +  apply (rule exR)
   19.98 +  apply (erule thinR)
   19.99 +  done
  19.100 +
  19.101 +(*The rules of LK*)
  19.102 +
  19.103 +ML {*
  19.104 +val prop_pack = empty_pack add_safes
  19.105 +                [thm "basic", thm "refl", thm "TrueR", thm "FalseL",
  19.106 +                 thm "conjL", thm "conjR", thm "disjL", thm "disjR", thm "impL", thm "impR",
  19.107 +                 thm "notL", thm "notR", thm "iffL", thm "iffR"];
  19.108 +
  19.109 +val LK_pack = prop_pack add_safes   [thm "allR", thm "exL"]
  19.110 +                        add_unsafes [thm "allL_thin", thm "exR_thin", thm "the_equality"];
  19.111 +
  19.112 +val LK_dup_pack = prop_pack add_safes   [thm "allR", thm "exL"]
  19.113 +                            add_unsafes [thm "allL", thm "exR", thm "the_equality"];
  19.114 +
  19.115 +
  19.116 +pack_ref() := LK_pack;
  19.117 +
  19.118 +local
  19.119 +  val thinR = thm "thinR"
  19.120 +  val thinL = thm "thinL"
  19.121 +  val cut = thm "cut"
  19.122 +in
  19.123 +
  19.124 +fun lemma_tac th i =
  19.125 +    rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
  19.126 +
  19.127 +end;
  19.128 +*}
  19.129 +
  19.130 +method_setup fast_prop =
  19.131 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac prop_pack)) *}
  19.132 +  "propositional reasoning"
  19.133 +
  19.134 +method_setup fast =
  19.135 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac LK_pack)) *}
  19.136 +  "classical reasoning"
  19.137 +
  19.138 +method_setup fast_dup =
  19.139 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac LK_dup_pack)) *}
  19.140 +  "classical reasoning"
  19.141 +
  19.142 +method_setup best =
  19.143 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac LK_pack)) *}
  19.144 +  "classical reasoning"
  19.145 +
  19.146 +method_setup best_dup =
  19.147 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac LK_dup_pack)) *}
  19.148 +  "classical reasoning"
  19.149  
  19.150  
  19.151 +lemma mp_R:
  19.152 +  assumes major: "$H |- $E, $F, P --> Q"
  19.153 +    and minor: "$H |- $E, $F, P"
  19.154 +  shows "$H |- $E, Q, $F"
  19.155 +  apply (rule thinRS [THEN cut], rule major)
  19.156 +  apply (tactic "step_tac LK_pack 1")
  19.157 +  apply (rule thinR, rule minor)
  19.158 +  done
  19.159 +
  19.160 +lemma mp_L:
  19.161 +  assumes major: "$H, $G |- $E, P --> Q"
  19.162 +    and minor: "$H, $G, Q |- $E"
  19.163 +  shows "$H, P, $G |- $E"
  19.164 +  apply (rule thinL [THEN cut], rule major)
  19.165 +  apply (tactic "step_tac LK_pack 1")
  19.166 +  apply (rule thinL, rule minor)
  19.167 +  done
  19.168 +
  19.169 +
  19.170 +(** Two rules to generate left- and right- rules from implications **)
  19.171 +
  19.172 +lemma R_of_imp:
  19.173 +  assumes major: "|- P --> Q"
  19.174 +    and minor: "$H |- $E, $F, P"
  19.175 +  shows "$H |- $E, Q, $F"
  19.176 +  apply (rule mp_R)
  19.177 +   apply (rule_tac [2] minor)
  19.178 +  apply (rule thinRS, rule major [THEN thinLS])
  19.179 +  done
  19.180 +
  19.181 +lemma L_of_imp:
  19.182 +  assumes major: "|- P --> Q"
  19.183 +    and minor: "$H, $G, Q |- $E"
  19.184 +  shows "$H, P, $G |- $E"
  19.185 +  apply (rule mp_L)
  19.186 +   apply (rule_tac [2] minor)
  19.187 +  apply (rule thinRS, rule major [THEN thinLS])
  19.188 +  done
  19.189 +
  19.190 +(*Can be used to create implications in a subgoal*)
  19.191 +lemma backwards_impR:
  19.192 +  assumes prem: "$H, $G |- $E, $F, P --> Q"
  19.193 +  shows "$H, P, $G |- $E, Q, $F"
  19.194 +  apply (rule mp_L)
  19.195 +   apply (rule_tac [2] basic)
  19.196 +  apply (rule thinR, rule prem)
  19.197 +  done
  19.198 +
  19.199 +lemma conjunct1: "|-P&Q ==> |-P"
  19.200 +  apply (erule thinR [THEN cut])
  19.201 +  apply fast
  19.202 +  done
  19.203 +
  19.204 +lemma conjunct2: "|-P&Q ==> |-Q"
  19.205 +  apply (erule thinR [THEN cut])
  19.206 +  apply fast
  19.207 +  done
  19.208 +
  19.209 +lemma spec: "|- (ALL x. P(x)) ==> |- P(x)"
  19.210 +  apply (erule thinR [THEN cut])
  19.211 +  apply fast
  19.212 +  done
  19.213 +
  19.214 +
  19.215 +(** Equality **)
  19.216 +
  19.217 +lemma sym: "|- a=b --> b=a"
  19.218 +  by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *})
  19.219 +
  19.220 +lemma trans: "|- a=b --> b=c --> a=c"
  19.221 +  by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *})
  19.222 +
  19.223 +(* Symmetry of equality in hypotheses *)
  19.224 +lemmas symL = sym [THEN L_of_imp, standard]
  19.225 +
  19.226 +(* Symmetry of equality in hypotheses *)
  19.227 +lemmas symR = sym [THEN R_of_imp, standard]
  19.228 +
  19.229 +lemma transR: "[| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F"
  19.230 +  by (rule trans [THEN R_of_imp, THEN mp_R])
  19.231 +
  19.232 +(* Two theorms for rewriting only one instance of a definition:
  19.233 +   the first for definitions of formulae and the second for terms *)
  19.234 +
  19.235 +lemma def_imp_iff: "(A == B) ==> |- A <-> B"
  19.236 +  apply unfold
  19.237 +  apply (rule iff_refl)
  19.238 +  done
  19.239 +
  19.240 +lemma meta_eq_to_obj_eq: "(A == B) ==> |- A = B"
  19.241 +  apply unfold
  19.242 +  apply (rule refl)
  19.243 +  done
  19.244 +
  19.245 +
  19.246 +(** if-then-else rules **)
  19.247 +
  19.248 +lemma if_True: "|- (if True then x else y) = x"
  19.249 +  unfolding If_def by fast
  19.250 +
  19.251 +lemma if_False: "|- (if False then x else y) = y"
  19.252 +  unfolding If_def by fast
  19.253 +
  19.254 +lemma if_P: "|- P ==> |- (if P then x else y) = x"
  19.255 +  apply (unfold If_def)
  19.256 +  apply (erule thinR [THEN cut])
  19.257 +  apply fast
  19.258 +  done
  19.259 +
  19.260 +lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y";
  19.261 +  apply (unfold If_def)
  19.262 +  apply (erule thinR [THEN cut])
  19.263 +  apply fast
  19.264 +  done
  19.265 +
  19.266 +end
    20.1 --- a/src/Sequents/Modal/ROOT.ML	Mon Nov 20 21:23:12 2006 +0100
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,22 +0,0 @@
    20.4 -(*  Title:      Modal/ex/ROOT.ML
    20.5 -    ID:         $Id$
    20.6 -    Author:     Martin Coen
    20.7 -    Copyright   1991  University of Cambridge
    20.8 -*)
    20.9 -
   20.10 -writeln "\nTheorems of T\n";
   20.11 -fun try s = (writeln s; prove_goal (theory "T") s (fn _=> [T_Prover.solve_tac 2]));
   20.12 -time_use "Tthms.ML";
   20.13 -
   20.14 -writeln "\nTheorems of S4\n";
   20.15 -fun try s = (writeln s; prove_goal (theory "S4") s (fn _=> [S4_Prover.solve_tac 2]));
   20.16 -time_use "Tthms.ML";
   20.17 -time_use "S4thms.ML";
   20.18 -
   20.19 -writeln "\nTheorems of S43\n";
   20.20 -fun try s = (writeln s;
   20.21 -             prove_goal (theory "S43") s (fn _=> [S43_Prover.solve_tac 2 ORELSE
   20.22 -                                           S43_Prover.solve_tac 3]));
   20.23 -time_use "Tthms.ML";
   20.24 -time_use "S4thms.ML";
   20.25 -time_use "S43thms.ML";
    21.1 --- a/src/Sequents/Modal/S43thms.ML	Mon Nov 20 21:23:12 2006 +0100
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,49 +0,0 @@
    21.4 -(*  Title:      91/Modal/ex/S43thms
    21.5 -    ID:         $Id$
    21.6 -    Author:     Martin Coen
    21.7 -    Copyright   1991  University of Cambridge
    21.8 -*)
    21.9 -
   21.10 -(* Theorems of system S43 *)
   21.11 -
   21.12 -try "|- <>[]P --> []<>P";
   21.13 -try "|- <>[]P --> [][]<>P";
   21.14 -try "|- [](<>P | <>Q) --> []<>P | []<>Q";
   21.15 -try "|- <>[]P & <>[]Q --> <>([]P & []Q)";
   21.16 -try "|- []([]P --> []Q) | []([]Q --> []P)";
   21.17 -try "|- [](<>P --> <>Q) | [](<>Q --> <>P)";
   21.18 -try "|- []([]P --> Q) | []([]Q --> P)";
   21.19 -try "|- [](P --> <>Q) | [](Q --> <>P)";
   21.20 -try "|- [](P --> []Q-->R) | [](P | ([]R --> Q))";
   21.21 -try "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)";
   21.22 -try "|- []([]P | Q) & [](P | []Q) --> []P | []Q";
   21.23 -try "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)";
   21.24 -try "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q";
   21.25 -try "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)";
   21.26 -try "|- <>[]<>P <-> []<>P";
   21.27 -try "|- []<>[]P <-> <>[]P";
   21.28 -
   21.29 -(* These are from Hailpern, LNCS 129 *)
   21.30 -
   21.31 -try "|- [](P & Q) <-> []P & []Q";
   21.32 -try "|- <>(P | Q) <-> <>P | <>Q";
   21.33 -try "|- <>(P --> Q) <-> []P --> <>Q";
   21.34 -
   21.35 -try "|- [](P --> Q) --> <>P --> <>Q";
   21.36 -try "|- []P --> []<>P";
   21.37 -try "|- <>[]P --> <>P";
   21.38 -try "|- []<>[]P --> []<>P";
   21.39 -try "|- <>[]P --> <>[]<>P";
   21.40 -try "|- <>[]P --> []<>P";
   21.41 -try "|- []<>[]P <-> <>[]P";
   21.42 -try "|- <>[]<>P <-> []<>P";
   21.43 -
   21.44 -try "|- []P | []Q --> [](P | Q)";
   21.45 -try "|- <>(P & Q) --> <>P & <>Q";
   21.46 -try "|- [](P | Q) --> []P | <>Q";
   21.47 -try "|- <>P & []Q --> <>(P & Q)";
   21.48 -try "|- [](P | Q) --> <>P | []Q";
   21.49 -try "|- [](P | Q) --> []<>P | []<>Q";
   21.50 -try "|- <>[]P & <>[]Q --> <>(P & Q)";
   21.51 -try "|- <>[](P & Q) <-> <>[]P & <>[]Q";
   21.52 -try "|- []<>(P | Q) <-> []<>P | []<>Q";
    22.1 --- a/src/Sequents/Modal/S4thms.ML	Mon Nov 20 21:23:12 2006 +0100
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,40 +0,0 @@
    22.4 -(*  Title:      91/Modal/ex/S4thms
    22.5 -    ID:         $Id$
    22.6 -    Author:     Martin Coen
    22.7 -    Copyright   1991  University of Cambridge
    22.8 -*)
    22.9 -
   22.10 -(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
   22.11 -
   22.12 -try "|- []A --> A";             (* refexivity *)
   22.13 -try "|- []A --> [][]A";         (* transitivity *)
   22.14 -try "|- []A --> <>A";           (* seriality *)
   22.15 -try "|- <>[](<>A --> []<>A)";
   22.16 -try "|- <>[](<>[]A --> []A)";
   22.17 -try "|- []P <-> [][]P";
   22.18 -try "|- <>P <-> <><>P";
   22.19 -try "|- <>[]<>P --> <>P";
   22.20 -try "|- []<>P <-> []<>[]<>P";
   22.21 -try "|- <>[]P <-> <>[]<>[]P";
   22.22 -
   22.23 -(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
   22.24 -
   22.25 -try "|- []P | []Q <-> []([]P | []Q)";
   22.26 -try "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)";
   22.27 -
   22.28 -(* These are from Hailpern, LNCS 129 *)
   22.29 -
   22.30 -try "|- [](P & Q) <-> []P & []Q";
   22.31 -try "|- <>(P | Q) <-> <>P | <>Q";
   22.32 -try "|- <>(P --> Q) <-> ([]P --> <>Q)";
   22.33 -
   22.34 -try "|- [](P --> Q) --> (<>P --> <>Q)";
   22.35 -try "|- []P --> []<>P";
   22.36 -try "|- <>[]P --> <>P";
   22.37 -
   22.38 -try "|- []P | []Q --> [](P | Q)";
   22.39 -try "|- <>(P & Q) --> <>P & <>Q";
   22.40 -try "|- [](P | Q) --> []P | <>Q";
   22.41 -try "|- <>P & []Q --> <>(P & Q)";
   22.42 -try "|- [](P | Q) --> <>P | []Q";
   22.43 -
    23.1 --- a/src/Sequents/Modal/Tthms.ML	Mon Nov 20 21:23:12 2006 +0100
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,31 +0,0 @@
    23.4 -(*  Title:      91/Modal/ex/Tthms
    23.5 -    ID:         $Id$
    23.6 -    Author:     Martin Coen
    23.7 -    Copyright   1991  University of Cambridge
    23.8 -*)
    23.9 -
   23.10 -(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
   23.11 -
   23.12 -try "|- []P --> P";
   23.13 -try "|- [](P-->Q) --> ([]P-->[]Q)";    (* normality*)
   23.14 -try "|- (P--<Q) --> []P --> []Q";
   23.15 -try "|- P --> <>P";
   23.16 -
   23.17 -try "|-  [](P & Q) <-> []P & []Q";
   23.18 -try "|-  <>(P | Q) <-> <>P | <>Q";
   23.19 -try "|-  [](P<->Q) <-> (P>-<Q)";
   23.20 -try "|-  <>(P-->Q) <-> ([]P--><>Q)";
   23.21 -try "|-        []P <-> ~<>(~P)";
   23.22 -try "|-     [](~P) <-> ~<>P";
   23.23 -try "|-       ~[]P <-> <>(~P)";
   23.24 -try "|-      [][]P <-> ~<><>(~P)";
   23.25 -try "|- ~<>(P | Q) <-> ~<>P & ~<>Q";
   23.26 -
   23.27 -try "|- []P | []Q --> [](P | Q)";
   23.28 -try "|- <>(P & Q) --> <>P & <>Q";
   23.29 -try "|- [](P | Q) --> []P | <>Q";
   23.30 -try "|- <>P & []Q --> <>(P & Q)";
   23.31 -try "|- [](P | Q) --> <>P | []Q";
   23.32 -try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)";
   23.33 -try "|- (P--<Q) & (Q--<R) --> (P--<R)";
   23.34 -try "|- []P --> <>Q --> <>(P & Q)";
    24.1 --- a/src/Sequents/Modal0.ML	Mon Nov 20 21:23:12 2006 +0100
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,30 +0,0 @@
    24.4 -(*  Title:      Modal/modal0
    24.5 -    ID:         $Id$
    24.6 -    Author:     Martin Coen
    24.7 -    Copyright   1991  University of Cambridge
    24.8 -*)
    24.9 -
   24.10 -structure Modal0_rls =
   24.11 -struct
   24.12 -
   24.13 -val rewrite_rls = [strimp_def,streqv_def];
   24.14 -
   24.15 -local
   24.16 -  val iffR = prove_goal (the_context ())
   24.17 -      "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
   24.18 -   (fn prems=>
   24.19 -    [ (rewtac iff_def),
   24.20 -      (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
   24.21 -
   24.22 -  val iffL = prove_goal (the_context ())
   24.23 -     "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
   24.24 -   (fn prems=>
   24.25 -    [ rewtac iff_def,
   24.26 -      (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ])
   24.27 -in
   24.28 -val safe_rls   = [basic,conjL,conjR,disjL,disjR,impL,impR,notL,notR,iffL,iffR];
   24.29 -val unsafe_rls = [allR,exL];
   24.30 -val bound_rls  = [allL,exR];
   24.31 -end
   24.32 -
   24.33 -end;
    25.1 --- a/src/Sequents/Modal0.thy	Mon Nov 20 21:23:12 2006 +0100
    25.2 +++ b/src/Sequents/Modal0.thy	Mon Nov 20 23:47:10 2006 +0100
    25.3 @@ -12,8 +12,8 @@
    25.4  consts
    25.5    box           :: "o=>o"       ("[]_" [50] 50)
    25.6    dia           :: "o=>o"       ("<>_" [50] 50)
    25.7 -  "--<"         :: "[o,o]=>o"   (infixr 25)
    25.8 -  ">-<"         :: "[o,o]=>o"   (infixr 25)
    25.9 +  strimp        :: "[o,o]=>o"   (infixr "--<" 25)
   25.10 +  streqv        :: "[o,o]=>o"   (infixr ">-<" 25)
   25.11    Lstar         :: "two_seqi"
   25.12    Rstar         :: "two_seqi"
   25.13  
   25.14 @@ -38,6 +38,23 @@
   25.15    strimp_def:    "P --< Q == [](P --> Q)"
   25.16    streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
   25.17  
   25.18 -ML {* use_legacy_bindings (the_context ()) *}
   25.19 +
   25.20 +lemmas rewrite_rls = strimp_def streqv_def
   25.21 +
   25.22 +lemma iffR:
   25.23 +    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
   25.24 +  apply (unfold iff_def)
   25.25 +  apply (assumption | rule conjR impR)+
   25.26 +  done
   25.27 +
   25.28 +lemma iffL:
   25.29 +    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
   25.30 +  apply (unfold iff_def)
   25.31 +  apply (assumption | rule conjL impL basic)+
   25.32 +  done
   25.33 +
   25.34 +lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR
   25.35 +  and unsafe_rls = allR exL
   25.36 +  and bound_rls = allL exR
   25.37  
   25.38  end
    26.1 --- a/src/Sequents/ROOT.ML	Mon Nov 20 21:23:12 2006 +0100
    26.2 +++ b/src/Sequents/ROOT.ML	Mon Nov 20 23:47:10 2006 +0100
    26.3 @@ -13,7 +13,11 @@
    26.4  Unify.search_bound := 40;
    26.5  
    26.6  use_thy "LK";
    26.7 +
    26.8  use_thy "ILL";
    26.9 +use_thy "ILL_predlog";
   26.10 +use_thy "Washing";
   26.11 +
   26.12  use_thy "Modal0";
   26.13  use_thy"T";
   26.14  use_thy"S4";
    27.1 --- a/src/Sequents/S4.ML	Mon Nov 20 21:23:12 2006 +0100
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,17 +0,0 @@
    27.4 -(*  Title:      Modal/S4.ML
    27.5 -    ID:         $Id$
    27.6 -    Author:     Martin Coen
    27.7 -    Copyright   1991  University of Cambridge
    27.8 -*)
    27.9 -
   27.10 -local open Modal0_rls
   27.11 -in structure MP_Rule : MODAL_PROVER_RULE =
   27.12 -   struct
   27.13 -    val rewrite_rls = rewrite_rls
   27.14 -    val safe_rls    = safe_rls
   27.15 -    val unsafe_rls  = unsafe_rls @ [boxR,diaL]
   27.16 -    val bound_rls   = bound_rls @ [boxL,diaR]
   27.17 -    val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
   27.18 -   end;
   27.19 -end;
   27.20 -structure S4_Prover = Modal_ProverFun(MP_Rule);
    28.1 --- a/src/Sequents/S4.thy	Mon Nov 20 21:23:12 2006 +0100
    28.2 +++ b/src/Sequents/S4.thy	Mon Nov 20 23:47:10 2006 +0100
    28.3 @@ -32,6 +32,81 @@
    28.4     "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
    28.5             $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
    28.6  
    28.7 -ML {* use_legacy_bindings (the_context ()) *}
    28.8 +ML {*
    28.9 +structure S4_Prover = Modal_ProverFun
   28.10 +(
   28.11 +  val rewrite_rls = thms "rewrite_rls"
   28.12 +  val safe_rls = thms "safe_rls"
   28.13 +  val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"]
   28.14 +  val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
   28.15 +  val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
   28.16 +    thm "rstar1", thm "rstar2"]
   28.17 +)
   28.18 +*}
   28.19 +
   28.20 +method_setup S4_solve =
   28.21 +{* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
   28.22 +
   28.23 +
   28.24 +(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
   28.25 +
   28.26 +lemma "|- []P --> P" by S4_solve
   28.27 +lemma "|- [](P-->Q) --> ([]P-->[]Q)" by S4_solve   (* normality*)
   28.28 +lemma "|- (P--<Q) --> []P --> []Q" by S4_solve
   28.29 +lemma "|- P --> <>P" by S4_solve
   28.30 +
   28.31 +lemma "|-  [](P & Q) <-> []P & []Q" by S4_solve
   28.32 +lemma "|-  <>(P | Q) <-> <>P | <>Q" by S4_solve
   28.33 +lemma "|-  [](P<->Q) <-> (P>-<Q)" by S4_solve
   28.34 +lemma "|-  <>(P-->Q) <-> ([]P--><>Q)" by S4_solve
   28.35 +lemma "|-        []P <-> ~<>(~P)" by S4_solve
   28.36 +lemma "|-     [](~P) <-> ~<>P" by S4_solve
   28.37 +lemma "|-       ~[]P <-> <>(~P)" by S4_solve
   28.38 +lemma "|-      [][]P <-> ~<><>(~P)" by S4_solve
   28.39 +lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by S4_solve
   28.40 +
   28.41 +lemma "|- []P | []Q --> [](P | Q)" by S4_solve
   28.42 +lemma "|- <>(P & Q) --> <>P & <>Q" by S4_solve
   28.43 +lemma "|- [](P | Q) --> []P | <>Q" by S4_solve
   28.44 +lemma "|- <>P & []Q --> <>(P & Q)" by S4_solve
   28.45 +lemma "|- [](P | Q) --> <>P | []Q" by S4_solve
   28.46 +lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by S4_solve
   28.47 +lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by S4_solve
   28.48 +lemma "|- []P --> <>Q --> <>(P & Q)" by S4_solve
   28.49 +
   28.50 +
   28.51 +(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
   28.52 +
   28.53 +lemma "|- []A --> A" by S4_solve             (* refexivity *)
   28.54 +lemma "|- []A --> [][]A" by S4_solve         (* transitivity *)
   28.55 +lemma "|- []A --> <>A" by S4_solve           (* seriality *)
   28.56 +lemma "|- <>[](<>A --> []<>A)" by S4_solve
   28.57 +lemma "|- <>[](<>[]A --> []A)" by S4_solve
   28.58 +lemma "|- []P <-> [][]P" by S4_solve
   28.59 +lemma "|- <>P <-> <><>P" by S4_solve
   28.60 +lemma "|- <>[]<>P --> <>P" by S4_solve
   28.61 +lemma "|- []<>P <-> []<>[]<>P" by S4_solve
   28.62 +lemma "|- <>[]P <-> <>[]<>[]P" by S4_solve
   28.63 +
   28.64 +(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
   28.65 +
   28.66 +lemma "|- []P | []Q <-> []([]P | []Q)" by S4_solve
   28.67 +lemma "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)" by S4_solve
   28.68 +
   28.69 +(* These are from Hailpern, LNCS 129 *)
   28.70 +
   28.71 +lemma "|- [](P & Q) <-> []P & []Q" by S4_solve
   28.72 +lemma "|- <>(P | Q) <-> <>P | <>Q" by S4_solve
   28.73 +lemma "|- <>(P --> Q) <-> ([]P --> <>Q)" by S4_solve
   28.74 +
   28.75 +lemma "|- [](P --> Q) --> (<>P --> <>Q)" by S4_solve
   28.76 +lemma "|- []P --> []<>P" by S4_solve
   28.77 +lemma "|- <>[]P --> <>P" by S4_solve
   28.78 +
   28.79 +lemma "|- []P | []Q --> [](P | Q)" by S4_solve
   28.80 +lemma "|- <>(P & Q) --> <>P & <>Q" by S4_solve
   28.81 +lemma "|- [](P | Q) --> []P | <>Q" by S4_solve
   28.82 +lemma "|- <>P & []Q --> <>(P & Q)" by S4_solve
   28.83 +lemma "|- [](P | Q) --> <>P | []Q" by S4_solve
   28.84  
   28.85  end
    29.1 --- a/src/Sequents/S43.ML	Mon Nov 20 21:23:12 2006 +0100
    29.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.3 @@ -1,17 +0,0 @@
    29.4 -(*  Title:      Modal/S43
    29.5 -    ID:         $Id$
    29.6 -    Author:     Martin Coen
    29.7 -    Copyright   1991  University of Cambridge
    29.8 -*)
    29.9 -
   29.10 -local open Modal0_rls
   29.11 -in structure MP_Rule : MODAL_PROVER_RULE =
   29.12 -   struct
   29.13 -    val rewrite_rls = rewrite_rls
   29.14 -    val safe_rls    = safe_rls
   29.15 -    val unsafe_rls  = unsafe_rls @ [pi1,pi2]
   29.16 -    val bound_rls   = bound_rls @ [boxL,diaR]
   29.17 -    val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2]
   29.18 -   end;
   29.19 -end;
   29.20 -structure S43_Prover = Modal_ProverFun(MP_Rule);
    30.1 --- a/src/Sequents/S43.thy	Mon Nov 20 21:23:12 2006 +0100
    30.2 +++ b/src/Sequents/S43.thy	Mon Nov 20 23:47:10 2006 +0100
    30.3 @@ -77,6 +77,130 @@
    30.4        S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
    30.5     $L |- $R1, []P, $R2"
    30.6  
    30.7 -ML {* use_legacy_bindings (the_context ()) *}
    30.8 +
    30.9 +ML {*
   30.10 +structure S43_Prover = Modal_ProverFun
   30.11 +(
   30.12 +  val rewrite_rls = thms "rewrite_rls"
   30.13 +  val safe_rls = thms "safe_rls"
   30.14 +  val unsafe_rls = thms "unsafe_rls" @ [thm "pi1", thm "pi2"]
   30.15 +  val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
   30.16 +  val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
   30.17 +    thm "rstar1", thm "rstar2", thm "S43pi0", thm "S43pi1", thm "S43pi2"]
   30.18 +)
   30.19 +*}
   30.20 +
   30.21 +
   30.22 +method_setup S43_solve = {*
   30.23 +  Method.no_args (Method.SIMPLE_METHOD
   30.24 +    (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))
   30.25 +*} "S4 solver"
   30.26 +
   30.27 +
   30.28 +(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
   30.29 +
   30.30 +lemma "|- []P --> P" by S43_solve
   30.31 +lemma "|- [](P-->Q) --> ([]P-->[]Q)" by S43_solve   (* normality*)
   30.32 +lemma "|- (P--<Q) --> []P --> []Q" by S43_solve
   30.33 +lemma "|- P --> <>P" by S43_solve
   30.34 +
   30.35 +lemma "|-  [](P & Q) <-> []P & []Q" by S43_solve
   30.36 +lemma "|-  <>(P | Q) <-> <>P | <>Q" by S43_solve
   30.37 +lemma "|-  [](P<->Q) <-> (P>-<Q)" by S43_solve
   30.38 +lemma "|-  <>(P-->Q) <-> ([]P--><>Q)" by S43_solve
   30.39 +lemma "|-        []P <-> ~<>(~P)" by S43_solve
   30.40 +lemma "|-     [](~P) <-> ~<>P" by S43_solve
   30.41 +lemma "|-       ~[]P <-> <>(~P)" by S43_solve
   30.42 +lemma "|-      [][]P <-> ~<><>(~P)" by S43_solve
   30.43 +lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by S43_solve
   30.44 +
   30.45 +lemma "|- []P | []Q --> [](P | Q)" by S43_solve
   30.46 +lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve
   30.47 +lemma "|- [](P | Q) --> []P | <>Q" by S43_solve
   30.48 +lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve
   30.49 +lemma "|- [](P | Q) --> <>P | []Q" by S43_solve
   30.50 +lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by S43_solve
   30.51 +lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by S43_solve
   30.52 +lemma "|- []P --> <>Q --> <>(P & Q)" by S43_solve
   30.53 +
   30.54 +
   30.55 +(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
   30.56 +
   30.57 +lemma "|- []A --> A" by S43_solve             (* refexivity *)
   30.58 +lemma "|- []A --> [][]A" by S43_solve         (* transitivity *)
   30.59 +lemma "|- []A --> <>A" by S43_solve           (* seriality *)
   30.60 +lemma "|- <>[](<>A --> []<>A)" by S43_solve
   30.61 +lemma "|- <>[](<>[]A --> []A)" by S43_solve
   30.62 +lemma "|- []P <-> [][]P" by S43_solve
   30.63 +lemma "|- <>P <-> <><>P" by S43_solve
   30.64 +lemma "|- <>[]<>P --> <>P" by S43_solve
   30.65 +lemma "|- []<>P <-> []<>[]<>P" by S43_solve
   30.66 +lemma "|- <>[]P <-> <>[]<>[]P" by S43_solve
   30.67 +
   30.68 +(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
   30.69 +
   30.70 +lemma "|- []P | []Q <-> []([]P | []Q)" by S43_solve
   30.71 +lemma "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)" by S43_solve
   30.72 +
   30.73 +(* These are from Hailpern, LNCS 129 *)
   30.74 +
   30.75 +lemma "|- [](P & Q) <-> []P & []Q" by S43_solve
   30.76 +lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve
   30.77 +lemma "|- <>(P --> Q) <-> ([]P --> <>Q)" by S43_solve
   30.78 +
   30.79 +lemma "|- [](P --> Q) --> (<>P --> <>Q)" by S43_solve
   30.80 +lemma "|- []P --> []<>P" by S43_solve
   30.81 +lemma "|- <>[]P --> <>P" by S43_solve
   30.82 +
   30.83 +lemma "|- []P | []Q --> [](P | Q)" by S43_solve
   30.84 +lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve
   30.85 +lemma "|- [](P | Q) --> []P | <>Q" by S43_solve
   30.86 +lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve
   30.87 +lemma "|- [](P | Q) --> <>P | []Q" by S43_solve
   30.88 +
   30.89 +
   30.90 +(* Theorems of system S43 *)
   30.91 +
   30.92 +lemma "|- <>[]P --> []<>P" by S43_solve
   30.93 +lemma "|- <>[]P --> [][]<>P" by S43_solve
   30.94 +lemma "|- [](<>P | <>Q) --> []<>P | []<>Q" by S43_solve
   30.95 +lemma "|- <>[]P & <>[]Q --> <>([]P & []Q)" by S43_solve
   30.96 +lemma "|- []([]P --> []Q) | []([]Q --> []P)" by S43_solve
   30.97 +lemma "|- [](<>P --> <>Q) | [](<>Q --> <>P)" by S43_solve
   30.98 +lemma "|- []([]P --> Q) | []([]Q --> P)" by S43_solve
   30.99 +lemma "|- [](P --> <>Q) | [](Q --> <>P)" by S43_solve
  30.100 +lemma "|- [](P --> []Q-->R) | [](P | ([]R --> Q))" by S43_solve
  30.101 +lemma "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)" by S43_solve
  30.102 +lemma "|- []([]P | Q) & [](P | []Q) --> []P | []Q" by S43_solve
  30.103 +lemma "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)" by S43_solve
  30.104 +lemma "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q" by S43_solve
  30.105 +lemma "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)" by S43_solve
  30.106 +lemma "|- <>[]<>P <-> []<>P" by S43_solve
  30.107 +lemma "|- []<>[]P <-> <>[]P" by S43_solve
  30.108 +
  30.109 +(* These are from Hailpern, LNCS 129 *)
  30.110 +
  30.111 +lemma "|- [](P & Q) <-> []P & []Q" by S43_solve
  30.112 +lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve
  30.113 +lemma "|- <>(P --> Q) <-> []P --> <>Q" by S43_solve
  30.114 +
  30.115 +lemma "|- [](P --> Q) --> <>P --> <>Q" by S43_solve
  30.116 +lemma "|- []P --> []<>P" by S43_solve
  30.117 +lemma "|- <>[]P --> <>P" by S43_solve
  30.118 +lemma "|- []<>[]P --> []<>P" by S43_solve
  30.119 +lemma "|- <>[]P --> <>[]<>P" by S43_solve
  30.120 +lemma "|- <>[]P --> []<>P" by S43_solve
  30.121 +lemma "|- []<>[]P <-> <>[]P" by S43_solve
  30.122 +lemma "|- <>[]<>P <-> []<>P" by S43_solve
  30.123 +
  30.124 +lemma "|- []P | []Q --> [](P | Q)" by S43_solve
  30.125 +lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve
  30.126 +lemma "|- [](P | Q) --> []P | <>Q" by S43_solve
  30.127 +lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve
  30.128 +lemma "|- [](P | Q) --> <>P | []Q" by S43_solve
  30.129 +lemma "|- [](P | Q) --> []<>P | []<>Q" by S43_solve
  30.130 +lemma "|- <>[]P & <>[]Q --> <>(P & Q)" by S43_solve
  30.131 +lemma "|- <>[](P & Q) <-> <>[]P & <>[]Q" by S43_solve
  30.132 +lemma "|- []<>(P | Q) <-> []<>P | []<>Q" by S43_solve
  30.133  
  30.134  end
    31.1 --- a/src/Sequents/T.ML	Mon Nov 20 21:23:12 2006 +0100
    31.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.3 @@ -1,17 +0,0 @@
    31.4 -(*  Title:      Modal/T.ML
    31.5 -    ID:         $Id$
    31.6 -    Author:     Martin Coen
    31.7 -    Copyright   1991  University of Cambridge
    31.8 -*)
    31.9 -
   31.10 -local open Modal0_rls
   31.11 -in structure MP_Rule : MODAL_PROVER_RULE =
   31.12 -   struct
   31.13 -    val rewrite_rls = rewrite_rls
   31.14 -    val safe_rls    = safe_rls
   31.15 -    val unsafe_rls  = unsafe_rls @ [boxR,diaL]
   31.16 -    val bound_rls   = bound_rls @ [boxL,diaR]
   31.17 -    val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
   31.18 -   end
   31.19 -end;
   31.20 -structure T_Prover = Modal_ProverFun(MP_Rule);
    32.1 --- a/src/Sequents/T.thy	Mon Nov 20 21:23:12 2006 +0100
    32.2 +++ b/src/Sequents/T.thy	Mon Nov 20 23:47:10 2006 +0100
    32.3 @@ -31,6 +31,46 @@
    32.4     "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
    32.5                 $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
    32.6  
    32.7 -ML {* use_legacy_bindings (the_context ()) *}
    32.8 +ML {*
    32.9 +structure T_Prover = Modal_ProverFun
   32.10 +(
   32.11 +  val rewrite_rls = thms "rewrite_rls"
   32.12 +  val safe_rls = thms "safe_rls"
   32.13 +  val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"]
   32.14 +  val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
   32.15 +  val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
   32.16 +    thm "rstar1", thm "rstar2"]
   32.17 +)
   32.18 +*}
   32.19 +
   32.20 +method_setup T_solve =
   32.21 +{* Method.no_args (Method.SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
   32.22 +
   32.23 +
   32.24 +(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
   32.25 +
   32.26 +lemma "|- []P --> P" by T_solve
   32.27 +lemma "|- [](P-->Q) --> ([]P-->[]Q)" by T_solve   (* normality*)
   32.28 +lemma "|- (P--<Q) --> []P --> []Q" by T_solve
   32.29 +lemma "|- P --> <>P" by T_solve
   32.30 +
   32.31 +lemma "|-  [](P & Q) <-> []P & []Q" by T_solve
   32.32 +lemma "|-  <>(P | Q) <-> <>P | <>Q" by T_solve
   32.33 +lemma "|-  [](P<->Q) <-> (P>-<Q)" by T_solve
   32.34 +lemma "|-  <>(P-->Q) <-> ([]P--><>Q)" by T_solve
   32.35 +lemma "|-        []P <-> ~<>(~P)" by T_solve
   32.36 +lemma "|-     [](~P) <-> ~<>P" by T_solve
   32.37 +lemma "|-       ~[]P <-> <>(~P)" by T_solve
   32.38 +lemma "|-      [][]P <-> ~<><>(~P)" by T_solve
   32.39 +lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by T_solve
   32.40 +
   32.41 +lemma "|- []P | []Q --> [](P | Q)" by T_solve
   32.42 +lemma "|- <>(P & Q) --> <>P & <>Q" by T_solve
   32.43 +lemma "|- [](P | Q) --> []P | <>Q" by T_solve
   32.44 +lemma "|- <>P & []Q --> <>(P & Q)" by T_solve
   32.45 +lemma "|- [](P | Q) --> <>P | []Q" by T_solve
   32.46 +lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by T_solve
   32.47 +lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by T_solve
   32.48 +lemma "|- []P --> <>Q --> <>(P & Q)" by T_solve
   32.49  
   32.50  end
    33.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.2 +++ b/src/Sequents/Washing.thy	Mon Nov 20 23:47:10 2006 +0100
    33.3 @@ -0,0 +1,61 @@
    33.4 +
    33.5 +(* $Id$ *)
    33.6 +
    33.7 +(* code by Sara Kalvala, based on Paulson's LK
    33.8 +                           and Moore's tisl.ML *)
    33.9 +
   33.10 +theory Washing
   33.11 +imports ILL
   33.12 +begin
   33.13 +
   33.14 +consts
   33.15 +  dollar :: o
   33.16 +  quarter :: o
   33.17 +  loaded :: o
   33.18 +  dirty :: o
   33.19 +  wet :: o
   33.20 +  clean :: o
   33.21 +
   33.22 +axioms
   33.23 +  change:
   33.24 +  "dollar |- (quarter >< quarter >< quarter >< quarter)"
   33.25 +
   33.26 +  load1:
   33.27 +  "quarter , quarter , quarter , quarter , quarter |- loaded"
   33.28 +
   33.29 +  load2:
   33.30 +  "dollar , quarter |- loaded"
   33.31 +
   33.32 +  wash:
   33.33 +  "loaded , dirty |- wet"
   33.34 +
   33.35 +  dry:
   33.36 +  "wet, quarter , quarter , quarter |- clean"
   33.37 +
   33.38 +
   33.39 +(* "activate" definitions for use in proof *)
   33.40 +
   33.41 +ML_setup {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
   33.42 +ML_setup {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
   33.43 +ML_setup {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
   33.44 +ML_setup {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
   33.45 +
   33.46 +(* a load of dirty clothes and two dollars gives you clean clothes *)
   33.47 +
   33.48 +lemma "dollar , dollar , dirty |- clean"
   33.49 +  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
   33.50 +  done
   33.51 +
   33.52 +(* order of premises doesn't matter *)
   33.53 +
   33.54 +lemma "dollar , dirty , dollar |- clean"
   33.55 +  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
   33.56 +  done
   33.57 +
   33.58 +(* alternative formulation *)
   33.59 +
   33.60 +lemma "dollar , dollar |- dirty -o clean"
   33.61 +  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
   33.62 +  done
   33.63 +
   33.64 +end
    34.1 --- a/src/Sequents/simpdata.ML	Mon Nov 20 21:23:12 2006 +0100
    34.2 +++ b/src/Sequents/simpdata.ML	Mon Nov 20 23:47:10 2006 +0100
    34.3 @@ -10,11 +10,16 @@
    34.4  
    34.5  (*** Rewrite rules ***)
    34.6  
    34.7 +local
    34.8 +  val subst = thm "subst"
    34.9 +in
   34.10 +
   34.11  fun prove_fun s =
   34.12   (writeln s;
   34.13    prove_goal (the_context ()) s
   34.14     (fn prems => [ (cut_facts_tac prems 1),
   34.15                    (fast_tac (pack() add_safes [subst]) 1) ]));
   34.16 +end;
   34.17  
   34.18  val conj_simps = map prove_fun
   34.19   ["|- P & True <-> P",      "|- True & P <-> P",
   34.20 @@ -83,6 +88,12 @@
   34.21  
   34.22  (** Conversion into rewrite rules **)
   34.23  
   34.24 +local
   34.25 +  val mp_R = thm "mp_R";
   34.26 +  val conjunct1 = thm "conjunct1";
   34.27 +  val conjunct2 = thm "conjunct2";
   34.28 +  val spec = thm "spec";
   34.29 +in
   34.30  (*Make atomic rewrite rules*)
   34.31  fun atomize r =
   34.32   case concl_of r of
   34.33 @@ -99,22 +110,26 @@
   34.34               | _                     => [r])
   34.35        | _ => [])  (*ignore theorem unless it has precisely one conclusion*)
   34.36   | _ => [r];
   34.37 -
   34.38 +end;
   34.39  
   34.40  Goal "|- ~P ==> |- (P <-> False)";
   34.41 -by (etac (thinR RS cut) 1);
   34.42 +by (etac (thm "thinR" RS (thm "cut")) 1);
   34.43  by (Fast_tac 1);
   34.44  qed "P_iff_F";
   34.45  
   34.46 -val iff_reflection_F = P_iff_F RS iff_reflection;
   34.47 +bind_thm ("iff_reflection_F", thm "P_iff_F" RS thm "iff_reflection");
   34.48  
   34.49  Goal "|- P ==> |- (P <-> True)";
   34.50 -by (etac (thinR RS cut) 1);
   34.51 +by (etac (thm "thinR" RS (thm "cut")) 1);
   34.52  by (Fast_tac 1);
   34.53  qed "P_iff_T";
   34.54  
   34.55 -val iff_reflection_T = P_iff_T RS iff_reflection;
   34.56 +bind_thm ("iff_reflection_T", thm "P_iff_T" RS thm "iff_reflection");
   34.57  
   34.58 +local
   34.59 +  val eq_reflection = thm "eq_reflection"
   34.60 +  val iff_reflection = thm "iff_reflection"
   34.61 +in
   34.62  (*Make meta-equalities.*)
   34.63  fun mk_meta_eq th = case concl_of th of
   34.64      Const("==",_)$_$_           => th
   34.65 @@ -128,12 +143,12 @@
   34.66                      | _                       => th RS iff_reflection_T)
   34.67             | _ => error ("addsimps: unable to use theorem\n" ^
   34.68                           string_of_thm th));
   34.69 -
   34.70 +end;
   34.71  
   34.72  (*Replace premises x=y, X<->Y by X==Y*)
   34.73  val mk_meta_prems =
   34.74      rule_by_tactic
   34.75 -      (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
   34.76 +      (REPEAT_FIRST (resolve_tac [thm "meta_eq_to_obj_eq", thm "def_imp_iff"]));
   34.77  
   34.78  (*Congruence rules for = or <-> (instead of ==)*)
   34.79  fun mk_meta_cong rl =
   34.80 @@ -179,9 +194,9 @@
   34.81      "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')";
   34.82  by (lemma_tac p1 1);
   34.83  by (Safe_tac 1);
   34.84 -by (REPEAT (rtac cut 1
   34.85 +by (REPEAT (rtac (thm "cut") 1
   34.86              THEN
   34.87 -            DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
   34.88 +            DEPTH_SOLVE_1 (resolve_tac [thm "thinL", thm "thinR", p2 COMP thm "monotonic"] 1)
   34.89              THEN
   34.90              Safe_tac 1));
   34.91  qed "imp_cong";
   34.92 @@ -190,42 +205,23 @@
   34.93      "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')";
   34.94  by (lemma_tac p1 1);
   34.95  by (Safe_tac 1);
   34.96 -by (REPEAT (rtac cut 1
   34.97 +by (REPEAT (rtac (thm "cut") 1
   34.98              THEN
   34.99 -            DEPTH_SOLVE_1 (resolve_tac [thinL, thinR, p2 COMP monotonic] 1)
  34.100 +            DEPTH_SOLVE_1 (resolve_tac [thm "thinL", thm "thinR", p2 COMP thm "monotonic"] 1)
  34.101              THEN
  34.102              Safe_tac 1));
  34.103  qed "conj_cong";
  34.104  
  34.105  Goal "|- (x=y) <-> (y=x)";
  34.106 -by (fast_tac (pack() add_safes [subst]) 1);
  34.107 +by (fast_tac (pack() add_safes [thm "subst"]) 1);
  34.108  qed "eq_sym_conv";
  34.109  
  34.110  
  34.111 -(** if-then-else rules **)
  34.112 -
  34.113 -Goalw [If_def] "|- (if True then x else y) = x";
  34.114 -by (Fast_tac 1);
  34.115 -qed "if_True";
  34.116 -
  34.117 -Goalw [If_def] "|- (if False then x else y) = y";
  34.118 -by (Fast_tac 1);
  34.119 -qed "if_False";
  34.120 -
  34.121 -Goalw [If_def] "|- P ==> |- (if P then x else y) = x";
  34.122 -by (etac (thinR RS cut) 1);
  34.123 -by (Fast_tac 1);
  34.124 -qed "if_P";
  34.125 -
  34.126 -Goalw [If_def] "|- ~P ==> |- (if P then x else y) = y";
  34.127 -by (etac (thinR RS cut) 1);
  34.128 -by (Fast_tac 1);
  34.129 -qed "if_not_P";
  34.130 -
  34.131  
  34.132  (*** Standard simpsets ***)
  34.133  
  34.134 -val triv_rls = [FalseL, TrueR, basic, refl, iff_refl, reflexive_thm];
  34.135 +val triv_rls = [thm "FalseL", thm "TrueR", thm "basic", thm "refl",
  34.136 +  thm "iff_refl", reflexive_thm];
  34.137  
  34.138  fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
  34.139                                   assume_tac];
  34.140 @@ -244,7 +240,7 @@
  34.141  
  34.142  val LK_simps =
  34.143     [triv_forall_equality, (* prunes params *)
  34.144 -    refl RS P_iff_T] @
  34.145 +    thm "refl" RS P_iff_T] @
  34.146      conj_simps @ disj_simps @ not_simps @
  34.147      imp_simps @ iff_simps @quant_simps @ all_simps @ ex_simps @
  34.148      [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2] @
  34.149 @@ -269,10 +265,10 @@
  34.150      asm_simp_tac LK_basic_ss 1]);
  34.151  
  34.152  Goal "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))";
  34.153 -by (res_inst_tac [ ("P","Q") ] cut 1);
  34.154 -by (simp_tac (simpset() addsimps [if_P]) 2);
  34.155 -by (res_inst_tac [ ("P","~Q") ] cut 1);
  34.156 -by (simp_tac (simpset() addsimps [if_not_P]) 2);
  34.157 +by (res_inst_tac [ ("P","Q") ] (thm "cut") 1);
  34.158 +by (simp_tac (simpset() addsimps [thm "if_P"]) 2);
  34.159 +by (res_inst_tac [ ("P","~Q") ] (thm "cut") 1);
  34.160 +by (simp_tac (simpset() addsimps [thm "if_not_P"]) 2);
  34.161  by (Fast_tac 1);
  34.162  qed "split_if";
  34.163  
  34.164 @@ -284,8 +280,8 @@
  34.165  Goal "|- (if x=y then y else x) = x";
  34.166  by (lemma_tac split_if 1);
  34.167  by (Safe_tac 1);
  34.168 -by (rtac symL 1);
  34.169 -by (rtac basic 1);
  34.170 +by (rtac (thm "symL") 1);
  34.171 +by (rtac (thm "basic") 1);
  34.172  qed "if_eq_cancel";
  34.173  
  34.174  (*Putting in automatic case splits seems to require a lot of work.*)