# HG changeset patch # User paulson # Date 844860753 -7200 # Node ID fb0655539d05dc8567460b6ebd5b20c665a9797c # Parent 6ac12b9478d5d9e8e0e6ffb9ad1b46fdb45500ec New unified treatment of sequent calculi by Sara Kalvala combines the old LK and Modal with the new ILL (Int. Linear Logic) diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ILL.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ILL.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,140 @@ +(* Title: Sequents/ILL.ML + ID: $Id$ + Author: Sara Kalvala and Valeria de Paiva + Copyright 1992 University of Cambridge + +*) + +open ILL; + + +val lazy_cs = empty_pack + add_safes [tensl, conjr, disjl, promote0, + context2,context3] + add_unsafes [identity, zerol, conjll, conjlr, disjrl, disjrr, + impr, tensr, impl, derelict, weaken, + promote1, promote2,context1,context4a,context4b]; + +fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n); + +fun auto x = prove_goal thy x (fn prems => [best_tac lazy_cs 1]); + +val aux_impl = prove_goal thy "$F, $G |- A ==> $F, !(A -o B), $G |- B" +(fn prems => [rtac derelict 1 THEN rtac impl 1 THEN rtac identity 2 + THEN rtac context1 1 THEN rtac (hd(prems)) 1]); + +val conj_lemma = +prove_goal thy " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C" +(fn prems => [rtac contract 1, + res_inst_tac [("A","(!A) >< (!B)")] cut 1, + rtac tensr 2, + rtac (auto "! (A && B) |- !A") 3, + rtac (auto "! (A && B) |- !B") 3, + rtac context1 2, + rtac tensl 2, + rtac (hd(prems)) 2, + rtac context3 1, + rtac context3 1, + rtac context1 1]); + +val impr_contract = +prove_goal thy "!A, !A, $G |- B ==> $G |- (!A) -o B" +(fn prems => [rtac impr 1 THEN rtac contract 1 + THEN rtac (hd(prems)) 1]); + + +val impr_contr_der = +prove_goal thy "A, !A, $G |- B ==> $G |- (!A) -o B" +(fn prems => [rtac impr 1 THEN rtac contract 1 THEN rtac derelict 1 + THEN rtac (hd(prems)) 1]); + +val contrad1 = +prove_goal thy "$F, (!B) -o 0, $G, !B, $H |- A" +(fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1, + rtac zerol 1]); + + +val contrad2 = +prove_goal thy "$F, !B, $G, (!B) -o 0, $H |- A" +(fn _ => [rtac impl 1,rtac identity 3,rtac context3 1,rtac context1 1, + rtac zerol 1]); + +val ll_mp = +prove_goal thy "A -o B, A |- B" +(fn _ => [rtac impl 1 THEN rtac identity 2 THEN rtac identity 2 + THEN rtac context1 1]); + +val mp_rule1 = +prove_goal thy "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C" +(fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2, + rtac (hd(prems)) 2, rtac context3 1, rtac context3 1, + rtac context1 1]); + +val mp_rule2 = +prove_goal thy "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C" +(fn prems => [res_inst_tac [("A","B")] cut 1, rtac ll_mp 2, + rtac (hd(prems)) 2, rtac context3 1, rtac context3 1, + rtac context1 1]); + +val or_to_and = +prove_goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))" +(fn _ => [best_tac lazy_cs 1]); + +val o_a_rule = +prove_goal thy "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==> \ +\ $F, !((!(A ++ B)) -o 0), $G |- C" +(fn prems => [rtac cut 1, rtac or_to_and 2, rtac (hd(prems)) 2, + rtac context3 1, rtac context1 1]); + + + +val conj_imp = + prove_goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C" +(fn _ => [rtac impr 1,rtac conj_lemma 1, rtac disjl 1, + ALLGOALS (rtac mp_rule1 THEN' best_tac lazy_cs)]); + + +val not_imp = auto "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"; + +val a_not_a = +prove_goal thy "!A -o (!A -o 0) |- !A -o 0" + (fn _ => [rtac impr 1, rtac contract 1, rtac impl 1, + rtac context1 1 THEN rtac identity 2, best_tac lazy_cs 1]); + +val a_not_a_rule = +prove_goal thy "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B" + (fn prems => [res_inst_tac [("A","!A -o 0")] cut 1, + rtac a_not_a 2 THEN rtac (hd(prems)) 2 + THEN best_tac lazy_cs 1]); + +fun thm_to_rule x y = +prove_goal thy x (fn prems => [rtac cut 1, rtac y 2, rtac (hd(prems)) 2, + best_tac lazy_cs 1]); + +val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1, + contrad2, mp_rule1, mp_rule2, o_a_rule, + a_not_a_rule] + add_unsafes [aux_impl]; + +val power_cs = safe_cs add_unsafes [impr_contr_der]; + +fun auto1 x = prove_goal thy x (fn prems => [best_tac safe_cs 1]) ; + +fun auto2 x = prove_goal thy x (fn prems => [best_tac power_cs 1]) ; + + +(* some examples from Troelstra and van Dalen + +auto1 "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"; + +auto1 "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))"; + +auto1 "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |- \ +\ (!A) -o ( (! ((!B) -o 0)) -o 0)"; + + +auto2 "!( (!A) -o ( (! ((!B) -o 0)) -o 0) ) |- \ +\ (!((! ((!A) -o B) ) -o 0)) -o 0"; + + + *) diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ILL.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ILL.thy Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,134 @@ +(* Title: ILL.thy + ID: $Id$ + Author: Sara Kalvala and Valeria de Paiva + Copyright 1995 University of Cambridge +*) + + +ILL = Sequents + + +consts + + + Trueprop :: "two_seqi" + "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5) + + + +"><" ::"[o, o] => o" (infixr 35) +"-o" ::"[o, o] => o" (infixr 45) +"o-o" ::"[o, o] => o" (infixr 45) +FShriek ::"o => o" ("! _" [100] 1000) +"&&" ::"[o, o] => o" (infixr 35) +"++" ::"[o, o] => o" (infixr 35) +zero ::"o" ("0") +top ::"o" ("1") +eye ::"o" ("I") +aneg ::"o=>o" ("~_") + + + (* syntax for context manipulation *) + + Context :: "two_seqi" +"@Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5) + + (* syntax for promotion rule *) + + PromAux :: "three_seqi" +"@PromAux":: "three_seqe" ("promaux {_||_||_}") + +defs + +liff_def "P o-o Q == (P -o Q) >< (Q -o P)" + +aneg_def "~A == A -o 0" + + + + +rules + +identity "P |- P" + +zerol "$G, 0, $H |- A" + + (* RULES THAT DO NOT DIVIDE CONTEXT *) + +derelict "$F, A, $G |- C ==> $F, !A, $G |- C" + (* unfortunately, this one removes !A *) + +contract "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" + +weaken "$F, $G |- C ==> $G, !A, $F |- C" + (* weak form of weakening, in practice just to clean context *) + (* weaken and contract not needed (CHECK) *) + +promote2 "promaux{ || $H || B} ==> $H |- !B" +promote1 "promaux{!A, $G || $H || B} + ==> promaux {$G || $H, !A || B}" +promote0 "$G |- A ==> promaux {$G || || A}" + + + +tensl "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" + +impr "A, $F |- B ==> $F |- A -o B" + +conjr "[| $F |- A ; + $F |- B |] + ==> $F |- (A && B)" + +conjll "$G, A, $H |- C ==> $G, A && B, $H |- C" + +conjlr "$G, B, $H |- C ==> $G, A && B, $H |- C" + +disjrl "$G |- A ==> $G |- A ++ B" +disjrr "$G |- B ==> $G |- A ++ B" +disjl "[| $G, A, $H |- C ; + $G, B, $H |- C |] + ==> $G, A ++ B, $H |- C" + + + (* RULES THAT DIVIDE CONTEXT *) + +tensr "[| $F, $J :=: $G; + $F |- A ; + $J |- B |] + ==> $G |- A >< B" + +impl "[| $G, $F :=: $J, $H ; + B, $F |- C ; + $G |- A |] + ==> $J, A -o B, $H |- C" + + +cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ; + $H1, $H2, $H3, $H4 |- A ; + $J1, $J2, A, $J3, $J4 |- B |] ==> $F |- B" + + + (* CONTEXT RULES *) + +context1 "$G :=: $G" +context2 "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" +context3 "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" +context4a "$F :=: $H, $G ==> $F :=: $H, !A, $G" +context4b "$F, $H :=: $G ==> $F, !A, $H :=: $G" +context5 "$F, $G :=: $H ==> $G, $F :=: $H" + + + + +end + +ML + +val parse_translation = [("@Trueprop",Sequents.single_tr "Trueprop"), + ("@Context",Sequents.two_seq_tr "Context"), + ("@PromAux", Sequents.three_seq_tr "PromAux")]; + +val print_translation = [("Trueprop",Sequents.single_tr' "@Trueprop"), + ("Context",Sequents.two_seq_tr'"@Context"), + ("PromAux", Sequents.three_seq_tr'"@PromAux")]; + + diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/LK.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/LK.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,82 @@ +(* Title: LK/LK.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Tactics and lemmas for lk.thy (thanks also to Philippe de Groote) +*) + +open LK; + +(*Higher precedence than := facilitates use of references*) +infix 4 add_safes add_unsafes; + +(*Cut and thin, replacing the right-side formula*) +fun cutR_tac (sP: string) i = + res_inst_tac [ ("P",sP) ] cut i THEN rtac thinR i; + +(*Cut and thin, replacing the left-side formula*) +fun cutL_tac (sP: string) i = + res_inst_tac [ ("P",sP) ] cut i THEN rtac thinL (i+1); + + +(** If-and-only-if rules **) +qed_goalw "iffR" LK.thy [iff_def] + "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F" + (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]); + +qed_goalw "iffL" LK.thy [iff_def] + "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E" + (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]); + +qed_goalw "TrueR" LK.thy [True_def] + "$H |- $E, True, $F" + (fn _=> [ rtac impR 1, rtac basic 1 ]); + + +(** Weakened quantifier rules. Incomplete, they let the search terminate.**) + +qed_goal "allL_thin" LK.thy + "$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E" + (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]); + +qed_goal "exR_thin" LK.thy + "$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F" + (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]); + +(* Symmetry of equality in hypotheses *) +qed_goal "symL" LK.thy + "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" + (fn prems=> + [ (rtac cut 1), + (rtac thinL 2), + (resolve_tac prems 2), + (resolve_tac [basic RS sym] 1) ]); + + + + +(*The rules of LK*) +val prop_pack = empty_pack add_safes + [basic, refl, conjL, conjR, disjL, disjR, impL, impR, + notL, notR, iffL, iffR]; + +val LK_pack = prop_pack add_safes [allR, exL] + add_unsafes [allL_thin, exR_thin]; + +val LK_dup_pack = prop_pack add_safes [allR, exL] + add_unsafes [allL, exR]; + + + +(** Contraction. Useful since some rules are not complete. **) + +qed_goal "conR" LK.thy + "$H |- $E, P, $F, P ==> $H |- $E, P, $F" + (fn prems=> + [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]); + +qed_goal "conL" LK.thy + "$H, P, $G, P |- $E ==> $H, P, $G |- $E" + (fn prems=> + [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]); diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/LK.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/LK.thy Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,84 @@ +(* Title: LK/lk.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Classical First-Order Sequent Calculus + +There may be printing problems if a seqent is in expanded normal form + (eta-expanded, beta-contracted) +*) + +LK = Sequents + + + +consts + + Trueprop :: "two_seqi" + "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) + + + True,False :: o + "=" :: ['a,'a] => o (infixl 50) + Not :: o => o ("~ _" [40] 40) + "&" :: [o,o] => o (infixr 35) + "|" :: [o,o] => o (infixr 30) + "-->","<->" :: [o,o] => o (infixr 25) + The :: ('a => o) => 'a (binder "THE " 10) + All :: ('a => o) => o (binder "ALL " 10) + Ex :: ('a => o) => o (binder "EX " 10) + +rules + (*Structural rules*) + + basic "$H, P, $G |- $E, P, $F" + + thinR "$H |- $E, $F ==> $H |- $E, P, $F" + thinL "$H, $G |- $E ==> $H, P, $G |- $E" + + cut "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" + + (*Propositional rules*) + + conjR "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" + conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" + + disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" + disjL "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" + + impR "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" + impL "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" + + notR "$H, P |- $E, $F ==> $H |- $E, ~P, $F" + notL "$H, $G |- $E, P ==> $H, ~P, $G |- $E" + + FalseL "$H, False, $G |- $E" + + True_def "True == False-->False" + iff_def "P<->Q == (P-->Q) & (Q-->P)" + + (*Quantifiers*) + + allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F" + allL "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E" + + exR "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F" + exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E" + + (*Equality*) + + refl "$H |- $E, a=a, $F" + sym "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F" + trans "[| $H|- $E, a=b, $F; $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F" + + + (*Descriptions*) + + The "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> + $H |- $E, P(THE x.P(x)), $F" +end + + ML + +val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")]; +val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")]; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/Makefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/Makefile Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,72 @@ +# $Id$ +######################################################################### +# # +# Makefile for Isabelle (Sequents) # +# # +######################################################################### + +#To make the system, cd to this directory and type +# make +#To make the system and test it on standard examples, type +# make test +#To generate HTML files for every theory, set the environment variable +#MAKE_HTML or add the parameter "MAKE_HTML=". + +#Environment variable ISABELLECOMP specifies the compiler. +#Environment variable ISABELLEBIN specifies the destination directory. +#For Poly/ML, ISABELLEBIN must begin with a / + +#Makes Pure if this file is ABSENT -- but not +#if it is out of date, since this Makefile does not know its dependencies! + +BIN = $(ISABELLEBIN) +COMP = $(ISABELLECOMP) +NAMES = ILL LK S4 S43 T +FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML) + +ILL_NAMES = ILL_predlog washing +EX_FILES = ex/ROOT.ML \ + ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML ex/LK/quant.ML \ + ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \ + ex/ILL/ILL_kleene_lemmas.ML \ + $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML) + +$(BIN)/Sequents: $(BIN)/Pure $(FILES) + case "$(COMP)" in \ + poly*) echo 'make_database"$(BIN)/Sequents"; quit();' \ + | $(COMP) $(BIN)/Pure;\ + if [ "$${MAKE_HTML}" = "true" ]; \ + then echo 'open PolyML; make_html := true; exit_use_dir".";' \ + | $(COMP) $(BIN)/Sequents;\ + elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ + then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/Sequents;\ + else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/Sequents;\ + fi;\ + discgarb -c $(BIN)/Sequents;;\ + sml*) if [ "$${MAKE_HTML}" = "true" ]; \ + then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/Sequents" banner;' | $(BIN)/Pure;\ + elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ + then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/Sequents" banner;' \ + | $(BIN)/Pure;\ + else echo 'exit_use_dir"."; xML"$(BIN)/Sequents" banner;' \ + | $(BIN)/Pure;\ + fi;;\ + *) echo Bad value for ISABELLECOMP: \ + $(COMP) is not poly or sml;;\ + esac + +$(BIN)/Pure: + cd ../Pure; $(MAKE) + +test: $(BIN)/Sequents $(EX_FILES) + case "$(COMP)" in \ + poly*) echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\ + sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\ + *) echo Bad value for ISABELLECOMP: \ + $(COMP) is not poly or sml;;\ + esac + + + + +.PRECIOUS: $(BIN)/Pure $(BIN)/Sequents diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/Modal0.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/Modal0.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,30 @@ +(* Title: Modal/modal0 + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge +*) + +structure Modal0_rls = +struct + +val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def]; + +local + val iffR = prove_goal thy + "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F" + (fn prems=> + [ (rewtac iff_def), + (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]); + + val iffL = prove_goal thy + "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E" + (fn prems=> + [ rewtac iff_def, + (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]) +in +val safe_rls = [basic,conjL,conjR,disjL,disjR,impL,impR,notL,notR,iffL,iffR]; +val unsafe_rls = [allR,exL]; +val bound_rls = [allL,exR]; +end + +end; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/Modal0.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/Modal0.thy Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,40 @@ +(* Title: Modal/modal0 + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge +*) + +Modal0 = LK + + +consts + box :: "o=>o" ("[]_" [50] 50) + dia :: "o=>o" ("<>_" [50] 50) + "--<",">-<" :: "[o,o]=>o" (infixr 25) + "@Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) + "@Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5) + Lstar,Rstar :: "two_seqi" + +rules + (* Definitions *) + + strimp_def "P --< Q == [](P --> Q)" + streqv_def "P >-< Q == (P --< Q) & (Q --< P)" +end + +ML + +local + + val Lstar = "Lstar"; + val Rstar = "Rstar"; + val SLstar = "@Lstar"; + val SRstar = "@Rstar"; + + fun star_tr c [s1,s2] = + Const(c,dummyT)$Sequents.seq_tr s1$Sequents.seq_tr s2; + fun star_tr' c [s1,s2] = + Const(c,dummyT) $ Sequents.seq_tr' s1 $ Sequents.seq_tr' s2; +in +val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)]; +val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] +end; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/README.html Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,67 @@ + +Sequents/ReadMe + +

Sequents: Various Sequent Calculi

+ +This directory contains the Standard ML sources of the Isabelle system for +various Sequent, Linear, and Modal Logic. Important files include + +
+
ROOT.ML +
loads all source files. Enter an ML image containing Pure +Isabelle and type: use "ROOT.ML"; + +
Makefile +
compiles the files under Poly/ML or SML of New Jersey + + +
ex +
subdirectory containing examples. Files are arranged in +subdirectories. To execute all of them, enter an ML image containing +Sequents and type +
+	use "ex/ROOT.ML";
+
+To execute examples in a particular logic (LK/ILL/Modal) use the +appropriate command: +
+	use "ex/LK/ROOT.ML";
+	use "ex/ILL/ROOT.ML";
+	use "ex/Modal/ROOT.ML";
+
+
+ +

Much of the work in Modal logic was done by Martin Coen. Thanks to +Rajeev Gore' for supplying the inference system for S43. Sara Kalvala +reorganized the files and supplied Linear Logic. Jacob Frost provided +some improvements to the syntax of sequents. + +

Useful references on sequent calculi: + +

+ +Useful references on Modal Logics: + + +Useful references on Linear Logic: + + + diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ROOT.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,30 @@ +(* Title: Sequents/ROOT + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1991 University of Cambridge + +Adds Classical Sequent Calculus to a database containing pure Isabelle. +*) + +val banner = "Sequent Calculii"; +writeln banner; + +init_thy_reader(); + +print_depth 1; + +use_thy "Sequents"; +use "prover.ML"; + +use_thy "LK"; +use_thy "ILL"; + +use_thy "Modal0"; +use_thy"T"; +use_thy"S4"; +use_thy"S43"; + +use "../Pure/install_pp.ML"; +print_depth 8; + +val Sequents_build_completed = (); (*indicate successful build*) diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/S4.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/S4.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,17 @@ +(* Title: Modal/S4 + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge +*) + +local open Modal0_rls S4 +in structure MP_Rule : MODAL_PROVER_RULE = + struct + val rewrite_rls = rewrite_rls + val safe_rls = safe_rls + val unsafe_rls = unsafe_rls @ [boxR,diaL] + val bound_rls = bound_rls @ [boxL,diaR] + val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2] + end; +end; +structure S4_Prover = Modal_ProverFun(MP_Rule); diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/S4.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/S4.thy Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,31 @@ +(* Title: Modal/S4 + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge +*) + +S4 = Modal0 + +rules +(* Definition of the star operation using a set of Horn clauses *) +(* For system S4: gamma * == {[]P | []P : gamma} *) +(* delta * == {<>P | <>P : delta} *) + + lstar0 "|L>" + lstar1 "$G |L> $H ==> []P, $G |L> []P, $H" + lstar2 "$G |L> $H ==> P, $G |L> $H" + rstar0 "|R>" + rstar1 "$G |R> $H ==> <>P, $G |R> <>P, $H" + rstar2 "$G |R> $H ==> P, $G |R> $H" + +(* Rules for [] and <> *) + + boxR + "[| $E |L> $E'; $F |R> $F'; $G |R> $G'; + $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G" + boxL "$E,P,$F,[]P |- $G ==> $E, []P, $F |- $G" + + diaR "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G" + diaL + "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; + $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G" +end diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/S43.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/S43.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,19 @@ +(* Title: Modal/S43 + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge + +This implements Rajeev Gore's sequent calculus for S43. +*) + +local open Modal0_rls S43 +in structure MP_Rule : MODAL_PROVER_RULE = + struct + val rewrite_rls = rewrite_rls + val safe_rls = safe_rls + val unsafe_rls = unsafe_rls @ [pi1,pi2] + val bound_rls = bound_rls @ [boxL,diaR] + val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2] + end; +end; +structure S43_Prover = Modal_ProverFun(MP_Rule); diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/S43.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/S43.thy Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,78 @@ +(* Title: Modal/S43 + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge + +This implements Rajeev Gore's sequent calculus for S43. +*) + +S43 = Modal0 + + +consts + S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq', + seq'=>seq', seq'=>seq', seq'=>seq'] => prop" + "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop" + ("S43pi((_);(_);(_);(_);(_);(_))" [] 5) + +rules +(* Definition of the star operation using a set of Horn clauses *) +(* For system S43: gamma * == {[]P | []P : gamma} *) +(* delta * == {<>P | <>P : delta} *) + + lstar0 "|L>" + lstar1 "$G |L> $H ==> []P, $G |L> []P, $H" + lstar2 "$G |L> $H ==> P, $G |L> $H" + rstar0 "|R>" + rstar1 "$G |R> $H ==> <>P, $G |R> <>P, $H" + rstar2 "$G |R> $H ==> P, $G |R> $H" + +(* Set of Horn clauses to generate the antecedents for the S43 pi rule *) +(* ie *) +(* S1...Sk,Sk+1...Sk+m *) +(* ---------------------------------- *) +(* <>P1...<>Pk, $G |- $H, []Q1...[]Qm *) +(* *) +(* where Si == <>P1...<>Pi-1,<>Pi+1,..<>Pk,Pi, $G * |- $H *, []Q1...[]Qm *) +(* and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj *) +(* and 1<=i<=k and kP,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia |] ==> + S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia" + S43pi2 + "[| (S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia |] ==> + S43pi $L';; $R'; []P,$R; $Lbox;$Rdia" + +(* Rules for [] and <> for S43 *) + + boxL "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" + diaR "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" + pi1 + "[| $L1,<>P,$L2 |L> $Lbox; $L1,<>P,$L2 |R> $Ldia; $R |L> $Rbox; $R |R> $Rdia; + S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> + $L1, <>P, $L2 |- $R" + pi2 + "[| $L |L> $Lbox; $L |R> $Ldia; $R1,[]P,$R2 |L> $Rbox; $R1,[]P,$R2 |R> $Rdia; + S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> + $L |- $R1, []P, $R2" +end + +ML + +local + + val S43pi = "S43pi"; + val SS43pi = "@S43pi"; + + val tr = Sequents.seq_tr; + val tr' = Sequents.seq_tr'; + + fun s43pi_tr[s1,s2,s3,s4,s5,s6]= + Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6; + fun s43pi_tr'[s1,s2,s3,s4,s5,s6] = + Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6; +in +val parse_translation = [(SS43pi,s43pi_tr)]; +val print_translation = [(S43pi,s43pi_tr')] +end diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/Sequents.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/Sequents.thy Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,147 @@ +(* Title: LK/lk.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Classical First-Order Sequent Calculus +*) + +Sequents = Pure + + +types + o + +arities + o :: logic + + +(* Sequences *) + +types + seq' + +consts + SeqO' :: "[o,seq']=>seq'" + Seq1' :: "o=>seq'" + + +(* concrete syntax *) + +types + seq seqobj seqcont + + +syntax + SeqEmp :: "seq" ("") + SeqApp :: "[seqobj,seqcont] => seq" ("__") + + SeqContEmp :: "seqcont" ("") + SeqContApp :: "[seqobj,seqcont] => seqcont" (",/ __") + + SeqO :: "o => seqobj" ("_") + SeqId :: "id => seqobj" ("$_") + SeqVar :: "var => seqobj" ("$_") + +types + + single_seqe = "[seq,seqobj] => prop" + single_seqi = "[seq'=>seq',seq'=>seq'] => prop" + two_seqi = "[seq'=>seq', seq'=>seq'] => prop" + two_seqe = "[seq, seq] => prop" + three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop" + three_seqe = "[seq, seq, seq] => prop" + four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop" + four_seqe = "[seq, seq, seq, seq] => prop" + +end + +ML + +(* parse translation for sequences *) + +fun abs_seq' t = Abs("s", Type("seq'",[]), t); + +fun seqobj_tr(Const("SeqO",_)$f) = Const("SeqO'",dummyT)$f | + seqobj_tr(_$i) = i; + +fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 | + seqcont_tr(Const("SeqContApp",_)$so$sc) = + (seqobj_tr so)$(seqcont_tr sc); + +fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) | + seq_tr(Const("SeqApp",_)$so$sc) = + abs_seq'(seqobj_tr(so)$seqcont_tr(sc)); + + +fun singlobj_tr(Const("SeqO",_)$f) = + abs_seq' ((Const("SeqO'",dummyT)$f)$Bound 0); + + + +(* print translation for sequences *) + +fun seqcont_tr' (Bound 0) = + Const("SeqContEmp",dummyT) | + seqcont_tr' (Const("SeqO'",_)$f$s) = + Const("SeqContApp",dummyT)$ + (Const("SeqO",dummyT)$f)$ + (seqcont_tr' s) | +(* seqcont_tr' ((a as Abs(_,_,_))$s)= + seqcont_tr'(betapply(a,s)) | *) + seqcont_tr' (i$s) = + Const("SeqContApp",dummyT)$ + (Const("SeqId",dummyT)$i)$ + (seqcont_tr' s); + +fun seq_tr' s = + let fun seq_itr' (Bound 0) = + Const("SeqEmp",dummyT) | + seq_itr' (Const("SeqO'",_)$f$s) = + Const("SeqApp",dummyT)$ + (Const("SeqO",dummyT)$f)$(seqcont_tr' s) | +(* seq_itr' ((a as Abs(_,_,_))$s) = + seq_itr'(betapply(a,s)) | *) + seq_itr' (i$s) = + Const("SeqApp",dummyT)$ + (Const("SeqId",dummyT)$i)$ + (seqcont_tr' s) + in case s of + Abs(_,_,t) => seq_itr' t | + _ => s$(Bound 0) + end; + + + + +fun single_tr c [s1,s2] = + Const(c,dummyT)$seq_tr s1$singlobj_tr s2; + +fun two_seq_tr c [s1,s2] = + Const(c,dummyT)$seq_tr s1$seq_tr s2; + +fun three_seq_tr c [s1,s2,s3] = + Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3; + +fun four_seq_tr c [s1,s2,s3,s4] = + Const(c,dummyT)$seq_tr s1$seq_tr s2$seq_tr s3$seq_tr s4; + + +fun singlobj_tr'(Const("SeqO'",_)$fm) = fm | + singlobj_tr'(id) = Const("@SeqId",dummyT)$id; + + +fun single_tr' c [s1, s2] = +(Const (c, dummyT)$seq_tr' s1$seq_tr' s2 ); + + +fun two_seq_tr' c [s1, s2] = + Const (c, dummyT)$seq_tr' s1$seq_tr' s2; + +fun three_seq_tr' c [s1, s2, s3] = + Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3; + +fun four_seq_tr' c [s1, s2, s3, s4] = + Const (c, dummyT)$seq_tr' s1$seq_tr' s2$seq_tr' s3$seq_tr' s4; + + + diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/T.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/T.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,17 @@ +(* Title: Modal/T + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge +*) + +local open Modal0_rls T +in structure MP_Rule : MODAL_PROVER_RULE = + struct + val rewrite_rls = rewrite_rls + val safe_rls = safe_rls + val unsafe_rls = unsafe_rls @ [boxR,diaL] + val bound_rls = bound_rls @ [boxL,diaR] + val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2] + end +end; +structure T_Prover = Modal_ProverFun(MP_Rule); diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/T.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/T.thy Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,30 @@ +(* Title: Modal/T + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge +*) + +T = Modal0 + +rules +(* Definition of the star operation using a set of Horn clauses *) +(* For system T: gamma * == {P | []P : gamma} *) +(* delta * == {P | <>P : delta} *) + + lstar0 "|L>" + lstar1 "$G |L> $H ==> []P, $G |L> P, $H" + lstar2 "$G |L> $H ==> P, $G |L> $H" + rstar0 "|R>" + rstar1 "$G |R> $H ==> <>P, $G |R> P, $H" + rstar2 "$G |R> $H ==> P, $G |R> $H" + +(* Rules for [] and <> *) + + boxR + "[| $E |L> $E'; $F |R> $F'; $G |R> $G'; + $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G" + boxL "$E, P, $F |- $G ==> $E, []P, $F |- $G" + diaR "$E |- $F, P, $G ==> $E |- $F, <>P, $G" + diaL + "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; + $E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G" +end diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/ILL/ILL_kleene_lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/ILL/ILL_kleene_lemmas.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,81 @@ + +(* from [kleene 52] pp 118,119 *) + + +val k49a = auto1 "|- [* A > ( - ( - A)) *]"; + +val k49b = auto1 "|- [*( - ( - ( - A))) = ( - A)*]"; + +val k49c = auto1 "|- [* (A | - A) > ( - - A = A) *]"; + +val k50a = auto2 "|- [* - (A = - A) *]"; + +(* + [rtac impr_contract 1 THEN REPEAT (rtac conj_lemma 1), + res_inst_tac [("A","!((! A) -o 0)")] cut 1 + THEN rtac context1 1 + THEN ALLGOALS (best_tac power_cs)]); +*) + +val k51a = auto2 "|- [* - - (A | - A) *]"; + +val k51b = auto2 "|- [* - - (- - A > A) *]"; + +val k56a = auto1 "|- [* (A | B) > - (- A & - B) *]"; + +val k56b = auto1 "|- [* (-A | B) > - (A & -B) *]"; + +val k57a = auto1 "|- [* (A & B) > - (-A | -B) *]"; + +val k57b = auto2 "|- [* (A & -B) > -(-A | B) *]"; + +val k58a = auto1 "|- [* (A > B) > - (A & -B) *]"; + +val k58b = auto1 "|- [* (A > -B) = -(A & B) *]"; + +val k58c = auto1 "|- [* - (A & B) = (- - A > - B) *]"; + +val k58d = auto1 "|- [* (- - A > - B) = - - (-A | -B) *]"; + +val k58e = auto1 "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]"; + +val k58f = auto1 "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]"; + +val k58g = auto1 "|- [* (- -A > B) > - (A & -B) *]"; + +val k59a = auto1 "|- [* (-A | B) > (A > B) *]"; + +val k59b = auto2 "|- [* (A > B) > - - (-A | B) *]"; + +val k59c = auto2 "|- [* (-A > B) > - -(A | B) *]"; + +val k60a = auto1 "|- [* (A & B) > - (A > -B) *]"; + +val k60b = auto1 "|- [* (A & -B) > - (A > B) *]"; + +val k60c = auto1 "|- [* ( - - A & B) > - (A > -B) *]"; + +val k60d = auto1 "|- [* (- - A & - B) = - (A > B) *]"; + +val k60e = auto1 "|- [* - (A > B) = - (-A | B) *]"; + +val k60f = auto1 "|- [* - (-A | B) = - - (A & -B) *]"; + +val k60g = auto2 "|- [* - - (A > B) = - (A & -B) *]"; + +(* + [step_tac safe_cs 1, best_tac safe_cs 1, + rtac impr 1 THEN rtac impr_contract 1 + THEN best_tac safe_cs 1]; +*) + +val k60h = auto1 "|- [* - (A & -B) = (A > - -B) *]"; + +val k60i = auto1 "|- [* (A > - -B) = (- -A > - -B) *]"; + +val k61a = auto1 "|- [* (A | B) > (-A > B) *]"; + +val k61b = auto2 "|- [* - (A | B) = - (-A > B) *]"; + +val k62a = auto1 "|- [* (-A | -B) > - (A & B) *]"; + diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/ILL/ILL_predlog.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/ILL/ILL_predlog.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,9 @@ + +open ILL_predlog; + + +fun auto1 x = prove_goal thy x + (fn prems => [best_tac safe_cs 1]) ; + +fun auto2 x = prove_goal thy x + (fn prems => [best_tac power_cs 1]) ; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/ILL/ILL_predlog.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/ILL/ILL_predlog.thy Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,42 @@ +(* + File: /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy + Theory Name: pred_log + Logic Image: HOL +*) + +ILL_predlog = ILL + + +types + + plf + +arities + + plf :: logic + +consts + + "&" :: "[plf,plf] => plf" (infixr 35) + "|" :: "[plf,plf] => plf" (infixr 35) + ">" :: "[plf,plf] => plf" (infixr 35) + "=" :: "[plf,plf] => plf" (infixr 35) + "@NG" :: "plf => plf" ("- _ " [50] 55) + ff :: "plf" + + PL :: "plf => o" ("[* / _ / *]" [] 100) + + +translations + + "[* A & B *]" == "[*A*] && [*B*]" + "[* A | B *]" == "![*A*] ++ ![*B*]" + "[* - A *]" == "[*A > ff*]" + "[* ff *]" == "0" + "[* A = B *]" => "[* (A > B) & (B > A) *]" + + "[* A > B *]" == "![*A*] -o [*B*]" + +(* another translations for linear implication: + "[* A > B *]" == "!([*A*] -o [*B*])" *) + +end diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/ILL/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/ILL/ROOT.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,12 @@ + +Sequents_build_completed; (*Cause examples to fail if LK did*) + +writeln"Root file for ILL examples"; + +proof_timing := true; +time_use_thy "ex/ILL/washing"; + +time_use_thy "ex/ILL/ILL_predlog"; +time_use "ex/ILL/ILL_kleene_lemmas.ML"; + +maketest"END: Root file for ILL examples"; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/ILL/washing.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/ILL/washing.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,33 @@ + +open washing; + +(* "activate" definitions for use in proof *) + +val changeI = [context1] RL ([change] RLN (2,[cut])); +val load1I = [context1] RL ([load1] RLN (2,[cut])); +val washI = [context1] RL ([wash] RLN (2,[cut])); +val dryI = [context1] RL ([dry] RLN (2,[cut])); + + + +(* a load of dirty clothes and two dollars gives you clean clothes *) + +goal thy "dollar , dollar , dirty |- clean"; + +by (best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1); + + +(* order of premises doesn't matter *) + +prove_goal thy "dollar , dirty , dollar |- clean" +(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]); + + +(* alternative formulation *) + +prove_goal thy "dollar , dollar |- dirty -o clean" +(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]); + + + + diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/ILL/washing.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/ILL/washing.thy Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,33 @@ + + +(* code by Sara Kalvala, based on Paulson's LK + and Moore's tisl.ML *) + +washing = ILL + + +consts + +dollar,quarter,loaded,dirty,wet,clean :: "o" + + +rules + + + change + "dollar |- (quarter >< quarter >< quarter >< quarter)" + + load1 + "quarter , quarter , quarter , quarter , quarter |- loaded" + + load2 + "dollar , quarter |- loaded" + + wash + "loaded , dirty |- wet" + + dry + "wet, quarter , quarter , quarter |- clean" + +end + + \ No newline at end of file diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/LK/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/LK/ROOT.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,18 @@ +(* Title: LK/ex/ROOT + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Executes all examples for Classical Logic. +*) + +Sequents_build_completed; (*Cause examples to fail if LK did*) + +writeln"Root file for LK examples"; + +proof_timing := true; +time_use "ex/LK/prop.ML"; +time_use "ex/LK/quant.ML"; +time_use "ex/LK/hardquant.ML"; + +maketest"END: Root file for LK examples"; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/LK/hardquant.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/LK/hardquant.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,278 @@ +(* Title: LK/ex/hard-quant + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Hard examples with quantifiers. Can be read to test the LK system. +From F. J. Pelletier, + Seventy-Five Problems for Testing Automatic Theorem Provers, + J. Automated Reasoning 2 (1986), 191-216. + Errata, JAR 4 (1988), 236-236. + +Uses pc_tac rather than fast_tac when the former is significantly faster. +*) + +writeln"File LK/ex/hard-quant."; + +goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; +by (fast_tac LK_pack 1); +result(); + +goal LK.thy "|- (EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))"; +by (fast_tac LK_pack 1); +result(); + +goal LK.thy "|- (EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q"; +by (fast_tac LK_pack 1); +result(); + +goal LK.thy "|- (ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problems requiring quantifier duplication"; + +(*Not provable by fast_tac LK_pack: needs multiple instantiation of ALL*) +goal LK.thy "|- (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; +by (best_tac LK_dup_pack 1); +result(); + +(*Needs double instantiation of the quantifier*) +goal LK.thy "|- EX x. P(x) --> P(a) & P(b)"; +by (fast_tac LK_dup_pack 1); +result(); + +goal LK.thy "|- EX z. P(z) --> (ALL x. P(x))"; +by (best_tac LK_dup_pack 1); +result(); + +writeln"Hard examples with quantifiers"; + +writeln"Problem 18"; +goal LK.thy "|- EX y. ALL x. P(y)-->P(x)"; +by (best_tac LK_dup_pack 1); +result(); + +writeln"Problem 19"; +goal LK.thy "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"; +by (best_tac LK_dup_pack 1); +result(); + +writeln"Problem 20"; +goal LK.thy "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \ +\ --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 21"; +goal LK.thy "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"; +by (best_tac LK_dup_pack 1); +result(); + +writeln"Problem 22"; +goal LK.thy "|- (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 23"; +goal LK.thy "|- (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))"; +by (best_tac LK_pack 1); +result(); + +writeln"Problem 24"; +goal LK.thy "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ +\ ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x)) \ +\ --> (EX x. P(x)&R(x))"; +by (pc_tac LK_pack 1); +result(); + +writeln"Problem 25"; +goal LK.thy "|- (EX x. P(x)) & \ +\ (ALL x. L(x) --> ~ (M(x) & R(x))) & \ +\ (ALL x. P(x) --> (M(x) & L(x))) & \ +\ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \ +\ --> (EX x. Q(x)&P(x))"; +by (best_tac LK_pack 1); +result(); + +writeln"Problem 26"; +goal LK.thy "|- ((EX x. p(x)) <-> (EX x. q(x))) & \ +\ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \ +\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"; +by (pc_tac LK_pack 1); +result(); + +writeln"Problem 27"; +goal LK.thy "|- (EX x. P(x) & ~Q(x)) & \ +\ (ALL x. P(x) --> R(x)) & \ +\ (ALL x. M(x) & L(x) --> P(x)) & \ +\ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \ +\ --> (ALL x. M(x) --> ~L(x))"; +by (pc_tac LK_pack 1); +result(); + +writeln"Problem 28. AMENDED"; +goal LK.thy "|- (ALL x. P(x) --> (ALL x. Q(x))) & \ +\ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \ +\ ((EX x.S(x)) --> (ALL x. L(x) --> M(x))) \ +\ --> (ALL x. P(x) & L(x) --> M(x))"; +by (pc_tac LK_pack 1); +result(); + +writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; +goal LK.thy "|- (EX x. P(x)) & (EX y. Q(y)) \ +\ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \ +\ (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"; +by (pc_tac LK_pack 1); +result(); + +writeln"Problem 30"; +goal LK.thy "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \ +\ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \ +\ --> (ALL x. S(x))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 31"; +goal LK.thy "|- ~(EX x.P(x) & (Q(x) | R(x))) & \ +\ (EX x. L(x) & P(x)) & \ +\ (ALL x. ~ R(x) --> M(x)) \ +\ --> (EX x. L(x) & M(x))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 32"; +goal LK.thy "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \ +\ (ALL x. S(x) & R(x) --> L(x)) & \ +\ (ALL x. M(x) --> R(x)) \ +\ --> (ALL x. P(x) & M(x) --> L(x))"; +by (best_tac LK_pack 1); +result(); + +writeln"Problem 33"; +goal LK.thy "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> \ +\ (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 34 AMENDED (TWICE!!) NOT PROVED AUTOMATICALLY"; +(*Andrews's challenge*) +goal LK.thy "|- ((EX x. ALL y. p(x) <-> p(y)) <-> \ +\ ((EX x. q(x)) <-> (ALL y. p(y)))) <-> \ +\ ((EX x. ALL y. q(x) <-> q(y)) <-> \ +\ ((EX x. p(x)) <-> (ALL y. q(y))))"; +by (safe_goal_tac LK_pack 1); (*53 secs*) (*13 secs*) +by (TRYALL (fast_tac LK_pack)); (*165 secs*) (*117 secs*) (*138 secs*) +(*for some reason, pc_tac leaves 14 subgoals instead of 6*) +by (TRYALL (best_tac LK_dup_pack)); (*55 secs*) (*29 secs*) (*54 secs*) +result(); + + +writeln"Problem 35"; +goal LK.thy "|- EX x y. P(x,y) --> (ALL u v. P(u,v))"; +by (best_tac LK_dup_pack 1); (*27 secs??*) +result(); + +writeln"Problem 36"; +goal LK.thy "|- (ALL x. EX y. J(x,y)) & \ +\ (ALL x. EX y. G(x,y)) & \ +\ (ALL x y. J(x,y) | G(x,y) --> \ +\ (ALL z. J(y,z) | G(y,z) --> H(x,z))) \ +\ --> (ALL x. EX y. H(x,y))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 37"; +goal LK.thy "|- (ALL z. EX w. ALL x. EX y. \ +\ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \ +\ (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \ +\ ((EX x y. Q(x,y)) --> (ALL x. R(x,x))) \ +\ --> (ALL x. EX y. R(x,y))"; +by (pc_tac LK_pack 1); +result(); + +writeln"Problem 38"; +goal LK.thy + "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) --> \ +\ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <-> \ +\ (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) & \ +\ (~p(a) | ~(EX y. p(y) & r(x,y)) | \ +\ (EX z. EX w. p(z) & r(x,w) & r(w,z))))"; +by (pc_tac LK_pack 1); +result(); + +writeln"Problem 39"; +goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 40. AMENDED"; +goal LK.thy "|- (EX y. ALL x. F(x,y) <-> F(x,x)) --> \ +\ ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 41"; +goal LK.thy "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) \ +\ --> ~ (EX z. ALL x. f(x,z))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 42"; +goal LK.thy "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))"; + +writeln"Problem 43 NOT PROVED AUTOMATICALLY"; +goal LK.thy "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \ +\ --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))"; + +writeln"Problem 44"; +goal LK.thy "|- (ALL x. f(x) --> \ +\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ +\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \ +\ --> (EX x. j(x) & ~f(x))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 45"; +goal LK.thy "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y)) \ +\ --> (ALL y. g(y) & h(x,y) --> k(y))) & \ +\ ~ (EX y. l(y) & k(y)) & \ +\ (EX x. f(x) & (ALL y. h(x,y) --> l(y)) \ +\ & (ALL y. g(y) & h(x,y) --> j(x,y))) \ +\ --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))"; +by (best_tac LK_pack 1); +result(); + + +writeln"Problem 50"; +goal LK.thy + "|- (ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))"; +by (best_tac LK_dup_pack 1); +result(); + +writeln"Problem 57"; +goal LK.thy + "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \ +\ (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Problem 59"; +(*Unification works poorly here -- the abstraction %sobj prevents efficient + operation of the occurs check*) +Unify.trace_bound := !Unify.search_bound - 1; +goal LK.thy "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"; +by (best_tac LK_dup_pack 1); +result(); + +writeln"Problem 60"; +goal LK.thy + "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Reached end of file."; + +(*18 June 92: loaded in 372 secs*) +(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*) +(*29 June 92: loaded in 370 secs*) diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/LK/prop.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/LK/prop.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,194 @@ +(* Title: LK/ex/prop + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Classical sequent calculus: examples with propositional connectives +Can be read to test the LK system. +*) + +writeln"LK/ex/prop: propositional examples"; + +writeln"absorptive laws of & and | "; + +goal LK.thy "|- P & P <-> P"; +by (fast_tac prop_pack 1); +result(); + +goal LK.thy "|- P | P <-> P"; +by (fast_tac prop_pack 1); +result(); + +writeln"commutative laws of & and | "; + +goal LK.thy "|- P & Q <-> Q & P"; +by (fast_tac prop_pack 1); +result(); + +goal LK.thy "|- P | Q <-> Q | P"; +by (fast_tac prop_pack 1); +result(); + + +writeln"associative laws of & and | "; + +goal LK.thy "|- (P & Q) & R <-> P & (Q & R)"; +by (fast_tac prop_pack 1); +result(); + +goal LK.thy "|- (P | Q) | R <-> P | (Q | R)"; +by (fast_tac prop_pack 1); +result(); + +writeln"distributive laws of & and | "; +goal LK.thy "|- (P & Q) | R <-> (P | R) & (Q | R)"; +by (fast_tac prop_pack 1); +result(); + +goal LK.thy "|- (P | Q) & R <-> (P & R) | (Q & R)"; +by (fast_tac prop_pack 1); +result(); + +writeln"Laws involving implication"; + +goal LK.thy "|- (P|Q --> R) <-> (P-->R) & (Q-->R)"; +by (fast_tac prop_pack 1); +result(); + +goal LK.thy "|- (P & Q --> R) <-> (P--> (Q-->R))"; +by (fast_tac prop_pack 1); +result(); + + +goal LK.thy "|- (P --> Q & R) <-> (P-->Q) & (P-->R)"; +by (fast_tac prop_pack 1); +result(); + + +writeln"Classical theorems"; + +goal LK.thy "|- P|Q --> P| ~P&Q"; +by (fast_tac prop_pack 1); +result(); + + +goal LK.thy "|- (P-->Q)&(~P-->R) --> (P&Q | R)"; +by (fast_tac prop_pack 1); +result(); + + +goal LK.thy "|- P&Q | ~P&R <-> (P-->Q)&(~P-->R)"; +by (fast_tac prop_pack 1); +result(); + + +goal LK.thy "|- (P-->Q) | (P-->R) <-> (P --> Q | R)"; +by (fast_tac prop_pack 1); +result(); + + +(*If and only if*) + +goal LK.thy "|- (P<->Q) <-> (Q<->P)"; +by (fast_tac prop_pack 1); +result(); + +goal LK.thy "|- ~ (P <-> ~P)"; +by (fast_tac prop_pack 1); +result(); + + +(*Sample problems from + F. J. Pelletier, + Seventy-Five Problems for Testing Automatic Theorem Provers, + J. Automated Reasoning 2 (1986), 191-216. + Errata, JAR 4 (1988), 236-236. +*) + +(*1*) +goal LK.thy "|- (P-->Q) <-> (~Q --> ~P)"; +by (fast_tac prop_pack 1); +result(); + +(*2*) +goal LK.thy "|- ~ ~ P <-> P"; +by (fast_tac prop_pack 1); +result(); + +(*3*) +goal LK.thy "|- ~(P-->Q) --> (Q-->P)"; +by (fast_tac prop_pack 1); +result(); + +(*4*) +goal LK.thy "|- (~P-->Q) <-> (~Q --> P)"; +by (fast_tac prop_pack 1); +result(); + +(*5*) +goal LK.thy "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))"; +by (fast_tac prop_pack 1); +result(); + +(*6*) +goal LK.thy "|- P | ~ P"; +by (fast_tac prop_pack 1); +result(); + +(*7*) +goal LK.thy "|- P | ~ ~ ~ P"; +by (fast_tac prop_pack 1); +result(); + +(*8. Peirce's law*) +goal LK.thy "|- ((P-->Q) --> P) --> P"; +by (fast_tac prop_pack 1); +result(); + +(*9*) +goal LK.thy "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; +by (fast_tac prop_pack 1); +result(); + +(*10*) +goal LK.thy "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q"; +by (fast_tac prop_pack 1); +result(); + +(*11. Proved in each direction (incorrectly, says Pelletier!!) *) +goal LK.thy "|- P<->P"; +by (fast_tac prop_pack 1); +result(); + +(*12. "Dijkstra's law"*) +goal LK.thy "|- ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"; +by (fast_tac prop_pack 1); +result(); + +(*13. Distributive law*) +goal LK.thy "|- P | (Q & R) <-> (P | Q) & (P | R)"; +by (fast_tac prop_pack 1); +result(); + +(*14*) +goal LK.thy "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))"; +by (fast_tac prop_pack 1); +result(); + + +(*15*) +goal LK.thy "|- (P --> Q) <-> (~P | Q)"; +by (fast_tac prop_pack 1); +result(); + +(*16*) +goal LK.thy "|- (P-->Q) | (Q-->P)"; +by (fast_tac prop_pack 1); +result(); + +(*17*) +goal LK.thy "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"; +by (fast_tac prop_pack 1); +result(); + +writeln"Reached end of file."; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/LK/quant.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/LK/quant.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,160 @@ +(* Title: LK/ex/quant + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Classical sequent calculus: examples with quantifiers. +*) + + +writeln"LK/ex/quant: Examples with quantifiers"; + +goal LK.thy "|- (ALL x. P) <-> P"; +by (fast_tac LK_pack 1); +result(); + +goal LK.thy "|- (ALL x y.P(x,y)) <-> (ALL y x.P(x,y))"; +by (fast_tac LK_pack 1); +result(); + +goal LK.thy "ALL u.P(u), ALL v.Q(v) |- ALL u v. P(u) & Q(v)"; +by (fast_tac LK_pack 1); +result(); + +writeln"Permutation of existential quantifier."; +goal LK.thy "|- (EX x y.P(x,y)) <-> (EX y x.P(x,y))"; +by (fast_tac LK_pack 1); +result(); + +goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))"; +by (fast_tac LK_pack 1); +result(); + + +(*Converse is invalid*) +goal LK.thy "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))"; +by (fast_tac LK_pack 1); +result(); + + +writeln"Pushing ALL into an implication."; +goal LK.thy "|- (ALL x. P --> Q(x)) <-> (P --> (ALL x. Q(x)))"; +by (fast_tac LK_pack 1); +result(); + + +goal LK.thy "|- (ALL x.P(x)-->Q) <-> ((EX x.P(x)) --> Q)"; +by (fast_tac LK_pack 1); +result(); + + +goal LK.thy "|- (EX x. P) <-> P"; +by (fast_tac LK_pack 1); +result(); + + +writeln"Distribution of EX over disjunction."; +goal LK.thy "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"; +by (fast_tac LK_pack 1); +result(); +(*5 secs*) + +(*Converse is invalid*) +goal LK.thy "|- (EX x. P(x) & Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"; +by (fast_tac LK_pack 1); +result(); + + +writeln"Harder examples: classical theorems."; + +goal LK.thy "|- (EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))"; +by (fast_tac LK_pack 1); +result(); +(*3 secs*) + + +goal LK.thy "|- (EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q"; +by (fast_tac LK_pack 1); +result(); +(*5 secs*) + + +goal LK.thy "|- (ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)"; +by (fast_tac LK_pack 1); +result(); + + +writeln"Basic test of quantifier reasoning"; +goal LK.thy + "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; +by (fast_tac LK_pack 1); +result(); + + +goal LK.thy "|- (ALL x. Q(x)) --> (EX x. Q(x))"; +by (fast_tac LK_pack 1); +result(); + + +writeln"The following are invalid!"; + +(*INVALID*) +goal LK.thy "|- (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"; +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; +(*Check that subgoals remain: proof failed.*) +getgoal 1; + +(*INVALID*) +goal LK.thy "|- (EX x. Q(x)) --> (ALL x. Q(x))"; +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; +getgoal 1; + +goal LK.thy "|- P(?a) --> (ALL x.P(x))"; +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; +(*Check that subgoals remain: proof failed.*) +getgoal 1; + +goal LK.thy "|- (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))"; +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; +getgoal 1; + + +writeln"Back to things that are provable..."; + +goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))"; +by (fast_tac LK_pack 1); +result(); + +(*An example of why exR should be delayed as long as possible*) +goal LK.thy "|- (P--> (EX x.Q(x))) & P--> (EX x.Q(x))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Solving for a Var"; +goal LK.thy + "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"; +by (fast_tac LK_pack 1); +result(); + + +writeln"Principia Mathematica *11.53"; +goal LK.thy + "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"; +by (fast_tac LK_pack 1); +result(); + + +writeln"Principia Mathematica *11.55"; +goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y.Q(x,y)))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Principia Mathematica *11.61"; +goal LK.thy + "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"; +by (fast_tac LK_pack 1); +result(); + +writeln"Reached end of file."; + +(*21 August 88: loaded in 45.7 secs*) diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/Modal/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/Modal/ROOT.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,28 @@ +(* Title: Modal/ex/ROOT + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge +*) + +Sequents_build_completed; (*Cause examples to fail if Modal did*) + +proof_timing := true; + +writeln "\nTheorems of T\n"; +fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2])); +time_use "ex/Modal/Tthms.ML"; + +writeln "\nTheorems of S4\n"; +fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2])); +time_use "ex/Modal/Tthms.ML"; +time_use "ex/Modal/S4thms.ML"; + +writeln "\nTheorems of S43\n"; +fun try s = (writeln s; + prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE + S43_Prover.solve_tac 3])); +time_use "ex/Modal/Tthms.ML"; +time_use "ex/Modal/S4thms.ML"; +time_use "ex/Modal/S43thms.ML"; + +maketest"END: Root file for Modal examples"; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/Modal/S43thms.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/Modal/S43thms.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,49 @@ +(* Title: 91/Modal/ex/S43thms + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge +*) + +(* Theorems of system S43 *) + +try "|- <>[]P --> []<>P"; +try "|- <>[]P --> [][]<>P"; +try "|- [](<>P | <>Q) --> []<>P | []<>Q"; +try "|- <>[]P & <>[]Q --> <>([]P & []Q)"; +try "|- []([]P --> []Q) | []([]Q --> []P)"; +try "|- [](<>P --> <>Q) | [](<>Q --> <>P)"; +try "|- []([]P --> Q) | []([]Q --> P)"; +try "|- [](P --> <>Q) | [](Q --> <>P)"; +try "|- [](P --> []Q-->R) | [](P | ([]R --> Q))"; +try "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)"; +try "|- []([]P | Q) & [](P | []Q) --> []P | []Q"; +try "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)"; +try "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q"; +try "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)"; +try "|- <>[]<>P <-> []<>P"; +try "|- []<>[]P <-> <>[]P"; + +(* These are from Hailpern, LNCS 129 *) + +try "|- [](P & Q) <-> []P & []Q"; +try "|- <>(P | Q) <-> <>P | <>Q"; +try "|- <>(P --> Q) <-> []P --> <>Q"; + +try "|- [](P --> Q) --> <>P --> <>Q"; +try "|- []P --> []<>P"; +try "|- <>[]P --> <>P"; +try "|- []<>[]P --> []<>P"; +try "|- <>[]P --> <>[]<>P"; +try "|- <>[]P --> []<>P"; +try "|- []<>[]P <-> <>[]P"; +try "|- <>[]<>P <-> []<>P"; + +try "|- []P | []Q --> [](P | Q)"; +try "|- <>(P & Q) --> <>P & <>Q"; +try "|- [](P | Q) --> []P | <>Q"; +try "|- <>P & []Q --> <>(P & Q)"; +try "|- [](P | Q) --> <>P | []Q"; +try "|- [](P | Q) --> []<>P | []<>Q"; +try "|- <>[]P & <>[]Q --> <>(P & Q)"; +try "|- <>[](P & Q) <-> <>[]P & <>[]Q"; +try "|- []<>(P | Q) <-> []<>P | []<>Q"; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/Modal/S4thms.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/Modal/S4thms.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,40 @@ +(* Title: 91/Modal/ex/S4thms + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge +*) + +(* Theorems of system S4 from Hughes and Cresswell, p.46 *) + +try "|- []A --> A"; (* refexivity *) +try "|- []A --> [][]A"; (* transitivity *) +try "|- []A --> <>A"; (* seriality *) +try "|- <>[](<>A --> []<>A)"; +try "|- <>[](<>[]A --> []A)"; +try "|- []P <-> [][]P"; +try "|- <>P <-> <><>P"; +try "|- <>[]<>P --> <>P"; +try "|- []<>P <-> []<>[]<>P"; +try "|- <>[]P <-> <>[]<>[]P"; + +(* Theorems for system S4 from Hughes and Cresswell, p.60 *) + +try "|- []P | []Q <-> []([]P | []Q)"; +try "|- ((P>- ((P>- []P & []Q"; +try "|- <>(P | Q) <-> <>P | <>Q"; +try "|- <>(P --> Q) <-> ([]P --> <>Q)"; + +try "|- [](P --> Q) --> (<>P --> <>Q)"; +try "|- []P --> []<>P"; +try "|- <>[]P --> <>P"; + +try "|- []P | []Q --> [](P | Q)"; +try "|- <>(P & Q) --> <>P & <>Q"; +try "|- [](P | Q) --> []P | <>Q"; +try "|- <>P & []Q --> <>(P & Q)"; +try "|- [](P | Q) --> <>P | []Q"; + diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/Modal/Tthms.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/Modal/Tthms.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,31 @@ +(* Title: 91/Modal/ex/Tthms + ID: $Id$ + Author: Martin Coen + Copyright 1991 University of Cambridge +*) + +(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) + +try "|- []P --> P"; +try "|- [](P-->Q) --> ([]P-->[]Q)"; (* normality*) +try "|- (P-- []P --> []Q"; +try "|- P --> <>P"; + +try "|- [](P & Q) <-> []P & []Q"; +try "|- <>(P | Q) <-> <>P | <>Q"; +try "|- [](P<->Q) <-> (P>-(P-->Q) <-> ([]P--><>Q)"; +try "|- []P <-> ~<>(~P)"; +try "|- [](~P) <-> ~<>P"; +try "|- ~[]P <-> <>(~P)"; +try "|- [][]P <-> ~<><>(~P)"; +try "|- ~<>(P | Q) <-> ~<>P & ~<>Q"; + +try "|- []P | []Q --> [](P | Q)"; +try "|- <>(P & Q) --> <>P & <>Q"; +try "|- [](P | Q) --> []P | <>Q"; +try "|- <>P & []Q --> <>(P & Q)"; +try "|- [](P | Q) --> <>P | []Q"; +try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)"; +try "|- (P-- (P-- <>Q --> <>(P & Q)"; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/ex/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/ex/ROOT.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,4 @@ + +use "ex/LK/ROOT.ML"; +use "ex/ILL/ROOT.ML"; +use "ex/Modal/ROOT.ML"; diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/index.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/index.html Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,15 @@ +Isabelle/Sequents +

Isabelle/Sequents

+The name of every theory is linked to its theory file
+\/ stands for subtheories (child theories)
+/\ stands for supertheories (parent theories)

+Back to the index of Isabelle logics +
View the ReadMe file. +

\//\ Sequents
+\//\ LK
+\//\ ILL
+\//\ Modal0
+\//\ T
+\//\ S4
+\//\ S43
+ \ No newline at end of file diff -r 6ac12b9478d5 -r fb0655539d05 src/Sequents/prover.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Sequents/prover.ML Wed Oct 09 13:32:33 1996 +0200 @@ -0,0 +1,223 @@ +(* Title: LK/LK.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge +*) + + +(**** Theorem Packs ****) + +(* based largely on LK *) + +datatype pack = Pack of thm list * thm list; + +(*A theorem pack has the form (safe rules, unsafe rules) + An unsafe rule is incomplete or introduces variables in subgoals, + and is tried only when the safe rules are not applicable. *) + +fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2); + +val empty_pack = Pack([],[]); + +infix 4 add_safes add_unsafes; + +fun (Pack(safes,unsafes)) add_safes ths = + Pack(sort less (ths@safes), unsafes); + +fun (Pack(safes,unsafes)) add_unsafes ths = + Pack(safes, sort less (ths@unsafes)); + + +(*Returns the list of all formulas in the sequent*) +fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u + | forms_of_seq (H $ u) = forms_of_seq u + | forms_of_seq _ = []; + +(*Tests whether two sequences (left or right sides) could be resolved. + seqp is a premise (subgoal), seqc is a conclusion of an object-rule. + Assumes each formula in seqc is surrounded by sequence variables + -- checks that each concl formula looks like some subgoal formula. + It SHOULD check order as well, using recursion rather than forall/exists*) +fun could_res (seqp,seqc) = + forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) + (forms_of_seq seqp)) + (forms_of_seq seqc); + + +(*Tests whether two sequents or pairs of sequents could be resolved*) +fun could_resolve_seq (prem,conc) = + case (prem,conc) of + (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp), + _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) => + could_res (leftp,leftc) andalso could_res (rightp,rightc) + | (_ $ Abs(_,_,leftp) $ rightp, + _ $ Abs(_,_,leftc) $ rightc) => + could_res (leftp,leftc) andalso could_unify (rightp,rightc) + | _ => false; + + +(*Like filt_resolve_tac, using could_resolve_seq + Much faster than resolve_tac when there are many rules. + Resolve subgoal i using the rules, unless more than maxr are compatible. *) +fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) => + let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules) + in if length rls > maxr then no_tac + else (*((rtac derelict 1 THEN rtac impl 1 + THEN (rtac identity 2 ORELSE rtac ll_mp 2) + THEN rtac context1 1) + ORELSE *) resolve_tac rls i + end); + + +(*Predicate: does the rule have n premises? *) +fun has_prems n rule = (nprems_of rule = n); + +(*Continuation-style tactical for resolution. + The list of rules is partitioned into 0, 1, 2 premises. + The resulting tactic, gtac, tries to resolve with rules. + If successful, it recursively applies nextac to the new subgoals only. + Else fails. (Treatment of goals due to Ph. de Groote) + Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *) + +(*Takes rule lists separated in to 0, 1, 2, >2 premises. + The abstraction over state prevents needless divergence in recursion. + The 9999 should be a parameter, to delay treatment of flexible goals. *) + +fun RESOLVE_THEN rules = + let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules; + fun tac nextac i = STATE (fn state => + filseq_resolve_tac rls0 9999 i + ORELSE + (DETERM(filseq_resolve_tac rls1 9999 i) THEN TRY(nextac i)) + ORELSE + (DETERM(filseq_resolve_tac rls2 9999 i) THEN TRY(nextac(i+1)) + THEN TRY(nextac i)) ) + in tac end; + + + +(*repeated resolution applied to the designated goal*) +fun reresolve_tac rules = + let val restac = RESOLVE_THEN rules; (*preprocessing done now*) + fun gtac i = restac gtac i + in gtac end; + +(*tries the safe rules repeatedly before the unsafe rules. *) +fun repeat_goal_tac (Pack(safes,unsafes)) = + let val restac = RESOLVE_THEN safes + and lastrestac = RESOLVE_THEN unsafes; + fun gtac i = restac gtac i ORELSE (print_tac THEN lastrestac gtac i) + in gtac end; + + +(*Tries safe rules only*) +fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes; + +(*Tries a safe rule or else a unsafe rule. Single-step for tracing. *) +fun step_tac (thm_pack as Pack(safes,unsafes)) = + safe_goal_tac thm_pack ORELSE' + filseq_resolve_tac unsafes 9999; + + +(* Tactic for reducing a goal, using Predicate Calculus rules. + A decision procedure for Propositional Calculus, it is incomplete + for Predicate-Calculus because of allL_thin and exR_thin. + Fails if it can do nothing. *) +fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1)); + + +(*The following two tactics are analogous to those provided by + Provers/classical. In fact, pc_tac is usually FASTER than fast_tac!*) +fun fast_tac thm_pack = + SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1)); + +fun best_tac thm_pack = + SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) + (step_tac thm_pack 1)); + + + +signature MODAL_PROVER_RULE = +sig + val rewrite_rls : thm list + val safe_rls : thm list + val unsafe_rls : thm list + val bound_rls : thm list + val aside_rls : thm list +end; + +signature MODAL_PROVER = +sig + val rule_tac : thm list -> int ->tactic + val step_tac : int -> tactic + val solven_tac : int -> int -> tactic + val solve_tac : int -> tactic +end; + +functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = +struct +local open Modal_Rule +in + +(*Returns the list of all formulas in the sequent*) +fun forms_of_seq (Const("SeqO",_) $ P $ u) = P :: forms_of_seq u + | forms_of_seq (H $ u) = forms_of_seq u + | forms_of_seq _ = []; + +(*Tests whether two sequences (left or right sides) could be resolved. + seqp is a premise (subgoal), seqc is a conclusion of an object-rule. + Assumes each formula in seqc is surrounded by sequence variables + -- checks that each concl formula looks like some subgoal formula.*) +fun could_res (seqp,seqc) = + forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) + (forms_of_seq seqp)) + (forms_of_seq seqc); + +(*Tests whether two sequents G|-H could be resolved, comparing each side.*) +fun could_resolve_seq (prem,conc) = + case (prem,conc) of + (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp), + _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) => + could_res (leftp,leftc) andalso could_res (rightp,rightc) + | _ => false; + +(*Like filt_resolve_tac, using could_resolve_seq + Much faster than resolve_tac when there are many rules. + Resolve subgoal i using the rules, unless more than maxr are compatible. *) +fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) => + let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules) + in if length rls > maxr then no_tac else resolve_tac rls i + end); + +fun fresolve_tac rls n = filseq_resolve_tac rls 999 n; + +(* NB No back tracking possible with aside rules *) + +fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n)); +fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n; + +val fres_safe_tac = fresolve_tac safe_rls; +val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac; +val fres_bound_tac = fresolve_tac bound_rls; + +fun UPTOGOAL n tf = let fun tac i = if i tac(nprems_of state)) end; + +(* Depth first search bounded by d *) +fun solven_tac d n = STATE (fn state => + if d<0 then no_tac + else if (nprems_of state = 0) then all_tac + else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE + ((fres_unsafe_tac n THEN UPTOGOAL n (solven_tac d)) APPEND + (fres_bound_tac n THEN UPTOGOAL n (solven_tac (d-1))))); + +fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1; + +fun step_tac n = STATE (fn state => + if (nprems_of state = 0) then all_tac + else (DETERM(fres_safe_tac n)) ORELSE + (fres_unsafe_tac n APPEND fres_bound_tac n)); + +end; +end;