author | blanchet |
Fri, 14 Mar 2014 10:08:33 +0100 | |
changeset 56123 | a27859b0ef7d |
parent 54742 | 7a86358a3c0b |
child 59164 | ff40c53d1af9 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Sequents/modal.ML |
7096 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1992 University of Cambridge |
|
4 |
||
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24584
diff
changeset
|
5 |
Simple modal reasoner. |
7096 | 6 |
*) |
7 |
||
8 |
signature MODAL_PROVER_RULE = |
|
9 |
sig |
|
10 |
val rewrite_rls : thm list |
|
11 |
val safe_rls : thm list |
|
12 |
val unsafe_rls : thm list |
|
13 |
val bound_rls : thm list |
|
14 |
val aside_rls : thm list |
|
15 |
end; |
|
16 |
||
17 |
signature MODAL_PROVER = |
|
18 |
sig |
|
19 |
val rule_tac : thm list -> int ->tactic |
|
20 |
val step_tac : int -> tactic |
|
21 |
val solven_tac : int -> int -> tactic |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
41449
diff
changeset
|
22 |
val solve_tac : Proof.context -> int -> tactic |
7096 | 23 |
end; |
24 |
||
25 |
functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = |
|
26 |
struct |
|
27 |
||
28 |
(*Returns the list of all formulas in the sequent*) |
|
38500 | 29 |
fun forms_of_seq (Const(@{const_name SeqO'},_) $ P $ u) = P :: forms_of_seq u |
7096 | 30 |
| forms_of_seq (H $ u) = forms_of_seq u |
31 |
| forms_of_seq _ = []; |
|
32 |
||
33 |
(*Tests whether two sequences (left or right sides) could be resolved. |
|
34 |
seqp is a premise (subgoal), seqc is a conclusion of an object-rule. |
|
35 |
Assumes each formula in seqc is surrounded by sequence variables |
|
36 |
-- checks that each concl formula looks like some subgoal formula.*) |
|
37 |
fun could_res (seqp,seqc) = |
|
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
24584
diff
changeset
|
38 |
forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) |
7096 | 39 |
(forms_of_seq seqp)) |
40 |
(forms_of_seq seqc); |
|
41 |
||
42 |
(*Tests whether two sequents G|-H could be resolved, comparing each side.*) |
|
43 |
fun could_resolve_seq (prem,conc) = |
|
44 |
case (prem,conc) of |
|
45 |
(_ $ Abs(_,_,leftp) $ Abs(_,_,rightp), |
|
46 |
_ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) => |
|
47 |
could_res (leftp,leftc) andalso could_res (rightp,rightc) |
|
48 |
| _ => false; |
|
49 |
||
50 |
(*Like filt_resolve_tac, using could_resolve_seq |
|
51 |
Much faster than resolve_tac when there are many rules. |
|
52 |
Resolve subgoal i using the rules, unless more than maxr are compatible. *) |
|
53 |
fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) => |
|
54 |
let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules) |
|
55 |
in if length rls > maxr then no_tac else resolve_tac rls i |
|
56 |
end); |
|
57 |
||
58 |
fun fresolve_tac rls n = filseq_resolve_tac rls 999 n; |
|
59 |
||
60 |
(* NB No back tracking possible with aside rules *) |
|
61 |
||
41449 | 62 |
fun aside_tac n = DETERM(REPEAT (filt_resolve_tac Modal_Rule.aside_rls 999 n)); |
7096 | 63 |
fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n; |
64 |
||
41449 | 65 |
val fres_safe_tac = fresolve_tac Modal_Rule.safe_rls; |
66 |
val fres_unsafe_tac = fresolve_tac Modal_Rule.unsafe_rls THEN' aside_tac; |
|
67 |
val fres_bound_tac = fresolve_tac Modal_Rule.bound_rls; |
|
7096 | 68 |
|
69 |
fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac |
|
70 |
else tf(i) THEN tac(i-1) |
|
71 |
in fn st => tac (nprems_of st) st end; |
|
72 |
||
73 |
(* Depth first search bounded by d *) |
|
74 |
fun solven_tac d n state = state |> |
|
75 |
(if d<0 then no_tac |
|
76 |
else if (nprems_of state = 0) then all_tac |
|
77 |
else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE |
|
78 |
((fres_unsafe_tac n THEN UPTOGOAL n (solven_tac d)) APPEND |
|
79 |
(fres_bound_tac n THEN UPTOGOAL n (solven_tac (d-1))))); |
|
80 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
41449
diff
changeset
|
81 |
fun solve_tac ctxt d = rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac d 1; |
7096 | 82 |
|
83 |
fun step_tac n = |
|
84 |
COND (has_fewer_prems 1) all_tac |
|
85 |
(DETERM(fres_safe_tac n) ORELSE |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
29269
diff
changeset
|
86 |
(fres_unsafe_tac n APPEND fres_bound_tac n)); |
7096 | 87 |
|
88 |
end; |