New unified treatment of sequent calculi by Sara Kalvala
authorpaulson
Wed Oct 09 13:32:33 1996 +0200 (1996-10-09)
changeset 2073fb0655539d05
parent 2072 6ac12b9478d5
child 2074 30a65172e003
New unified treatment of sequent calculi by Sara Kalvala
combines the old LK and Modal with the new ILL (Int. Linear Logic)
src/Sequents/ILL.ML
src/Sequents/ILL.thy
src/Sequents/LK.ML
src/Sequents/LK.thy
src/Sequents/Makefile
src/Sequents/Modal0.ML
src/Sequents/Modal0.thy
src/Sequents/README.html
src/Sequents/ROOT.ML
src/Sequents/S4.ML
src/Sequents/S4.thy
src/Sequents/S43.ML
src/Sequents/S43.thy
src/Sequents/Sequents.thy
src/Sequents/T.ML
src/Sequents/T.thy
src/Sequents/ex/ILL/ILL_kleene_lemmas.ML
src/Sequents/ex/ILL/ILL_predlog.ML
src/Sequents/ex/ILL/ILL_predlog.thy
src/Sequents/ex/ILL/ROOT.ML
src/Sequents/ex/ILL/washing.ML
src/Sequents/ex/ILL/washing.thy
src/Sequents/ex/LK/ROOT.ML
src/Sequents/ex/LK/hardquant.ML
src/Sequents/ex/LK/prop.ML
src/Sequents/ex/LK/quant.ML
src/Sequents/ex/Modal/ROOT.ML
src/Sequents/ex/Modal/S43thms.ML
src/Sequents/ex/Modal/S4thms.ML
src/Sequents/ex/Modal/Tthms.ML
src/Sequents/ex/ROOT.ML
src/Sequents/index.html
src/Sequents/prover.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Sequents/ILL.ML	Wed Oct 09 13:32:33 1996 +0200
     1.3 @@ -0,0 +1,140 @@
     1.4 +(*  Title:      Sequents/ILL.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sara Kalvala and Valeria de Paiva
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +*)
    1.10 +
    1.11 +open ILL;
    1.12 +
    1.13 +
    1.14 +val lazy_cs = empty_pack
    1.15 + add_safes [tensl, conjr, disjl, promote0,
    1.16 +	    context2,context3]
    1.17 + add_unsafes [identity, zerol, conjll, conjlr, disjrl, disjrr,
    1.18 +	       impr, tensr, impl, derelict, weaken,
    1.19 +		 promote1, promote2,context1,context4a,context4b];
    1.20 +
    1.21 +fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n);
    1.22 +
    1.23 +fun auto x = prove_goal thy x (fn prems => [best_tac lazy_cs 1]);
    1.24 +
    1.25 +val aux_impl = prove_goal thy "$F, $G |- A ==> $F, !(A -o B), $G |- B"
    1.26 +(fn prems => [rtac derelict 1 THEN rtac impl 1 THEN rtac identity 2
    1.27 +	THEN rtac context1 1 THEN rtac (hd(prems)) 1]);
    1.28 +
    1.29 +val conj_lemma =
    1.30 +prove_goal thy " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
    1.31 +(fn prems => [rtac contract 1,
    1.32 +	res_inst_tac [("A","(!A) >< (!B)")] cut 1,
    1.33 +	rtac tensr 2,
    1.34 +	rtac (auto "! (A && B) |- !A") 3,
    1.35 +	rtac (auto "! (A && B) |- !B") 3,
    1.36 +	rtac context1 2,
    1.37 +	rtac tensl 2,
    1.38 +	rtac (hd(prems)) 2,
    1.39 +	rtac context3 1,
    1.40 +	rtac context3 1,
    1.41 +	rtac context1 1]);
    1.42 +
    1.43 +val impr_contract =
    1.44 +prove_goal thy "!A, !A, $G |- B ==> $G |- (!A) -o B"
    1.45 +(fn prems => [rtac impr 1 THEN rtac contract 1
    1.46 +		 THEN rtac (hd(prems)) 1]);
    1.47 +
    1.48 +
    1.49 +val impr_contr_der =
    1.50 +prove_goal thy "A, !A, $G |- B ==> $G |- (!A) -o B"
    1.51 +(fn prems => [rtac impr 1 THEN rtac contract 1 THEN rtac derelict 1
    1.52 +		 THEN rtac (hd(prems)) 1]);
    1.53 +
    1.54 +val contrad1 =
    1.55 +prove_goal thy "$F, (!B) -o 0, $G, !B, $H |- A"
    1.56 +(fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1,
    1.57 +	  rtac zerol 1]);
    1.58 +
    1.59 +
    1.60 +val contrad2 =
    1.61 +prove_goal thy "$F, !B, $G, (!B) -o 0, $H |- A"
    1.62 +(fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1,
    1.63 +	  rtac zerol 1]);
    1.64 +
    1.65 +val ll_mp =
    1.66 +prove_goal thy "A -o B, A |- B"
    1.67 +(fn _ => [rtac impl 1 THEN rtac identity 2 THEN rtac identity 2
    1.68 +	 THEN rtac context1 1]);
    1.69 +
    1.70 +val mp_rule1 =
    1.71 +prove_goal thy "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
    1.72 +(fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2,
    1.73 +		rtac (hd(prems)) 2, rtac context3 1, rtac context3 1,
    1.74 +		rtac context1 1]);
    1.75 +
    1.76 +val mp_rule2 =
    1.77 +prove_goal thy "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
    1.78 +(fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2,
    1.79 +		rtac (hd(prems)) 2, rtac context3 1, rtac context3 1,
    1.80 +		rtac context1 1]);
    1.81 +
    1.82 +val or_to_and =
    1.83 +prove_goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
    1.84 +(fn _ => [best_tac lazy_cs 1]);
    1.85 +
    1.86 +val o_a_rule =
    1.87 +prove_goal thy "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \
    1.88 +\         $F, !((!(A ++ B)) -o 0), $G |- C"
    1.89 +(fn prems => [rtac cut 1, rtac or_to_and 2, rtac (hd(prems)) 2,
    1.90 +		rtac context3 1, rtac context1 1]);
    1.91 +
    1.92 +
    1.93 +
    1.94 +val conj_imp =
    1.95 + prove_goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
    1.96 +(fn _ => [rtac impr 1,rtac conj_lemma 1, rtac disjl 1,
    1.97 +	  ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs)]);
    1.98 +
    1.99 +
   1.100 +val not_imp = auto "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0";
   1.101 +
   1.102 +val a_not_a =
   1.103 +prove_goal thy "!A -o (!A -o 0) |- !A -o 0"
   1.104 +     (fn _ => [rtac impr 1, rtac contract 1, rtac impl 1,
   1.105 +	  rtac context1 1 THEN rtac identity 2, best_tac lazy_cs 1]);
   1.106 +
   1.107 +val a_not_a_rule =
   1.108 +prove_goal thy "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
   1.109 + (fn prems => [res_inst_tac [("A","!A -o 0")] cut 1,
   1.110 +               rtac a_not_a 2 THEN rtac (hd(prems)) 2
   1.111 +		 THEN best_tac lazy_cs 1]);
   1.112 +
   1.113 +fun thm_to_rule x y =
   1.114 +prove_goal thy x (fn prems => [rtac cut 1, rtac y 2, rtac (hd(prems)) 2,
   1.115 +				best_tac lazy_cs 1]);
   1.116 +
   1.117 +val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1,
   1.118 +			contrad2, mp_rule1, mp_rule2, o_a_rule,
   1.119 +			a_not_a_rule]
   1.120 +		add_unsafes [aux_impl];
   1.121 +
   1.122 +val power_cs = safe_cs add_unsafes [impr_contr_der];
   1.123 +
   1.124 +fun auto1 x = prove_goal thy x (fn prems => [best_tac safe_cs 1]) ;
   1.125 +
   1.126 +fun auto2 x = prove_goal thy x (fn prems => [best_tac power_cs 1]) ;
   1.127 +
   1.128 +
   1.129 +(* some examples from Troelstra and van Dalen
   1.130 +
   1.131 +auto1  "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0";
   1.132 +
   1.133 +auto1  "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))";
   1.134 +
   1.135 +auto1  "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |- \
   1.136 +\        (!A) -o ( (!  ((!B) -o 0)) -o 0)";
   1.137 +
   1.138 +
   1.139 +auto2  "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |- \
   1.140 +\         (!((! ((!A) -o B) ) -o 0)) -o 0";
   1.141 +
   1.142 +
   1.143 +                                                         *)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Sequents/ILL.thy	Wed Oct 09 13:32:33 1996 +0200
     2.3 @@ -0,0 +1,134 @@
     2.4 +(*  Title:      ILL.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Sara Kalvala and Valeria de Paiva
     2.7 +    Copyright   1995  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +
    2.11 +ILL = Sequents +
    2.12 +
    2.13 +consts
    2.14 +
    2.15 +  
    2.16 + Trueprop	:: "two_seqi"
    2.17 + "@Trueprop"	:: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
    2.18 + 
    2.19 + 
    2.20 +
    2.21 +"><"    ::"[o, o] => o"        (infixr 35)
    2.22 +"-o"    ::"[o, o] => o"        (infixr 45)
    2.23 +"o-o"   ::"[o, o] => o"        (infixr 45)
    2.24 +FShriek ::"o => o"             ("! _" [100] 1000)
    2.25 +"&&"    ::"[o, o] => o"        (infixr 35)
    2.26 +"++"    ::"[o, o] => o"        (infixr 35)
    2.27 +zero    ::"o"                  ("0")
    2.28 +top     ::"o"                  ("1")
    2.29 +eye     ::"o"                  ("I")
    2.30 +aneg    ::"o=>o"               ("~_")
    2.31 +
    2.32 +
    2.33 +  (* syntax for context manipulation *)
    2.34 +
    2.35 + Context      :: "two_seqi"
    2.36 +"@Context"    :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
    2.37 +
    2.38 +  (* syntax for promotion rule *)
    2.39 +
    2.40 +  PromAux :: "three_seqi"
    2.41 +"@PromAux":: "three_seqe" ("promaux {_||_||_}")
    2.42 +
    2.43 +defs
    2.44 +
    2.45 +liff_def        "P o-o Q == (P -o Q) >< (Q -o P)"
    2.46 +
    2.47 +aneg_def        "~A == A -o 0"
    2.48 +
    2.49 +
    2.50 +
    2.51 +
    2.52 +rules
    2.53 +  
    2.54 +identity        "P |- P"
    2.55 +
    2.56 +zerol           "$G, 0, $H |- A"
    2.57 +
    2.58 +  (* RULES THAT DO NOT DIVIDE CONTEXT *)
    2.59 +
    2.60 +derelict   "$F, A, $G |- C ==> $F, !A, $G |- C"
    2.61 +  (* unfortunately, this one removes !A  *)
    2.62 +
    2.63 +contract  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
    2.64 +  
    2.65 +weaken     "$F, $G |- C ==> $G, !A, $F |- C"
    2.66 +  (* weak form of weakening, in practice just to clean context *)
    2.67 +  (* weaken and contract not needed (CHECK)  *)
    2.68 +
    2.69 +promote2        "promaux{ || $H || B} ==> $H |- !B"
    2.70 +promote1        "promaux{!A, $G || $H || B}
    2.71 +                 ==> promaux {$G || $H, !A || B}"
    2.72 +promote0        "$G |- A ==> promaux {$G || || A}"
    2.73 +
    2.74 +
    2.75 +  
    2.76 +tensl     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
    2.77 +
    2.78 +impr      "A, $F |- B ==> $F |- A -o B"
    2.79 +
    2.80 +conjr           "[| $F |- A ;
    2.81 +                 $F |- B |]
    2.82 +                ==> $F |- (A && B)"
    2.83 +
    2.84 +conjll          "$G, A, $H |- C ==> $G, A && B, $H |- C"
    2.85 +
    2.86 +conjlr          "$G, B, $H |- C ==> $G, A && B, $H |- C"
    2.87 +
    2.88 +disjrl          "$G |- A ==> $G |- A ++ B"
    2.89 +disjrr          "$G |- B ==> $G |- A ++ B"
    2.90 +disjl           "[| $G, A, $H |- C ;
    2.91 +                    $G, B, $H |- C |]
    2.92 +                ==> $G, A ++ B, $H |- C"
    2.93 +
    2.94 +
    2.95 +      (* RULES THAT DIVIDE CONTEXT *)
    2.96 +
    2.97 +tensr           "[| $F, $J :=: $G;
    2.98 +                    $F |- A ;
    2.99 +                    $J |- B     |]
   2.100 +                    ==> $G |- A >< B"
   2.101 +
   2.102 +impl            "[| $G, $F :=: $J, $H ;
   2.103 +                    B, $F |- C ;
   2.104 +                       $G |- A |]
   2.105 +                    ==> $J, A -o B, $H |- C"
   2.106 +
   2.107 +    
   2.108 +cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
   2.109 +         $H1, $H2, $H3, $H4 |- A ;
   2.110 +         $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
   2.111 +
   2.112 +
   2.113 +  (* CONTEXT RULES *)
   2.114 +
   2.115 +context1     "$G :=: $G"
   2.116 +context2     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
   2.117 +context3     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
   2.118 +context4a    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
   2.119 +context4b    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
   2.120 +context5     "$F, $G :=: $H ==> $G, $F :=: $H"
   2.121 +
   2.122 +
   2.123 +
   2.124 + 
   2.125 +end
   2.126 +
   2.127 +ML
   2.128 +
   2.129 +val parse_translation = [("@Trueprop",Sequents.single_tr "Trueprop"),
   2.130 +                         ("@Context",Sequents.two_seq_tr "Context"),
   2.131 +                         ("@PromAux", Sequents.three_seq_tr "PromAux")];
   2.132 +
   2.133 +val print_translation = [("Trueprop",Sequents.single_tr' "@Trueprop"),
   2.134 +                         ("Context",Sequents.two_seq_tr'"@Context"),
   2.135 +                         ("PromAux", Sequents.three_seq_tr'"@PromAux")];
   2.136 +
   2.137 + 
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Sequents/LK.ML	Wed Oct 09 13:32:33 1996 +0200
     3.3 @@ -0,0 +1,82 @@
     3.4 +(*  Title:      LK/LK.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1992  University of Cambridge
     3.8 +
     3.9 +Tactics and lemmas for lk.thy (thanks also to Philippe de Groote)  
    3.10 +*)
    3.11 +
    3.12 +open LK;
    3.13 +
    3.14 +(*Higher precedence than := facilitates use of references*)
    3.15 +infix 4 add_safes add_unsafes;
    3.16 +
    3.17 +(*Cut and thin, replacing the right-side formula*)
    3.18 +fun cutR_tac (sP: string) i = 
    3.19 +    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
    3.20 +
    3.21 +(*Cut and thin, replacing the left-side formula*)
    3.22 +fun cutL_tac (sP: string) i = 
    3.23 +    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
    3.24 +
    3.25 +
    3.26 +(** If-and-only-if rules **)
    3.27 +qed_goalw "iffR" LK.thy [iff_def]
    3.28 +    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    3.29 + (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
    3.30 +
    3.31 +qed_goalw "iffL" LK.thy [iff_def]
    3.32 +   "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    3.33 + (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
    3.34 +
    3.35 +qed_goalw "TrueR" LK.thy [True_def]
    3.36 +    "$H |- $E, True, $F"
    3.37 + (fn _=> [ rtac impR 1, rtac basic 1 ]);
    3.38 +
    3.39 +
    3.40 +(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
    3.41 +
    3.42 +qed_goal "allL_thin" LK.thy 
    3.43 +    "$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E"
    3.44 + (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);
    3.45 +
    3.46 +qed_goal "exR_thin" LK.thy 
    3.47 +    "$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F"
    3.48 + (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);
    3.49 +
    3.50 +(* Symmetry of equality in hypotheses *)
    3.51 +qed_goal "symL" LK.thy 
    3.52 +    "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" 
    3.53 + (fn prems=>
    3.54 +  [ (rtac cut 1),
    3.55 +    (rtac thinL 2),
    3.56 +    (resolve_tac prems 2),
    3.57 +    (resolve_tac [basic RS sym] 1) ]);
    3.58 +
    3.59 +
    3.60 +
    3.61 +
    3.62 +(*The rules of LK*)
    3.63 +val prop_pack = empty_pack add_safes 
    3.64 +                [basic, refl, conjL, conjR, disjL, disjR, impL, impR, 
    3.65 +                 notL, notR, iffL, iffR];
    3.66 +
    3.67 +val LK_pack = prop_pack add_safes   [allR, exL] 
    3.68 +                        add_unsafes [allL_thin, exR_thin];
    3.69 +
    3.70 +val LK_dup_pack = prop_pack add_safes   [allR, exL] 
    3.71 +                            add_unsafes [allL, exR];
    3.72 +
    3.73 +
    3.74 +
    3.75 +(** Contraction.  Useful since some rules are not complete. **)
    3.76 +
    3.77 +qed_goal "conR" LK.thy 
    3.78 +    "$H |- $E, P, $F, P ==> $H |- $E, P, $F"
    3.79 + (fn prems=>
    3.80 +  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
    3.81 +
    3.82 +qed_goal "conL" LK.thy 
    3.83 +    "$H, P, $G, P |- $E ==> $H, P, $G |- $E"
    3.84 + (fn prems=>
    3.85 +  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Sequents/LK.thy	Wed Oct 09 13:32:33 1996 +0200
     4.3 @@ -0,0 +1,84 @@
     4.4 +(*  Title:      LK/lk.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1993  University of Cambridge
     4.8 +
     4.9 +Classical First-Order Sequent Calculus
    4.10 +
    4.11 +There may be printing problems if a seqent is in expanded normal form
    4.12 +	(eta-expanded, beta-contracted)
    4.13 +*)
    4.14 +
    4.15 +LK = Sequents +
    4.16 +
    4.17 +
    4.18 +consts
    4.19 +
    4.20 + Trueprop	:: "two_seqi"
    4.21 + "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
    4.22 +
    4.23 +
    4.24 +  True,False   :: o
    4.25 +  "="          :: ['a,'a] => o       (infixl 50)
    4.26 +  Not          :: o => o             ("~ _" [40] 40)
    4.27 +  "&"          :: [o,o] => o         (infixr 35)
    4.28 +  "|"          :: [o,o] => o         (infixr 30)
    4.29 +  "-->","<->"  :: [o,o] => o         (infixr 25)
    4.30 +  The          :: ('a => o) => 'a    (binder "THE " 10)
    4.31 +  All          :: ('a => o) => o     (binder "ALL " 10)
    4.32 +  Ex           :: ('a => o) => o     (binder "EX " 10)
    4.33 +
    4.34 +rules
    4.35 +  (*Structural rules*)
    4.36 +
    4.37 +  basic "$H, P, $G |- $E, P, $F"
    4.38 +
    4.39 +  thinR "$H |- $E, $F ==> $H |- $E, P, $F"
    4.40 +  thinL "$H, $G |- $E ==> $H, P, $G |- $E"
    4.41 +
    4.42 +  cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
    4.43 +
    4.44 +  (*Propositional rules*)
    4.45 +
    4.46 +  conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
    4.47 +  conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
    4.48 +
    4.49 +  disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
    4.50 +  disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
    4.51 +
    4.52 +  impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
    4.53 +  impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
    4.54 +
    4.55 +  notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
    4.56 +  notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
    4.57 +
    4.58 +  FalseL "$H, False, $G |- $E"
    4.59 +
    4.60 +  True_def "True == False-->False"
    4.61 +  iff_def  "P<->Q == (P-->Q) & (Q-->P)"
    4.62 +
    4.63 +  (*Quantifiers*)
    4.64 +
    4.65 +  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
    4.66 +  allL  "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
    4.67 +
    4.68 +  exR   "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
    4.69 +  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
    4.70 +
    4.71 +  (*Equality*)
    4.72 +
    4.73 +  refl  "$H |- $E, a=a, $F"
    4.74 +  sym   "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F"
    4.75 +  trans "[| $H|- $E, a=b, $F;  $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F"
    4.76 +
    4.77 +
    4.78 +  (*Descriptions*)
    4.79 +
    4.80 +  The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
    4.81 +          $H |- $E, P(THE x.P(x)), $F"
    4.82 +end
    4.83 +
    4.84 +  ML
    4.85 +
    4.86 +val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
    4.87 +val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Sequents/Makefile	Wed Oct 09 13:32:33 1996 +0200
     5.3 @@ -0,0 +1,72 @@
     5.4 +# $Id$
     5.5 +#########################################################################
     5.6 +#									#
     5.7 +# 			Makefile for Isabelle (Sequents)		#
     5.8 +#									#
     5.9 +#########################################################################
    5.10 +
    5.11 +#To make the system, cd to this directory and type
    5.12 +#	make
    5.13 +#To make the system and test it on standard examples, type 
    5.14 +#	make test
    5.15 +#To generate HTML files for every theory, set the environment variable
    5.16 +#MAKE_HTML or add the parameter "MAKE_HTML=".
    5.17 +
    5.18 +#Environment variable ISABELLECOMP specifies the compiler.
    5.19 +#Environment variable ISABELLEBIN specifies the destination directory.
    5.20 +#For Poly/ML, ISABELLEBIN must begin with a /
    5.21 +
    5.22 +#Makes Pure if this file is ABSENT -- but not 
    5.23 +#if it is out of date, since this Makefile does not know its dependencies!
    5.24 +
    5.25 +BIN = $(ISABELLEBIN)
    5.26 +COMP = $(ISABELLECOMP)
    5.27 +NAMES = ILL LK S4 S43 T
    5.28 +FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
    5.29 +
    5.30 +ILL_NAMES = ILL_predlog washing 
    5.31 +EX_FILES = ex/ROOT.ML \
    5.32 +    ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML ex/LK/quant.ML \
    5.33 +    ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \
    5.34 +    ex/ILL/ILL_kleene_lemmas.ML \
    5.35 +    $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
    5.36 +
    5.37 +$(BIN)/Sequents:   $(BIN)/Pure  $(FILES) 
    5.38 +	case "$(COMP)" in \
    5.39 +	poly*)	echo 'make_database"$(BIN)/Sequents"; quit();'  \
    5.40 +			| $(COMP) $(BIN)/Pure;\
    5.41 +                if [ "$${MAKE_HTML}" = "true" ]; \
    5.42 +                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    5.43 +                       | $(COMP) $(BIN)/Sequents;\
    5.44 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    5.45 +                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Sequents;\
    5.46 +                else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/Sequents;\
    5.47 +                fi;\
    5.48 +		discgarb -c $(BIN)/Sequents;;\
    5.49 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    5.50 +                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Sequents" banner;' | $(BIN)/Pure;\
    5.51 +                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    5.52 +                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/Sequents" banner;' \
    5.53 +                       | $(BIN)/Pure;\
    5.54 +                else echo 'exit_use_dir"."; xML"$(BIN)/Sequents" banner;' \
    5.55 +                       | $(BIN)/Pure;\
    5.56 +                fi;;\
    5.57 +	*)	echo Bad value for ISABELLECOMP: \
    5.58 +                	$(COMP) is not poly or sml;;\
    5.59 +	esac
    5.60 +
    5.61 +$(BIN)/Pure:
    5.62 +	cd ../Pure;  $(MAKE)
    5.63 +
    5.64 +test:   $(BIN)/Sequents  $(EX_FILES)
    5.65 +	case "$(COMP)" in \
    5.66 +	poly*)	echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\
    5.67 +	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\
    5.68 +	*)	echo Bad value for ISABELLECOMP: \
    5.69 +                	$(COMP) is not poly or sml;;\
    5.70 +	esac
    5.71 +
    5.72 +
    5.73 +
    5.74 +
    5.75 +.PRECIOUS:  $(BIN)/Pure $(BIN)/Sequents 
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Sequents/Modal0.ML	Wed Oct 09 13:32:33 1996 +0200
     6.3 @@ -0,0 +1,30 @@
     6.4 +(*  Title:      Modal/modal0
     6.5 +    ID:         $Id$
     6.6 +    Author:     Martin Coen
     6.7 +    Copyright   1991  University of Cambridge
     6.8 +*)
     6.9 +
    6.10 +structure Modal0_rls = 
    6.11 +struct
    6.12 +
    6.13 +val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def];
    6.14 +
    6.15 +local
    6.16 +  val iffR = prove_goal thy 
    6.17 +      "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    6.18 +   (fn prems=>
    6.19 +    [ (rewtac iff_def),
    6.20 +      (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
    6.21 +
    6.22 +  val iffL = prove_goal thy 
    6.23 +     "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    6.24 +   (fn prems=>
    6.25 +    [ rewtac iff_def,
    6.26 +      (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ])
    6.27 +in
    6.28 +val safe_rls   = [basic,conjL,conjR,disjL,disjR,impL,impR,notL,notR,iffL,iffR];
    6.29 +val unsafe_rls = [allR,exL];
    6.30 +val bound_rls  = [allL,exR];
    6.31 +end
    6.32 +
    6.33 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Sequents/Modal0.thy	Wed Oct 09 13:32:33 1996 +0200
     7.3 @@ -0,0 +1,40 @@
     7.4 +(*  Title:      Modal/modal0
     7.5 +    ID:         $Id$
     7.6 +    Author:     Martin Coen
     7.7 +    Copyright   1991  University of Cambridge
     7.8 +*)
     7.9 +
    7.10 +Modal0 = LK +
    7.11 +
    7.12 +consts
    7.13 +  box           :: "o=>o"       ("[]_" [50] 50)
    7.14 +  dia           :: "o=>o"       ("<>_" [50] 50)
    7.15 +  "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
    7.16 +  "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    7.17 +  "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    7.18 +  Lstar,Rstar   :: "two_seqi"
    7.19 +
    7.20 +rules
    7.21 +  (* Definitions *)
    7.22 +
    7.23 +  strimp_def    "P --< Q == [](P --> Q)"
    7.24 +  streqv_def    "P >-< Q == (P --< Q) & (Q --< P)"
    7.25 +end
    7.26 +
    7.27 +ML
    7.28 +
    7.29 +local
    7.30 +
    7.31 +  val Lstar = "Lstar";
    7.32 +  val Rstar = "Rstar";
    7.33 +  val SLstar = "@Lstar";
    7.34 +  val SRstar = "@Rstar";
    7.35 +
    7.36 +  fun star_tr c [s1,s2] =
    7.37 +      Const(c,dummyT)$Sequents.seq_tr s1$Sequents.seq_tr s2;
    7.38 +  fun star_tr' c [s1,s2] = 
    7.39 +      Const(c,dummyT) $ Sequents.seq_tr' s1 $ Sequents.seq_tr' s2;
    7.40 +in
    7.41 +val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
    7.42 +val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
    7.43 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Sequents/README.html	Wed Oct 09 13:32:33 1996 +0200
     8.3 @@ -0,0 +1,67 @@
     8.4 +<!-- $Id$ -->
     8.5 +<HTML><HEAD><TITLE>Sequents/ReadMe</TITLE></HEAD><BODY>
     8.6 +
     8.7 +<H2>Sequents: Various Sequent Calculi</H2>
     8.8 +
     8.9 +This directory contains the Standard ML sources of the Isabelle system for
    8.10 +various Sequent, Linear, and Modal Logic.  Important files include
    8.11 +
    8.12 +<DL>
    8.13 +<DT>ROOT.ML
    8.14 +<DD>loads all source files.  Enter an ML image containing Pure
    8.15 +Isabelle and type:    use "ROOT.ML";
    8.16 +
    8.17 +<DT>Makefile
    8.18 +<DD>compiles the files under Poly/ML or SML of New Jersey
    8.19 +
    8.20 +
    8.21 +<DT>ex
    8.22 +<DD>subdirectory containing examples.  Files are arranged in
    8.23 +subdirectories. To execute all of them, enter an ML image containing
    8.24 +Sequents and type 
    8.25 +<PRE>
    8.26 +	use "ex/ROOT.ML";
    8.27 +</PRE>
    8.28 +To execute examples in a particular logic (LK/ILL/Modal) use the
    8.29 +appropriate command:
    8.30 +<PRE>
    8.31 +	use "ex/LK/ROOT.ML";
    8.32 +	use "ex/ILL/ROOT.ML";
    8.33 +	use "ex/Modal/ROOT.ML";
    8.34 +</PRE>
    8.35 +</DL>
    8.36 +
    8.37 +<P>Much of the work in Modal logic was done by Martin Coen. Thanks to
    8.38 +Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
    8.39 +reorganized the files and supplied Linear Logic. Jacob Frost provided
    8.40 +some improvements to the syntax of sequents.
    8.41 +
    8.42 +<P>Useful references on sequent calculi:
    8.43 +
    8.44 +<UL>
    8.45 +<LI>Steve Reeves and Michael Clarke,<BR>
    8.46 +    Logic for Computer Science (Addison-Wesley, 1990)
    8.47 +<LI>G. Takeuti,<BR>
    8.48 +    Proof Theory (North Holland, 1987)
    8.49 +</UL>
    8.50 +
    8.51 +Useful references on Modal Logics:
    8.52 +<UL>
    8.53 +<LI>Melvin C Fitting,<BR>
    8.54 +    Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
    8.55 +
    8.56 +<LI>Lincoln A. Wallen,<BR>
    8.57 +    Automated Deduction in Nonclassical Logics (MIT Press, 1990)
    8.58 +</UL>
    8.59 +
    8.60 +Useful references on Linear Logic:
    8.61 +<UL>
    8.62 +<LI>A. S. Troelstra<BR>
    8.63 +    Lectures on Linear Logic (CSLI, 1992)
    8.64 +
    8.65 +<LI>S. Kalvala and V. de Paiva<BR>
    8.66 +    Linear Logic in Isabelle (in TR 379, University of Cambridge
    8.67 +				Computer Lab, 1995, ed L. Paulson)
    8.68 +</UL>
    8.69 +</UL>
    8.70 +</BODY></HTML>
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Sequents/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
     9.3 @@ -0,0 +1,30 @@
     9.4 +(*  Title:      Sequents/ROOT
     9.5 +    ID:         $Id$
     9.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 +    Copyright   1991  University of Cambridge
     9.8 +
     9.9 +Adds Classical Sequent Calculus to a database containing pure Isabelle. 
    9.10 +*)
    9.11 +
    9.12 +val banner = "Sequent Calculii";
    9.13 +writeln banner;
    9.14 +
    9.15 +init_thy_reader();
    9.16 +
    9.17 +print_depth 1;  
    9.18 +
    9.19 +use_thy "Sequents";
    9.20 +use "prover.ML";
    9.21 +
    9.22 +use_thy "LK";
    9.23 +use_thy "ILL";
    9.24 +
    9.25 +use_thy "Modal0";
    9.26 +use_thy"T";
    9.27 +use_thy"S4";
    9.28 +use_thy"S43";
    9.29 +
    9.30 +use "../Pure/install_pp.ML";
    9.31 +print_depth 8;
    9.32 +
    9.33 +val Sequents_build_completed = ();    (*indicate successful build*)
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Sequents/S4.ML	Wed Oct 09 13:32:33 1996 +0200
    10.3 @@ -0,0 +1,17 @@
    10.4 +(*  Title:      Modal/S4
    10.5 +    ID:         $Id$
    10.6 +    Author:     Martin Coen
    10.7 +    Copyright   1991  University of Cambridge
    10.8 +*)
    10.9 +
   10.10 +local open Modal0_rls S4
   10.11 +in structure MP_Rule : MODAL_PROVER_RULE =
   10.12 +   struct
   10.13 +    val rewrite_rls = rewrite_rls
   10.14 +    val safe_rls    = safe_rls
   10.15 +    val unsafe_rls  = unsafe_rls @ [boxR,diaL]
   10.16 +    val bound_rls   = bound_rls @ [boxL,diaR]
   10.17 +    val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
   10.18 +   end;
   10.19 +end;
   10.20 +structure S4_Prover = Modal_ProverFun(MP_Rule);
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Sequents/S4.thy	Wed Oct 09 13:32:33 1996 +0200
    11.3 @@ -0,0 +1,31 @@
    11.4 +(*  Title:      Modal/S4
    11.5 +    ID:         $Id$
    11.6 +    Author:     Martin Coen
    11.7 +    Copyright   1991  University of Cambridge
    11.8 +*)
    11.9 +
   11.10 +S4 = Modal0 +
   11.11 +rules
   11.12 +(* Definition of the star operation using a set of Horn clauses *)
   11.13 +(* For system S4:  gamma * == {[]P | []P : gamma}               *)
   11.14 +(*                 delta * == {<>P | <>P : delta}               *)
   11.15 +
   11.16 +  lstar0         "|L>"
   11.17 +  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
   11.18 +  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
   11.19 +  rstar0         "|R>"
   11.20 +  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
   11.21 +  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
   11.22 +
   11.23 +(* Rules for [] and <> *)
   11.24 +
   11.25 +  boxR
   11.26 +   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
   11.27 +           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
   11.28 +  boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
   11.29 +
   11.30 +  diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
   11.31 +  diaL
   11.32 +   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
   11.33 +           $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
   11.34 +end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Sequents/S43.ML	Wed Oct 09 13:32:33 1996 +0200
    12.3 @@ -0,0 +1,19 @@
    12.4 +(*  Title:      Modal/S43
    12.5 +    ID:         $Id$
    12.6 +    Author:     Martin Coen
    12.7 +    Copyright   1991  University of Cambridge
    12.8 +
    12.9 +This implements Rajeev Gore's sequent calculus for S43.
   12.10 +*)
   12.11 +
   12.12 +local open Modal0_rls S43
   12.13 +in structure MP_Rule : MODAL_PROVER_RULE =
   12.14 +   struct
   12.15 +    val rewrite_rls = rewrite_rls
   12.16 +    val safe_rls    = safe_rls
   12.17 +    val unsafe_rls  = unsafe_rls @ [pi1,pi2]
   12.18 +    val bound_rls   = bound_rls @ [boxL,diaR]
   12.19 +    val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2]
   12.20 +   end;
   12.21 +end;
   12.22 +structure S43_Prover = Modal_ProverFun(MP_Rule);  
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Sequents/S43.thy	Wed Oct 09 13:32:33 1996 +0200
    13.3 @@ -0,0 +1,78 @@
    13.4 +(*  Title:      Modal/S43
    13.5 +    ID:         $Id$
    13.6 +    Author:     Martin Coen
    13.7 +    Copyright   1991  University of Cambridge
    13.8 +
    13.9 +This implements Rajeev Gore's sequent calculus for S43.
   13.10 +*)
   13.11 +
   13.12 +S43 = Modal0 +
   13.13 +
   13.14 +consts
   13.15 +  S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
   13.16 +             seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
   13.17 +  "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
   13.18 +                         ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
   13.19 +
   13.20 +rules
   13.21 +(* Definition of the star operation using a set of Horn clauses  *)
   13.22 +(* For system S43: gamma * == {[]P | []P : gamma}                *)
   13.23 +(*                 delta * == {<>P | <>P : delta}                *)
   13.24 +
   13.25 +  lstar0         "|L>"
   13.26 +  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
   13.27 +  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
   13.28 +  rstar0         "|R>"
   13.29 +  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
   13.30 +  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
   13.31 +
   13.32 +(* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
   13.33 +(* ie                                                                        *)
   13.34 +(*           S1...Sk,Sk+1...Sk+m                                             *)
   13.35 +(*     ----------------------------------                                    *)
   13.36 +(*     <>P1...<>Pk, $G |- $H, []Q1...[]Qm                                    *)
   13.37 +(*                                                                           *)
   13.38 +(*  where Si == <>P1...<>Pi-1,<>Pi+1,..<>Pk,Pi, $G * |- $H *, []Q1...[]Qm    *)
   13.39 +(*    and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
   13.40 +(*    and 1<=i<=k and k<j<=k+m                                               *)
   13.41 +
   13.42 +  S43pi0         "S43pi $L;; $R;; $Lbox; $Rdia"
   13.43 +  S43pi1
   13.44 +   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==> 
   13.45 +       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
   13.46 +  S43pi2
   13.47 +   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==> 
   13.48 +       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
   13.49 +
   13.50 +(* Rules for [] and <> for S43 *)
   13.51 +
   13.52 +  boxL           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
   13.53 +  diaR           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
   13.54 +  pi1
   13.55 +   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;  
   13.56 +      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
   13.57 +   $L1, <>P, $L2 |- $R"
   13.58 +  pi2
   13.59 +   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;  
   13.60 +      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
   13.61 +   $L |- $R1, []P, $R2"
   13.62 +end
   13.63 +
   13.64 +ML
   13.65 +
   13.66 +local
   13.67 +
   13.68 +  val S43pi  = "S43pi";
   13.69 +  val SS43pi = "@S43pi";
   13.70 +
   13.71 +  val tr  = Sequents.seq_tr;
   13.72 +  val tr' = Sequents.seq_tr';
   13.73 +
   13.74 +  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
   13.75 +        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
   13.76 +  fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
   13.77 +        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
   13.78 +in
   13.79 +val parse_translation = [(SS43pi,s43pi_tr)];
   13.80 +val print_translation = [(S43pi,s43pi_tr')]
   13.81 +end
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Sequents/Sequents.thy	Wed Oct 09 13:32:33 1996 +0200
    14.3 @@ -0,0 +1,147 @@
    14.4 +(*  Title: 	LK/lk.thy
    14.5 +    ID:         $Id$
    14.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7 +    Copyright   1993  University of Cambridge
    14.8 +
    14.9 +Classical First-Order Sequent Calculus
   14.10 +*)
   14.11 +
   14.12 +Sequents = Pure +
   14.13 +
   14.14 +types
   14.15 +  o 
   14.16 +
   14.17 +arities
   14.18 +  o :: logic
   14.19 +
   14.20 +
   14.21 +(* Sequences *)
   14.22 +
   14.23 +types
   14.24 + seq'
   14.25 +
   14.26 +consts
   14.27 + SeqO'         :: "[o,seq']=>seq'"
   14.28 + Seq1'         :: "o=>seq'"
   14.29 +    
   14.30 +
   14.31 +(* concrete syntax *)
   14.32 +
   14.33 +types
   14.34 +  seq seqobj seqcont
   14.35 +
   14.36 +
   14.37 +syntax
   14.38 + SeqEmp         :: "seq"                                ("")
   14.39 + SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
   14.40 +
   14.41 + SeqContEmp     :: "seqcont"                            ("")
   14.42 + SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
   14.43 +  
   14.44 + SeqO           :: "o => seqobj"                        ("_")
   14.45 + SeqId          :: "id => seqobj"                       ("$_")
   14.46 + SeqVar         :: "var => seqobj"                      ("$_")
   14.47 +
   14.48 +types
   14.49 +    
   14.50 + single_seqe = "[seq,seqobj] => prop"
   14.51 + single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
   14.52 + two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
   14.53 + two_seqe = "[seq, seq] => prop"
   14.54 + three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
   14.55 + three_seqe = "[seq, seq, seq] => prop"
   14.56 + four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
   14.57 + four_seqe = "[seq, seq, seq, seq] => prop"
   14.58 +
   14.59 +end
   14.60 +
   14.61 +ML
   14.62 +
   14.63 +(* parse translation for sequences *)
   14.64 +
   14.65 +fun abs_seq' t = Abs("s", Type("seq'",[]), t);
   14.66 +
   14.67 +fun seqobj_tr(Const("SeqO",_)$f) = Const("SeqO'",dummyT)$f |
   14.68 +    seqobj_tr(_$i) = i;
   14.69 +    
   14.70 +fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
   14.71 +    seqcont_tr(Const("SeqContApp",_)$so$sc) = 
   14.72 +      (seqobj_tr so)$(seqcont_tr sc);
   14.73 +
   14.74 +fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
   14.75 +    seq_tr(Const("SeqApp",_)$so$sc) = 
   14.76 +      abs_seq'(seqobj_tr(so)$seqcont_tr(sc));
   14.77 +
   14.78 +
   14.79 +fun singlobj_tr(Const("SeqO",_)$f) =
   14.80 +    abs_seq' ((Const("SeqO'",dummyT)$f)$Bound 0);
   14.81 +    
   14.82 +
   14.83 +    
   14.84 +(* print translation for sequences *)
   14.85 +
   14.86 +fun seqcont_tr' (Bound 0) = 
   14.87 +      Const("SeqContEmp",dummyT) |
   14.88 +    seqcont_tr' (Const("SeqO'",_)$f$s) =
   14.89 +      Const("SeqContApp",dummyT)$
   14.90 +      (Const("SeqO",dummyT)$f)$
   14.91 +      (seqcont_tr' s) |
   14.92 +(*    seqcont_tr' ((a as Abs(_,_,_))$s)= 
   14.93 +      seqcont_tr'(betapply(a,s)) | *)
   14.94 +    seqcont_tr' (i$s) = 
   14.95 +      Const("SeqContApp",dummyT)$
   14.96 +      (Const("SeqId",dummyT)$i)$
   14.97 +      (seqcont_tr' s);
   14.98 +
   14.99 +fun seq_tr' s =
  14.100 +    let fun seq_itr' (Bound 0) = 
  14.101 +              Const("SeqEmp",dummyT) |
  14.102 +            seq_itr' (Const("SeqO'",_)$f$s) =
  14.103 +              Const("SeqApp",dummyT)$
  14.104 +              (Const("SeqO",dummyT)$f)$(seqcont_tr' s) |
  14.105 +(*            seq_itr' ((a as Abs(_,_,_))$s) =
  14.106 +              seq_itr'(betapply(a,s)) |    *)
  14.107 +            seq_itr' (i$s) =
  14.108 +              Const("SeqApp",dummyT)$
  14.109 +              (Const("SeqId",dummyT)$i)$
  14.110 +              (seqcont_tr' s)
  14.111 +    in case s of 
  14.112 +         Abs(_,_,t) => seq_itr' t |
  14.113 +         _ => s$(Bound 0)
  14.114 +    end;
  14.115 +
  14.116 +
  14.117 +
  14.118 +
  14.119 +fun single_tr c [s1,s2] =
  14.120 +    Const(c,dummyT)$seq_tr s1$singlobj_tr s2;
  14.121 +
  14.122 +fun two_seq_tr c [s1,s2] =
  14.123 +    Const(c,dummyT)$seq_tr s1$seq_tr s2;
  14.124 +
  14.125 +fun three_seq_tr c [s1,s2,s3] =
  14.126 +    Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3;
  14.127 +
  14.128 +fun four_seq_tr c [s1,s2,s3,s4] =
  14.129 +    Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3$seq_tr s4;
  14.130 +
  14.131 +
  14.132 +fun singlobj_tr'(Const("SeqO'",_)$fm) = fm |
  14.133 +    singlobj_tr'(id) = Const("@SeqId",dummyT)$id;
  14.134 +
  14.135 +
  14.136 +fun single_tr' c [s1, s2] =
  14.137 +(Const (c, dummyT)$seq_tr' s1$seq_tr' s2 ); 
  14.138 +
  14.139 +
  14.140 +fun two_seq_tr' c [s1, s2] =
  14.141 +  Const (c, dummyT)$seq_tr' s1$seq_tr' s2; 
  14.142 +
  14.143 +fun three_seq_tr' c [s1, s2, s3] =
  14.144 +  Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3; 
  14.145 +
  14.146 +fun four_seq_tr' c [s1, s2, s3, s4] =
  14.147 +  Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3$seq_tr' s4; 
  14.148 +
  14.149 +
  14.150 +			 
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/Sequents/T.ML	Wed Oct 09 13:32:33 1996 +0200
    15.3 @@ -0,0 +1,17 @@
    15.4 +(*  Title:      Modal/T
    15.5 +    ID:         $Id$
    15.6 +    Author:     Martin Coen
    15.7 +    Copyright   1991  University of Cambridge
    15.8 +*)
    15.9 +
   15.10 +local open Modal0_rls T
   15.11 +in structure MP_Rule : MODAL_PROVER_RULE =
   15.12 +   struct
   15.13 +    val rewrite_rls = rewrite_rls
   15.14 +    val safe_rls    = safe_rls
   15.15 +    val unsafe_rls  = unsafe_rls @ [boxR,diaL]
   15.16 +    val bound_rls   = bound_rls @ [boxL,diaR]
   15.17 +    val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
   15.18 +   end
   15.19 +end;
   15.20 +structure T_Prover = Modal_ProverFun(MP_Rule);  
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Sequents/T.thy	Wed Oct 09 13:32:33 1996 +0200
    16.3 @@ -0,0 +1,30 @@
    16.4 +(*  Title:      Modal/T
    16.5 +    ID:         $Id$
    16.6 +    Author:     Martin Coen
    16.7 +    Copyright   1991  University of Cambridge
    16.8 +*)
    16.9 +
   16.10 +T = Modal0 +
   16.11 +rules
   16.12 +(* Definition of the star operation using a set of Horn clauses *)
   16.13 +(* For system T:  gamma * == {P | []P : gamma}                  *)
   16.14 +(*                delta * == {P | <>P : delta}                  *)
   16.15 +
   16.16 +  lstar0         "|L>"
   16.17 +  lstar1         "$G |L> $H ==> []P, $G |L> P, $H"
   16.18 +  lstar2         "$G |L> $H ==>   P, $G |L>    $H"
   16.19 +  rstar0         "|R>"
   16.20 +  rstar1         "$G |R> $H ==> <>P, $G |R> P, $H"
   16.21 +  rstar2         "$G |R> $H ==>   P, $G |R>    $H"
   16.22 +
   16.23 +(* Rules for [] and <> *)
   16.24 +
   16.25 +  boxR
   16.26 +   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
   16.27 +               $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
   16.28 +  boxL     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
   16.29 +  diaR     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
   16.30 +  diaL
   16.31 +   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
   16.32 +               $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
   16.33 +end
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Sequents/ex/ILL/ILL_kleene_lemmas.ML	Wed Oct 09 13:32:33 1996 +0200
    17.3 @@ -0,0 +1,81 @@
    17.4 +
    17.5 +(* from [kleene 52] pp 118,119 *)
    17.6 +
    17.7 +
    17.8 +val k49a = auto1 "|- [* A > ( - ( - A)) *]";
    17.9 +
   17.10 +val k49b = auto1 "|- [*( - ( - ( - A))) = ( - A)*]";
   17.11 +
   17.12 +val k49c = auto1 "|- [* (A | - A) > ( - - A = A) *]";
   17.13 +
   17.14 +val k50a = auto2 "|- [* - (A = - A) *]";
   17.15 +
   17.16 +(*
   17.17 +         [rtac impr_contract 1 THEN REPEAT (rtac conj_lemma 1),
   17.18 +	  res_inst_tac [("A","!((! A) -o 0)")] cut 1
   17.19 +	  THEN rtac context1 1
   17.20 +	  THEN ALLGOALS (best_tac power_cs)]);
   17.21 +*)
   17.22 +
   17.23 +val k51a = auto2 "|- [* - - (A | - A) *]";
   17.24 +    
   17.25 +val k51b = auto2 "|- [* - - (- - A > A) *]";
   17.26 +    
   17.27 +val k56a = auto1 "|- [* (A | B) > - (- A & - B) *]";
   17.28 +
   17.29 +val k56b = auto1 "|- [* (-A | B) > - (A & -B) *]";
   17.30 +    
   17.31 +val k57a = auto1 "|- [* (A & B) > - (-A | -B) *]";
   17.32 +    
   17.33 +val k57b = auto2 "|- [* (A & -B) > -(-A | B) *]";
   17.34 +    
   17.35 +val k58a = auto1 "|- [* (A > B) > - (A & -B) *]";
   17.36 +    
   17.37 +val k58b = auto1 "|- [* (A > -B) = -(A & B) *]";
   17.38 +    
   17.39 +val k58c = auto1 "|- [* - (A & B) = (- - A > - B) *]";
   17.40 +    
   17.41 +val k58d = auto1 "|- [* (- - A > - B) = - - (-A | -B) *]";
   17.42 +    
   17.43 +val k58e = auto1 "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]";
   17.44 +    
   17.45 +val k58f = auto1 "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]";
   17.46 +    
   17.47 +val k58g = auto1 "|- [* (- -A > B) > - (A & -B) *]";
   17.48 +    
   17.49 +val k59a = auto1 "|- [* (-A | B) > (A > B) *]";
   17.50 +
   17.51 +val k59b = auto2 "|- [* (A > B) > - - (-A | B) *]";
   17.52 +    
   17.53 +val k59c = auto2 "|- [* (-A > B) > - -(A | B) *]";
   17.54 +    
   17.55 +val k60a = auto1 "|- [* (A & B) > - (A > -B) *]";
   17.56 +    
   17.57 +val k60b = auto1 "|- [* (A & -B) > - (A > B) *]";
   17.58 +    
   17.59 +val k60c = auto1 "|- [* ( - - A & B) > - (A > -B) *]";
   17.60 +    
   17.61 +val k60d = auto1 "|- [* (- - A & - B) = - (A > B) *]";
   17.62 +    
   17.63 +val k60e = auto1 "|- [* - (A > B) = - (-A | B) *]";
   17.64 +    
   17.65 +val k60f = auto1 "|- [* - (-A | B) = - - (A & -B) *]";
   17.66 +    
   17.67 +val k60g = auto2 "|- [* - - (A > B) = - (A & -B) *]";
   17.68 +    
   17.69 +(*
   17.70 + [step_tac safe_cs 1, best_tac safe_cs 1,
   17.71 + rtac impr 1 THEN rtac impr_contract 1
   17.72 + THEN best_tac safe_cs 1];
   17.73 +*)
   17.74 +
   17.75 +val k60h = auto1 "|- [* - (A & -B) = (A > - -B) *]";
   17.76 +
   17.77 +val k60i = auto1 "|- [* (A > - -B) = (- -A > - -B) *]";
   17.78 +
   17.79 +val k61a = auto1 "|- [* (A | B) > (-A > B) *]";
   17.80 +
   17.81 +val k61b = auto2 "|- [* - (A | B) = - (-A > B) *]";
   17.82 +
   17.83 +val k62a = auto1 "|- [* (-A | -B) > - (A & B) *]";
   17.84 +
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/Sequents/ex/ILL/ILL_predlog.ML	Wed Oct 09 13:32:33 1996 +0200
    18.3 @@ -0,0 +1,9 @@
    18.4 +
    18.5 +open ILL_predlog;
    18.6 +
    18.7 +
    18.8 +fun auto1 x = prove_goal thy x
    18.9 + (fn prems => [best_tac safe_cs 1]) ;
   18.10 +
   18.11 +fun auto2 x = prove_goal thy x
   18.12 + (fn prems => [best_tac power_cs 1]) ;
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/Sequents/ex/ILL/ILL_predlog.thy	Wed Oct 09 13:32:33 1996 +0200
    19.3 @@ -0,0 +1,42 @@
    19.4 +(* 
    19.5 +    File:	 /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy
    19.6 +    Theory Name: pred_log
    19.7 +    Logic Image: HOL
    19.8 +*)
    19.9 +
   19.10 +ILL_predlog  =  ILL +
   19.11 +
   19.12 +types
   19.13 +
   19.14 +    plf
   19.15 +    
   19.16 +arities
   19.17 +
   19.18 +    plf :: logic
   19.19 +    
   19.20 +consts
   19.21 +
   19.22 +  "&"   :: "[plf,plf] => plf"   (infixr 35)
   19.23 +  "|"   :: "[plf,plf] => plf"   (infixr 35)
   19.24 +  ">"   :: "[plf,plf] => plf"   (infixr 35)
   19.25 +  "="   :: "[plf,plf] => plf"   (infixr 35)
   19.26 +  "@NG" :: "plf => plf"   ("- _ " [50] 55)
   19.27 +  ff    :: "plf"
   19.28 +  
   19.29 +  PL    :: "plf => o"      ("[* / _ / *]" [] 100)
   19.30 +
   19.31 +
   19.32 +translations
   19.33 +
   19.34 +  "[* A & B *]" == "[*A*] && [*B*]" 
   19.35 +  "[* A | B *]" == "![*A*] ++ ![*B*]"
   19.36 +  "[* - A *]"   == "[*A > ff*]"
   19.37 +  "[* ff *]"    == "0"
   19.38 +  "[* A = B *]" => "[* (A > B) & (B > A) *]"
   19.39 +  
   19.40 +  "[* A > B *]" == "![*A*] -o [*B*]"
   19.41 +  
   19.42 +(* another translations for linear implication:
   19.43 +  "[* A > B *]" == "!([*A*] -o [*B*])" *)
   19.44 +
   19.45 +end
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/Sequents/ex/ILL/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
    20.3 @@ -0,0 +1,12 @@
    20.4 +
    20.5 +Sequents_build_completed;    (*Cause examples to fail if LK did*)
    20.6 +
    20.7 +writeln"Root file for ILL examples";
    20.8 +
    20.9 +proof_timing := true;
   20.10 +time_use_thy "ex/ILL/washing";
   20.11 +
   20.12 +time_use_thy "ex/ILL/ILL_predlog";
   20.13 +time_use "ex/ILL/ILL_kleene_lemmas.ML";
   20.14 +
   20.15 +maketest"END: Root file for ILL examples";
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/Sequents/ex/ILL/washing.ML	Wed Oct 09 13:32:33 1996 +0200
    21.3 @@ -0,0 +1,33 @@
    21.4 +
    21.5 +open washing;
    21.6 +
    21.7 +(* "activate" definitions for use in proof *)
    21.8 +
    21.9 +val changeI = [context1] RL ([change] RLN (2,[cut]));
   21.10 +val load1I =  [context1] RL ([load1]  RLN (2,[cut]));
   21.11 +val washI =   [context1] RL ([wash]   RLN (2,[cut]));
   21.12 +val dryI =    [context1] RL ([dry]    RLN (2,[cut]));
   21.13 +
   21.14 +
   21.15 +
   21.16 +(* a load of dirty clothes and two dollars gives you clean clothes *)
   21.17 +
   21.18 +goal thy "dollar , dollar , dirty |- clean";
   21.19 +
   21.20 +by (best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1);
   21.21 +
   21.22 +
   21.23 +(* order of premises doesn't matter *)
   21.24 +
   21.25 +prove_goal thy "dollar , dirty , dollar |- clean"
   21.26 +(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
   21.27 +
   21.28 +
   21.29 +(* alternative formulation *)
   21.30 +
   21.31 +prove_goal thy "dollar , dollar |- dirty -o clean"
   21.32 +(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
   21.33 +
   21.34 +
   21.35 +
   21.36 +
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/Sequents/ex/ILL/washing.thy	Wed Oct 09 13:32:33 1996 +0200
    22.3 @@ -0,0 +1,33 @@
    22.4 +
    22.5 +
    22.6 +(* code by Sara Kalvala, based on Paulson's LK 
    22.7 +                           and Moore's tisl.ML *)
    22.8 +
    22.9 +washing = ILL +
   22.10 +
   22.11 +consts
   22.12 +
   22.13 +dollar,quarter,loaded,dirty,wet,clean        :: "o"			
   22.14 +
   22.15 +  
   22.16 +rules
   22.17 +
   22.18 +
   22.19 +  change
   22.20 +  "dollar |- (quarter >< quarter >< quarter >< quarter)"
   22.21 +
   22.22 +  load1
   22.23 +  "quarter , quarter , quarter , quarter , quarter |- loaded"
   22.24 +
   22.25 +  load2
   22.26 +  "dollar , quarter |- loaded"
   22.27 +
   22.28 +  wash
   22.29 +  "loaded , dirty |- wet"
   22.30 +
   22.31 +  dry
   22.32 +  "wet, quarter , quarter , quarter |- clean"
   22.33 +
   22.34 +end
   22.35 +
   22.36 +  
   22.37 \ No newline at end of file
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/Sequents/ex/LK/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
    23.3 @@ -0,0 +1,18 @@
    23.4 +(*  Title:      LK/ex/ROOT
    23.5 +    ID:         $Id$
    23.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.7 +    Copyright   1992  University of Cambridge
    23.8 +
    23.9 +Executes all examples for Classical Logic. 
   23.10 +*)
   23.11 +
   23.12 +Sequents_build_completed;    (*Cause examples to fail if LK did*)
   23.13 +
   23.14 +writeln"Root file for LK examples";
   23.15 +
   23.16 +proof_timing := true;
   23.17 +time_use "ex/LK/prop.ML";
   23.18 +time_use "ex/LK/quant.ML";
   23.19 +time_use "ex/LK/hardquant.ML";
   23.20 +
   23.21 +maketest"END: Root file for LK examples";
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/Sequents/ex/LK/hardquant.ML	Wed Oct 09 13:32:33 1996 +0200
    24.3 @@ -0,0 +1,278 @@
    24.4 +(*  Title:      LK/ex/hard-quant
    24.5 +    ID:         $Id$
    24.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    24.7 +    Copyright   1992  University of Cambridge
    24.8 +
    24.9 +Hard examples with quantifiers.  Can be read to test the LK system.
   24.10 +From  F. J. Pelletier,
   24.11 +  Seventy-Five Problems for Testing Automatic Theorem Provers,
   24.12 +  J. Automated Reasoning 2 (1986), 191-216.
   24.13 +  Errata, JAR 4 (1988), 236-236.
   24.14 +
   24.15 +Uses pc_tac rather than fast_tac when the former is significantly faster.
   24.16 +*)
   24.17 +
   24.18 +writeln"File LK/ex/hard-quant.";
   24.19 +
   24.20 +goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
   24.21 +by (fast_tac LK_pack 1);
   24.22 +result(); 
   24.23 +
   24.24 +goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
   24.25 +by (fast_tac LK_pack 1);
   24.26 +result(); 
   24.27 +
   24.28 +goal LK.thy "|- (EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
   24.29 +by (fast_tac LK_pack 1);
   24.30 +result(); 
   24.31 +
   24.32 +goal LK.thy "|- (ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
   24.33 +by (fast_tac LK_pack 1);
   24.34 +result(); 
   24.35 +
   24.36 +writeln"Problems requiring quantifier duplication";
   24.37 +
   24.38 +(*Not provable by fast_tac LK_pack: needs multiple instantiation of ALL*)
   24.39 +goal LK.thy "|- (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
   24.40 +by (best_tac LK_dup_pack 1);
   24.41 +result();
   24.42 +
   24.43 +(*Needs double instantiation of the quantifier*)
   24.44 +goal LK.thy "|- EX x. P(x) --> P(a) & P(b)";
   24.45 +by (fast_tac LK_dup_pack 1);
   24.46 +result();
   24.47 +
   24.48 +goal LK.thy "|- EX z. P(z) --> (ALL x. P(x))";
   24.49 +by (best_tac LK_dup_pack 1);
   24.50 +result();
   24.51 +
   24.52 +writeln"Hard examples with quantifiers";
   24.53 +
   24.54 +writeln"Problem 18";
   24.55 +goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
   24.56 +by (best_tac LK_dup_pack 1);
   24.57 +result(); 
   24.58 +
   24.59 +writeln"Problem 19";
   24.60 +goal LK.thy "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
   24.61 +by (best_tac LK_dup_pack 1);
   24.62 +result();
   24.63 +
   24.64 +writeln"Problem 20";
   24.65 +goal LK.thy "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
   24.66 +\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
   24.67 +by (fast_tac LK_pack 1); 
   24.68 +result();
   24.69 +
   24.70 +writeln"Problem 21";
   24.71 +goal LK.thy "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
   24.72 +by (best_tac LK_dup_pack 1);
   24.73 +result();
   24.74 +
   24.75 +writeln"Problem 22";
   24.76 +goal LK.thy "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
   24.77 +by (fast_tac LK_pack 1); 
   24.78 +result();
   24.79 +
   24.80 +writeln"Problem 23";
   24.81 +goal LK.thy "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
   24.82 +by (best_tac LK_pack 1);  
   24.83 +result();
   24.84 +
   24.85 +writeln"Problem 24";
   24.86 +goal LK.thy "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
   24.87 +\    ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
   24.88 +\   --> (EX x. P(x)&R(x))";
   24.89 +by (pc_tac LK_pack 1);
   24.90 +result();
   24.91 +
   24.92 +writeln"Problem 25";
   24.93 +goal LK.thy "|- (EX x. P(x)) &  \
   24.94 +\       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
   24.95 +\       (ALL x. P(x) --> (M(x) & L(x))) &   \
   24.96 +\       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
   24.97 +\   --> (EX x. Q(x)&P(x))";
   24.98 +by (best_tac LK_pack 1);  
   24.99 +result();
  24.100 +
  24.101 +writeln"Problem 26";
  24.102 +goal LK.thy "|- ((EX x. p(x)) <-> (EX x. q(x))) &       \
  24.103 +\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
  24.104 +\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
  24.105 +by (pc_tac LK_pack 1);
  24.106 +result();
  24.107 +
  24.108 +writeln"Problem 27";
  24.109 +goal LK.thy "|- (EX x. P(x) & ~Q(x)) &   \
  24.110 +\             (ALL x. P(x) --> R(x)) &   \
  24.111 +\             (ALL x. M(x) & L(x) --> P(x)) &   \
  24.112 +\             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
  24.113 +\         --> (ALL x. M(x) --> ~L(x))";
  24.114 +by (pc_tac LK_pack 1); 
  24.115 +result();
  24.116 +
  24.117 +writeln"Problem 28.  AMENDED";
  24.118 +goal LK.thy "|- (ALL x. P(x) --> (ALL x. Q(x))) &   \
  24.119 +\       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
  24.120 +\       ((EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
  24.121 +\   --> (ALL x. P(x) & L(x) --> M(x))";
  24.122 +by (pc_tac LK_pack 1);  
  24.123 +result();
  24.124 +
  24.125 +writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
  24.126 +goal LK.thy "|- (EX x. P(x)) & (EX y. Q(y))  \
  24.127 +\   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
  24.128 +\        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
  24.129 +by (pc_tac LK_pack 1); 
  24.130 +result();
  24.131 +
  24.132 +writeln"Problem 30";
  24.133 +goal LK.thy "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
  24.134 +\       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
  24.135 +\   --> (ALL x. S(x))";
  24.136 +by (fast_tac LK_pack 1);  
  24.137 +result();
  24.138 +
  24.139 +writeln"Problem 31";
  24.140 +goal LK.thy "|- ~(EX x.P(x) & (Q(x) | R(x))) & \
  24.141 +\       (EX x. L(x) & P(x)) & \
  24.142 +\       (ALL x. ~ R(x) --> M(x))  \
  24.143 +\   --> (EX x. L(x) & M(x))";
  24.144 +by (fast_tac LK_pack 1);
  24.145 +result();
  24.146 +
  24.147 +writeln"Problem 32";
  24.148 +goal LK.thy "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
  24.149 +\       (ALL x. S(x) & R(x) --> L(x)) & \
  24.150 +\       (ALL x. M(x) --> R(x))  \
  24.151 +\   --> (ALL x. P(x) & M(x) --> L(x))";
  24.152 +by (best_tac LK_pack 1);
  24.153 +result();
  24.154 +
  24.155 +writeln"Problem 33";
  24.156 +goal LK.thy "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
  24.157 +\    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
  24.158 +by (fast_tac LK_pack 1);
  24.159 +result();
  24.160 +
  24.161 +writeln"Problem 34  AMENDED (TWICE!!)  NOT PROVED AUTOMATICALLY";
  24.162 +(*Andrews's challenge*)
  24.163 +goal LK.thy "|- ((EX x. ALL y. p(x) <-> p(y))  <->              \
  24.164 +\              ((EX x. q(x)) <-> (ALL y. p(y))))     <->        \
  24.165 +\             ((EX x. ALL y. q(x) <-> q(y))  <->                \
  24.166 +\              ((EX x. p(x)) <-> (ALL y. q(y))))";
  24.167 +by (safe_goal_tac LK_pack 1);   (*53 secs*) (*13 secs*)
  24.168 +by (TRYALL (fast_tac LK_pack)); (*165 secs*)  (*117 secs*)  (*138 secs*)
  24.169 +(*for some reason, pc_tac leaves 14 subgoals instead of 6*)
  24.170 +by (TRYALL (best_tac LK_dup_pack)); (*55 secs*) (*29 secs*) (*54 secs*)
  24.171 +result();
  24.172 +
  24.173 +
  24.174 +writeln"Problem 35";
  24.175 +goal LK.thy "|- EX x y. P(x,y) -->  (ALL u v. P(u,v))";
  24.176 +by (best_tac LK_dup_pack 1);  (*27 secs??*)
  24.177 +result();
  24.178 +
  24.179 +writeln"Problem 36";
  24.180 +goal LK.thy "|- (ALL x. EX y. J(x,y)) & \
  24.181 +\       (ALL x. EX y. G(x,y)) & \
  24.182 +\       (ALL x y. J(x,y) | G(x,y) -->   \
  24.183 +\       (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
  24.184 +\   --> (ALL x. EX y. H(x,y))";
  24.185 +by (fast_tac LK_pack 1);
  24.186 +result();
  24.187 +
  24.188 +writeln"Problem 37";
  24.189 +goal LK.thy "|- (ALL z. EX w. ALL x. EX y. \
  24.190 +\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
  24.191 +\       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
  24.192 +\       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
  24.193 +\   --> (ALL x. EX y. R(x,y))";
  24.194 +by (pc_tac LK_pack 1);
  24.195 +result();
  24.196 +
  24.197 +writeln"Problem 38";
  24.198 +goal LK.thy
  24.199 + "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
  24.200 +\            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
  24.201 +\    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
  24.202 +\            (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
  24.203 +\             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
  24.204 +by (pc_tac LK_pack 1);
  24.205 +result();
  24.206 +
  24.207 +writeln"Problem 39";
  24.208 +goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
  24.209 +by (fast_tac LK_pack 1);
  24.210 +result();
  24.211 +
  24.212 +writeln"Problem 40.  AMENDED";
  24.213 +goal LK.thy "|- (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
  24.214 +\                    ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
  24.215 +by (fast_tac LK_pack 1);
  24.216 +result();
  24.217 +
  24.218 +writeln"Problem 41";
  24.219 +goal LK.thy "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))      \
  24.220 +\         --> ~ (EX z. ALL x. f(x,z))";
  24.221 +by (fast_tac LK_pack 1);
  24.222 +result();
  24.223 +
  24.224 +writeln"Problem 42";
  24.225 +goal LK.thy "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))";
  24.226 +
  24.227 +writeln"Problem 43  NOT PROVED AUTOMATICALLY";
  24.228 +goal LK.thy "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \
  24.229 +\         --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))";
  24.230 +
  24.231 +writeln"Problem 44";
  24.232 +goal LK.thy "|- (ALL x. f(x) -->                                        \
  24.233 +\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
  24.234 +\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
  24.235 +\             --> (EX x. j(x) & ~f(x))";
  24.236 +by (fast_tac LK_pack 1);
  24.237 +result();
  24.238 +
  24.239 +writeln"Problem 45";
  24.240 +goal LK.thy "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))        \
  24.241 +\                     --> (ALL y. g(y) & h(x,y) --> k(y))) &    \
  24.242 +\     ~ (EX y. l(y) & k(y)) &                                   \
  24.243 +\     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
  24.244 +\                  & (ALL y. g(y) & h(x,y) --> j(x,y)))         \
  24.245 +\     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
  24.246 +by (best_tac LK_pack 1); 
  24.247 +result();
  24.248 +
  24.249 +
  24.250 +writeln"Problem 50";  
  24.251 +goal LK.thy
  24.252 +    "|- (ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
  24.253 +by (best_tac LK_dup_pack 1);
  24.254 +result();
  24.255 +
  24.256 +writeln"Problem 57";
  24.257 +goal LK.thy
  24.258 +    "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
  24.259 +\    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
  24.260 +by (fast_tac LK_pack 1);
  24.261 +result();
  24.262 +
  24.263 +writeln"Problem 59";
  24.264 +(*Unification works poorly here -- the abstraction %sobj prevents efficient
  24.265 +  operation of the occurs check*)
  24.266 +Unify.trace_bound := !Unify.search_bound - 1; 
  24.267 +goal LK.thy "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
  24.268 +by (best_tac LK_dup_pack 1);
  24.269 +result();
  24.270 +
  24.271 +writeln"Problem 60";
  24.272 +goal LK.thy
  24.273 +    "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
  24.274 +by (fast_tac LK_pack 1);
  24.275 +result();
  24.276 +
  24.277 +writeln"Reached end of file.";
  24.278 +
  24.279 +(*18 June 92: loaded in 372 secs*)
  24.280 +(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
  24.281 +(*29 June 92: loaded in 370 secs*)
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/src/Sequents/ex/LK/prop.ML	Wed Oct 09 13:32:33 1996 +0200
    25.3 @@ -0,0 +1,194 @@
    25.4 +(*  Title:      LK/ex/prop
    25.5 +    ID:         $Id$
    25.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.7 +    Copyright   1992  University of Cambridge
    25.8 +
    25.9 +Classical sequent calculus: examples with propositional connectives
   25.10 +Can be read to test the LK system.
   25.11 +*)
   25.12 +
   25.13 +writeln"LK/ex/prop: propositional examples";
   25.14 +
   25.15 +writeln"absorptive laws of & and | ";
   25.16 +
   25.17 +goal LK.thy "|- P & P <-> P";
   25.18 +by (fast_tac prop_pack 1);
   25.19 +result();
   25.20 +
   25.21 +goal LK.thy "|- P | P <-> P";
   25.22 +by (fast_tac prop_pack 1);
   25.23 +result();
   25.24 +
   25.25 +writeln"commutative laws of & and | ";
   25.26 +
   25.27 +goal LK.thy "|- P & Q  <->  Q & P";
   25.28 +by (fast_tac prop_pack 1);
   25.29 +result();
   25.30 +
   25.31 +goal LK.thy "|- P | Q  <->  Q | P";
   25.32 +by (fast_tac prop_pack 1);
   25.33 +result();
   25.34 +
   25.35 +
   25.36 +writeln"associative laws of & and | ";
   25.37 +
   25.38 +goal LK.thy "|- (P & Q) & R  <->  P & (Q & R)";
   25.39 +by (fast_tac prop_pack 1);
   25.40 +result();
   25.41 +
   25.42 +goal LK.thy "|- (P | Q) | R  <->  P | (Q | R)";
   25.43 +by (fast_tac prop_pack 1);
   25.44 +result();
   25.45 +
   25.46 +writeln"distributive laws of & and | ";
   25.47 +goal LK.thy "|- (P & Q) | R  <-> (P | R) & (Q | R)";
   25.48 +by (fast_tac prop_pack 1);
   25.49 +result();
   25.50 +
   25.51 +goal LK.thy "|- (P | Q) & R  <-> (P & R) | (Q & R)";
   25.52 +by (fast_tac prop_pack 1);
   25.53 +result();
   25.54 +
   25.55 +writeln"Laws involving implication";
   25.56 +
   25.57 +goal LK.thy "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
   25.58 +by (fast_tac prop_pack 1);
   25.59 +result(); 
   25.60 +
   25.61 +goal LK.thy "|- (P & Q --> R) <-> (P--> (Q-->R))";
   25.62 +by (fast_tac prop_pack 1);
   25.63 +result(); 
   25.64 +
   25.65 +
   25.66 +goal LK.thy "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
   25.67 +by (fast_tac prop_pack 1);
   25.68 +result();
   25.69 +
   25.70 +
   25.71 +writeln"Classical theorems";
   25.72 +
   25.73 +goal LK.thy "|- P|Q --> P| ~P&Q";
   25.74 +by (fast_tac prop_pack 1);
   25.75 +result();
   25.76 +
   25.77 +
   25.78 +goal LK.thy "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
   25.79 +by (fast_tac prop_pack 1);
   25.80 +result();
   25.81 +
   25.82 +
   25.83 +goal LK.thy "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
   25.84 +by (fast_tac prop_pack 1);
   25.85 +result();
   25.86 +
   25.87 +
   25.88 +goal LK.thy "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
   25.89 +by (fast_tac prop_pack 1);
   25.90 +result();
   25.91 +
   25.92 +
   25.93 +(*If and only if*)
   25.94 +
   25.95 +goal LK.thy "|- (P<->Q) <-> (Q<->P)";
   25.96 +by (fast_tac prop_pack 1);
   25.97 +result();
   25.98 +
   25.99 +goal LK.thy "|- ~ (P <-> ~P)";
  25.100 +by (fast_tac prop_pack 1);
  25.101 +result();
  25.102 +
  25.103 +
  25.104 +(*Sample problems from 
  25.105 +  F. J. Pelletier, 
  25.106 +  Seventy-Five Problems for Testing Automatic Theorem Provers,
  25.107 +  J. Automated Reasoning 2 (1986), 191-216.
  25.108 +  Errata, JAR 4 (1988), 236-236.
  25.109 +*)
  25.110 +
  25.111 +(*1*)
  25.112 +goal LK.thy "|- (P-->Q)  <->  (~Q --> ~P)";
  25.113 +by (fast_tac prop_pack 1);
  25.114 +result();
  25.115 +
  25.116 +(*2*)
  25.117 +goal LK.thy "|- ~ ~ P  <->  P";
  25.118 +by (fast_tac prop_pack 1);
  25.119 +result();
  25.120 +
  25.121 +(*3*)
  25.122 +goal LK.thy "|- ~(P-->Q) --> (Q-->P)";
  25.123 +by (fast_tac prop_pack 1);
  25.124 +result();
  25.125 +
  25.126 +(*4*)
  25.127 +goal LK.thy "|- (~P-->Q)  <->  (~Q --> P)";
  25.128 +by (fast_tac prop_pack 1);
  25.129 +result();
  25.130 +
  25.131 +(*5*)
  25.132 +goal LK.thy "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
  25.133 +by (fast_tac prop_pack 1);
  25.134 +result();
  25.135 +
  25.136 +(*6*)
  25.137 +goal LK.thy "|- P | ~ P";
  25.138 +by (fast_tac prop_pack 1);
  25.139 +result();
  25.140 +
  25.141 +(*7*)
  25.142 +goal LK.thy "|- P | ~ ~ ~ P";
  25.143 +by (fast_tac prop_pack 1);
  25.144 +result();
  25.145 +
  25.146 +(*8.  Peirce's law*)
  25.147 +goal LK.thy "|- ((P-->Q) --> P)  -->  P";
  25.148 +by (fast_tac prop_pack 1);
  25.149 +result();
  25.150 +
  25.151 +(*9*)
  25.152 +goal LK.thy "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
  25.153 +by (fast_tac prop_pack 1);
  25.154 +result();
  25.155 +
  25.156 +(*10*)
  25.157 +goal LK.thy "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
  25.158 +by (fast_tac prop_pack 1);
  25.159 +result();
  25.160 +
  25.161 +(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
  25.162 +goal LK.thy "|- P<->P";
  25.163 +by (fast_tac prop_pack 1);
  25.164 +result();
  25.165 +
  25.166 +(*12.  "Dijkstra's law"*)
  25.167 +goal LK.thy "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
  25.168 +by (fast_tac prop_pack 1);
  25.169 +result();
  25.170 +
  25.171 +(*13.  Distributive law*)
  25.172 +goal LK.thy "|- P | (Q & R)  <-> (P | Q) & (P | R)";
  25.173 +by (fast_tac prop_pack 1);
  25.174 +result();
  25.175 +
  25.176 +(*14*)
  25.177 +goal LK.thy "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
  25.178 +by (fast_tac prop_pack 1);
  25.179 +result();
  25.180 +
  25.181 +
  25.182 +(*15*)
  25.183 +goal LK.thy "|- (P --> Q) <-> (~P | Q)";
  25.184 +by (fast_tac prop_pack 1);
  25.185 +result();
  25.186 +
  25.187 +(*16*)
  25.188 +goal LK.thy "|- (P-->Q) | (Q-->P)";
  25.189 +by (fast_tac prop_pack 1);
  25.190 +result();
  25.191 +
  25.192 +(*17*)
  25.193 +goal LK.thy "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
  25.194 +by (fast_tac prop_pack 1);
  25.195 +result();
  25.196 +
  25.197 +writeln"Reached end of file.";
    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/src/Sequents/ex/LK/quant.ML	Wed Oct 09 13:32:33 1996 +0200
    26.3 @@ -0,0 +1,160 @@
    26.4 +(*  Title:      LK/ex/quant
    26.5 +    ID:         $Id$
    26.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    26.7 +    Copyright   1992  University of Cambridge
    26.8 +
    26.9 +Classical sequent calculus: examples with quantifiers.
   26.10 +*)
   26.11 +
   26.12 +
   26.13 +writeln"LK/ex/quant: Examples with quantifiers";
   26.14 +
   26.15 +goal LK.thy "|- (ALL x. P)  <->  P";
   26.16 +by (fast_tac LK_pack 1);
   26.17 +result(); 
   26.18 +
   26.19 +goal LK.thy "|- (ALL x y.P(x,y))  <->  (ALL y x.P(x,y))";
   26.20 +by (fast_tac LK_pack 1);
   26.21 +result(); 
   26.22 +
   26.23 +goal LK.thy "ALL u.P(u), ALL v.Q(v) |- ALL u v. P(u) & Q(v)";
   26.24 +by (fast_tac LK_pack 1);
   26.25 +result(); 
   26.26 +
   26.27 +writeln"Permutation of existential quantifier.";
   26.28 +goal LK.thy "|- (EX x y.P(x,y)) <-> (EX y x.P(x,y))";
   26.29 +by (fast_tac LK_pack 1);
   26.30 +result(); 
   26.31 +
   26.32 +goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))";
   26.33 +by (fast_tac LK_pack 1);
   26.34 +result(); 
   26.35 +
   26.36 +
   26.37 +(*Converse is invalid*)
   26.38 +goal LK.thy "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
   26.39 +by (fast_tac LK_pack 1);
   26.40 +result(); 
   26.41 +
   26.42 +
   26.43 +writeln"Pushing ALL into an implication.";
   26.44 +goal LK.thy "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))";
   26.45 +by (fast_tac LK_pack 1);
   26.46 +result(); 
   26.47 +
   26.48 +
   26.49 +goal LK.thy "|- (ALL x.P(x)-->Q)  <->  ((EX x.P(x)) --> Q)";
   26.50 +by (fast_tac LK_pack 1);
   26.51 +result(); 
   26.52 +
   26.53 +
   26.54 +goal LK.thy "|- (EX x. P)  <->  P";
   26.55 +by (fast_tac LK_pack 1);
   26.56 +result(); 
   26.57 +
   26.58 +
   26.59 +writeln"Distribution of EX over disjunction.";
   26.60 +goal LK.thy "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))";
   26.61 +by (fast_tac LK_pack 1);
   26.62 +result(); 
   26.63 +(*5 secs*)
   26.64 +
   26.65 +(*Converse is invalid*)
   26.66 +goal LK.thy "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))";
   26.67 +by (fast_tac LK_pack 1);
   26.68 +result(); 
   26.69 +
   26.70 +
   26.71 +writeln"Harder examples: classical theorems.";
   26.72 +
   26.73 +goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
   26.74 +by (fast_tac LK_pack 1);
   26.75 +result(); 
   26.76 +(*3 secs*)
   26.77 +
   26.78 +
   26.79 +goal LK.thy "|- (EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
   26.80 +by (fast_tac LK_pack 1);
   26.81 +result(); 
   26.82 +(*5 secs*)
   26.83 +
   26.84 +
   26.85 +goal LK.thy "|- (ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
   26.86 +by (fast_tac LK_pack 1);
   26.87 +result(); 
   26.88 +
   26.89 +
   26.90 +writeln"Basic test of quantifier reasoning";
   26.91 +goal LK.thy
   26.92 +   "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
   26.93 +by (fast_tac LK_pack 1);
   26.94 +result();  
   26.95 +
   26.96 +
   26.97 +goal LK.thy "|- (ALL x. Q(x))  -->  (EX x. Q(x))";
   26.98 +by (fast_tac LK_pack 1);
   26.99 +result();  
  26.100 +
  26.101 +
  26.102 +writeln"The following are invalid!";
  26.103 +
  26.104 +(*INVALID*)
  26.105 +goal LK.thy "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
  26.106 +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; 
  26.107 +(*Check that subgoals remain: proof failed.*)
  26.108 +getgoal 1; 
  26.109 +
  26.110 +(*INVALID*)
  26.111 +goal LK.thy "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
  26.112 +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  26.113 +getgoal 1; 
  26.114 +
  26.115 +goal LK.thy "|- P(?a) --> (ALL x.P(x))";
  26.116 +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  26.117 +(*Check that subgoals remain: proof failed.*)
  26.118 +getgoal 1;  
  26.119 +
  26.120 +goal LK.thy "|- (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
  26.121 +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  26.122 +getgoal 1;  
  26.123 +
  26.124 +
  26.125 +writeln"Back to things that are provable...";
  26.126 +
  26.127 +goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
  26.128 +by (fast_tac LK_pack 1); 
  26.129 +result();  
  26.130 +
  26.131 +(*An example of why exR should be delayed as long as possible*)
  26.132 +goal LK.thy "|- (P--> (EX x.Q(x))) & P--> (EX x.Q(x))";
  26.133 +by (fast_tac LK_pack 1);
  26.134 +result();  
  26.135 +
  26.136 +writeln"Solving for a Var";
  26.137 +goal LK.thy 
  26.138 +   "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
  26.139 +by (fast_tac LK_pack 1);
  26.140 +result();
  26.141 +
  26.142 +
  26.143 +writeln"Principia Mathematica *11.53";
  26.144 +goal LK.thy 
  26.145 +    "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
  26.146 +by (fast_tac LK_pack 1);
  26.147 +result();
  26.148 +
  26.149 +
  26.150 +writeln"Principia Mathematica *11.55";
  26.151 +goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y.Q(x,y)))";
  26.152 +by (fast_tac LK_pack 1);
  26.153 +result();
  26.154 +
  26.155 +writeln"Principia Mathematica *11.61";
  26.156 +goal LK.thy
  26.157 +   "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
  26.158 +by (fast_tac LK_pack 1);
  26.159 +result();
  26.160 +
  26.161 +writeln"Reached end of file.";
  26.162 +
  26.163 +(*21 August 88: loaded in 45.7 secs*)
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/src/Sequents/ex/Modal/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
    27.3 @@ -0,0 +1,28 @@
    27.4 +(*  Title:      Modal/ex/ROOT
    27.5 +    ID:         $Id$
    27.6 +    Author:     Martin Coen
    27.7 +    Copyright   1991  University of Cambridge
    27.8 +*)
    27.9 +
   27.10 +Sequents_build_completed;    (*Cause examples to fail if Modal did*)
   27.11 +
   27.12 +proof_timing := true;
   27.13 +
   27.14 +writeln "\nTheorems of T\n";
   27.15 +fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
   27.16 +time_use "ex/Modal/Tthms.ML";
   27.17 +
   27.18 +writeln "\nTheorems of S4\n";
   27.19 +fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2]));
   27.20 +time_use "ex/Modal/Tthms.ML";
   27.21 +time_use "ex/Modal/S4thms.ML";
   27.22 +
   27.23 +writeln "\nTheorems of S43\n";
   27.24 +fun try s = (writeln s;
   27.25 +             prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE 
   27.26 +                                           S43_Prover.solve_tac 3]));
   27.27 +time_use "ex/Modal/Tthms.ML";
   27.28 +time_use "ex/Modal/S4thms.ML";
   27.29 +time_use "ex/Modal/S43thms.ML";
   27.30 +
   27.31 +maketest"END: Root file for Modal examples";
    28.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.2 +++ b/src/Sequents/ex/Modal/S43thms.ML	Wed Oct 09 13:32:33 1996 +0200
    28.3 @@ -0,0 +1,49 @@
    28.4 +(*  Title:      91/Modal/ex/S43thms
    28.5 +    ID:         $Id$
    28.6 +    Author:     Martin Coen
    28.7 +    Copyright   1991  University of Cambridge
    28.8 +*)
    28.9 +
   28.10 +(* Theorems of system S43 *)
   28.11 +
   28.12 +try "|- <>[]P --> []<>P";
   28.13 +try "|- <>[]P --> [][]<>P";
   28.14 +try "|- [](<>P | <>Q) --> []<>P | []<>Q";
   28.15 +try "|- <>[]P & <>[]Q --> <>([]P & []Q)";
   28.16 +try "|- []([]P --> []Q) | []([]Q --> []P)";
   28.17 +try "|- [](<>P --> <>Q) | [](<>Q --> <>P)";
   28.18 +try "|- []([]P --> Q) | []([]Q --> P)";
   28.19 +try "|- [](P --> <>Q) | [](Q --> <>P)";
   28.20 +try "|- [](P --> []Q-->R) | [](P | ([]R --> Q))";
   28.21 +try "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)";
   28.22 +try "|- []([]P | Q) & [](P | []Q) --> []P | []Q";
   28.23 +try "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)";
   28.24 +try "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q";
   28.25 +try "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)";
   28.26 +try "|- <>[]<>P <-> []<>P";
   28.27 +try "|- []<>[]P <-> <>[]P";
   28.28 +
   28.29 +(* These are from Hailpern, LNCS 129 *)
   28.30 +
   28.31 +try "|- [](P & Q) <-> []P & []Q";
   28.32 +try "|- <>(P | Q) <-> <>P | <>Q";
   28.33 +try "|- <>(P --> Q) <-> []P --> <>Q";
   28.34 +
   28.35 +try "|- [](P --> Q) --> <>P --> <>Q";
   28.36 +try "|- []P --> []<>P";
   28.37 +try "|- <>[]P --> <>P";
   28.38 +try "|- []<>[]P --> []<>P";
   28.39 +try "|- <>[]P --> <>[]<>P";
   28.40 +try "|- <>[]P --> []<>P";
   28.41 +try "|- []<>[]P <-> <>[]P";
   28.42 +try "|- <>[]<>P <-> []<>P";
   28.43 +
   28.44 +try "|- []P | []Q --> [](P | Q)";
   28.45 +try "|- <>(P & Q) --> <>P & <>Q";
   28.46 +try "|- [](P | Q) --> []P | <>Q";
   28.47 +try "|- <>P & []Q --> <>(P & Q)";
   28.48 +try "|- [](P | Q) --> <>P | []Q";
   28.49 +try "|- [](P | Q) --> []<>P | []<>Q";
   28.50 +try "|- <>[]P & <>[]Q --> <>(P & Q)";
   28.51 +try "|- <>[](P & Q) <-> <>[]P & <>[]Q";
   28.52 +try "|- []<>(P | Q) <-> []<>P | []<>Q";
    29.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.2 +++ b/src/Sequents/ex/Modal/S4thms.ML	Wed Oct 09 13:32:33 1996 +0200
    29.3 @@ -0,0 +1,40 @@
    29.4 +(*  Title:      91/Modal/ex/S4thms
    29.5 +    ID:         $Id$
    29.6 +    Author:     Martin Coen
    29.7 +    Copyright   1991  University of Cambridge
    29.8 +*)
    29.9 +
   29.10 +(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
   29.11 +
   29.12 +try "|- []A --> A";             (* refexivity *)
   29.13 +try "|- []A --> [][]A";         (* transitivity *)
   29.14 +try "|- []A --> <>A";           (* seriality *)
   29.15 +try "|- <>[](<>A --> []<>A)";
   29.16 +try "|- <>[](<>[]A --> []A)";
   29.17 +try "|- []P <-> [][]P";
   29.18 +try "|- <>P <-> <><>P";
   29.19 +try "|- <>[]<>P --> <>P";
   29.20 +try "|- []<>P <-> []<>[]<>P";
   29.21 +try "|- <>[]P <-> <>[]<>[]P";
   29.22 +
   29.23 +(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
   29.24 +
   29.25 +try "|- []P | []Q <-> []([]P | []Q)";
   29.26 +try "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)";
   29.27 +
   29.28 +(* These are from Hailpern, LNCS 129 *)
   29.29 +
   29.30 +try "|- [](P & Q) <-> []P & []Q";
   29.31 +try "|- <>(P | Q) <-> <>P | <>Q";
   29.32 +try "|- <>(P --> Q) <-> ([]P --> <>Q)";
   29.33 +
   29.34 +try "|- [](P --> Q) --> (<>P --> <>Q)";
   29.35 +try "|- []P --> []<>P";
   29.36 +try "|- <>[]P --> <>P";
   29.37 +
   29.38 +try "|- []P | []Q --> [](P | Q)";
   29.39 +try "|- <>(P & Q) --> <>P & <>Q";
   29.40 +try "|- [](P | Q) --> []P | <>Q";
   29.41 +try "|- <>P & []Q --> <>(P & Q)";
   29.42 +try "|- [](P | Q) --> <>P | []Q";
   29.43 +
    30.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.2 +++ b/src/Sequents/ex/Modal/Tthms.ML	Wed Oct 09 13:32:33 1996 +0200
    30.3 @@ -0,0 +1,31 @@
    30.4 +(*  Title:      91/Modal/ex/Tthms
    30.5 +    ID:         $Id$
    30.6 +    Author:     Martin Coen
    30.7 +    Copyright   1991  University of Cambridge
    30.8 +*)
    30.9 +
   30.10 +(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
   30.11 +
   30.12 +try "|- []P --> P";
   30.13 +try "|- [](P-->Q) --> ([]P-->[]Q)";    (* normality*)
   30.14 +try "|- (P--<Q) --> []P --> []Q";
   30.15 +try "|- P --> <>P";
   30.16 +
   30.17 +try "|-  [](P & Q) <-> []P & []Q";
   30.18 +try "|-  <>(P | Q) <-> <>P | <>Q";
   30.19 +try "|-  [](P<->Q) <-> (P>-<Q)";
   30.20 +try "|-  <>(P-->Q) <-> ([]P--><>Q)";
   30.21 +try "|-        []P <-> ~<>(~P)";
   30.22 +try "|-     [](~P) <-> ~<>P";
   30.23 +try "|-       ~[]P <-> <>(~P)";
   30.24 +try "|-      [][]P <-> ~<><>(~P)";
   30.25 +try "|- ~<>(P | Q) <-> ~<>P & ~<>Q";
   30.26 +
   30.27 +try "|- []P | []Q --> [](P | Q)";
   30.28 +try "|- <>(P & Q) --> <>P & <>Q";
   30.29 +try "|- [](P | Q) --> []P | <>Q";
   30.30 +try "|- <>P & []Q --> <>(P & Q)";
   30.31 +try "|- [](P | Q) --> <>P | []Q";
   30.32 +try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)";
   30.33 +try "|- (P--<Q) & (Q--<R) --> (P--<R)";
   30.34 +try "|- []P --> <>Q --> <>(P & Q)";
    31.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.2 +++ b/src/Sequents/ex/ROOT.ML	Wed Oct 09 13:32:33 1996 +0200
    31.3 @@ -0,0 +1,4 @@
    31.4 +
    31.5 +use "ex/LK/ROOT.ML";
    31.6 +use "ex/ILL/ROOT.ML";
    31.7 +use "ex/Modal/ROOT.ML";
    32.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.2 +++ b/src/Sequents/index.html	Wed Oct 09 13:32:33 1996 +0200
    32.3 @@ -0,0 +1,15 @@
    32.4 +<HTML><HEAD><TITLE>Isabelle/Sequents</TITLE></HEAD>
    32.5 +<BODY><H2>Isabelle/Sequents</H2>
    32.6 +The name of every theory is linked to its theory file<BR>
    32.7 +<IMG SRC = "../Tools/red_arrow.gif" ALT = \/></A> stands for subtheories (child theories)<BR>
    32.8 +<IMG SRC = "../Tools/blue_arrow.gif" ALT = /\></A> stands for supertheories (parent theories)<P>
    32.9 +<A HREF = "../index.html">Back</A> to the index of Isabelle logics
   32.10 +<BR>View the <A HREF = "README.html">ReadMe</A> file.
   32.11 +<HR><A HREF = ".Sequents_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".Sequents_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".Sequents.html">Sequents</A><BR>
   32.12 +<A HREF = ".LK_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".LK_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".LK.html">LK</A><BR>
   32.13 +<A HREF = ".ILL_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".ILL_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".ILL.html">ILL</A><BR>
   32.14 +<A HREF = ".Modal0_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".Modal0_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".Modal0.html">Modal0</A><BR>
   32.15 +<A HREF = ".T_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".T_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".T.html">T</A><BR>
   32.16 +<A HREF = ".S4_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".S4_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".S4.html">S4</A><BR>
   32.17 +<A HREF = ".S43_sub.html"><IMG SRC = "../Tools/red_arrow.gif" BORDER=0 ALT = \/></A><A HREF = ".S43_sup.html"><IMG SRC = "../Tools/blue_arrow.gif" BORDER=0 ALT = /\></A> <A HREF = ".S43.html">S43</A><BR>
   32.18 +<!-->
   32.19 \ No newline at end of file
    33.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.2 +++ b/src/Sequents/prover.ML	Wed Oct 09 13:32:33 1996 +0200
    33.3 @@ -0,0 +1,223 @@
    33.4 +(*  Title:      LK/LK.ML
    33.5 +    ID:         $Id$
    33.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    33.7 +    Copyright   1992  University of Cambridge
    33.8 +*)
    33.9 +
   33.10 +
   33.11 +(**** Theorem Packs ****)
   33.12 +
   33.13 +(* based largely on LK *)
   33.14 +
   33.15 +datatype pack = Pack of thm list * thm list;
   33.16 +
   33.17 +(*A theorem pack has the form  (safe rules, unsafe rules)
   33.18 +  An unsafe rule is incomplete or introduces variables in subgoals,
   33.19 +  and is tried only when the safe rules are not applicable.  *)
   33.20 +
   33.21 +fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
   33.22 +
   33.23 +val empty_pack = Pack([],[]);
   33.24 +
   33.25 +infix 4 add_safes add_unsafes;
   33.26 +
   33.27 +fun (Pack(safes,unsafes)) add_safes ths   = 
   33.28 +    Pack(sort less (ths@safes), unsafes);
   33.29 +
   33.30 +fun (Pack(safes,unsafes)) add_unsafes ths = 
   33.31 +    Pack(safes, sort less (ths@unsafes));
   33.32 +
   33.33 +
   33.34 +(*Returns the list of all formulas in the sequent*)
   33.35 +fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
   33.36 +  | forms_of_seq (H $ u) = forms_of_seq u
   33.37 +  | forms_of_seq _ = [];
   33.38 +
   33.39 +(*Tests whether two sequences (left or right sides) could be resolved.
   33.40 +  seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
   33.41 +  Assumes each formula in seqc is surrounded by sequence variables
   33.42 +  -- checks that each concl formula looks like some subgoal formula.
   33.43 +  It SHOULD check order as well, using recursion rather than forall/exists*)
   33.44 +fun could_res (seqp,seqc) =
   33.45 +      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
   33.46 +                              (forms_of_seq seqp))
   33.47 +             (forms_of_seq seqc);
   33.48 +
   33.49 +
   33.50 +(*Tests whether two sequents or pairs of sequents could be resolved*)
   33.51 +fun could_resolve_seq (prem,conc) =
   33.52 +  case (prem,conc) of
   33.53 +      (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
   33.54 +       _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
   33.55 +	  could_res (leftp,leftc) andalso could_res (rightp,rightc)
   33.56 +    | (_ $ Abs(_,_,leftp) $ rightp,
   33.57 +       _ $ Abs(_,_,leftc) $ rightc) =>
   33.58 +	  could_res (leftp,leftc)  andalso  could_unify (rightp,rightc)
   33.59 +    | _ => false;
   33.60 +
   33.61 +
   33.62 +(*Like filt_resolve_tac, using could_resolve_seq
   33.63 +  Much faster than resolve_tac when there are many rules.
   33.64 +  Resolve subgoal i using the rules, unless more than maxr are compatible. *)
   33.65 +fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
   33.66 +  let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
   33.67 +  in  if length rls > maxr  then  no_tac
   33.68 +	  else (*((rtac derelict 1 THEN rtac impl 1
   33.69 +		 THEN (rtac identity 2 ORELSE rtac ll_mp 2)
   33.70 +		 THEN rtac context1 1)
   33.71 +		 ORELSE *) resolve_tac rls i
   33.72 +  end);
   33.73 +
   33.74 +
   33.75 +(*Predicate: does the rule have n premises? *)
   33.76 +fun has_prems n rule =  (nprems_of rule = n);
   33.77 +
   33.78 +(*Continuation-style tactical for resolution.
   33.79 +  The list of rules is partitioned into 0, 1, 2 premises.
   33.80 +  The resulting tactic, gtac, tries to resolve with rules.
   33.81 +  If successful, it recursively applies nextac to the new subgoals only.
   33.82 +  Else fails.  (Treatment of goals due to Ph. de Groote) 
   33.83 +  Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)
   33.84 +
   33.85 +(*Takes rule lists separated in to 0, 1, 2, >2 premises.
   33.86 +  The abstraction over state prevents needless divergence in recursion.
   33.87 +  The 9999 should be a parameter, to delay treatment of flexible goals. *)
   33.88 +
   33.89 +fun RESOLVE_THEN rules =
   33.90 +  let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
   33.91 +      fun tac nextac i = STATE (fn state =>  
   33.92 +	  filseq_resolve_tac rls0 9999 i 
   33.93 +	  ORELSE
   33.94 +	  (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
   33.95 +	  ORELSE
   33.96 +	  (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
   33.97 +					THEN  TRY(nextac i)) )
   33.98 +  in  tac  end;
   33.99 +
  33.100 +
  33.101 +
  33.102 +(*repeated resolution applied to the designated goal*)
  33.103 +fun reresolve_tac rules = 
  33.104 +  let val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
  33.105 +      fun gtac i = restac gtac i
  33.106 +  in  gtac  end; 
  33.107 +
  33.108 +(*tries the safe rules repeatedly before the unsafe rules. *)
  33.109 +fun repeat_goal_tac (Pack(safes,unsafes)) = 
  33.110 +  let val restac  =    RESOLVE_THEN safes
  33.111 +      and lastrestac = RESOLVE_THEN unsafes;
  33.112 +      fun gtac i = restac gtac i  ORELSE  (print_tac THEN lastrestac gtac i)
  33.113 +  in  gtac  end; 
  33.114 +
  33.115 +
  33.116 +(*Tries safe rules only*)
  33.117 +fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;
  33.118 +
  33.119 +(*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
  33.120 +fun step_tac (thm_pack as Pack(safes,unsafes)) =
  33.121 +    safe_goal_tac thm_pack  ORELSE'
  33.122 +    filseq_resolve_tac unsafes 9999;
  33.123 +
  33.124 +
  33.125 +(* Tactic for reducing a goal, using Predicate Calculus rules.
  33.126 +   A decision procedure for Propositional Calculus, it is incomplete
  33.127 +   for Predicate-Calculus because of allL_thin and exR_thin.  
  33.128 +   Fails if it can do nothing.      *)
  33.129 +fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1));
  33.130 +
  33.131 +
  33.132 +(*The following two tactics are analogous to those provided by 
  33.133 +  Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
  33.134 +fun fast_tac thm_pack =
  33.135 +  SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1));
  33.136 +
  33.137 +fun best_tac thm_pack  = 
  33.138 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
  33.139 +	       (step_tac thm_pack 1));
  33.140 +
  33.141 +
  33.142 +
  33.143 +signature MODAL_PROVER_RULE =
  33.144 +sig
  33.145 +    val rewrite_rls      : thm list
  33.146 +    val safe_rls         : thm list
  33.147 +    val unsafe_rls       : thm list
  33.148 +    val bound_rls        : thm list
  33.149 +    val aside_rls        : thm list
  33.150 +end;
  33.151 +
  33.152 +signature MODAL_PROVER = 
  33.153 +sig
  33.154 +    val rule_tac   : thm list -> int ->tactic
  33.155 +    val step_tac   : int -> tactic
  33.156 +    val solven_tac : int -> int -> tactic
  33.157 +    val solve_tac  : int -> tactic
  33.158 +end;
  33.159 +
  33.160 +functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
  33.161 +struct
  33.162 +local open Modal_Rule
  33.163 +in 
  33.164 +
  33.165 +(*Returns the list of all formulas in the sequent*)
  33.166 +fun forms_of_seq (Const("SeqO",_) $ P $ u) = P :: forms_of_seq u
  33.167 +  | forms_of_seq (H $ u) = forms_of_seq u
  33.168 +  | forms_of_seq _ = [];
  33.169 +
  33.170 +(*Tests whether two sequences (left or right sides) could be resolved.
  33.171 +  seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
  33.172 +  Assumes each formula in seqc is surrounded by sequence variables
  33.173 +  -- checks that each concl formula looks like some subgoal formula.*)
  33.174 +fun could_res (seqp,seqc) =
  33.175 +      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
  33.176 +                              (forms_of_seq seqp))
  33.177 +             (forms_of_seq seqc);
  33.178 +
  33.179 +(*Tests whether two sequents G|-H could be resolved, comparing each side.*)
  33.180 +fun could_resolve_seq (prem,conc) =
  33.181 +  case (prem,conc) of
  33.182 +      (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
  33.183 +       _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
  33.184 +          could_res (leftp,leftc)  andalso  could_res (rightp,rightc)
  33.185 +    | _ => false;
  33.186 +
  33.187 +(*Like filt_resolve_tac, using could_resolve_seq
  33.188 +  Much faster than resolve_tac when there are many rules.
  33.189 +  Resolve subgoal i using the rules, unless more than maxr are compatible. *)
  33.190 +fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
  33.191 +  let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
  33.192 +  in  if length rls > maxr  then  no_tac  else resolve_tac rls i
  33.193 +  end);
  33.194 +
  33.195 +fun fresolve_tac rls n = filseq_resolve_tac rls 999 n;
  33.196 +
  33.197 +(* NB No back tracking possible with aside rules *)
  33.198 +
  33.199 +fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n));
  33.200 +fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;
  33.201 +
  33.202 +val fres_safe_tac = fresolve_tac safe_rls;
  33.203 +val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac;
  33.204 +val fres_bound_tac = fresolve_tac bound_rls;
  33.205 +
  33.206 +fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
  33.207 +                                    else tf(i) THEN tac(i-1)
  33.208 +                    in STATE(fn state=> tac(nprems_of state)) end;
  33.209 +
  33.210 +(* Depth first search bounded by d *)
  33.211 +fun solven_tac d n = STATE (fn state =>
  33.212 +        if d<0 then no_tac
  33.213 +        else if (nprems_of state = 0) then all_tac 
  33.214 +        else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
  33.215 +                 ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
  33.216 +                   (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
  33.217 +
  33.218 +fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
  33.219 +
  33.220 +fun step_tac n = STATE (fn state =>  
  33.221 +      if (nprems_of state = 0) then all_tac 
  33.222 +      else (DETERM(fres_safe_tac n)) ORELSE 
  33.223 +           (fres_unsafe_tac n APPEND fres_bound_tac n));
  33.224 +
  33.225 +end;
  33.226 +end;