author  wenzelm 
Mon, 16 Nov 1998 11:09:02 +0100  
changeset 5885  6c920d876098 
parent 5841  d05df8752a8a 
child 5927  991483daa1a4 
permissions  rwrr 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

1 
(* Title: Provers/classical.ML 
0  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

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

7 
theory, etc. 

8 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

9 
Rules must be classified as intr, elim, safe, hazardous (unsafe). 
0  10 

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

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

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

14 
the conclusion. 

5841  15 

16 
TODO: 

17 
 only BASIC_CLASSICAL made pervasive; 

18 
 fix global claset data; 

0  19 
*) 
20 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

21 
(*higher precedence than := facilitates use of references*) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

22 
infix 4 addSIs addSEs addSDs addIs addEs addDs delrules 
4651  23 
addSWrapper delSWrapper addWrapper delWrapper 
5523  24 
addSbefore addSaltern addbefore addaltern 
25 
addD2 addE2 addSD2 addSE2; 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

26 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

27 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

28 
(*should be a type abbreviation in signature CLASSICAL*) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

29 
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; 
4651  30 
type wrapper = (int > tactic) > (int > tactic); 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

31 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

32 
signature CLASET_THY_DATA = 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

33 
sig 
5001  34 
val clasetN: string 
35 
val clasetK: Object.kind 

36 
exception ClasetData of Object.T ref 

4854  37 
val setup: (theory > theory) list 
5001  38 
val fix_methods: Object.T * (Object.T > Object.T) * 
39 
(Object.T * Object.T > Object.T) * (Sign.sg > Object.T > unit) > unit 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

40 
end; 
2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset

41 

0  42 
signature CLASSICAL_DATA = 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

43 
sig 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

44 
val mp : thm (* [ P>Q; P ] ==> Q *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

45 
val not_elim : thm (* [ ~P; P ] ==> R *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

46 
val classical : thm (* (~P ==> P) ==> P *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

47 
val sizef : thm > int (* size function for BEST_FIRST *) 
0  48 
val hyp_subst_tacs: (int > tactic) list 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

49 
end; 
0  50 

5841  51 
signature BASIC_CLASSICAL = 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

52 
sig 
0  53 
type claset 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

54 
val empty_cs: claset 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

55 
val print_cs: claset > unit 
4380  56 
val print_claset: theory > unit 
4653  57 
val rep_cs: (* BLAST_DATA in blast.ML dependent on this *) 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

58 
claset > {safeIs: thm list, safeEs: thm list, 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

59 
hazIs: thm list, hazEs: thm list, 
4651  60 
swrappers: (string * wrapper) list, 
61 
uwrappers: (string * wrapper) list, 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

62 
safe0_netpair: netpair, safep_netpair: netpair, 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

63 
haz_netpair: netpair, dup_netpair: netpair} 
1711  64 
val merge_cs : claset * claset > claset 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

65 
val addDs : claset * thm list > claset 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

66 
val addEs : claset * thm list > claset 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

67 
val addIs : claset * thm list > claset 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

68 
val addSDs : claset * thm list > claset 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

69 
val addSEs : claset * thm list > claset 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

70 
val addSIs : claset * thm list > claset 
1800  71 
val delrules : claset * thm list > claset 
4651  72 
val addSWrapper : claset * (string * wrapper) > claset 
73 
val delSWrapper : claset * string > claset 

74 
val addWrapper : claset * (string * wrapper) > claset 

75 
val delWrapper : claset * string > claset 

76 
val addSbefore : claset * (string * (int > tactic)) > claset 

77 
val addSaltern : claset * (string * (int > tactic)) > claset 

78 
val addbefore : claset * (string * (int > tactic)) > claset 

79 
val addaltern : claset * (string * (int > tactic)) > claset 

5523  80 
val addD2 : claset * (string * thm) > claset 
81 
val addE2 : claset * (string * thm) > claset 

82 
val addSD2 : claset * (string * thm) > claset 

83 
val addSE2 : claset * (string * thm) > claset 

4765  84 
val appSWrappers : claset > wrapper 
4651  85 
val appWrappers : claset > wrapper 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

86 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

87 
val claset_ref_of_sg: Sign.sg > claset ref 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

88 
val claset_ref_of: theory > claset ref 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

89 
val claset_of_sg: Sign.sg > claset 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

90 
val claset_of: theory > claset 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

91 
val CLASET: (claset > tactic) > tactic 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

92 
val CLASET': (claset > 'a > tactic) > 'a > tactic 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

93 
val claset: unit > claset 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

94 
val claset_ref: unit > claset ref 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

95 

1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

96 
val fast_tac : claset > int > tactic 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

97 
val slow_tac : claset > int > tactic 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

98 
val weight_ASTAR : int ref 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

99 
val astar_tac : claset > int > tactic 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

100 
val slow_astar_tac : claset > int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

101 
val best_tac : claset > int > tactic 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

102 
val slow_best_tac : claset > int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

103 
val depth_tac : claset > int > int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

104 
val deepen_tac : claset > int > int > tactic 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

105 

e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

106 
val contr_tac : int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

107 
val dup_elim : thm > thm 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

108 
val dup_intr : thm > thm 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

109 
val dup_step_tac : claset > int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

110 
val eq_mp_tac : int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

111 
val haz_step_tac : claset > int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

112 
val joinrules : thm list * thm list > (bool * thm) list 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

113 
val mp_tac : int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

114 
val safe_tac : claset > tactic 
5757  115 
val safe_steps_tac : claset > int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

116 
val safe_step_tac : claset > int > tactic 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

117 
val clarify_tac : claset > int > tactic 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

118 
val clarify_step_tac : claset > int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

119 
val step_tac : claset > int > tactic 
2630  120 
val slow_step_tac : claset > int > tactic 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

121 
val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

122 
val swapify : thm list > thm list 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

123 
val swap_res_tac : thm list > int > tactic 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

124 
val inst_step_tac : claset > int > tactic 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

125 
val inst0_step_tac : claset > int > tactic 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

126 
val instp_step_tac : claset > int > tactic 
1724  127 

128 
val AddDs : thm list > unit 

129 
val AddEs : thm list > unit 

130 
val AddIs : thm list > unit 

131 
val AddSDs : thm list > unit 

132 
val AddSEs : thm list > unit 

133 
val AddSIs : thm list > unit 

1807  134 
val Delrules : thm list > unit 
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

135 
val Safe_tac : tactic 
1814  136 
val Safe_step_tac : int > tactic 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

137 
val Clarify_tac : int > tactic 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

138 
val Clarify_step_tac : int > tactic 
1800  139 
val Step_tac : int > tactic 
1724  140 
val Fast_tac : int > tactic 
1800  141 
val Best_tac : int > tactic 
2066  142 
val Slow_tac : int > tactic 
143 
val Slow_best_tac : int > tactic 

1800  144 
val Deepen_tac : int > int > tactic 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

145 
end; 
1724  146 

5841  147 
signature CLASSICAL = 
148 
sig 

149 
include BASIC_CLASSICAL 

150 
val print_local_claset: Proof.context > unit 

151 
val get_local_claset: Proof.context > claset 

152 
val put_local_claset: claset > Proof.context > Proof.context 

5885  153 
val haz_dest_global: theory attribute 
154 
val haz_elim_global: theory attribute 

155 
val haz_intro_global: theory attribute 

5841  156 
val safe_dest_global: theory attribute 
157 
val safe_elim_global: theory attribute 

158 
val safe_intro_global: theory attribute 

5885  159 
val delrule_global: theory attribute 
160 
val haz_dest_local: Proof.context attribute 

161 
val haz_elim_local: Proof.context attribute 

162 
val haz_intro_local: Proof.context attribute 

5841  163 
val safe_dest_local: Proof.context attribute 
164 
val safe_elim_local: Proof.context attribute 

165 
val safe_intro_local: Proof.context attribute 

5885  166 
val delrule_local: Proof.context attribute 
5841  167 
val trace_rules: bool ref 
168 
val single_tac: claset > tthm list > int > tactic 

169 
val setup: (theory > theory) list 

170 
end; 

171 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

172 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

173 
structure ClasetThyData: CLASET_THY_DATA = 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

174 
struct 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

175 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

176 
(* data kind claset  forward declaration *) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

177 

5001  178 
val clasetN = "Provers/claset"; 
179 
val clasetK = Object.kind clasetN; 

180 
exception ClasetData of Object.T ref; 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

181 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

182 
local 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

183 
fun undef _ = raise Match; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

184 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

185 
val empty_ref = ref ERROR; 
5001  186 
val prep_ext_fn = ref (undef: Object.T > Object.T); 
187 
val merge_fn = ref (undef: Object.T * Object.T > Object.T); 

188 
val print_fn = ref (undef: Sign.sg > Object.T > unit); 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

189 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

190 
val empty = ClasetData empty_ref; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

191 
fun prep_ext exn = ! prep_ext_fn exn; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

192 
fun merge exn = ! merge_fn exn; 
4259  193 
fun print sg exn = ! print_fn sg exn; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

194 
in 
5001  195 
val setup = [Theory.init_data clasetK (empty, prep_ext, merge, print)]; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

196 
fun fix_methods (e, ext, mrg, prt) = 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

197 
(empty_ref := e; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

198 
end; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

199 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

200 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

201 
end; 
0  202 

203 

204 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 

205 
struct 

206 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

207 
local open ClasetThyData Data in 
0  208 

1800  209 
(*** Useful tactics for classical reasoning ***) 
0  210 

1524  211 
val imp_elim = (*cannot use bind_thm within a structure!*) 
212 
store_thm ("imp_elim", make_elim mp); 

0  213 

4392  214 
(*Prove goal that assumes both P and ~P. 
215 
No backtracking if it finds an equal assumption. Perhaps should call 

216 
ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) 

217 
val contr_tac = eresolve_tac [not_elim] THEN' 

218 
(eq_assume_tac ORELSE' assume_tac); 

0  219 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

220 
(*Finds P>Q and P in the assumptions, replaces implication by Q. 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

221 
Could do the same thing for P<>Q and P... *) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

222 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  223 

224 
(*Like mp_tac but instantiates no variables*) 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

225 
fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i THEN eq_assume_tac i; 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

226 

1524  227 
val swap = 
228 
store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical)); 

0  229 

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

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

232 

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

234 
trying rules in order. *) 

235 
fun swap_res_tac rls = 

54  236 
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls 
237 
in assume_tac ORELSE' 

238 
contr_tac ORELSE' 

239 
biresolve_tac (foldr addrl (rls,[])) 

0  240 
end; 
241 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

242 
(*Duplication of hazardous rules, for complete provers*) 
2689
6d3d893453de
dup_intr & dup_elim no longer call standard  this
paulson
parents:
2630
diff
changeset

243 
fun dup_intr th = zero_var_indexes (th RS classical); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

244 

4646  245 
fun dup_elim th = 
246 
th RSN (2, revcut_rl) > assumption 2 > Seq.hd > 

247 
rule_by_tactic (TRYALL (etac revcut_rl)) 

248 
handle _ => error ("Bad format for elimination rule\n" ^ string_of_thm th); 

0  249 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

250 

1800  251 
(**** Classical rule sets ****) 
0  252 

253 
datatype claset = 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

254 
CS of {safeIs : thm list, (*safe introduction rules*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

255 
safeEs : thm list, (*safe elimination rules*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

256 
hazIs : thm list, (*unsafe introduction rules*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

257 
hazEs : thm list, (*unsafe elimination rules*) 
4651  258 
swrappers : (string * wrapper) list, (*for transf. safe_step_tac*) 
259 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

260 
safe0_netpair : netpair, (*nets for trivial cases*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

261 
safep_netpair : netpair, (*nets for >0 subgoals*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

262 
haz_netpair : netpair, (*nets for unsafe rules*) 
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

263 
dup_netpair : netpair}; (*nets for duplication*) 
0  264 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

265 
(*Desired invariants are 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

266 
safe0_netpair = build safe0_brls, 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

267 
safep_netpair = build safep_brls, 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

268 
haz_netpair = build (joinrules(hazIs, hazEs)), 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

269 
dup_netpair = build (joinrules(map dup_intr hazIs, 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

270 
map dup_elim hazEs))} 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

271 

b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

272 
where build = build_netpair(Net.empty,Net.empty), 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

273 
safe0_brls contains all brules that solve the subgoal, and 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

274 
safep_brls contains all brules that generate 1 or more new subgoals. 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

275 
The theorem lists are largely comments, though they are used in merge_cs and print_cs. 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

276 
Nets must be built incrementally, to save space and time. 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

277 
*) 
0  278 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

279 
val empty_cs = 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

280 
CS{safeIs = [], 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

281 
safeEs = [], 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

282 
hazIs = [], 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

283 
hazEs = [], 
4651  284 
swrappers = [], 
285 
uwrappers = [], 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

286 
safe0_netpair = (Net.empty,Net.empty), 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

287 
safep_netpair = (Net.empty,Net.empty), 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

288 
haz_netpair = (Net.empty,Net.empty), 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

289 
dup_netpair = (Net.empty,Net.empty)}; 
0  290 

3546  291 
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, ...}) = 
292 
let val pretty_thms = map Display.pretty_thm in 

293 
Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs)); 

4624  294 
Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs)); 
4625  295 
Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs)); 
296 
Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs)) 

3546  297 
end; 
0  298 

4653  299 
fun rep_cs (CS args) = args; 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

300 

4651  301 
local 
302 
fun calc_wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac); 

303 
in 

304 
fun appSWrappers (CS{swrappers,...}) = calc_wrap swrappers; 

305 
fun appWrappers (CS{uwrappers,...}) = calc_wrap uwrappers; 

306 
end; 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

307 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

308 

1800  309 
(*** Adding (un)safe introduction or elimination rules. 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

310 

b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

311 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  312 
***) 
0  313 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

314 
(*For use with biresolve_tac. Combines intr rules with swap to handle negated 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

315 
assumptions. Pairs elim rules with true. *) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

316 
fun joinrules (intrs,elims) = 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

317 
(map (pair true) (elims @ swapify intrs) @ 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

318 
map (pair false) intrs); 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

319 

b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

320 
(*Priority: prefer rules with fewest subgoals, 
1231  321 
then rules added most recently (preferring the head of the list).*) 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

322 
fun tag_brls k [] = [] 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

323 
 tag_brls k (brl::brls) = 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

324 
(1000000*subgoals_of_brl brl + k, brl) :: 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

325 
tag_brls (k+1) brls; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

326 

1800  327 
fun insert_tagged_list kbrls netpr = foldr insert_tagged_brl (kbrls, netpr); 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

328 

b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

329 
(*Insert into netpair that already has nI intr rules and nE elim rules. 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

330 
Count the intr rules double (to account for swapify). Negate to give the 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

331 
new insertions the lowest priority.*) 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

332 
fun insert (nI,nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

333 

1800  334 
fun delete_tagged_list brls netpr = foldr delete_tagged_brl (brls, netpr); 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

335 

1800  336 
val delete = delete_tagged_list o joinrules; 
337 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

338 
val mem_thm = gen_mem eq_thm 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

339 
and rem_thm = gen_rem eq_thm; 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

340 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

341 
(*Warn if the rule is already present ELSEWHERE in the claset. The addition 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

342 
is still allowed.*) 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

343 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

344 
if mem_thm (th, safeIs) then 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

345 
warning ("Rule already in claset as Safe Intr\n" ^ string_of_thm th) 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

346 
else if mem_thm (th, safeEs) then 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

347 
warning ("Rule already in claset as Safe Elim\n" ^ string_of_thm th) 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

348 
else if mem_thm (th, hazIs) then 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

349 
warning ("Rule already in claset as unsafe Intr\n" ^ string_of_thm th) 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

350 
else if mem_thm (th, hazEs) then 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

351 
warning ("Rule already in claset as unsafe Elim\n" ^ string_of_thm th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

352 
else (); 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

353 

1800  354 
(*** Safe rules ***) 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

355 

4651  356 
fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

357 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

358 
th) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

359 
if mem_thm (th, safeIs) then 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

360 
(warning ("Ignoring duplicate Safe Intr\n" ^ string_of_thm th); 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

361 
cs) 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

362 
else 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

363 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

364 
partition (fn rl => nprems_of rl=0) [th] 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

365 
val nI = length safeIs + 1 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

366 
and nE = length safeEs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

367 
in warn_dup th cs; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

368 
CS{safeIs = th::safeIs, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

369 
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

370 
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

371 
safeEs = safeEs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

372 
hazIs = hazIs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

373 
hazEs = hazEs, 
4651  374 
swrappers = swrappers, 
375 
uwrappers = uwrappers, 

2630  376 
haz_netpair = haz_netpair, 
377 
dup_netpair = dup_netpair} 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

378 
end; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

379 

4651  380 
fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

381 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

382 
th) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

383 
if mem_thm (th, safeEs) then 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

384 
(warning ("Ignoring duplicate Safe Elim\n" ^ string_of_thm th); 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

385 
cs) 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

386 
else 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

387 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

388 
partition (fn rl => nprems_of rl=1) [th] 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

389 
val nI = length safeIs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

390 
and nE = length safeEs + 1 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

391 
in warn_dup th cs; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

392 
CS{safeEs = th::safeEs, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

393 
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

394 
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

395 
safeIs = safeIs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

396 
hazIs = hazIs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

397 
hazEs = hazEs, 
4651  398 
swrappers = swrappers, 
399 
uwrappers = uwrappers, 

2630  400 
haz_netpair = haz_netpair, 
401 
dup_netpair = dup_netpair} 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

402 
end; 
0  403 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

404 
fun rev_foldl f (e, l) = foldl f (e, rev l); 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

405 

6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

406 
val op addSIs = rev_foldl addSI; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

407 
val op addSEs = rev_foldl addSE; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

408 

0  409 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
410 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

411 

1800  412 
(*** Hazardous (unsafe) rules ***) 
0  413 

4651  414 
fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

415 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

416 
th)= 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

417 
if mem_thm (th, hazIs) then 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

418 
(warning ("Ignoring duplicate unsafe Intr\n" ^ string_of_thm th); 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

419 
cs) 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

420 
else 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

421 
let val nI = length hazIs + 1 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

422 
and nE = length hazEs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

423 
in warn_dup th cs; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

424 
CS{hazIs = th::hazIs, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

425 
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

426 
dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

427 
safeIs = safeIs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

428 
safeEs = safeEs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

429 
hazEs = hazEs, 
4651  430 
swrappers = swrappers, 
431 
uwrappers = uwrappers, 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

432 
safe0_netpair = safe0_netpair, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

433 
safep_netpair = safep_netpair} 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

434 
end; 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

435 

4651  436 
fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

437 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

438 
th) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

439 
if mem_thm (th, hazEs) then 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

440 
(warning ("Ignoring duplicate unsafe Elim\n" ^ string_of_thm th); 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

441 
cs) 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

442 
else 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

443 
let val nI = length hazIs 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

444 
and nE = length hazEs + 1 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

445 
in warn_dup th cs; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

446 
CS{hazEs = th::hazEs, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

447 
haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

448 
dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

449 
safeIs = safeIs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

450 
safeEs = safeEs, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

451 
hazIs = hazIs, 
4651  452 
swrappers = swrappers, 
453 
uwrappers = uwrappers, 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

454 
safe0_netpair = safe0_netpair, 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

455 
safep_netpair = safep_netpair} 
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

456 
end; 
0  457 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

458 
val op addIs = rev_foldl addI; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

459 
val op addEs = rev_foldl addE; 
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

460 

0  461 
fun cs addDs ths = cs addEs (map make_elim ths); 
462 

1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

463 

1800  464 
(*** Deletion of rules 
465 
Working out what to delete, requires repeating much of the code used 

466 
to insert. 

1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

467 
Separate functions delSI, etc., are not exported; instead delrules 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

468 
searches in all the lists and chooses the relevant delXX functions. 
1800  469 
***) 
470 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

471 
fun delSI th 
4651  472 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

473 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

474 
if mem_thm (th, safeIs) then 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

475 
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th] 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

476 
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

477 
safep_netpair = delete (safep_rls, []) safep_netpair, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

478 
safeIs = rem_thm (safeIs,th), 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

479 
safeEs = safeEs, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

480 
hazIs = hazIs, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

481 
hazEs = hazEs, 
4651  482 
swrappers = swrappers, 
483 
uwrappers = uwrappers, 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

484 
haz_netpair = haz_netpair, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

485 
dup_netpair = dup_netpair} 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

486 
end 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

487 
else cs; 
1800  488 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

489 
fun delSE th 
4651  490 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

491 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

492 
if mem_thm (th, safeEs) then 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

493 
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th] 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

494 
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

495 
safep_netpair = delete ([], safep_rls) safep_netpair, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

496 
safeIs = safeIs, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

497 
safeEs = rem_thm (safeEs,th), 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

498 
hazIs = hazIs, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

499 
hazEs = hazEs, 
4651  500 
swrappers = swrappers, 
501 
uwrappers = uwrappers, 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

502 
haz_netpair = haz_netpair, 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

503 
dup_netpair = dup_netpair} 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

504 
end 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

505 
else cs; 
1800  506 

507 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

508 
fun delI th 
4651  509 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

510 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

511 
if mem_thm (th, hazIs) then 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

512 
CS{haz_netpair = delete ([th], []) haz_netpair, 
1800  513 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
514 
safeIs = safeIs, 

515 
safeEs = safeEs, 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

516 
hazIs = rem_thm (hazIs,th), 
1800  517 
hazEs = hazEs, 
4651  518 
swrappers = swrappers, 
519 
uwrappers = uwrappers, 

1800  520 
safe0_netpair = safe0_netpair, 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

521 
safep_netpair = safep_netpair} 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

522 
else cs; 
1800  523 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

524 
fun delE th 
4651  525 
(cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

526 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) = 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

527 
if mem_thm (th, hazEs) then 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

528 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
1800  529 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
530 
safeIs = safeIs, 

531 
safeEs = safeEs, 

532 
hazIs = hazIs, 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

533 
hazEs = rem_thm (hazEs,th), 
4651  534 
swrappers = swrappers, 
535 
uwrappers = uwrappers, 

1800  536 
safe0_netpair = safe0_netpair, 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

537 
safep_netpair = safep_netpair} 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

538 
else cs; 
1800  539 

2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

540 
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) 
1800  541 
fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

542 
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

543 
mem_thm (th, hazIs) orelse mem_thm (th, hazEs) 
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

544 
then delSI th (delSE th (delI th (delE th cs))) 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

545 
else (warning ("Rule not in claset\n" ^ (string_of_thm th)); 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

546 
cs); 
1800  547 

548 
val op delrules = foldl delrule; 

549 

550 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

551 
(*** Modifying the wrapper tacticals ***) 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

552 
fun update_swrappers 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

553 
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

554 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) f = 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

555 
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

556 
swrappers = f swrappers, uwrappers = uwrappers, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

557 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

558 
haz_netpair = haz_netpair, dup_netpair = dup_netpair}; 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

559 

b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

560 
fun update_uwrappers 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

561 
(CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

562 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) f = 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

563 
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

564 
swrappers = swrappers, uwrappers = f uwrappers, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

565 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

566 
haz_netpair = haz_netpair, dup_netpair = dup_netpair}; 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

567 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

568 

4651  569 
(*Add/replace a safe wrapper*) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

570 
fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers => 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

571 
(case assoc_string (swrappers,(fst new_swrapper)) of None =>() 
4651  572 
 Some x => warning("overwriting safe wrapper "^fst new_swrapper); 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

573 
overwrite (swrappers, new_swrapper))); 
4651  574 

575 
(*Add/replace an unsafe wrapper*) 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

576 
fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers => 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

577 
(case assoc_string (uwrappers,(fst new_uwrapper)) of None =>() 
4651  578 
 Some x => warning ("overwriting unsafe wrapper "^fst new_uwrapper); 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

579 
overwrite (uwrappers, new_uwrapper))); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

580 

4651  581 
(*Remove a safe wrapper*) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

582 
fun cs delSWrapper name = update_swrappers cs (fn swrappers => 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

583 
let val (del,rest) = partition (fn (n,_) => n=name) swrappers 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

584 
in if null del then (warning ("No such safe wrapper in claset: "^ name); 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

585 
swrappers) else rest end); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

586 

4651  587 
(*Remove an unsafe wrapper*) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

588 
fun cs delWrapper name = update_uwrappers cs (fn uwrappers => 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

589 
let val (del,rest) = partition (fn (n,_) => n=name) uwrappers 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

590 
in if null del then (warning ("No such unsafe wrapper in claset: " ^ name); 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

591 
uwrappers) else rest end); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

592 

2630  593 
(*compose a safe tactic sequentially before/alternatively after safe_step_tac*) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

594 
fun cs addSbefore (name, tac1) = 
5523  595 
cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

596 
fun cs addSaltern (name, tac2) = 
5523  597 
cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2); 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

598 

2630  599 
(*compose a tactic sequentially before/alternatively after the step tactic*) 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

600 
fun cs addbefore (name, tac1) = 
5523  601 
cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

602 
fun cs addaltern (name, tac2) = 
5523  603 
cs addWrapper (name, fn tac1 => tac1 APPEND' tac2); 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

604 

5523  605 
fun cs addD2 (name, thm) = 
606 
cs addaltern (name, dtac thm THEN' atac); 

607 
fun cs addE2 (name, thm) = 

608 
cs addaltern (name, etac thm THEN' atac); 

609 
fun cs addSD2 (name, thm) = 

610 
cs addSaltern (name, dmatch_tac [thm] THEN' eq_assume_tac); 

611 
fun cs addSE2 (name, thm) = 

612 
cs addSaltern (name, ematch_tac [thm] THEN' eq_assume_tac); 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

613 

1711  614 
(*Merge works by adding all new rules of the 2nd claset into the 1st claset. 
615 
Merging the term nets may look more efficient, but the rather delicate 

616 
treatment of priority might get muddled up.*) 

617 
fun merge_cs 

2630  618 
(cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, 
4765  619 
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, 
620 
swrappers, uwrappers, ...}) = 

1711  621 
let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) 
622 
val safeEs' = gen_rems eq_thm (safeEs2,safeEs) 

2630  623 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
624 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

625 
val cs1 = cs addSIs safeIs' 
4765  626 
addSEs safeEs' 
627 
addIs hazIs' 

628 
addEs hazEs' 

4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

629 
val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers); 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

630 
val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); 
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

631 
in cs3 
1711  632 
end; 
633 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

634 

1800  635 
(**** Simple tactics for theorem proving ****) 
0  636 

637 
(*Attack subgoals using safe inferences  matching, not resolution*) 

2630  638 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  639 
appSWrappers cs (FIRST' [ 
2630  640 
eq_assume_tac, 
641 
eq_mp_tac, 

642 
bimatch_from_nets_tac safe0_netpair, 

643 
FIRST' hyp_subst_tacs, 

644 
bimatch_from_nets_tac safep_netpair]); 

0  645 

5757  646 
(*Repeatedly attack a subgoal using safe inferences  it's deterministic!*) 
647 
fun safe_steps_tac cs = REPEAT_DETERM1 o 

648 
(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); 

649 

0  650 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 
5757  651 
fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs)); 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

652 

3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

653 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

654 
(*** Clarify_tac: do safe steps without causing branching ***) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

655 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

656 
fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n); 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

657 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

658 
(*version of bimatch_from_nets_tac that only applies rules that 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

659 
create precisely n subgoals.*) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

660 
fun n_bimatch_from_nets_tac n = 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

661 
biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true; 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

662 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

663 
fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

664 
val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

665 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

666 
(*Twoway branching is allowed only if one of the branches immediately closes*) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

667 
fun bimatch2_tac netpair i = 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

668 
n_bimatch_from_nets_tac 2 netpair i THEN 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

669 
(eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1)); 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

670 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

671 
(*Attack subgoals using safe inferences  matching, not resolution*) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

672 
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  673 
appSWrappers cs (FIRST' [ 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

674 
eq_assume_contr_tac, 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

675 
bimatch_from_nets_tac safe0_netpair, 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

676 
FIRST' hyp_subst_tacs, 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

677 
n_bimatch_from_nets_tac 1 safep_netpair, 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

678 
bimatch2_tac safep_netpair]); 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

679 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

680 
fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1)); 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

681 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

682 

76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

683 
(*** Unsafe steps instantiate variables or lose information ***) 
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

684 

4066  685 
(*Backtracking is allowed among the various these unsafe ways of 
686 
proving a subgoal. *) 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

687 
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

688 
assume_tac APPEND' 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

689 
contr_tac APPEND' 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

690 
biresolve_from_nets_tac safe0_netpair; 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

691 

4066  692 
(*These unsafe steps could generate more subgoals.*) 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

693 
fun instp_step_tac (CS{safep_netpair,...}) = 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

694 
biresolve_from_nets_tac safep_netpair; 
0  695 

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

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

697 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  698 

982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

699 
fun haz_step_tac (CS{haz_netpair,...}) = 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

700 
biresolve_from_nets_tac haz_netpair; 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

701 

0  702 
(*Single step for the prover. FAILS unless it makes progress. *) 
5523  703 
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
704 
(inst_step_tac cs ORELSE' haz_step_tac cs) i; 

0  705 

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

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

5523  708 
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
709 
(inst_step_tac cs APPEND' haz_step_tac cs) i; 

0  710 

1800  711 
(**** The following tactics all fail unless they solve one goal ****) 
0  712 

713 
(*Dumb but fast*) 

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

715 

716 
(*Slower but smarter than fast_tac*) 

717 
fun best_tac cs = 

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

719 

720 
fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); 

721 

722 
fun slow_best_tac cs = 

723 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); 

724 

681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

725 

1800  726 
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

727 
val weight_ASTAR = ref 5; 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

728 

e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

729 
fun astar_tac cs = 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

730 
SELECT_GOAL ( ASTAR (has_fewer_prems 1 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

731 
, fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

732 
(step_tac cs 1)); 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

733 

e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

734 
fun slow_astar_tac cs = 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

735 
SELECT_GOAL ( ASTAR (has_fewer_prems 1 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

736 
, fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

737 
(slow_step_tac cs 1)); 
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset

738 

1800  739 
(**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

740 
of much experimentation! Changing APPEND to ORELSE below would prove 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

741 
easy theorems faster, but loses completeness  and many of the harder 
1800  742 
theorems such as 43. ****) 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

743 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

744 
(*Nondeterministic! Could always expand the first unsafe connective. 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

745 
That's hard to implement and did not perform better in experiments, due to 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

746 
greater search depth required.*) 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

747 
fun dup_step_tac (cs as (CS{dup_netpair,...})) = 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

748 
biresolve_from_nets_tac dup_netpair; 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

749 

5523  750 
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) 
5757  751 
local 
752 
fun slow_step_tac' cs = appWrappers cs 

753 
(instp_step_tac cs APPEND' dup_step_tac cs); 

754 
in fun depth_tac cs m i state = SELECT_GOAL 

755 
(safe_steps_tac cs 1 THEN_ELSE 

756 
(DEPTH_SOLVE (depth_tac cs m 1), 

757 
inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac 

758 
(slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m1) 1)) 

759 
)) i state; 

760 
end; 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

761 

2173  762 
(*Search, with depth bound m. 
763 
This is the "entry point", which does safe inferences first.*) 

747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

764 
fun safe_depth_tac cs m = 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

765 
SUBGOAL 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

766 
(fn (prem,i) => 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

767 
let val deti = 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

768 
(*No Vars in the goal? No need to backtrack between goals.*) 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

769 
case term_vars prem of 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

770 
[] => DETERM 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

771 
 _::_ => I 
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

772 
in SELECT_GOAL (TRY (safe_tac cs) THEN 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

773 
DEPTH_SOLVE (deti (depth_tac cs m 1))) i 
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

774 
end); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

775 

2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset

776 
fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs); 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

777 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

778 

1724  779 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

780 
(** claset theory data **) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

781 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

782 
(* init data kind claset *) 
1724  783 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

784 
exception CSData of claset ref; 
1724  785 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

786 
local 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

787 
val empty = CSData (ref empty_cs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

788 

9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

789 
(*create new references*) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

790 
fun prep_ext (ClasetData (ref (CSData (ref cs)))) = 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

791 
ClasetData (ref (CSData (ref cs))); 
1724  792 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

793 
fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) = 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

794 
ClasetData (ref (CSData (ref (merge_cs (cs1, cs2))))); 
1724  795 

4259  796 
fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

797 
in 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

798 
val _ = fix_methods (empty, prep_ext, merge, print); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

799 
end; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

800 

1724  801 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

802 
(* access claset *) 
1724  803 

5001  804 
val print_claset = Theory.print_data clasetK; 
4380  805 

5001  806 
val claset_ref_of_sg = Sign.get_data clasetK (fn ClasetData (ref (CSData r)) => r); 
1807  807 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

808 
val claset_ref_of = claset_ref_of_sg o sign_of; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

809 
val claset_of_sg = ! o claset_ref_of_sg; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

810 
val claset_of = claset_of_sg o sign_of; 
1800  811 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

812 
fun CLASET tacf state = tacf (claset_of_sg (sign_of_thm state)) state; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

813 
fun CLASET' tacf i state = tacf (claset_of_sg (sign_of_thm state)) i state; 
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

814 

5028  815 
val claset = claset_of o Context.the_context; 
816 
val claset_ref = claset_ref_of_sg o sign_of o Context.the_context; 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

817 

3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset

818 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

819 
(* change claset *) 
1800  820 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

821 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  822 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

823 
val AddDs = change_claset (op addDs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

824 
val AddEs = change_claset (op addEs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

825 
val AddIs = change_claset (op addIs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

826 
val AddSDs = change_claset (op addSDs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

827 
val AddSEs = change_claset (op addSEs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

828 
val AddSIs = change_claset (op addSIs); 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

829 
val Delrules = change_claset (op delrules); 
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset

830 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

831 

5841  832 
(* proof data kind 'Provers/claset' *) 
833 

834 
structure LocalClasetArgs = 

835 
struct 

836 
val name = "Provers/claset"; 

837 
type T = claset; 

838 
val init = claset_of; 

839 
fun print _ cs = print_cs cs; 

840 
end; 

841 

842 
structure LocalClaset = ProofDataFun(LocalClasetArgs); 

843 
val print_local_claset = LocalClaset.print; 

844 
val get_local_claset = LocalClaset.get; 

845 
val put_local_claset = LocalClaset.put; 

846 

847 

5885  848 
(* attributes *) 
849 

850 
fun change_global_cs f (thy, th) = 

851 
let val r = claset_ref_of thy 

852 
in r := f (! r, [Attribute.thm_of th]); (thy, th) end; 

853 

854 
fun change_local_cs f (ctxt, th) = 

855 
let val cs = f (get_local_claset ctxt, [Attribute.thm_of th]) 

856 
in (put_local_claset cs ctxt, th) end; 

857 

858 
val haz_dest_global = change_global_cs (op addDs); 

859 
val haz_elim_global = change_global_cs (op addEs); 

860 
val haz_intro_global = change_global_cs (op addIs); 

861 
val safe_dest_global = change_global_cs (op addSDs); 

862 
val safe_elim_global = change_global_cs (op addSEs); 

863 
val safe_intro_global = change_global_cs (op addSIs); 

864 
val delrule_global = change_global_cs (op delrules); 

865 

866 
val haz_dest_local = change_local_cs (op addDs); 

867 
val haz_elim_local = change_local_cs (op addEs); 

868 
val haz_intro_local = change_local_cs (op addIs); 

869 
val safe_dest_local = change_local_cs (op addSDs); 

870 
val safe_elim_local = change_local_cs (op addSEs); 

871 
val safe_intro_local = change_local_cs (op addSIs); 

872 
val delrule_local = change_local_cs (op delrules); 

873 

874 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

875 
(* tactics referring to the implicit claset *) 
1800  876 

4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

877 
(*the abstraction over the proof state delays the dereferencing*) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

878 
fun Safe_tac st = safe_tac (claset()) st; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

879 
fun Safe_step_tac i st = safe_step_tac (claset()) i st; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

880 
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

881 
fun Clarify_tac i st = clarify_tac (claset()) i st; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

882 
fun Step_tac i st = step_tac (claset()) i st; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

883 
fun Fast_tac i st = fast_tac (claset()) i st; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

884 
fun Best_tac i st = best_tac (claset()) i st; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

885 
fun Slow_tac i st = slow_tac (claset()) i st; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

886 
fun Slow_best_tac i st = slow_best_tac (claset()) i st; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

887 
fun Deepen_tac m = deepen_tac (claset()) m; 
2066  888 

1800  889 

0  890 
end; 
5841  891 

892 

893 

5885  894 
(** concrete syntax of attributes **) 
5841  895 

896 
(* add / del rules *) 

897 

898 
val introN = "intro"; 

899 
val elimN = "elim"; 

900 
val destN = "dest"; 

901 
val delN = "del"; 

5885  902 
val delruleN = "delrule"; 
5841  903 

5885  904 
val bang = Args.$$$ "!"; 
5841  905 

5885  906 
fun cla_att change haz safe = 
907 
Attrib.syntax (Scan.lift ((bang >> K haz  Scan.succeed safe) >> change)); 

5841  908 

5885  909 
fun cla_attr f g = (cla_att change_global_cs f g, cla_att change_local_cs f g); 
910 
val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local); 

5841  911 

912 

913 
(* setup_attrs *) 

914 

915 
val setup_attrs = Attrib.add_attributes 

5885  916 
[(destN, cla_attr (op addDs) (op addSDs), "destruction rule"), 
917 
(elimN, cla_attr (op addEs) (op addSEs), "elimination rule"), 

918 
(introN, cla_attr (op addIs) (op addSIs), "introduction rule"), 

919 
(delruleN, del_attr, "delete rule")]; 

5841  920 

921 

922 

5885  923 
(** single rule proof method **) 
5841  924 

925 
(* utils *) 

926 

927 
fun resolve_from_seq_tac rq i st = Seq.flat (Seq.map (fn r => rtac r i st) rq); 

928 
fun order_rules xs = map snd (Tactic.orderlist xs); 

929 

930 
fun find_rules concl nets = 

931 
let fun rules_of (inet, _) = order_rules (Net.unify_term inet concl) 

932 
in flat (map rules_of nets) end; 

933 

934 
fun find_erules [] _ = [] 

935 
 find_erules facts nets = 

936 
let 

937 
fun may_unify net = Net.unify_term net o #prop o Thm.rep_thm; 

938 
fun erules_of (_, enet) = order_rules (flat (map (may_unify enet) facts)); 

939 
in flat (map erules_of nets) end; 

940 

941 

942 
(* trace rules *) 

943 

944 
val trace_rules = ref false; 

945 

946 
fun print_rules rules i = 

947 
if not (! trace_rules) then () 

948 
else 

949 
Pretty.writeln (Pretty.big_list ("trying standard rule(s) on goal #" ^ string_of_int i ^ ":") 

950 
(map Display.pretty_thm rules)); 

951 

952 

953 
(* single_tac *) 

954 

955 
fun single_tac cs tfacts = 

956 
let 

957 
val CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...} = cs; 

5885  958 
val facts = Attribute.thms_of tfacts; 
5841  959 
val nets = [safe0_netpair, safep_netpair, haz_netpair, dup_netpair]; 
960 
val erules = find_erules facts nets; 

961 

962 
val tac = SUBGOAL (fn (goal, i) => 

963 
let 

964 
val irules = find_rules (Logic.strip_assums_concl goal) nets; 

965 
val rules = erules @ irules; 

966 
val ruleq = Method.forward_chain facts rules; 

967 
in 

968 
print_rules rules i; 

969 
fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end); 

970 
in tac end; 

971 

972 
val single = Method.METHOD (FIRSTGOAL o (fn facts => CLASET' (fn cs => single_tac cs facts))); 

973 

974 

975 

976 
(** automatic methods **) 

977 

5885  978 
val cla_args = 
979 
Method.only_sectioned_args 

980 
[Args.$$$ destN  bang >> K haz_dest_local, 

981 
Args.$$$ destN >> K safe_dest_local, 

982 
Args.$$$ elimN  bang >> K haz_elim_local, 

983 
Args.$$$ elimN >> K safe_elim_local, 

984 
Args.$$$ introN  bang >> K haz_intro_local, 

985 
Args.$$$ introN >> K safe_intro_local, 

986 
Args.$$$ delN >> K delrule_local]; 

5841  987 

5885  988 
fun cla_meth tac ctxt = Method.METHOD0 (tac (get_local_claset ctxt)); 
989 
fun cla_meth' tac ctxt = Method.METHOD0 (FIRSTGOAL (tac (get_local_claset ctxt))); 

5841  990 

5885  991 
val cla_method = cla_args o cla_meth; 
992 
val cla_method' = cla_args o cla_meth'; 

5841  993 

994 

995 

996 
(** setup_methods **) 

997 

998 
val setup_methods = Method.add_methods 

999 
[("single", Method.no_args single, "apply standard rule (single step)"), 

1000 
("default", Method.no_args single, "apply standard rule (single step)"), 

5885  1001 
("safe_tac", cla_method safe_tac, "safe_tac"), 
1002 
("safe_step", cla_method' safe_step_tac, "step_tac"), 

1003 
("fast", cla_method' fast_tac, "fast_tac"), 

1004 
("best", cla_method' best_tac, "best_tac"), 

1005 
("slow", cla_method' slow_tac, "slow_tac"), 

1006 
("slow_best", cla_method' slow_best_tac, "slow_best_tac")]; 

5841  1007 

1008 

1009 

1010 
(** theory setup **) 

1011 

1012 
(* FIXME claset theory data *) 

1013 

1014 
val setup = [LocalClaset.init, setup_attrs, setup_methods]; 

1015 

1016 

1017 
end; 