author  wenzelm 
Tue, 17 Aug 1999 17:30:08 +0200  
changeset 7230  4ca0d7839ff1 
parent 7154  687657a3f7e6 
child 7272  d20f51e43909 
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. 

15 
*) 

16 

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

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

18 
infix 4 addSIs addSEs addSDs addIs addEs addDs delrules 
4651  19 
addSWrapper delSWrapper addWrapper delWrapper 
5523  20 
addSbefore addSaltern addbefore addaltern 
21 
addD2 addE2 addSD2 addSE2; 

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

22 

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

23 

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

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

25 
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; 
4651  26 
type wrapper = (int > tactic) > (int > tactic); 
4079
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 
signature CLASET_THY_DATA = 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

29 
sig 
5001  30 
val clasetN: string 
31 
val clasetK: Object.kind 

32 
exception ClasetData of Object.T ref 

4854  33 
val setup: (theory > theory) list 
6556  34 
val fix_methods: Object.T * (Object.T > Object.T) * (Object.T > Object.T) * 
5001  35 
(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

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

37 

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

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

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

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

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

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

45 
end; 
0  46 

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

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

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

51 
val print_cs: claset > unit 
4380  52 
val print_claset: theory > unit 
4653  53 
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

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

55 
hazIs: thm list, hazEs: thm list, 
6955  56 
xtraIs: thm list, xtraEs: thm list, 
4651  57 
swrappers: (string * wrapper) list, 
58 
uwrappers: (string * wrapper) list, 

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

59 
safe0_netpair: netpair, safep_netpair: netpair, 
6955  60 
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} 
1711  61 
val merge_cs : claset * claset > claset 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

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

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

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

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

67 
val addSIs : claset * thm list > claset 
1800  68 
val delrules : claset * thm list > claset 
4651  69 
val addSWrapper : claset * (string * wrapper) > claset 
70 
val delSWrapper : claset * string > claset 

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

72 
val delWrapper : claset * string > claset 

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

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

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

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

5523  77 
val addD2 : claset * (string * thm) > claset 
78 
val addE2 : claset * (string * thm) > claset 

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

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

4765  81 
val appSWrappers : claset > wrapper 
4651  82 
val appWrappers : claset > wrapper 
5927  83 
val trace_rules : bool ref 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

84 

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

85 
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

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

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

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

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

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

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

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

93 

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

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

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

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

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

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

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

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

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

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

103 

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

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

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

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

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

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

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

110 
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

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

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

114 
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

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

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

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

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

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

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

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

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

124 
val instp_step_tac : claset > int > tactic 
1724  125 

126 
val AddDs : thm list > unit 

127 
val AddEs : thm list > unit 

128 
val AddIs : thm list > unit 

129 
val AddSDs : thm list > unit 

130 
val AddSEs : thm list > unit 

131 
val AddSIs : thm list > unit 

6955  132 
val AddXDs : thm list > unit 
133 
val AddXEs : thm list > unit 

134 
val AddXIs : thm list > unit 

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

136 
val Safe_tac : tactic 
1814  137 
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

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

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

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

146 
end; 
1724  147 

5841  148 
signature CLASSICAL = 
149 
sig 

150 
include BASIC_CLASSICAL 

151 
val print_local_claset: Proof.context > unit 

152 
val get_local_claset: Proof.context > claset 

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

154 
val safe_dest_global: theory attribute 

155 
val safe_elim_global: theory attribute 

156 
val safe_intro_global: theory attribute 

6955  157 
val haz_dest_global: theory attribute 
158 
val haz_elim_global: theory attribute 

159 
val haz_intro_global: theory attribute 

160 
val xtra_dest_global: theory attribute 

161 
val xtra_elim_global: theory attribute 

162 
val xtra_intro_global: theory attribute 

5885  163 
val delrule_global: theory attribute 
6955  164 
val safe_dest_local: Proof.context attribute 
165 
val safe_elim_local: Proof.context attribute 

166 
val safe_intro_local: Proof.context attribute 

5885  167 
val haz_dest_local: Proof.context attribute 
168 
val haz_elim_local: Proof.context attribute 

169 
val haz_intro_local: Proof.context attribute 

6955  170 
val xtra_dest_local: Proof.context attribute 
171 
val xtra_elim_local: Proof.context attribute 

172 
val xtra_intro_local: Proof.context attribute 

5885  173 
val delrule_local: Proof.context attribute 
5927  174 
val cla_modifiers: (Args.T list > (Proof.context attribute * Args.T list)) list 
7154  175 
val cla_meth: (claset > tactic) > Proof.context > Proof.method 
176 
val cla_meth': (claset > int > tactic) > Proof.context > Proof.method 

5927  177 
val cla_method: (claset > tactic) > Args.src > Proof.context > Proof.method 
178 
val cla_method': (claset > int > tactic) > Args.src > Proof.context > Proof.method 

5841  179 
val setup: (theory > theory) list 
180 
end; 

181 

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

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

183 
struct 
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 
(* data kind claset  forward declaration *) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

186 

5001  187 
val clasetN = "Provers/claset"; 
188 
val clasetK = Object.kind clasetN; 

189 
exception ClasetData of Object.T ref; 

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

190 

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

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

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

193 

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

194 
val empty_ref = ref ERROR; 
6556  195 
val copy_fn = ref (undef: Object.T > Object.T); 
5001  196 
val prep_ext_fn = ref (undef: Object.T > Object.T); 
197 
val merge_fn = ref (undef: Object.T * Object.T > Object.T); 

198 
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

199 

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

200 
val empty = ClasetData empty_ref; 
6556  201 
fun copy exn = ! copy_fn exn; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

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

203 
fun merge exn = ! merge_fn exn; 
4259  204 
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

205 
in 
6556  206 
val setup = [Theory.init_data clasetK (empty, copy, prep_ext, merge, print)]; 
207 
fun fix_methods (e, cp, ext, mrg, prt) = 

208 
(empty_ref := e; copy_fn := cp; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt); 

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

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

210 

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

211 

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

212 
end; 
0  213 

214 

5927  215 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  216 
struct 
217 

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

218 
local open ClasetThyData Data in 
0  219 

1800  220 
(*** Useful tactics for classical reasoning ***) 
0  221 

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

0  224 

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

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

228 
val contr_tac = eresolve_tac [not_elim] THEN' 

229 
(eq_assume_tac ORELSE' assume_tac); 

0  230 

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

231 
(*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

232 
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

233 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  234 

235 
(*Like mp_tac but instantiates no variables*) 

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

236 
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

237 

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

0  240 

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

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

243 

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

245 
trying rules in order. *) 

246 
fun swap_res_tac rls = 

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

249 
contr_tac ORELSE' 

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

0  251 
end; 
252 

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

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

254 
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

255 

6967  256 
fun dup_elim th = 
257 
(case try 

258 
(rule_by_tactic (TRYALL (etac revcut_rl))) 

259 
(th RSN (2, revcut_rl) > assumption 2 > Seq.hd) of 

260 
Some th' => th' 

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

0  262 

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

263 

1800  264 
(**** Classical rule sets ****) 
0  265 

266 
datatype claset = 

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

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

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

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

270 
hazEs : thm list, (*unsafe elimination rules*) 
6955  271 
xtraIs : thm list, (*extra introduction rules*) 
272 
xtraEs : thm list, (*extra elimination rules*) 

4651  273 
swrappers : (string * wrapper) list, (*for transf. safe_step_tac*) 
274 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 

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

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

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

277 
haz_netpair : netpair, (*nets for unsafe rules*) 
6955  278 
dup_netpair : netpair, (*nets for duplication*) 
279 
xtra_netpair : netpair}; (*nets for extra rules*) 

0  280 

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

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

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

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

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

285 
dup_netpair = build (joinrules(map dup_intr hazIs, 
6955  286 
map dup_elim hazEs)), 
287 
xtra_netpair = build (joinrules(xtraIs, xtraEs))} 

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

288 

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

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

290 
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

291 
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

292 
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

293 
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

294 
*) 
0  295 

6502  296 
val empty_netpair = (Net.empty, Net.empty); 
297 

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

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

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

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

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

302 
hazEs = [], 
6955  303 
xtraIs = [], 
304 
xtraEs = [], 

4651  305 
swrappers = [], 
306 
uwrappers = [], 

6502  307 
safe0_netpair = empty_netpair, 
308 
safep_netpair = empty_netpair, 

309 
haz_netpair = empty_netpair, 

6955  310 
dup_netpair = empty_netpair, 
311 
xtra_netpair = empty_netpair}; 

0  312 

6955  313 
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
3546  314 
let val pretty_thms = map Display.pretty_thm in 
315 
Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs)); 

4624  316 
Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs)); 
6955  317 
Pretty.writeln (Pretty.big_list "extra introduction rules:" (pretty_thms xtraIs)); 
4625  318 
Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs)); 
6955  319 
Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs)); 
320 
Pretty.writeln (Pretty.big_list "extra elimination rules:" (pretty_thms xtraEs)) 

3546  321 
end; 
0  322 

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

324 

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

327 
in 

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

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

330 
end; 

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

331 

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

332 

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

334 

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

335 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  336 
***) 
0  337 

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

338 
(*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

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

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

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

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

343 

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

344 
(*Priority: prefer rules with fewest subgoals, 
1231  345 
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

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

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

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

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

350 

1800  351 
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

352 

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

353 
(*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

354 
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

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

356 
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

357 

1800  358 
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

359 

1800  360 
val delete = delete_tagged_list o joinrules; 
361 

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

362 
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

363 
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

364 

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

365 
(*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

366 
is still allowed.*) 
6955  367 
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

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

369 
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

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

371 
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

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

373 
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

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

375 
warning ("Rule already in claset as unsafe Elim\n" ^ string_of_thm th) 
6955  376 
else if mem_thm (th, xtraIs) then 
377 
warning ("Rule already in claset as extra Intr\n" ^ string_of_thm th) 

378 
else if mem_thm (th, xtraEs) then 

379 
warning ("Rule already in claset as extra Elim\n" ^ string_of_thm th) 

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

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

381 

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

383 

6955  384 
fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
385 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 

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

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

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

388 
(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

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

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

391 
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

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

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

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

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

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

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

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

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

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

401 
hazEs = hazEs, 
6955  402 
xtraIs = xtraIs, 
403 
xtraEs = xtraEs, 

4651  404 
swrappers = swrappers, 
405 
uwrappers = uwrappers, 

2630  406 
haz_netpair = haz_netpair, 
6955  407 
dup_netpair = dup_netpair, 
408 
xtra_netpair = xtra_netpair} 

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

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

410 

6955  411 
fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
412 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 

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

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

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

415 
(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

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

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

418 
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

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

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

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

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

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

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

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

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

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

428 
hazEs = hazEs, 
6955  429 
xtraIs = xtraIs, 
430 
xtraEs = xtraEs, 

4651  431 
swrappers = swrappers, 
432 
uwrappers = uwrappers, 

2630  433 
haz_netpair = haz_netpair, 
6955  434 
dup_netpair = dup_netpair, 
435 
xtra_netpair = xtra_netpair} 

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

436 
end; 
0  437 

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

438 
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

439 

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

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

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

442 

0  443 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
444 

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

445 

1800  446 
(*** Hazardous (unsafe) rules ***) 
0  447 

6955  448 
fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
449 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 

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

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

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

452 
(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

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

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

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

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

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

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

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

460 
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

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

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

463 
hazEs = hazEs, 
6955  464 
xtraIs = xtraIs, 
465 
xtraEs = xtraEs, 

4651  466 
swrappers = swrappers, 
467 
uwrappers = uwrappers, 

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

468 
safe0_netpair = safe0_netpair, 
6955  469 
safep_netpair = safep_netpair, 
470 
xtra_netpair = xtra_netpair} 

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

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

472 

6955  473 
fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
474 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 

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

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

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

477 
(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

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

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

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

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

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

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

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

485 
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

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

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

488 
hazIs = hazIs, 
6955  489 
xtraIs = xtraIs, 
490 
xtraEs = xtraEs, 

4651  491 
swrappers = swrappers, 
492 
uwrappers = uwrappers, 

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

493 
safe0_netpair = safe0_netpair, 
6955  494 
safep_netpair = safep_netpair, 
495 
xtra_netpair = xtra_netpair} 

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

496 
end; 
0  497 

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

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

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

500 

0  501 
fun cs addDs ths = cs addEs (map make_elim ths); 
502 

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

503 

6955  504 
(*** Extra (single step) rules ***) 
505 

506 
fun addXI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 

507 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 

508 
th)= 

509 
if mem_thm (th, xtraIs) then 

510 
(warning ("Ignoring duplicate extra Intr\n" ^ string_of_thm th); 

511 
cs) 

512 
else 

513 
let val nI = length xtraIs + 1 

514 
and nE = length xtraEs 

515 
in warn_dup th cs; 

516 
CS{xtraIs = th::xtraIs, 

517 
xtra_netpair = insert (nI,nE) ([th], []) xtra_netpair, 

518 
safeIs = safeIs, 

519 
safeEs = safeEs, 

520 
hazIs = hazIs, 

521 
hazEs = hazEs, 

522 
xtraEs = xtraEs, 

523 
swrappers = swrappers, 

524 
uwrappers = uwrappers, 

525 
safe0_netpair = safe0_netpair, 

526 
safep_netpair = safep_netpair, 

527 
haz_netpair = haz_netpair, 

528 
dup_netpair = dup_netpair} 

529 
end; 

530 

531 
fun addXE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 

532 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 

533 
th) = 

534 
if mem_thm (th, xtraEs) then 

535 
(warning ("Ignoring duplicate extra Elim\n" ^ string_of_thm th); 

536 
cs) 

537 
else 

538 
let val nI = length xtraIs 

539 
and nE = length xtraEs + 1 

540 
in warn_dup th cs; 

541 
CS{xtraEs = th::xtraEs, 

542 
xtra_netpair = insert (nI,nE) ([], [th]) xtra_netpair, 

543 
safeIs = safeIs, 

544 
safeEs = safeEs, 

545 
hazIs = hazIs, 

546 
hazEs = hazEs, 

547 
xtraIs = xtraIs, 

548 
swrappers = swrappers, 

549 
uwrappers = uwrappers, 

550 
safe0_netpair = safe0_netpair, 

551 
safep_netpair = safep_netpair, 

552 
haz_netpair = haz_netpair, 

553 
dup_netpair = dup_netpair} 

554 
end; 

555 

556 
infix 4 addXIs addXEs addXDs; 

557 

558 
val op addXIs = rev_foldl addXI; 

559 
val op addXEs = rev_foldl addXE; 

560 

561 
fun cs addXDs ths = cs addXEs (map make_elim ths); 

562 

563 

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

566 
to insert. 

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

567 
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

568 
searches in all the lists and chooses the relevant delXX functions. 
1800  569 
***) 
570 

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

571 
fun delSI th 
6955  572 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
573 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

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

574 
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

575 
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

576 
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

577 
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

578 
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

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

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

581 
hazEs = hazEs, 
6955  582 
xtraIs = xtraIs, 
583 
xtraEs = xtraEs, 

4651  584 
swrappers = swrappers, 
585 
uwrappers = uwrappers, 

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

586 
haz_netpair = haz_netpair, 
6955  587 
dup_netpair = dup_netpair, 
588 
xtra_netpair = xtra_netpair} 

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

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

590 
else cs; 
1800  591 

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

592 
fun delSE th 
6955  593 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
594 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

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

595 
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

596 
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

597 
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

598 
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

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

600 
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

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

602 
hazEs = hazEs, 
6955  603 
xtraIs = xtraIs, 
604 
xtraEs = xtraEs, 

4651  605 
swrappers = swrappers, 
606 
uwrappers = uwrappers, 

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

607 
haz_netpair = haz_netpair, 
6955  608 
dup_netpair = dup_netpair, 
609 
xtra_netpair = xtra_netpair} 

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

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

611 
else cs; 
1800  612 

613 

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

614 
fun delI th 
6955  615 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
616 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

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

617 
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

618 
CS{haz_netpair = delete ([th], []) haz_netpair, 
1800  619 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
620 
safeIs = safeIs, 

621 
safeEs = safeEs, 

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

622 
hazIs = rem_thm (hazIs,th), 
1800  623 
hazEs = hazEs, 
6955  624 
xtraIs = xtraIs, 
625 
xtraEs = xtraEs, 

4651  626 
swrappers = swrappers, 
627 
uwrappers = uwrappers, 

1800  628 
safe0_netpair = safe0_netpair, 
6955  629 
safep_netpair = safep_netpair, 
630 
xtra_netpair = xtra_netpair} 

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

631 
else cs; 
1800  632 

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

633 
fun delE th 
6955  634 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
635 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

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

636 
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

637 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
1800  638 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
639 
safeIs = safeIs, 

640 
safeEs = safeEs, 

641 
hazIs = hazIs, 

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

642 
hazEs = rem_thm (hazEs,th), 
6955  643 
xtraIs = xtraIs, 
644 
xtraEs = xtraEs, 

645 
swrappers = swrappers, 

646 
uwrappers = uwrappers, 

647 
safe0_netpair = safe0_netpair, 

648 
safep_netpair = safep_netpair, 

649 
xtra_netpair = xtra_netpair} 

650 
else cs; 

651 

652 

653 
fun delXI th 

654 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 

655 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

656 
if mem_thm (th, xtraIs) then 

657 
CS{xtra_netpair = delete ([th], []) xtra_netpair, 

658 
safeIs = safeIs, 

659 
safeEs = safeEs, 

660 
hazIs = hazIs, 

661 
hazEs = hazEs, 

662 
xtraIs = rem_thm (xtraIs,th), 

663 
xtraEs = xtraEs, 

4651  664 
swrappers = swrappers, 
665 
uwrappers = uwrappers, 

1800  666 
safe0_netpair = safe0_netpair, 
6955  667 
safep_netpair = safep_netpair, 
668 
haz_netpair = haz_netpair, 

669 
dup_netpair = dup_netpair} 

670 
else cs; 

671 

672 
fun delXE th 

673 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 

674 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = 

675 
if mem_thm (th, xtraEs) then 

676 
CS{xtra_netpair = delete ([], [th]) xtra_netpair, 

677 
safeIs = safeIs, 

678 
safeEs = safeEs, 

679 
hazIs = hazIs, 

680 
hazEs = hazEs, 

681 
xtraIs = xtraIs, 

682 
xtraEs = rem_thm (xtraEs,th), 

683 
swrappers = swrappers, 

684 
uwrappers = uwrappers, 

685 
safe0_netpair = safe0_netpair, 

686 
safep_netpair = safep_netpair, 

687 
haz_netpair = haz_netpair, 

688 
dup_netpair = dup_netpair} 

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

689 
else cs; 
1800  690 

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

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

693 
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse 
6955  694 
mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse 
695 
mem_thm (th, xtraIs) orelse mem_thm (th, xtraEs) 

696 
then delSI th (delSE th (delI th (delE th (delXI th (delXE th cs))))) 

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

697 
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

698 
cs); 
1800  699 

700 
val op delrules = foldl delrule; 

701 

702 

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

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

704 
fun update_swrappers 
6955  705 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
706 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = 

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

707 
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 
6955  708 
xtraIs = xtraIs, xtraEs = xtraEs, 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

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

710 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  711 
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

712 

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

713 
fun update_uwrappers 
6955  714 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
715 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = 

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

716 
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, 
6955  717 
xtraIs = xtraIs, xtraEs = xtraEs, 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

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

719 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  720 
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; 
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset

721 

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

722 

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

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

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

727 
overwrite (swrappers, new_swrapper))); 
4651  728 

729 
(*Add/replace an unsafe wrapper*) 

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

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

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

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

734 

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

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

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

738 
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

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

740 

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

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

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

744 
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

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

746 

2630  747 
(*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

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

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

752 

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

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

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

758 

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

761 
fun cs addE2 (name, thm) = 

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

763 
fun cs addSD2 (name, thm) = 

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

765 
fun cs addSE2 (name, thm) = 

766 
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

767 

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

770 
treatment of priority might get muddled up.*) 

771 
fun merge_cs 

6955  772 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, 
4765  773 
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, 
6955  774 
xtraIs=xtraIs2, xtraEs=xtraEs2, swrappers, uwrappers, ...}) = 
1711  775 
let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) 
776 
val safeEs' = gen_rems eq_thm (safeEs2,safeEs) 

2630  777 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
778 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

6955  779 
val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs) 
780 
val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs) 

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

781 
val cs1 = cs addSIs safeIs' 
4765  782 
addSEs safeEs' 
783 
addIs hazIs' 

784 
addEs hazEs' 

6955  785 
addXIs xtraIs' 
786 
addXEs xtraEs' 

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

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

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

789 
in cs3 
1711  790 
end; 
791 

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

792 

1800  793 
(**** Simple tactics for theorem proving ****) 
0  794 

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

2630  796 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  797 
appSWrappers cs (FIRST' [ 
2630  798 
eq_assume_tac, 
799 
eq_mp_tac, 

800 
bimatch_from_nets_tac safe0_netpair, 

801 
FIRST' hyp_subst_tacs, 

802 
bimatch_from_nets_tac safep_netpair]); 

0  803 

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

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

807 

0  808 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 
5757  809 
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

810 

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

811 

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

812 
(*** 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

813 

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

814 
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

815 

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

816 
(*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

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

818 
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

819 
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

820 

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

821 
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

822 
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

823 

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

824 
(*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

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

826 
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

827 
(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

828 

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

829 
(*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

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

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

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

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

835 
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

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

837 

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

838 
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

839 

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

840 

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

841 
(*** 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

842 

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

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

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

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

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

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

849 

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

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

852 
biresolve_from_nets_tac safep_netpair; 
0  853 

854 
(*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

855 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  856 

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

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

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

859 

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

0  863 

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

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

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

0  868 

1800  869 
(**** The following tactics all fail unless they solve one goal ****) 
0  870 

871 
(*Dumb but fast*) 

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

873 

874 
(*Slower but smarter than fast_tac*) 

875 
fun best_tac cs = 

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

877 

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

879 

880 
fun slow_best_tac cs = 

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

882 

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

883 

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

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

886 

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

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

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

889 
, 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

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

891 

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

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

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

894 
, 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

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

896 

1800  897 
(**** 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

898 
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

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

901 

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

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

903 
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

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

905 
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

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

907 

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

911 
(instp_step_tac cs APPEND' dup_step_tac cs); 

912 
in fun depth_tac cs m i state = SELECT_GOAL 

913 
(safe_steps_tac cs 1 THEN_ELSE 

914 
(DEPTH_SOLVE (depth_tac cs m 1), 

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

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

917 
)) i state; 

918 
end; 

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

919 

2173  920 
(*Search, with depth bound m. 
921 
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

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

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

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

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

926 
(*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

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

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

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

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

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

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

933 

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

934 
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

935 

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

936 

1724  937 

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

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

939 

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

940 
(* init data kind claset *) 
1724  941 

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

942 
exception CSData of claset ref; 
1724  943 

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

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

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

946 

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

947 
(*create new references*) 
6556  948 
fun copy (ClasetData (ref (CSData (ref cs)))) = 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

949 
ClasetData (ref (CSData (ref cs))); 
6556  950 
val prep_ext = copy; 
1724  951 

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

952 
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

953 
ClasetData (ref (CSData (ref (merge_cs (cs1, cs2))))); 
1724  954 

4259  955 
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

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

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

959 

1724  960 

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

961 
(* access claset *) 
1724  962 

5001  963 
val print_claset = Theory.print_data clasetK; 
4380  964 

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

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

968 
val claset_of_sg = ! o claset_ref_of_sg; 
6391  969 
val claset_of = claset_of_sg o Theory.sign_of; 
1800  970 

6391  971 
fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state; 
972 
fun CLASET' tacf i state = tacf (claset_of_sg (Thm.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

973 

5028  974 
val claset = claset_of o Context.the_context; 
6391  975 
val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

976 

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

977 

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

978 
(* change claset *) 
1800  979 

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

980 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  981 

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

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

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

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

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

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

987 
val AddSIs = change_claset (op addSIs); 
6955  988 
val AddXDs = change_claset (op addXDs); 
989 
val AddXEs = change_claset (op addXEs); 

990 
val AddXIs = change_claset (op addXIs); 

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

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

992 

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

993 

5841  994 
(* proof data kind 'Provers/claset' *) 
995 

996 
structure LocalClasetArgs = 

997 
struct 

998 
val name = "Provers/claset"; 

999 
type T = claset; 

1000 
val init = claset_of; 

1001 
fun print _ cs = print_cs cs; 

1002 
end; 

1003 

1004 
structure LocalClaset = ProofDataFun(LocalClasetArgs); 

1005 
val print_local_claset = LocalClaset.print; 

1006 
val get_local_claset = LocalClaset.get; 

1007 
val put_local_claset = LocalClaset.put; 

1008 

1009 

5885  1010 
(* attributes *) 
1011 

1012 
fun change_global_cs f (thy, th) = 

1013 
let val r = claset_ref_of thy 

6096  1014 
in r := f (! r, [th]); (thy, th) end; 
5885  1015 

1016 
fun change_local_cs f (ctxt, th) = 

6096  1017 
let val cs = f (get_local_claset ctxt, [th]) 
5885  1018 
in (put_local_claset cs ctxt, th) end; 
1019 

1020 
val safe_dest_global = change_global_cs (op addSDs); 

1021 
val safe_elim_global = change_global_cs (op addSEs); 

1022 
val safe_intro_global = change_global_cs (op addSIs); 

6955  1023 
val haz_dest_global = change_global_cs (op addDs); 
1024 
val haz_elim_global = change_global_cs (op addEs); 

1025 
val haz_intro_global = change_global_cs (op addIs); 

1026 
val xtra_dest_global = change_global_cs (op addXDs); 

1027 
val xtra_elim_global = change_global_cs (op addXEs); 

1028 
val xtra_intro_global = change_global_cs (op addXIs); 

5885  1029 
val delrule_global = change_global_cs (op delrules); 
1030 

6955  1031 
val safe_dest_local = change_local_cs (op addSDs); 
1032 
val safe_elim_local = change_local_cs (op addSEs); 

1033 
val safe_intro_local = change_local_cs (op addSIs); 

5885  1034 
val haz_dest_local = change_local_cs (op addDs); 
1035 
val haz_elim_local = change_local_cs (op addEs); 

1036 
val haz_intro_local = change_local_cs (op addIs); 

6955  1037 
val xtra_dest_local = change_local_cs (op addXDs); 
1038 
val xtra_elim_local = change_local_cs (op addXEs); 

1039 
val xtra_intro_local = change_local_cs (op addXIs); 

5885  1040 
val delrule_local = change_local_cs (op delrules); 
1041 

1042 

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

1043 
(* tactics referring to the implicit claset *) 
1800  1044 

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

1045 
(*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

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

1047 
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

1048 
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

1049 
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

1050 
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

1051 
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

1052 
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

1053 
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

1054 
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

1055 
fun Deepen_tac m = deepen_tac (claset()) m; 
2066  1056 

1800  1057 

0  1058 
end; 
5841  1059 

1060 

1061 

5885  1062 
(** concrete syntax of attributes **) 
5841  1063 

1064 
(* add / del rules *) 

1065 

1066 
val introN = "intro"; 

1067 
val elimN = "elim"; 

1068 
val destN = "dest"; 

1069 
val delN = "del"; 

5885  1070 
val delruleN = "delrule"; 
5841  1071 

5885  1072 
val bang = Args.$$$ "!"; 
6955  1073 
val bbang = Args.$$$ "!!"; 
5841  1074 

6955  1075 
fun cla_att change xtra haz safe = Attrib.syntax 
1076 
(Scan.lift ((bbang >> K xtra  bang >> K haz  Scan.succeed safe) >> change)); 

5841  1077 

6955  1078 
fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); 
5885  1079 
val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local); 
5841  1080 

1081 

1082 
(* setup_attrs *) 

1083 

1084 
val setup_attrs = Attrib.add_attributes 

6955  1085 
[(destN, cla_attr (op addXDs) (op addDs) (op addSDs), "destruction rule"), 
1086 
(elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "elimination rule"), 

1087 
(introN, cla_attr (op addXIs) (op addIs) (op addSIs), "introduction rule"), 

5885  1088 
(delruleN, del_attr, "delete rule")]; 
5841  1089 

1090 

1091 

7230  1092 
(** proof methods **) 
1093 

1094 
(* get nets (appropriate order for semiautomatic methods) *) 

1095 

1096 
local 

1097 
val imp_elim_netpair = insert (0, 0) ([], [imp_elim]) empty_netpair; 

1098 
val not_elim_netpair = insert (0, 0) ([], [Data.not_elim]) empty_netpair; 

1099 
in 

1100 
fun get_nets (CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair, ...}) = 

1101 
[imp_elim_netpair, safe0_netpair, safep_netpair, not_elim_netpair, haz_netpair, dup_netpair, xtra_netpair]; 

1102 
end; 

1103 

1104 

1105 
(* METHOD_CLASET' *) 

5841  1106 

7230  1107 
fun METHOD_CLASET' tac = 
1108 
Method.METHOD (FIRSTGOAL o (fn facts => CLASET' (fn cs => tac cs facts))); 

1109 

1110 

1111 
val trace_rules = ref false; 

5841  1112 

7230  1113 
local 
1114 

1115 
fun trace rules i = 

1116 
if not (! trace_rules) then () 

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

1118 
(map Display.pretty_thm rules)); 

1119 

1120 

5841  1121 
fun order_rules xs = map snd (Tactic.orderlist xs); 
1122 

1123 
fun find_rules concl nets = 

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

1125 
in flat (map rules_of nets) end; 

1126 

1127 
fun find_erules [] _ = [] 

6955  1128 
 find_erules (fact :: _) nets = 
5841  1129 
let 
6502  1130 
fun may_unify net = Net.unify_term net o Logic.strip_assums_concl o #prop o Thm.rep_thm; 
6955  1131 
fun erules_of (_, enet) = order_rules (may_unify enet fact); 
6502  1132 
in flat (map erules_of nets) end; 
5841  1133 

1134 

7230  1135 
fun some_rule_tac cs facts = 
5841  1136 
let 
7230  1137 
val nets = get_nets cs; 
6492  1138 
val erules = find_erules facts nets; 
5841  1139 

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

1141 
let 

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

1143 
val rules = erules @ irules; 

1144 
val ruleq = Method.forward_chain facts rules; 

7230  1145 
in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end); 
5841  1146 
in tac end; 
1147 

7230  1148 
in 
1149 
val some_rule = METHOD_CLASET' some_rule_tac; 

1150 
end; 

5841  1151 

1152 

7230  1153 
(* intro / elim methods *) 
1154 

1155 
local 

1156 

1157 
fun intro_elim_tac netpair_of _ [] cs facts = 

1158 
Method.same_tac facts THEN' FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs)) 

1159 
 intro_elim_tac _ res_tac rules _ facts = 

1160 
Method.same_tac facts THEN' res_tac rules; 

6502  1161 

7230  1162 
val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) resolve_tac; 
1163 
val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) eresolve_tac; 

1164 

1165 
in 

1166 
val intro = METHOD_CLASET' o intro_tac; 

1167 
val elim = METHOD_CLASET' o elim_tac; 

1168 
end; 

1169 

1170 

1171 
(* contradiction method *) 

6502  1172 

7132  1173 
val contradiction = Method.METHOD (fn facts => 
1174 
FIRSTGOAL (Method.same_tac facts THEN' contr_tac)); 

6502  1175 

1176 

1177 
(* automatic methods *) 

5841  1178 

5927  1179 
val cla_modifiers = 
6955  1180 
[Args.$$$ destN  bbang >> K xtra_dest_local, 
1181 
Args.$$$ destN  bang >> K haz_dest_local, 

5927  1182 
Args.$$$ destN >> K safe_dest_local, 
6955  1183 
Args.$$$ elimN  bbang >> K xtra_elim_local, 
5927  1184 
Args.$$$ elimN  bang >> K haz_elim_local, 
1185 
Args.$$$ elimN >> K safe_elim_local, 

6955  1186 
Args.$$$ introN  bbang >> K xtra_intro_local, 
5927  1187 
Args.$$$ introN  bang >> K haz_intro_local, 
1188 
Args.$$$ introN >> K safe_intro_local, 

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

1190 

1191 
val cla_args = Method.only_sectioned_args cla_modifiers; 

5841  1192 

7132  1193 
fun cla_meth tac ctxt = Method.METHOD (fn facts => 
1194 
ALLGOALS (Method.same_tac facts) THEN tac (get_local_claset ctxt)); 

1195 

1196 
fun cla_meth' tac ctxt = Method.METHOD (fn facts => 

1197 
FIRSTGOAL (Method.same_tac facts THEN' tac (get_local_claset ctxt))); 

5841  1198 

5885  1199 
val cla_method = cla_args o cla_meth; 
1200 
val cla_method' = cla_args o cla_meth'; 

5841  1201 

1202 

1203 

1204 
(** setup_methods **) 

1205 

1206 
val setup_methods = Method.add_methods 

7230  1207 
[("default", Method.no_args some_rule, "apply some standard rule"), 
1208 
("some_rule", Method.no_args some_rule, "apply some standard rule"), 

1209 
("intro", Method.thms_args intro, "apply some introduction rule"), 

1210 
("elim", Method.thms_args elim, "apply some elimination rule"), 

6502  1211 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
7132  1212 
("safe_tac", cla_method safe_tac, "safe_tac (improper!)"), 
1213 
("safe_step_tac", cla_method' safe_step_tac, "safe_step_tac (improper!)"), 

1214 
("step_tac", cla_method' step_tac, "step_tac (improper!)"), 

7004  1215 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
1216 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 

1217 
("slow", cla_method' slow_tac, "classical prover (depthfirst, more backtracking)"), 

1218 
("slow_best", cla_method' slow_best_tac, "classical prover (bestfirst, more backtracking)")]; 

5841  1219 

1220 

1221 

1222 
(** theory setup **) 

1223 

1224 
(* FIXME claset theory data *) 

1225 

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

1227 

1228 

1229 
end; 