
1 (* Title: LK/LK.ML 

2 ID: $Id$ 

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 Copyright 1992 University of Cambridge 

5 *) 

6 

7 

8 (**** Theorem Packs ****) 

9 

10 (* based largely on LK *) 

11 

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

13 

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

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

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

17 

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

19 

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

21 

22 infix 4 add_safes add_unsafes; 

23 

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

25 Pack(sort less (ths@safes), unsafes); 

26 

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

28 Pack(safes, sort less (ths@unsafes)); 

29 

30 

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

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

33  forms_of_seq (H $ u) = forms_of_seq u 

34  forms_of_seq _ = []; 

35 

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

37 seqp is a premise (subgoal), seqc is a conclusion of an objectrule. 

38 Assumes each formula in seqc is surrounded by sequence variables 

39  checks that each concl formula looks like some subgoal formula. 

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

41 fun could_res (seqp,seqc) = 

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

43 (forms_of_seq seqp)) 

44 (forms_of_seq seqc); 

45 

46 

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

48 fun could_resolve_seq (prem,conc) = 

49 case (prem,conc) of 

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

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

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

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

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

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

56  _ => false; 

57 

58 

59 (*Like filt_resolve_tac, using could_resolve_seq 

60 Much faster than resolve_tac when there are many rules. 

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

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

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

64 in if length rls > maxr then no_tac 

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

66 THEN (rtac identity 2 ORELSE rtac ll_mp 2) 

67 THEN rtac context1 1) 

68 ORELSE *) resolve_tac rls i 

69 end); 

70 

71 

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

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

74 

75 (*Continuationstyle tactical for resolution. 

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

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

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

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

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

81 

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

83 The abstraction over state prevents needless divergence in recursion. 

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

85 

86 fun RESOLVE_THEN rules = 

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

88 fun tac nextac i = STATE (fn state => 

89 filseq_resolve_tac rls0 9999 i 

90 ORELSE 

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

92 ORELSE 

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

94 THEN TRY(nextac i)) ) 

95 in tac end; 

96 

97 

98 

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

100 fun reresolve_tac rules = 

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

102 fun gtac i = restac gtac i 

103 in gtac end; 

104 

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

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

107 let val restac = RESOLVE_THEN safes 

108 and lastrestac = RESOLVE_THEN unsafes; 

109 fun gtac i = restac gtac i ORELSE (print_tac THEN lastrestac gtac i) 

110 in gtac end; 

111 

112 

113 (*Tries safe rules only*) 

114 fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes; 

115 

116 (*Tries a safe rule or else a unsafe rule. Singlestep for tracing. *) 

117 fun step_tac (thm_pack as Pack(safes,unsafes)) = 

118 safe_goal_tac thm_pack ORELSE' 

119 filseq_resolve_tac unsafes 9999; 

120 

121 

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

123 A decision procedure for Propositional Calculus, it is incomplete 

124 for PredicateCalculus because of allL_thin and exR_thin. 

125 Fails if it can do nothing. *) 

126 fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1)); 

127 

128 

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

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

131 fun fast_tac thm_pack = 

132 SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1)); 

133 

134 fun best_tac thm_pack = 

135 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 

136 (step_tac thm_pack 1)); 

137 

138 

139 

140 signature MODAL_PROVER_RULE = 

141 sig 

142 val rewrite_rls : thm list 

143 val safe_rls : thm list 

144 val unsafe_rls : thm list 

145 val bound_rls : thm list 

146 val aside_rls : thm list 

147 end; 

148 

149 signature MODAL_PROVER = 

150 sig 

151 val rule_tac : thm list > int >tactic 

152 val step_tac : int > tactic 

153 val solven_tac : int > int > tactic 

154 val solve_tac : int > tactic 

155 end; 

156 

157 functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 

158 struct 

159 local open Modal_Rule 

160 in 

161 

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

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

164  forms_of_seq (H $ u) = forms_of_seq u 

165  forms_of_seq _ = []; 

166 

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

168 seqp is a premise (subgoal), seqc is a conclusion of an objectrule. 

169 Assumes each formula in seqc is surrounded by sequence variables 

170  checks that each concl formula looks like some subgoal formula.*) 

171 fun could_res (seqp,seqc) = 

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

173 (forms_of_seq seqp)) 

174 (forms_of_seq seqc); 

175 

176 (*Tests whether two sequents GH could be resolved, comparing each side.*) 

177 fun could_resolve_seq (prem,conc) = 

178 case (prem,conc) of 

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

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

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

182  _ => false; 

183 

184 (*Like filt_resolve_tac, using could_resolve_seq 

185 Much faster than resolve_tac when there are many rules. 

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

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

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

189 in if length rls > maxr then no_tac else resolve_tac rls i 

190 end); 

191 

192 fun fresolve_tac rls n = filseq_resolve_tac rls 999 n; 

193 

194 (* NB No back tracking possible with aside rules *) 

195 

196 fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n)); 

197 fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n; 

198 

199 val fres_safe_tac = fresolve_tac safe_rls; 

200 val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac; 

201 val fres_bound_tac = fresolve_tac bound_rls; 

202 

203 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac 

204 else tf(i) THEN tac(i1) 

205 in STATE(fn state=> tac(nprems_of state)) end; 

206 

207 (* Depth first search bounded by d *) 

208 fun solven_tac d n = STATE (fn state => 

209 if d<0 then no_tac 

210 else if (nprems_of state = 0) then all_tac 

211 else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE 

212 ((fres_unsafe_tac n THEN UPTOGOAL n (solven_tac d)) APPEND 

213 (fres_bound_tac n THEN UPTOGOAL n (solven_tac (d1))))); 

214 

215 fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1; 

216 

217 fun step_tac n = STATE (fn state => 

218 if (nprems_of state = 0) then all_tac 

219 else (DETERM(fres_safe_tac n)) ORELSE 

220 (fres_unsafe_tac n APPEND fres_bound_tac n)); 

221 

222 end; 

223 end; 