# HG changeset patch # User paulson # Date 844938828 -7200 # Node ID 80ef03e390581d9b9c7d620db149563ea641bf86 # Parent bcc9cbed10b1d2009aafe6884dc09accd952b306 Removed Modal since Sequents contains everything in it diff -r bcc9cbed10b1 -r 80ef03e39058 src/Modal/Makefile --- 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 diff -r bcc9cbed10b1 -r 80ef03e39058 src/Modal/Modal0.thy --- 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; diff -r bcc9cbed10b1 -r 80ef03e39058 src/Modal/README.html --- 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 @@ -Modal/ReadMe - -

Modal: First-Order Modal Sequent Calculus

- -This directory contains the Standard ML sources of the Isabelle system for -Modal Logic. Important files include - -
-
ROOT.ML -
loads all source files. Enter an ML image containing LK -Isabelle and type: use "ROOT.ML";

- -

ex -
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"; -
- -Thanks to Rajeev Gore' for supplying the inference system for S43.

- -Useful references on Modal Logics: - -

- diff -r bcc9cbed10b1 -r 80ef03e39058 src/Modal/ROOT.ML --- 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*) diff -r bcc9cbed10b1 -r 80ef03e39058 src/Modal/S4.thy --- 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 diff -r bcc9cbed10b1 -r 80ef03e39058 src/Modal/S43.thy --- 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 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 = 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 diff -r bcc9cbed10b1 -r 80ef03e39058 src/Modal/T.thy --- 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 diff -r bcc9cbed10b1 -r 80ef03e39058 src/Modal/ex/ROOT.ML --- 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"; diff -r bcc9cbed10b1 -r 80ef03e39058 src/Modal/ex/S43thms.ML --- 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"; diff -r bcc9cbed10b1 -r 80ef03e39058 src/Modal/ex/S4thms.ML --- 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>- ((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 bcc9cbed10b1 -r 80ef03e39058 src/Modal/ex/Tthms.ML --- 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-- []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 bcc9cbed10b1 -r 80ef03e39058 src/Modal/prover.ML --- 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 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;