--- a/src/Modal/Makefile Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (Modal) #
-# #
-#########################################################################
-
-#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 LK 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)
-FILES = ROOT.ML Modal0.thy prover.ML T.thy S4.thy S43.thy
-EX_FILES = ex/ROOT.ML ex/S43thms.ML ex/S4thms.ML ex/Tthms.ML
-
-#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/Modal: $(BIN)/LK $(FILES)
- case "$(COMP)" in \
- poly*) cp $(BIN)/LK $(BIN)/Modal;\
- if [ "$${MAKE_HTML}" = "true" ]; \
- then echo 'open PolyML; make_html := true; exit_use_dir".";' \
- | $(COMP) $(BIN)/Modal;\
- elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
- then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/Modal;\
- else echo 'open PolyML; exit_use_dir".";' \
- | $(COMP) $(BIN)/Modal;\
- fi;\
- discgarb -c $(BIN)/Modal;;\
- sml*) if [ "$${MAKE_HTML}" = "true" ]; \
- then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/Modal" banner;' | $(BIN)/LK;\
- elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
- then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/Modal" banner;' \
- | $(BIN)/LK;\
- else echo 'exit_use_dir"."; xML"$(BIN)/Modal" banner;' \
- | $(BIN)/LK;\
- fi;;\
- *) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
- esac
-
-$(BIN)/LK:
- cd ../LK; $(MAKE)
-
-test: ex/ROOT.ML $(BIN)/Modal $(EX_FILES)
- case "$(COMP)" in \
- poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/Modal ;;\
- sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Modal;;\
- *) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
- esac
-
-.PRECIOUS: $(BIN)/LK $(BIN)/Modal
--- a/src/Modal/Modal0.thy Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(* Title: 91/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" :: "[sequence,sequence]=>prop" ("(_)|L>(_)" [6,6] 5)
- "@Rstar" :: "[sequence,sequence]=>prop" ("(_)|R>(_)" [6,6] 5)
- Lstar,Rstar :: "[sobj=>sobj,sobj=>sobj]=>prop"
-
-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)$LK.seq_tr1 s1$LK.seq_tr1 s2;
- fun star_tr' c [Abs(_,_,s1),Abs(_,_,s2)] =
- Const(c,dummyT) $ LK.seq_tr1' s1 $ LK.seq_tr1' 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;
--- a/src/Modal/README.html Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-<HTML><HEAD><TITLE>Modal/ReadMe</TITLE></HEAD><BODY>
-
-<H2>Modal: First-Order Modal Sequent Calculus</H2>
-
-This directory contains the Standard ML sources of the Isabelle system for
-Modal Logic. Important files include
-
-<DL>
-<DT>ROOT.ML
-<DD>loads all source files. Enter an ML image containing LK
-Isabelle and type: use "ROOT.ML";<P>
-
-<DT>ex
-<DD>subdirectory containing examples. Files Tthms.ML, S4thms.ML and
-S43thms.ML contain the theorems of Modal Logics, so arranged since
-T<S4<S43. To execute them, enter an ML image containing Modal
-and type: use "ex/ROOT.ML";
-</DL>
-
-Thanks to Rajeev Gore' for supplying the inference system for S43.<P>
-
-Useful references on Modal Logics:
-
-<UL>
-<LI>Melvin C Fitting,<BR>
- Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
-<LI>Lincoln A. Wallen,<BR>
- Automated Deduction in Nonclassical Logics (MIT Press, 1990)
-</UL>
-</BODY></HTML>
--- a/src/Modal/ROOT.ML Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-(* Title: 91/Modal/ROOT
- ID: $Id$
- Author: Martin Coen
- Copyright 1991 University of Cambridge
-*)
-
-val banner = "Modal Logic (over LK)";
-writeln banner;
-
-use_thy "Modal0";
-
-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;
-
-use "prover.ML";
-
-use_thy"T";
-
-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);
-
-use_thy"S4";
-
-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);
-
-use_thy"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);
-
-val Modal_build_completed = (); (*indicate successful build*)
-
-(*printing functions are inherited from LK*)
--- a/src/Modal/S4.thy Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* Title: 91/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
--- a/src/Modal/S43.thy Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-(* Title: 91/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 :: "[sobj=>sobj, sobj=>sobj, sobj=>sobj,
- sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop"
- "@S43pi" :: "[sequence, sequence, sequence, sequence, sequence,
- sequence] => 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 k<j<=k+m *)
-
- S43pi0 "S43pi $L;; $R;; $Lbox; $Rdia"
- S43pi1
- "[| (S43pi <>P,$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 = LK.seq_tr1;
- val tr' = LK.seq_tr1';
-
- 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'[Abs(_,_,s1),Abs(_,_,s2),Abs(_,_,s3),
- Abs(_,_,s4),Abs(_,_,s5),Abs(_,_,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
--- a/src/Modal/T.thy Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: 91/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
--- a/src/Modal/ex/ROOT.ML Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: Modal/ex/ROOT
- ID: $Id$
- Author: Martin Coen
- Copyright 1991 University of Cambridge
-*)
-
-Modal_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/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/Tthms.ML";
-time_use "ex/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/Tthms.ML";
-time_use "ex/S4thms.ML";
-time_use "ex/S43thms.ML";
-
-maketest"END: Root file for Modal examples";
--- a/src/Modal/ex/S43thms.ML Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(* 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";
--- a/src/Modal/ex/S4thms.ML Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(* 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>-<Q) --< R) --> ((P>-<Q) --< []R)";
-
-(* 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 | []Q --> [](P | Q)";
-try "|- <>(P & Q) --> <>P & <>Q";
-try "|- [](P | Q) --> []P | <>Q";
-try "|- <>P & []Q --> <>(P & Q)";
-try "|- [](P | Q) --> <>P | []Q";
-
--- a/src/Modal/ex/Tthms.ML Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* 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--<Q) --> []P --> []Q";
-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 <-> ~<>(~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--<Q) & (Q--<R) --> (P--<R)";
-try "|- []P --> <>Q --> <>(P & Q)";
--- a/src/Modal/prover.ML Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-(* Title: 91/Modal/prover
- ID: $Id$
- Author: Martin Coen
- Copyright 1991 University of Cambridge
-*)
-
-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("Seqof",_) $ 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<n then all_tac
- else tf(i) THEN tac(i-1)
- in STATE(fn state=> 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;