diff --git a/src/Sequents/Modal0.thy b/src/Sequents/Modal0.thy --- a/src/Sequents/Modal0.thy +++ b/src/Sequents/Modal0.thy @@ -1,60 +1,60 @@ (* Title: Sequents/Modal0.thy Author: Martin Coen Copyright 1991 University of Cambridge *) theory Modal0 imports LK0 begin ML_file \modal.ML\ consts box :: "o\o" ("[]_" [50] 50) dia :: "o\o" ("<>_" [50] 50) Lstar :: "two_seqi" Rstar :: "two_seqi" syntax "_Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) "_Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5) ML \ - fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2; - fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2; + fun star_tr c [s1, s2] = Syntax.const c $ seq_tr s1 $ seq_tr s2; + fun star_tr' c [s1, s2] = Syntax.const c $ seq_tr' s1 $ seq_tr' s2; \ parse_translation \ [(\<^syntax_const>\_Lstar\, K (star_tr \<^const_syntax>\Lstar\)), (\<^syntax_const>\_Rstar\, K (star_tr \<^const_syntax>\Rstar\))] \ print_translation \ [(\<^const_syntax>\Lstar\, K (star_tr' \<^syntax_const>\_Lstar\)), (\<^const_syntax>\Rstar\, K (star_tr' \<^syntax_const>\_Rstar\))] \ definition strimp :: "[o,o]\o" (infixr "--<" 25) where "P --< Q == [](P \ Q)" definition streqv :: "[o,o]\o" (infixr ">-<" 25) where "P >-< Q == (P --< Q) \ (Q --< P)" lemmas rewrite_rls = strimp_def streqv_def lemma iffR: "\$H,P \ $E,Q,$F; $H,Q \ $E,P,$F\ \ $H \ $E, P \ Q, $F" apply (unfold iff_def) apply (assumption | rule conjR impR)+ done lemma iffL: "\$H,$G \ $E,P,Q; $H,Q,P,$G \ $E \ \ $H, P \ Q, $G \ $E" apply (unfold iff_def) apply (assumption | rule conjL impL basic)+ done lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR and unsafe_rls = allR exL and bound_rls = allL exR end diff --git a/src/Sequents/S43.thy b/src/Sequents/S43.thy --- a/src/Sequents/S43.thy +++ b/src/Sequents/S43.thy @@ -1,204 +1,204 @@ (* Title: Sequents/S43.thy Author: Martin Coen Copyright 1991 University of Cambridge This implements Rajeev Gore's sequent calculus for S43. *) theory S43 imports Modal0 begin consts S43pi :: "[seq'\seq', seq'\seq', seq'\seq', seq'\seq', seq'\seq', seq'\seq'] \ prop" syntax "_S43pi" :: "[seq, seq, seq, seq, seq, seq] \ prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5) parse_translation \ let val tr = seq_tr; fun s43pi_tr [s1, s2, s3, s4, s5, s6] = - Const (\<^const_syntax>\S43pi\, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6; + Syntax.const \<^const_syntax>\S43pi\ $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6; in [(\<^syntax_const>\_S43pi\, K s43pi_tr)] end \ print_translation \ let val tr' = seq_tr'; fun s43pi_tr' [s1, s2, s3, s4, s5, s6] = - Const(\<^syntax_const>\_S43pi\, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6; + Syntax.const \<^syntax_const>\_S43pi\ $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6; in [(\<^const_syntax>\S43pi\, K s43pi_tr')] end \ axiomatization where (* Definition of the star operation using a set of Horn clauses *) (* For system S43: gamma * == {[]P | []P : gamma} *) (* delta * == {<>P | <>P : delta} *) lstar0: "|L>" and lstar1: "$G |L> $H \ []P, $G |L> []P, $H" and lstar2: "$G |L> $H \ P, $G |L> $H" and rstar0: "|R>" and rstar1: "$G |R> $H \ <>P, $G |R> <>P, $H" and rstar2: "$G |R> $H \ P, $G |R> $H" and (* 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(S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox \ $R,$Rdia\ \ S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia" and S43pi2: "\(S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox \ $R',P,$R,$Rdia\ \ S43pi $L';; $R'; []P,$R; $Lbox;$Rdia" and (* Rules for [] and <> for S43 *) boxL: "$E, P, $F, []P \ $G \ $E, []P, $F \ $G" and diaR: "$E \ $F, P, $G, <>P \ $E \ $F, <>P, $G" and 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" and 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" ML \ structure S43_Prover = Modal_ProverFun ( val rewrite_rls = @{thms rewrite_rls} val safe_rls = @{thms safe_rls} val unsafe_rls = @{thms unsafe_rls} @ [@{thm pi1}, @{thm pi2}] val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}] val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0}, @{thm rstar1}, @{thm rstar2}, @{thm S43pi0}, @{thm S43pi1}, @{thm S43pi2}] ) \ method_setup S43_solve = \ Scan.succeed (fn ctxt => SIMPLE_METHOD (S43_Prover.solve_tac ctxt 2 ORELSE S43_Prover.solve_tac ctxt 3)) \ (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) lemma "\ []P \ P" by S43_solve lemma "\ [](P \ Q) \ ([]P \ []Q)" by S43_solve (* normality*) lemma "\ (P-- []P \ []Q" by S43_solve lemma "\ P \ <>P" by S43_solve lemma "\ [](P \ Q) \ []P \ []Q" by S43_solve lemma "\ <>(P \ Q) \ <>P \ <>Q" by S43_solve lemma "\ [](P \ Q) \ (P>- <>(P \ Q) \ ([]P \ <>Q)" by S43_solve lemma "\ []P \ \ <>(\ P)" by S43_solve lemma "\ [](\P) \ \ <>P" by S43_solve lemma "\ \ []P \ <>(\ P)" by S43_solve lemma "\ [][]P \ \ <><>(\ P)" by S43_solve lemma "\ \ <>(P \ Q) \ \ <>P \ \ <>Q" by S43_solve lemma "\ []P \ []Q \ [](P \ Q)" by S43_solve lemma "\ <>(P \ Q) \ <>P \ <>Q" by S43_solve lemma "\ [](P \ Q) \ []P \ <>Q" by S43_solve lemma "\ <>P \ []Q \ <>(P \ Q)" by S43_solve lemma "\ [](P \ Q) \ <>P \ []Q" by S43_solve lemma "\ <>(P \ (Q \ R)) \ ([]P \ <>Q) \ ([]P \ <>R)" by S43_solve lemma "\ (P --< Q) \ (Q -- (P --< R)" by S43_solve lemma "\ []P \ <>Q \ <>(P \ Q)" by S43_solve (* Theorems of system S4 from Hughes and Cresswell, p.46 *) lemma "\ []A \ A" by S43_solve (* refexivity *) lemma "\ []A \ [][]A" by S43_solve (* transitivity *) lemma "\ []A \ <>A" by S43_solve (* seriality *) lemma "\ <>[](<>A \ []<>A)" by S43_solve lemma "\ <>[](<>[]A \ []A)" by S43_solve lemma "\ []P \ [][]P" by S43_solve lemma "\ <>P \ <><>P" by S43_solve lemma "\ <>[]<>P \ <>P" by S43_solve lemma "\ []<>P \ []<>[]<>P" by S43_solve lemma "\ <>[]P \ <>[]<>[]P" by S43_solve (* Theorems for system S4 from Hughes and Cresswell, p.60 *) lemma "\ []P \ []Q \ []([]P \ []Q)" by S43_solve lemma "\ ((P >-< Q) --< R) \ ((P >-< Q) --< []R)" by S43_solve (* These are from Hailpern, LNCS 129 *) lemma "\ [](P \ Q) \ []P \ []Q" by S43_solve lemma "\ <>(P \ Q) \ <>P \ <>Q" by S43_solve lemma "\ <>(P \ Q) \ ([]P \ <>Q)" by S43_solve lemma "\ [](P \ Q) \ (<>P \ <>Q)" by S43_solve lemma "\ []P \ []<>P" by S43_solve lemma "\ <>[]P \ <>P" by S43_solve lemma "\ []P \ []Q \ [](P \ Q)" by S43_solve lemma "\ <>(P \ Q) \ <>P \ <>Q" by S43_solve lemma "\ [](P \ Q) \ []P \ <>Q" by S43_solve lemma "\ <>P \ []Q \ <>(P \ Q)" by S43_solve lemma "\ [](P \ Q) \ <>P \ []Q" by S43_solve (* Theorems of system S43 *) lemma "\ <>[]P \ []<>P" by S43_solve lemma "\ <>[]P \ [][]<>P" by S43_solve lemma "\ [](<>P \ <>Q) \ []<>P \ []<>Q" by S43_solve lemma "\ <>[]P \ <>[]Q \ <>([]P \ []Q)" by S43_solve lemma "\ []([]P \ []Q) \ []([]Q \ []P)" by S43_solve lemma "\ [](<>P \ <>Q) \ [](<>Q \ <>P)" by S43_solve lemma "\ []([]P \ Q) \ []([]Q \ P)" by S43_solve lemma "\ [](P \ <>Q) \ [](Q \ <>P)" by S43_solve lemma "\ [](P \ []Q \ R) \ [](P \ ([]R \ Q))" by S43_solve lemma "\ [](P \ (Q \ <>C)) \ [](P \ C \ <>Q)" by S43_solve lemma "\ []([]P \ Q) \ [](P \ []Q) \ []P \ []Q" by S43_solve lemma "\ <>P \ <>Q \ <>(<>P \ Q) \ <>(P \ <>Q)" by S43_solve lemma "\ [](P \ Q) \ []([]P \ Q) \ [](P \ []Q) \ []P \ []Q" by S43_solve lemma "\ <>P \ <>Q \ <>(P \ Q) \ <>(<>P \ Q) \ <>(P \ <>Q)" by S43_solve lemma "\ <>[]<>P \ []<>P" by S43_solve lemma "\ []<>[]P \ <>[]P" by S43_solve (* These are from Hailpern, LNCS 129 *) lemma "\ [](P \ Q) \ []P \ []Q" by S43_solve lemma "\ <>(P \ Q) \ <>P \ <>Q" by S43_solve lemma "\ <>(P \ Q) \ []P \ <>Q" by S43_solve lemma "\ [](P \ Q) \ <>P \ <>Q" by S43_solve lemma "\ []P \ []<>P" by S43_solve lemma "\ <>[]P \ <>P" by S43_solve lemma "\ []<>[]P \ []<>P" by S43_solve lemma "\ <>[]P \ <>[]<>P" by S43_solve lemma "\ <>[]P \ []<>P" by S43_solve lemma "\ []<>[]P \ <>[]P" by S43_solve lemma "\ <>[]<>P \ []<>P" by S43_solve lemma "\ []P \ []Q \ [](P \ Q)" by S43_solve lemma "\ <>(P \ Q) \ <>P \ <>Q" by S43_solve lemma "\ [](P \ Q) \ []P \ <>Q" by S43_solve lemma "\ <>P \ []Q \ <>(P \ Q)" by S43_solve lemma "\ [](P \ Q) \ <>P \ []Q" by S43_solve lemma "\ [](P \ Q) \ []<>P \ []<>Q" by S43_solve lemma "\ <>[]P \ <>[]Q \ <>(P \ Q)" by S43_solve lemma "\ <>[](P \ Q) \ <>[]P \ <>[]Q" by S43_solve lemma "\ []<>(P \ Q) \ []<>P \ []<>Q" by S43_solve end diff --git a/src/Sequents/Sequents.thy b/src/Sequents/Sequents.thy --- a/src/Sequents/Sequents.thy +++ b/src/Sequents/Sequents.thy @@ -1,149 +1,147 @@ (* Title: Sequents/Sequents.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge *) section \Parsing and pretty-printing of sequences\ theory Sequents imports Pure keywords "print_pack" :: diag begin setup Pure_Thy.old_appl_syntax_setup declare [[unify_trace_bound = 20, unify_search_bound = 40]] typedecl o subsection \Sequences\ typedecl seq' consts SeqO' :: "[o,seq']\seq'" Seq1' :: "o\seq'" subsection \Concrete syntax\ nonterminal seq and seqobj and seqcont syntax "_SeqEmp" :: seq ("") "_SeqApp" :: "[seqobj,seqcont] \ seq" ("__") "_SeqContEmp" :: seqcont ("") "_SeqContApp" :: "[seqobj,seqcont] \ seqcont" (",/ __") "_SeqO" :: "o \ seqobj" ("_") "_SeqId" :: "'a \ seqobj" ("$_") type_synonym single_seqe = "[seq,seqobj] \ prop" type_synonym single_seqi = "[seq'\seq',seq'\seq'] \ prop" type_synonym two_seqi = "[seq'\seq', seq'\seq'] \ prop" type_synonym two_seqe = "[seq, seq] \ prop" type_synonym three_seqi = "[seq'\seq', seq'\seq', seq'\seq'] \ prop" type_synonym three_seqe = "[seq, seq, seq] \ prop" type_synonym four_seqi = "[seq'\seq', seq'\seq', seq'\seq', seq'\seq'] \ prop" type_synonym four_seqe = "[seq, seq, seq, seq] \ prop" type_synonym sequence_name = "seq'\seq'" syntax (*Constant to allow definitions of SEQUENCES of formulas*) "_Side" :: "seq\(seq'\seq')" ("<<(_)>>") ML \ (* parse translation for sequences *) -fun abs_seq' t = Abs ("s", Type (\<^type_name>\seq'\, []), t); +fun abs_seq' t = Abs ("s", \<^Type>\seq'\, t); -fun seqobj_tr (Const (\<^syntax_const>\_SeqO\, _) $ f) = - Const (\<^const_syntax>\SeqO'\, dummyT) $ f +fun seqobj_tr (Const (\<^syntax_const>\_SeqO\, _) $ f) = Syntax.const \<^const_syntax>\SeqO'\ $ f | seqobj_tr (_ $ i) = i; fun seqcont_tr (Const (\<^syntax_const>\_SeqContEmp\, _)) = Bound 0 | seqcont_tr (Const (\<^syntax_const>\_SeqContApp\, _) $ so $ sc) = seqobj_tr so $ seqcont_tr sc; fun seq_tr (Const (\<^syntax_const>\_SeqEmp\, _)) = abs_seq' (Bound 0) | seq_tr (Const (\<^syntax_const>\_SeqApp\, _) $ so $ sc) = abs_seq'(seqobj_tr so $ seqcont_tr sc); fun singlobj_tr (Const (\<^syntax_const>\_SeqO\,_) $ f) = - abs_seq' ((Const (\<^const_syntax>\SeqO'\, dummyT) $ f) $ Bound 0); + abs_seq' ((Syntax.const \<^const_syntax>\SeqO'\ $ f) $ Bound 0); (* print translation for sequences *) -fun seqcont_tr' (Bound 0) = - Const (\<^syntax_const>\_SeqContEmp\, dummyT) +fun seqcont_tr' (Bound 0) = Syntax.const \<^syntax_const>\_SeqContEmp\ | seqcont_tr' (Const (\<^const_syntax>\SeqO'\, _) $ f $ s) = - Const (\<^syntax_const>\_SeqContApp\, dummyT) $ - (Const (\<^syntax_const>\_SeqO\, dummyT) $ f) $ seqcont_tr' s + Syntax.const \<^syntax_const>\_SeqContApp\ $ + (Syntax.const \<^syntax_const>\_SeqO\ $ f) $ seqcont_tr' s | seqcont_tr' (i $ s) = - Const (\<^syntax_const>\_SeqContApp\, dummyT) $ - (Const (\<^syntax_const>\_SeqId\, dummyT) $ i) $ seqcont_tr' s; + Syntax.const \<^syntax_const>\_SeqContApp\ $ + (Syntax.const \<^syntax_const>\_SeqId\ $ i) $ seqcont_tr' s; fun seq_tr' s = let - fun seq_itr' (Bound 0) = Const (\<^syntax_const>\_SeqEmp\, dummyT) + fun seq_itr' (Bound 0) = Syntax.const \<^syntax_const>\_SeqEmp\ | seq_itr' (Const (\<^const_syntax>\SeqO'\, _) $ f $ s) = - Const (\<^syntax_const>\_SeqApp\, dummyT) $ - (Const (\<^syntax_const>\_SeqO\, dummyT) $ f) $ seqcont_tr' s + Syntax.const \<^syntax_const>\_SeqApp\ $ + (Syntax.const \<^syntax_const>\_SeqO\ $ f) $ seqcont_tr' s | seq_itr' (i $ s) = - Const (\<^syntax_const>\_SeqApp\, dummyT) $ - (Const (\<^syntax_const>\_SeqId\, dummyT) $ i) $ seqcont_tr' s + Syntax.const \<^syntax_const>\_SeqApp\ $ + (Syntax.const \<^syntax_const>\_SeqId\ $ 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; + Syntax.const c $ seq_tr s1 $ singlobj_tr s2; fun two_seq_tr c [s1, s2] = - Const (c, dummyT) $ seq_tr s1 $ seq_tr s2; + Syntax.const c $ 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; + Syntax.const c $ 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; + Syntax.const c $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4; fun singlobj_tr' (Const (\<^const_syntax>\SeqO'\,_) $ fm) = fm - | singlobj_tr' id = Const (\<^syntax_const>\_SeqId\, dummyT) $ id; + | singlobj_tr' id = Syntax.const \<^syntax_const>\_SeqId\ $ id; fun single_tr' c [s1, s2] = - Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; + Syntax.const c $ seq_tr' s1 $ seq_tr' s2; fun two_seq_tr' c [s1, s2] = - Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; + Syntax.const c $ 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; + Syntax.const c $ 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; + Syntax.const c $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; (** for the <<...>> notation **) fun side_tr [s1] = seq_tr s1; \ parse_translation \[(\<^syntax_const>\_Side\, K side_tr)]\ subsection \Proof tools\ ML_file \prover.ML\ end diff --git a/src/Sequents/modal.ML b/src/Sequents/modal.ML --- a/src/Sequents/modal.ML +++ b/src/Sequents/modal.ML @@ -1,90 +1,90 @@ (* Title: Sequents/modal.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Simple modal reasoner. *) 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 : Proof.context -> thm list -> int ->tactic val step_tac : Proof.context -> int -> tactic val solven_tac : Proof.context -> int -> int -> tactic val solve_tac : Proof.context -> int -> tactic end; functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = struct (*Returns the list of all formulas in the sequent*) -fun forms_of_seq (Const(\<^const_name>\SeqO'\,_) $ P $ u) = P :: forms_of_seq u +fun forms_of_seq \<^Const_>\SeqO' for 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 => Term.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 ctxt 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 ctxt rls i end); fun fresolve_tac ctxt rls n = filseq_resolve_tac ctxt rls 999 n; (* NB No back tracking possible with aside rules *) val aside_net = Tactic.build_net Modal_Rule.aside_rls; fun aside_tac ctxt n = DETERM (REPEAT (filt_resolve_from_net_tac ctxt 999 aside_net n)); fun rule_tac ctxt rls n = fresolve_tac ctxt rls n THEN aside_tac ctxt n; fun fres_safe_tac ctxt = fresolve_tac ctxt Modal_Rule.safe_rls; fun fres_unsafe_tac ctxt = fresolve_tac ctxt Modal_Rule.unsafe_rls THEN' aside_tac ctxt; fun fres_bound_tac ctxt = fresolve_tac ctxt Modal_Rule.bound_rls; fun UPTOGOAL n tf = let fun tac i = if i tac (Thm.nprems_of st) st end; (* Depth first search bounded by d *) fun solven_tac ctxt d n st = st |> (if d < 0 then no_tac else if Thm.nprems_of st = 0 then all_tac else (DETERM(fres_safe_tac ctxt n) THEN UPTOGOAL n (solven_tac ctxt d)) ORELSE ((fres_unsafe_tac ctxt n THEN UPTOGOAL n (solven_tac ctxt d)) APPEND (fres_bound_tac ctxt n THEN UPTOGOAL n (solven_tac ctxt (d - 1))))); fun solve_tac ctxt d = rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac ctxt d 1; fun step_tac ctxt n = COND (has_fewer_prems 1) all_tac (DETERM(fres_safe_tac ctxt n) ORELSE (fres_unsafe_tac ctxt n APPEND fres_bound_tac ctxt n)); end; diff --git a/src/Sequents/prover.ML b/src/Sequents/prover.ML --- a/src/Sequents/prover.ML +++ b/src/Sequents/prover.ML @@ -1,237 +1,237 @@ (* Title: Sequents/prover.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Simple classical reasoner for the sequent calculus, based on "theorem packs". *) signature CLA = sig type pack val empty_pack: pack val get_pack: Proof.context -> pack val put_pack: pack -> Proof.context -> Proof.context val pretty_pack: Proof.context -> Pretty.T val add_safe: thm -> Proof.context -> Proof.context val add_unsafe: thm -> Proof.context -> Proof.context val safe_add: attribute val unsafe_add: attribute val method: (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser val trace: bool Config.T val forms_of_seq: term -> term list val safe_tac: Proof.context -> int -> tactic val step_tac: Proof.context -> int -> tactic val pc_tac: Proof.context -> int -> tactic val fast_tac: Proof.context -> int -> tactic val best_tac: Proof.context -> int -> tactic end; structure Cla: CLA = struct (** rule declarations **) (*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) = Thm.nprems_of rl1 < Thm.nprems_of rl2; val sort_rules = sort (make_ord less); datatype pack = Pack of thm list * thm list; val empty_pack = Pack ([], []); structure Pack = Generic_Data ( type T = pack; val empty = empty_pack; val extend = I; fun merge (Pack (safes, unsafes), Pack (safes', unsafes')) = Pack (sort_rules (Thm.merge_thms (safes, safes')), sort_rules (Thm.merge_thms (unsafes, unsafes'))); ); val put_pack = Context.proof_map o Pack.put; val get_pack = Pack.get o Context.Proof; fun get_rules ctxt = let val Pack rules = get_pack ctxt in rules end; (* print pack *) fun pretty_pack ctxt = let val (safes, unsafes) = get_rules ctxt in Pretty.chunks [Pretty.big_list "safe rules:" (map (Thm.pretty_thm ctxt) safes), Pretty.big_list "unsafe rules:" (map (Thm.pretty_thm ctxt) unsafes)] end; val _ = Outer_Syntax.command \<^command_keyword>\print_pack\ "print pack of classical rules" (Scan.succeed (Toplevel.keep (Pretty.writeln o pretty_pack o Toplevel.context_of))); (* declare rules *) fun add_rule which th context = context |> Pack.map (fn Pack rules => Pack (rules |> which (fn ths => if member Thm.eq_thm_prop ths th then let val _ = (case context of Context.Proof ctxt => if Context_Position.is_really_visible ctxt then warning ("Ignoring duplicate theorems:\n" ^ Thm.string_of_thm ctxt th) else () | _ => ()); in ths end else sort_rules (th :: ths)))); val add_safe = Context.proof_map o add_rule apfst; val add_unsafe = Context.proof_map o add_rule apsnd; (* attributes *) val safe_add = Thm.declaration_attribute (add_rule apfst); val unsafe_add = Thm.declaration_attribute (add_rule apsnd); val _ = Theory.setup (Attrib.setup \<^binding>\safe\ (Scan.succeed safe_add) "" #> Attrib.setup \<^binding>\unsafe\ (Scan.succeed unsafe_add) ""); (* proof method syntax *) fun method tac = Method.sections [Args.$$$ "add" -- Args.bang_colon >> K (Method.modifier safe_add \<^here>), Args.$$$ "add" -- Args.colon >> K (Method.modifier unsafe_add \<^here>)] >> K (SIMPLE_METHOD' o tac); (** tactics **) val trace = Attrib.setup_config_bool \<^binding>\cla_trace\ (K false); (*Returns the list of all formulas in the sequent*) -fun forms_of_seq (Const(\<^const_name>\SeqO'\,_) $ P $ u) = P :: forms_of_seq u +fun forms_of_seq \<^Const_>\SeqO' for 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 => Term.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 Term.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 ctxt 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 ctxt rls i end); (*Predicate: does the rule have n premises? *) fun has_prems n rule = (Thm.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 ctxt rules = let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules; fun tac nextac i state = state |> (filseq_resolve_tac ctxt rls0 9999 i ORELSE (DETERM(filseq_resolve_tac ctxt rls1 9999 i) THEN TRY(nextac i)) ORELSE (DETERM(filseq_resolve_tac ctxt 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 ctxt rules = let val restac = RESOLVE_THEN ctxt 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 ctxt = let val (safes, unsafes) = get_rules ctxt; val restac = RESOLVE_THEN ctxt safes; val lastrestac = RESOLVE_THEN ctxt unsafes; fun gtac i = restac gtac i ORELSE (if Config.get ctxt trace then print_tac ctxt "" THEN lastrestac gtac i else lastrestac gtac i) in gtac end; (*Tries safe rules only*) fun safe_tac ctxt = reresolve_tac ctxt (#1 (get_rules ctxt)); (*Tries a safe rule or else a unsafe rule. Single-step for tracing. *) fun step_tac ctxt = safe_tac ctxt ORELSE' filseq_resolve_tac ctxt (#2 (get_rules ctxt)) 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 ctxt = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac ctxt 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 ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); fun best_tac ctxt = SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); val _ = Theory.setup (Method.setup \<^binding>\safe\ (method safe_tac) "" #> Method.setup \<^binding>\step\ (method step_tac) "" #> Method.setup \<^binding>\pc\ (method pc_tac) "" #> Method.setup \<^binding>\fast\ (method fast_tac) "" #> Method.setup \<^binding>\best\ (method best_tac) ""); end; diff --git a/src/Sequents/simpdata.ML b/src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML +++ b/src/Sequents/simpdata.ML @@ -1,92 +1,92 @@ (* Title: Sequents/simpdata.ML Author: Lawrence C Paulson Copyright 1999 University of Cambridge Instantiation of the generic simplifier for LK. Borrows from the DC simplifier of Soren Heilmann. *) (** Conversion into rewrite rules **) (*Make atomic rewrite rules*) fun atomize r = case Thm.concl_of r of - Const(\<^const_name>\Trueprop\,_) $ Abs(_,_,a) $ Abs(_,_,c) => + \<^Const_>\Trueprop for \Abs(_,_,a)\ \Abs(_,_,c)\\ => (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of ([], [p]) => (case p of - Const(\<^const_name>\imp\,_)$_$_ => atomize(r RS @{thm mp_R}) - | Const(\<^const_name>\conj\,_)$_$_ => atomize(r RS @{thm conjunct1}) @ + \<^Const_>\imp for _ _\ => atomize(r RS @{thm mp_R}) + | \<^Const_>\conj for _ _\ => atomize(r RS @{thm conjunct1}) @ atomize(r RS @{thm conjunct2}) - | Const(\<^const_name>\All\,_)$_ => atomize(r RS @{thm spec}) - | Const(\<^const_name>\True\,_) => [] (*True is DELETED*) - | Const(\<^const_name>\False\,_) => [] (*should False do something?*) + | \<^Const_>\All _ for _\ => atomize(r RS @{thm spec}) + | \<^Const_>\True\ => [] (*True is DELETED*) + | \<^Const_>\False\ => [] (*should False do something?*) | _ => [r]) | _ => []) (*ignore theorem unless it has precisely one conclusion*) | _ => [r]; (*Make meta-equalities.*) fun mk_meta_eq ctxt th = case Thm.concl_of th of - Const(\<^const_name>\Pure.eq\,_)$_$_ => th - | Const(\<^const_name>\Trueprop\,_) $ Abs(_,_,a) $ Abs(_,_,c) => + \<^Const_>\Pure.eq _ for _ _\ => th + | \<^Const_>\Trueprop for \Abs(_,_,a)\ \Abs(_,_,c)\\ => (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of ([], [p]) => (case p of - (Const(\<^const_name>\equal\,_)$_$_) => th RS @{thm eq_reflection} - | (Const(\<^const_name>\iff\,_)$_$_) => th RS @{thm iff_reflection} - | (Const(\<^const_name>\Not\,_)$_) => th RS @{thm iff_reflection_F} + \<^Const_>\equal _ for _ _\ => th RS @{thm eq_reflection} + | \<^Const_>\iff for _ _\ => th RS @{thm iff_reflection} + | \<^Const_>\Not for _\ => th RS @{thm iff_reflection_F} | _ => th RS @{thm iff_reflection_T}) | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th)); (*Replace premises x=y, X<->Y by X==Y*) fun mk_meta_prems ctxt = rule_by_tactic ctxt (REPEAT_FIRST (resolve_tac ctxt [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); (*Congruence rules for = or <-> (instead of ==)*) fun mk_meta_cong ctxt rl = Drule.zero_var_indexes (mk_meta_eq ctxt (mk_meta_prems ctxt rl)) handle THM _ => error("Premises and conclusion of congruence rules must use =-equality or <->"); (*** Standard simpsets ***) val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl}, @{thm iff_refl}, reflexive_thm]; fun unsafe_solver ctxt = FIRST' [resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt), assume_tac ctxt]; (*No premature instantiation of variables during simplification*) fun safe_solver ctxt = FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i), eq_assume_tac]; (*No simprules, but basic infrastructure for simplification*) val LK_basic_ss = empty_simpset \<^context> setSSolver (mk_solver "safe" safe_solver) setSolver (mk_solver "unsafe" unsafe_solver) |> Simplifier.set_subgoaler asm_simp_tac |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt) |> Simplifier.set_mkcong mk_meta_cong |> simpset_of; val LK_simps = [@{thm triv_forall_equality}, (* prunes params *) @{thm refl} RS @{thm P_iff_T}] @ @{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @ @{thms imp_simps} @ @{thms iff_simps} @ @{thms quant_simps} @ @{thms all_simps} @ @{thms ex_simps} @ [@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @ @{thms LK_extra_simps}; val LK_ss = put_simpset LK_basic_ss \<^context> addsimps LK_simps |> Simplifier.add_eqcong @{thm left_cong} |> Simplifier.add_cong @{thm imp_cong} |> simpset_of;