author  wenzelm 
Sat, 09 Jul 2011 21:53:27 +0200  
changeset 43721  fad8634cee62 
parent 42799  4e33894aec6d 
child 58957  c9e744ea8a38 
permissions  rwrr 
37744  1 
(* Title: FOLP/classical.ML 
1459  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1992 University of Cambridge 
4 

5 
Like Provers/classical but modified because match_tac is unsuitable for 

6 
proof objects. 

7 

8 
Theorem prover for classical reasoning, including predicate calculus, set 

9 
theory, etc. 

10 

11 
Rules must be classified as intr, elim, safe, hazardous. 

12 

13 
A rule is unsafe unless it can be applied blindly without harmful results. 

14 
For a rule to be safe, its premises and conclusion should be logically 

15 
equivalent. There should be no variables in the premises that are not in 

16 
the conclusion. 

17 
*) 

18 

19 
signature CLASSICAL_DATA = 

20 
sig 

1459  21 
val mp: thm (* [ P>Q; P ] ==> Q *) 
22 
val not_elim: thm (* [ ~P; P ] ==> R *) 

23 
val swap: thm (* ~P ==> (~Q ==> P) ==> Q *) 

24 
val sizef : thm > int (* size function for BEST_FIRST *) 

0  25 
val hyp_subst_tacs: (int > tactic) list 
26 
end; 

27 

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

29 
infix 4 addSIs addSEs addSDs addIs addEs addDs; 

30 

31 

32 
signature CLASSICAL = 

33 
sig 

34 
type claset 

35 
val empty_cs: claset 

36 
val addDs : claset * thm list > claset 

37 
val addEs : claset * thm list > claset 

38 
val addIs : claset * thm list > claset 

39 
val addSDs: claset * thm list > claset 

40 
val addSEs: claset * thm list > claset 

41 
val addSIs: claset * thm list > claset 

42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
37744
diff
changeset

42 
val print_cs: Proof.context > claset > unit 
4653  43 
val rep_cs: claset > 
0  44 
{safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, 
45 
safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list, 

46 
haz_brls: (bool*thm)list} 

47 
val best_tac : claset > int > tactic 

48 
val contr_tac : int > tactic 

49 
val fast_tac : claset > int > tactic 

50 
val inst_step_tac : int > tactic 

51 
val joinrules : thm list * thm list > (bool * thm) list 

52 
val mp_tac: int > tactic 

53 
val safe_tac : claset > tactic 

54 
val safe_step_tac : claset > int > tactic 

55 
val slow_step_tac : claset > int > tactic 

56 
val step_tac : claset > int > tactic 

57 
val swapify : thm list > thm list 

58 
val swap_res_tac : thm list > int > tactic 

59 
val uniq_mp_tac: int > tactic 

60 
end; 

61 

62 

42799  63 
functor Classical(Data: CLASSICAL_DATA): CLASSICAL = 
0  64 
struct 
65 

66 
local open Data in 

67 

68 
(** Useful tactics for classical reasoning **) 

69 

70 
val imp_elim = make_elim mp; 

71 

72 
(*Solve goal that assumes both P and ~P. *) 

1459  73 
val contr_tac = etac not_elim THEN' assume_tac; 
0  74 

75 
(*Finds P>Q and P in the assumptions, replaces implication by Q *) 

76 
fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i THEN assume_tac i; 

77 

78 
(*Like mp_tac but instantiates no variables*) 

79 
fun uniq_mp_tac i = ematch_tac ([not_elim,imp_elim]) i THEN uniq_assume_tac i; 

80 

81 
(*Creates rules to eliminate ~A, from rules to introduce A*) 

82 
fun swapify intrs = intrs RLN (2, [swap]); 

83 

84 
(*Uses introduction rules in the normal way, or on negated assumptions, 

85 
trying rules in order. *) 

86 
fun swap_res_tac rls = 

87 
let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap)) 

88 
in assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls) 

89 
end; 

90 

91 

92 
(*** Classical rule sets ***) 

93 

94 
datatype claset = 

95 
CS of {safeIs: thm list, 

1459  96 
safeEs: thm list, 
97 
hazIs: thm list, 

98 
hazEs: thm list, 

99 
(*the following are computed from the above*) 

100 
safe0_brls: (bool*thm)list, 

101 
safep_brls: (bool*thm)list, 

102 
haz_brls: (bool*thm)list}; 

0  103 

4653  104 
fun rep_cs (CS x) = x; 
0  105 

106 
(*For use with biresolve_tac. Combines intrs with swap to catch negated 

107 
assumptions. Also pairs elims with true. *) 

108 
fun joinrules (intrs,elims) = 

109 
map (pair true) (elims @ swapify intrs) @ map (pair false) intrs; 

110 

111 
(*Note that allE precedes exI in haz_brls*) 

112 
fun make_cs {safeIs,safeEs,hazIs,hazEs} = 

113 
let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*) 

17496  114 
List.partition (curry (op =) 0 o subgoals_of_brl) 
4440  115 
(sort (make_ord lessb) (joinrules(safeIs, safeEs))) 
0  116 
in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, 
1459  117 
safe0_brls=safe0_brls, safep_brls=safep_brls, 
4440  118 
haz_brls = sort (make_ord lessb) (joinrules(hazIs, hazEs))} 
0  119 
end; 
120 

121 
(*** Manipulation of clasets ***) 

122 

123 
val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; 

124 

42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
37744
diff
changeset

125 
fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) = 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
26928
diff
changeset

126 
writeln (cat_lines 
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
37744
diff
changeset

127 
(["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @ 
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
37744
diff
changeset

128 
["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @ 
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
37744
diff
changeset

129 
["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @ 
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
37744
diff
changeset

130 
["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs)); 
0  131 

132 
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = 

133 
make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; 

134 

135 
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths = 

136 
make_cs {safeIs=safeIs, safeEs=ths@safeEs, hazIs=hazIs, hazEs=hazEs}; 

137 

138 
fun cs addSDs ths = cs addSEs (map make_elim ths); 

139 

140 
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addIs ths = 

141 
make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=ths@hazIs, hazEs=hazEs}; 

142 

143 
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addEs ths = 

144 
make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=ths@hazEs}; 

145 

146 
fun cs addDs ths = cs addEs (map make_elim ths); 

147 

148 
(*** Simple tactics for theorem proving ***) 

149 

150 
(*Attack subgoals using safe inferences*) 

151 
fun safe_step_tac (CS{safe0_brls,safep_brls,...}) = 

152 
FIRST' [uniq_assume_tac, 

1459  153 
uniq_mp_tac, 
154 
biresolve_tac safe0_brls, 

155 
FIRST' hyp_subst_tacs, 

156 
biresolve_tac safep_brls] ; 

0  157 

158 
(*Repeatedly attack subgoals using safe inferences*) 

159 
fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs)); 

160 

161 
(*These steps could instantiate variables and are therefore unsafe.*) 

162 
val inst_step_tac = assume_tac APPEND' contr_tac; 

163 

164 
(*Single step for the prover. FAILS unless it makes progress. *) 

165 
fun step_tac (cs as (CS{haz_brls,...})) i = 

166 
FIRST [safe_tac cs, 

167 
inst_step_tac i, 

168 
biresolve_tac haz_brls i]; 

169 

170 
(*** The following tactics all fail unless they solve one goal ***) 

171 

172 
(*Dumb but fast*) 

173 
fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); 

174 

175 
(*Slower but smarter than fast_tac*) 

176 
fun best_tac cs = 

177 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); 

178 

179 
(*Using a "safe" rule to instantiate variables is unsafe. This tactic 

180 
allows backtracking from "safe" rules to "unsafe" rules here.*) 

181 
fun slow_step_tac (cs as (CS{haz_brls,...})) i = 

182 
safe_tac cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i); 

183 

184 
end; 

185 
end; 