author  wenzelm 
Fri, 01 Jan 2016 10:49:00 +0100  
changeset 62020  5d208fd2507d 
parent 61268  abe08fb15a12 
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 *) 

60754  25 
val hyp_subst_tacs: Proof.context > (int > tactic) list 
0  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} 

58957  47 
val best_tac : Proof.context > claset > int > tactic 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

48 
val contr_tac : Proof.context > int > tactic 
58957  49 
val fast_tac : Proof.context > claset > int > tactic 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

50 
val inst_step_tac : Proof.context > int > tactic 
0  51 
val joinrules : thm list * thm list > (bool * thm) list 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

52 
val mp_tac: Proof.context > int > tactic 
58957  53 
val safe_tac : Proof.context > claset > tactic 
54 
val safe_step_tac : Proof.context > claset > int > tactic 

55 
val slow_step_tac : Proof.context > claset > int > tactic 

56 
val step_tac : Proof.context > claset > int > tactic 

0  57 
val swapify : thm list > thm list 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

58 
val swap_res_tac : Proof.context > thm list > int > tactic 
58957  59 
val uniq_mp_tac: Proof.context > int > tactic 
0  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. *) 

60754  73 
fun contr_tac ctxt = eresolve_tac ctxt [not_elim] THEN' assume_tac ctxt; 
0  74 

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

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

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

78 
(*Like mp_tac but instantiates no variables*) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

79 
fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i THEN uniq_assume_tac ctxt i; 
0  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. *) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

86 
fun swap_res_tac ctxt rls = 
60754  87 
let fun tacf rl = resolve_tac ctxt [rl] ORELSE' eresolve_tac ctxt [rl RSN (2, swap)] 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

88 
in assume_tac ctxt ORELSE' contr_tac ctxt ORELSE' FIRST' (map tacf rls) 
0  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 
61268  127 
(["Introduction rules"] @ map (Thm.string_of_thm ctxt) hazIs @ 
128 
["Safe introduction rules"] @ map (Thm.string_of_thm ctxt) safeIs @ 

129 
["Elimination rules"] @ map (Thm.string_of_thm ctxt) hazEs @ 

130 
["Safe elimination rules"] @ map (Thm.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*) 

58957  151 
fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) = 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

152 
FIRST' [uniq_assume_tac ctxt, 
58957  153 
uniq_mp_tac ctxt, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

154 
biresolve_tac ctxt safe0_brls, 
60754  155 
FIRST' (hyp_subst_tacs ctxt), 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

156 
biresolve_tac ctxt safep_brls] ; 
0  157 

158 
(*Repeatedly attack subgoals using safe inferences*) 

58957  159 
fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs)); 
0  160 

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

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

162 
fun inst_step_tac ctxt = assume_tac ctxt APPEND' contr_tac ctxt; 
0  163 

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

58957  165 
fun step_tac ctxt (cs as (CS{haz_brls,...})) i = 
166 
FIRST [safe_tac ctxt cs, 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

167 
inst_step_tac ctxt i, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

168 
biresolve_tac ctxt haz_brls i]; 
0  169 

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

171 

172 
(*Dumb but fast*) 

58957  173 
fun fast_tac ctxt cs = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt cs 1)); 
0  174 

175 
(*Slower but smarter than fast_tac*) 

58957  176 
fun best_tac ctxt cs = 
177 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac ctxt cs 1)); 

0  178 

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

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

58957  181 
fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

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

184 
end; 

185 
end; 