summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Sequents/prover.ML

author | wenzelm |

Thu Dec 07 00:42:04 2006 +0100 (2006-12-07) | |

changeset 21687 | f689f729afab |

parent 21428 | f84cf8e9cad8 |

child 22360 | 26ead7ed4f4b |

permissions | -rw-r--r-- |

reorganized structure Goal vs. Tactic;

1 (* Title: Sequents/prover

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1992 University of Cambridge

6 Simple classical reasoner for the sequent calculus, based on "theorem packs"

7 *)

10 (*Higher precedence than := facilitates use of references*)

11 infix 4 add_safes add_unsafes;

13 structure Cla =

15 struct

17 datatype pack = Pack of thm list * thm list;

19 val trace = ref false;

21 (*A theorem pack has the form (safe rules, unsafe rules)

22 An unsafe rule is incomplete or introduces variables in subgoals,

23 and is tried only when the safe rules are not applicable. *)

25 fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);

27 val empty_pack = Pack([],[]);

29 fun warn_duplicates [] = []

30 | warn_duplicates dups =

31 (warning (cat_lines ("Ignoring duplicate theorems:" :: map string_of_thm dups));

32 dups);

34 fun (Pack(safes,unsafes)) add_safes ths =

35 let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))

36 val ths' = subtract Drule.eq_thm_prop dups ths

37 in

38 Pack(sort (make_ord less) (ths'@safes), unsafes)

39 end;

41 fun (Pack(safes,unsafes)) add_unsafes ths =

42 let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))

43 val ths' = subtract Drule.eq_thm_prop dups ths

44 in

45 Pack(safes, sort (make_ord less) (ths'@unsafes))

46 end;

48 fun merge_pack (Pack(safes,unsafes), Pack(safes',unsafes')) =

49 Pack(sort (make_ord less) (safes@safes'),

50 sort (make_ord less) (unsafes@unsafes'));

53 fun print_pack (Pack(safes,unsafes)) =

54 (writeln "Safe rules:"; print_thms safes;

55 writeln "Unsafe rules:"; print_thms unsafes);

57 (*Returns the list of all formulas in the sequent*)

58 fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u

59 | forms_of_seq (H $ u) = forms_of_seq u

60 | forms_of_seq _ = [];

62 (*Tests whether two sequences (left or right sides) could be resolved.

63 seqp is a premise (subgoal), seqc is a conclusion of an object-rule.

64 Assumes each formula in seqc is surrounded by sequence variables

65 -- checks that each concl formula looks like some subgoal formula.

66 It SHOULD check order as well, using recursion rather than forall/exists*)

67 fun could_res (seqp,seqc) =

68 forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc))

69 (forms_of_seq seqp))

70 (forms_of_seq seqc);

73 (*Tests whether two sequents or pairs of sequents could be resolved*)

74 fun could_resolve_seq (prem,conc) =

75 case (prem,conc) of

76 (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),

77 _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>

78 could_res (leftp,leftc) andalso could_res (rightp,rightc)

79 | (_ $ Abs(_,_,leftp) $ rightp,

80 _ $ Abs(_,_,leftc) $ rightc) =>

81 could_res (leftp,leftc) andalso could_unify (rightp,rightc)

82 | _ => false;

85 (*Like filt_resolve_tac, using could_resolve_seq

86 Much faster than resolve_tac when there are many rules.

87 Resolve subgoal i using the rules, unless more than maxr are compatible. *)

88 fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>

89 let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)

90 in if length rls > maxr then no_tac

91 else (*((rtac derelict 1 THEN rtac impl 1

92 THEN (rtac identity 2 ORELSE rtac ll_mp 2)

93 THEN rtac context1 1)

94 ORELSE *) resolve_tac rls i

95 end);

98 (*Predicate: does the rule have n premises? *)

99 fun has_prems n rule = (nprems_of rule = n);

101 (*Continuation-style tactical for resolution.

102 The list of rules is partitioned into 0, 1, 2 premises.

103 The resulting tactic, gtac, tries to resolve with rules.

104 If successful, it recursively applies nextac to the new subgoals only.

105 Else fails. (Treatment of goals due to Ph. de Groote)

106 Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)

108 (*Takes rule lists separated in to 0, 1, 2, >2 premises.

109 The abstraction over state prevents needless divergence in recursion.

110 The 9999 should be a parameter, to delay treatment of flexible goals. *)

112 fun RESOLVE_THEN rules =

113 let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;

114 fun tac nextac i state = state |>

115 (filseq_resolve_tac rls0 9999 i

116 ORELSE

117 (DETERM(filseq_resolve_tac rls1 9999 i) THEN TRY(nextac i))

118 ORELSE

119 (DETERM(filseq_resolve_tac rls2 9999 i) THEN TRY(nextac(i+1))

120 THEN TRY(nextac i)))

121 in tac end;

125 (*repeated resolution applied to the designated goal*)

126 fun reresolve_tac rules =

127 let val restac = RESOLVE_THEN rules; (*preprocessing done now*)

128 fun gtac i = restac gtac i

129 in gtac end;

131 (*tries the safe rules repeatedly before the unsafe rules. *)

132 fun repeat_goal_tac (Pack(safes,unsafes)) =

133 let val restac = RESOLVE_THEN safes

134 and lastrestac = RESOLVE_THEN unsafes;

135 fun gtac i = restac gtac i

136 ORELSE (if !trace then

137 (print_tac "" THEN lastrestac gtac i)

138 else lastrestac gtac i)

139 in gtac end;

142 (*Tries safe rules only*)

143 fun safe_tac (Pack(safes,unsafes)) = reresolve_tac safes;

145 val safe_goal_tac = safe_tac; (*backwards compatibility*)

147 (*Tries a safe rule or else a unsafe rule. Single-step for tracing. *)

148 fun step_tac (pack as Pack(safes,unsafes)) =

149 safe_tac pack ORELSE'

150 filseq_resolve_tac unsafes 9999;

153 (* Tactic for reducing a goal, using Predicate Calculus rules.

154 A decision procedure for Propositional Calculus, it is incomplete

155 for Predicate-Calculus because of allL_thin and exR_thin.

156 Fails if it can do nothing. *)

157 fun pc_tac pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac pack 1));

160 (*The following two tactics are analogous to those provided by

161 Provers/classical. In fact, pc_tac is usually FASTER than fast_tac!*)

162 fun fast_tac pack =

163 SELECT_GOAL (DEPTH_SOLVE (step_tac pack 1));

165 fun best_tac pack =

166 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm)

167 (step_tac pack 1));

169 end;

172 open Cla;