author  wenzelm 
Sat, 01 Jul 2000 19:55:22 +0200  
changeset 9230  17ae63f82ad8 
parent 9184  c6c5b422241f 
child 9402  480a1b40fdd6 
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 

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

29 
sig 
9171  30 
val make_elim : thm > thm (* Tactic.make_elim or a classical version*) 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

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

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

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

36 
end; 
0  37 

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

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

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

42 
val print_cs: claset > unit 
4380  43 
val print_claset: theory > unit 
4653  44 
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

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

46 
hazIs: thm list, hazEs: thm list, 
6955  47 
xtraIs: thm list, xtraEs: thm list, 
4651  48 
swrappers: (string * wrapper) list, 
49 
uwrappers: (string * wrapper) list, 

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

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

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

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

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

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

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

58 
val addSIs : claset * thm list > claset 
1800  59 
val delrules : claset * thm list > claset 
4651  60 
val addSWrapper : claset * (string * wrapper) > claset 
61 
val delSWrapper : claset * string > claset 

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

63 
val delWrapper : claset * string > claset 

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

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

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

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

5523  68 
val addD2 : claset * (string * thm) > claset 
69 
val addE2 : claset * (string * thm) > claset 

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

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

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

75 

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

76 
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

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

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

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

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

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

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

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

84 

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

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

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

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

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

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

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

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

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

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

94 

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

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

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

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

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

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

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

101 
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

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

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

105 
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

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

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

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

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

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

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

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

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

115 
val instp_step_tac : claset > int > tactic 
1724  116 

117 
val AddDs : thm list > unit 

118 
val AddEs : thm list > unit 

119 
val AddIs : thm list > unit 

120 
val AddSDs : thm list > unit 

121 
val AddSEs : thm list > unit 

122 
val AddSIs : thm list > unit 

6955  123 
val AddXDs : thm list > unit 
124 
val AddXEs : thm list > unit 

125 
val AddXIs : thm list > unit 

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

127 
val Safe_tac : tactic 
1814  128 
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

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

130 
val Clarify_step_tac : int > tactic 
1800  131 
val Step_tac : int > tactic 
1724  132 
val Fast_tac : int > tactic 
1800  133 
val Best_tac : int > tactic 
2066  134 
val Slow_tac : int > tactic 
135 
val Slow_best_tac : int > tactic 

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

137 
end; 
1724  138 

5841  139 
signature CLASSICAL = 
140 
sig 

141 
include BASIC_CLASSICAL 

142 
val print_local_claset: Proof.context > unit 

143 
val get_local_claset: Proof.context > claset 

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

145 
val safe_dest_global: theory attribute 

146 
val safe_elim_global: theory attribute 

147 
val safe_intro_global: theory attribute 

6955  148 
val haz_dest_global: theory attribute 
149 
val haz_elim_global: theory attribute 

150 
val haz_intro_global: theory attribute 

151 
val xtra_dest_global: theory attribute 

152 
val xtra_elim_global: theory attribute 

153 
val xtra_intro_global: theory attribute 

5885  154 
val delrule_global: theory attribute 
6955  155 
val safe_dest_local: Proof.context attribute 
156 
val safe_elim_local: Proof.context attribute 

157 
val safe_intro_local: Proof.context attribute 

5885  158 
val haz_dest_local: Proof.context attribute 
159 
val haz_elim_local: Proof.context attribute 

160 
val haz_intro_local: Proof.context attribute 

6955  161 
val xtra_dest_local: Proof.context attribute 
162 
val xtra_elim_local: Proof.context attribute 

163 
val xtra_intro_local: Proof.context attribute 

5885  164 
val delrule_local: Proof.context attribute 
7272  165 
val cla_modifiers: (Args.T list > (Method.modifier * Args.T list)) list 
7559  166 
val cla_meth: (claset > tactic) > thm list > Proof.context > Proof.method 
167 
val cla_meth': (claset > int > tactic) > thm list > Proof.context > Proof.method 

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

5841  170 
val setup: (theory > theory) list 
171 
end; 

172 

0  173 

5927  174 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
0  175 
struct 
176 

7354  177 
local open Data in 
0  178 

1800  179 
(*** Useful tactics for classical reasoning ***) 
0  180 

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

0  183 

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

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

187 
val contr_tac = eresolve_tac [not_elim] THEN' 

188 
(eq_assume_tac ORELSE' assume_tac); 

0  189 

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

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

191 
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

192 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  193 

194 
(*Like mp_tac but instantiates no variables*) 

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

195 
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

196 

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

0  199 

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

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

202 

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

204 
trying rules in order. *) 

205 
fun swap_res_tac rls = 

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

208 
contr_tac ORELSE' 

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

0  210 
end; 
211 

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

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

213 
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

214 

6967  215 
fun dup_elim th = 
216 
(case try 

217 
(rule_by_tactic (TRYALL (etac revcut_rl))) 

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

219 
Some th' => th' 

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

0  221 

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

222 

1800  223 
(**** Classical rule sets ****) 
0  224 

225 
datatype claset = 

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

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

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

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

229 
hazEs : thm list, (*unsafe elimination rules*) 
6955  230 
xtraIs : thm list, (*extra introduction rules*) 
231 
xtraEs : thm list, (*extra elimination rules*) 

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

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

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

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

236 
haz_netpair : netpair, (*nets for unsafe rules*) 
6955  237 
dup_netpair : netpair, (*nets for duplication*) 
238 
xtra_netpair : netpair}; (*nets for extra rules*) 

0  239 

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

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

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

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

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

244 
dup_netpair = build (joinrules(map dup_intr hazIs, 
6955  245 
map dup_elim hazEs)), 
246 
xtra_netpair = build (joinrules(xtraIs, xtraEs))} 

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

247 

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

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

249 
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

250 
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

251 
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

252 
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

253 
*) 
0  254 

6502  255 
val empty_netpair = (Net.empty, Net.empty); 
256 

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

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

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

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

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

261 
hazEs = [], 
6955  262 
xtraIs = [], 
263 
xtraEs = [], 

4651  264 
swrappers = [], 
265 
uwrappers = [], 

6502  266 
safe0_netpair = empty_netpair, 
267 
safep_netpair = empty_netpair, 

268 
haz_netpair = empty_netpair, 

6955  269 
dup_netpair = empty_netpair, 
270 
xtra_netpair = empty_netpair}; 

0  271 

6955  272 
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
3546  273 
let val pretty_thms = map Display.pretty_thm in 
8727  274 
[Pretty.big_list "safe introduction rules:" (pretty_thms safeIs), 
275 
Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs), 

276 
Pretty.big_list "extra introduction rules:" (pretty_thms xtraIs), 

277 
Pretty.big_list "safe elimination rules:" (pretty_thms safeEs), 

278 
Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs), 

279 
Pretty.big_list "extra elimination rules:" (pretty_thms xtraEs)] 

280 
> Pretty.chunks > Pretty.writeln 

3546  281 
end; 
0  282 

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

284 

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

287 
in 

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

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

290 
end; 

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

291 

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

292 

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

294 

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

295 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  296 
***) 
0  297 

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

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

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

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

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

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

303 

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

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

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

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

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

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

310 

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

312 

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

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

314 
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

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

316 
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

317 

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

319 

1800  320 
val delete = delete_tagged_list o joinrules; 
321 

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

322 
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

323 
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

324 

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

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

326 
is still allowed.*) 
6955  327 
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

328 
if mem_thm (th, safeIs) then 
8926  329 
warning ("Rule already declared as safe introduction (intro)\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

330 
else if mem_thm (th, safeEs) then 
8926  331 
warning ("Rule already declared as safe elimination (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

332 
else if mem_thm (th, hazIs) then 
8926  333 
warning ("Rule already declared as unsafe introduction (intro?)\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

334 
else if mem_thm (th, hazEs) then 
8926  335 
warning ("Rule already declared as unsafe elimination (elim?)\n" ^ string_of_thm th) 
6955  336 
else if mem_thm (th, xtraIs) then 
8926  337 
warning ("Rule already declared as extra introduction (intro??)\n" ^ string_of_thm th) 
6955  338 
else if mem_thm (th, xtraEs) then 
8926  339 
warning ("Rule already declared as extra elimination (elim??)\n" ^ string_of_thm th) 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

341 

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

343 

6955  344 
fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
345 
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

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

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

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

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

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

351 
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) 
7559  352 
partition Thm.no_prems [th] 
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset

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

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

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

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

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

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

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

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

361 
hazEs = hazEs, 
6955  362 
xtraIs = xtraIs, 
363 
xtraEs = xtraEs, 

4651  364 
swrappers = swrappers, 
365 
uwrappers = uwrappers, 

2630  366 
haz_netpair = haz_netpair, 
6955  367 
dup_netpair = dup_netpair, 
368 
xtra_netpair = xtra_netpair} 

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

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

370 

6955  371 
fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
372 
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

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

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

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

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

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

378 
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

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

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

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

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

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

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

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

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

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

388 
hazEs = hazEs, 
6955  389 
xtraIs = xtraIs, 
390 
xtraEs = xtraEs, 

4651  391 
swrappers = swrappers, 
392 
uwrappers = uwrappers, 

2630  393 
haz_netpair = haz_netpair, 
6955  394 
dup_netpair = dup_netpair, 
395 
xtra_netpair = xtra_netpair} 

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

396 
end; 
0  397 

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

398 
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

399 

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

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

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

402 

0  403 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
404 

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

405 

1800  406 
(*** Hazardous (unsafe) rules ***) 
0  407 

6955  408 
fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
409 
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

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

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

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

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

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

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

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

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

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

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

420 
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

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

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

423 
hazEs = hazEs, 
6955  424 
xtraIs = xtraIs, 
425 
xtraEs = xtraEs, 

4651  426 
swrappers = swrappers, 
427 
uwrappers = uwrappers, 

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

428 
safe0_netpair = safe0_netpair, 
6955  429 
safep_netpair = safep_netpair, 
430 
xtra_netpair = xtra_netpair} 

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

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

432 

6955  433 
fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
434 
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

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

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

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

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

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

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

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

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

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

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

445 
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

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

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

448 
hazIs = hazIs, 
6955  449 
xtraIs = xtraIs, 
450 
xtraEs = xtraEs, 

4651  451 
swrappers = swrappers, 
452 
uwrappers = uwrappers, 

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

453 
safe0_netpair = safe0_netpair, 
6955  454 
safep_netpair = safep_netpair, 
455 
xtra_netpair = xtra_netpair} 

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

456 
end; 
0  457 

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

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

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

460 

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

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

463 

6955  464 
(*** Extra (single step) rules ***) 
465 

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

467 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 

468 
th)= 

469 
if mem_thm (th, xtraIs) then 

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

471 
cs) 

472 
else 

473 
let val nI = length xtraIs + 1 

474 
and nE = length xtraEs 

475 
in warn_dup th cs; 

476 
CS{xtraIs = th::xtraIs, 

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

478 
safeIs = safeIs, 

479 
safeEs = safeEs, 

480 
hazIs = hazIs, 

481 
hazEs = hazEs, 

482 
xtraEs = xtraEs, 

483 
swrappers = swrappers, 

484 
uwrappers = uwrappers, 

485 
safe0_netpair = safe0_netpair, 

486 
safep_netpair = safep_netpair, 

487 
haz_netpair = haz_netpair, 

488 
dup_netpair = dup_netpair} 

489 
end; 

490 

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

492 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 

493 
th) = 

494 
if mem_thm (th, xtraEs) then 

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

496 
cs) 

497 
else 

498 
let val nI = length xtraIs 

499 
and nE = length xtraEs + 1 

500 
in warn_dup th cs; 

501 
CS{xtraEs = th::xtraEs, 

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

503 
safeIs = safeIs, 

504 
safeEs = safeEs, 

505 
hazIs = hazIs, 

506 
hazEs = hazEs, 

507 
xtraIs = xtraIs, 

508 
swrappers = swrappers, 

509 
uwrappers = uwrappers, 

510 
safe0_netpair = safe0_netpair, 

511 
safep_netpair = safep_netpair, 

512 
haz_netpair = haz_netpair, 

513 
dup_netpair = dup_netpair} 

514 
end; 

515 

516 
infix 4 addXIs addXEs addXDs; 

517 

518 
val op addXIs = rev_foldl addXI; 

519 
val op addXEs = rev_foldl addXE; 

520 

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

522 

523 

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

526 
to insert. 

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

527 
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

528 
searches in all the lists and chooses the relevant delXX functions. 
1800  529 
***) 
530 

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

531 
fun delSI th 
6955  532 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
533 
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

534 
if mem_thm (th, safeIs) then 
7559  535 
let val (safe0_rls, safep_rls) = partition Thm.no_prems [th] 
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset

536 
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

537 
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

538 
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

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

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

541 
hazEs = hazEs, 
6955  542 
xtraIs = xtraIs, 
543 
xtraEs = xtraEs, 

4651  544 
swrappers = swrappers, 
545 
uwrappers = uwrappers, 

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

546 
haz_netpair = haz_netpair, 
6955  547 
dup_netpair = dup_netpair, 
548 
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

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

550 
else cs; 
1800  551 

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

552 
fun delSE th 
6955  553 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
554 
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

555 
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

556 
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

557 
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

558 
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

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

560 
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

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

562 
hazEs = hazEs, 
6955  563 
xtraIs = xtraIs, 
564 
xtraEs = xtraEs, 

4651  565 
swrappers = swrappers, 
566 
uwrappers = uwrappers, 

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

567 
haz_netpair = haz_netpair, 
6955  568 
dup_netpair = dup_netpair, 
569 
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

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

571 
else cs; 
1800  572 

573 

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

574 
fun delI th 
6955  575 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
576 
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

577 
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

578 
CS{haz_netpair = delete ([th], []) haz_netpair, 
1800  579 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
580 
safeIs = safeIs, 

581 
safeEs = safeEs, 

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

582 
hazIs = rem_thm (hazIs,th), 
1800  583 
hazEs = hazEs, 
6955  584 
xtraIs = xtraIs, 
585 
xtraEs = xtraEs, 

4651  586 
swrappers = swrappers, 
587 
uwrappers = uwrappers, 

1800  588 
safe0_netpair = safe0_netpair, 
6955  589 
safep_netpair = safep_netpair, 
590 
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

591 
else cs; 
1800  592 

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

593 
fun delE th 
6955  594 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
595 
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

596 
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

597 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
1800  598 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
599 
safeIs = safeIs, 

600 
safeEs = safeEs, 

601 
hazIs = hazIs, 

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

602 
hazEs = rem_thm (hazEs,th), 
6955  603 
xtraIs = xtraIs, 
604 
xtraEs = xtraEs, 

605 
swrappers = swrappers, 

606 
uwrappers = uwrappers, 

607 
safe0_netpair = safe0_netpair, 

608 
safep_netpair = safep_netpair, 

609 
xtra_netpair = xtra_netpair} 

610 
else cs; 

611 

612 

613 
fun delXI th 

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

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

616 
if mem_thm (th, xtraIs) then 

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

618 
safeIs = safeIs, 

619 
safeEs = safeEs, 

620 
hazIs = hazIs, 

621 
hazEs = hazEs, 

622 
xtraIs = rem_thm (xtraIs,th), 

623 
xtraEs = xtraEs, 

4651  624 
swrappers = swrappers, 
625 
uwrappers = uwrappers, 

1800  626 
safe0_netpair = safe0_netpair, 
6955  627 
safep_netpair = safep_netpair, 
628 
haz_netpair = haz_netpair, 

629 
dup_netpair = dup_netpair} 

630 
else cs; 

631 

632 
fun delXE th 

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

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

635 
if mem_thm (th, xtraEs) then 

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

637 
safeIs = safeIs, 

638 
safeEs = safeEs, 

639 
hazIs = hazIs, 

640 
hazEs = hazEs, 

641 
xtraIs = xtraIs, 

642 
xtraEs = rem_thm (xtraEs,th), 

643 
swrappers = swrappers, 

644 
uwrappers = uwrappers, 

645 
safe0_netpair = safe0_netpair, 

646 
safep_netpair = safep_netpair, 

647 
haz_netpair = haz_netpair, 

648 
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

649 
else cs; 
1800  650 

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

651 
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) 
6955  652 
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

653 
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse 
6955  654 
mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse 
655 
mem_thm (th, xtraIs) orelse mem_thm (th, xtraEs) 

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

8926  657 
else (warning ("Undeclared classical rule\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

658 
cs); 
1800  659 

660 
val op delrules = foldl delrule; 

661 

662 

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

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

664 
fun update_swrappers 
6955  665 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
666 
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

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

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

670 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  671 
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

672 

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

673 
fun update_uwrappers 
6955  674 
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
675 
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

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

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

679 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  680 
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

681 

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

682 

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

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

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

687 
overwrite (swrappers, new_swrapper))); 
4651  688 

689 
(*Add/replace an unsafe wrapper*) 

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

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

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

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

694 

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

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

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

698 
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

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

700 

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

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

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

704 
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

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

706 

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

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

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

712 

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

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

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

718 

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

721 
fun cs addE2 (name, thm) = 

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

723 
fun cs addSD2 (name, thm) = 

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

725 
fun cs addSE2 (name, thm) = 

726 
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

727 

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

730 
treatment of priority might get muddled up.*) 

731 
fun merge_cs 

6955  732 
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, 
4765  733 
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, 
6955  734 
xtraIs=xtraIs2, xtraEs=xtraEs2, swrappers, uwrappers, ...}) = 
1711  735 
let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) 
736 
val safeEs' = gen_rems eq_thm (safeEs2,safeEs) 

2630  737 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
738 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

6955  739 
val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs) 
740 
val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs) 

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

741 
val cs1 = cs addSIs safeIs' 
4765  742 
addSEs safeEs' 
743 
addIs hazIs' 

744 
addEs hazEs' 

6955  745 
addXIs xtraIs' 
746 
addXEs xtraEs' 

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

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

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

749 
in cs3 
1711  750 
end; 
751 

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

752 

1800  753 
(**** Simple tactics for theorem proving ****) 
0  754 

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

2630  756 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  757 
appSWrappers cs (FIRST' [ 
2630  758 
eq_assume_tac, 
759 
eq_mp_tac, 

760 
bimatch_from_nets_tac safe0_netpair, 

761 
FIRST' hyp_subst_tacs, 

762 
bimatch_from_nets_tac safep_netpair]); 

0  763 

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

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

767 

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

770 

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

771 

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

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

773 

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

774 
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

775 

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

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

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

778 
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

779 
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

780 

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

781 
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

782 
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

783 

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

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

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

786 
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

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

788 

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

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

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

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

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

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

795 
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

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

797 

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

798 
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

799 

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

800 

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

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

802 

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

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

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

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

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

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

809 

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

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

812 
biresolve_from_nets_tac safep_netpair; 
0  813 

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

815 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  816 

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

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

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

819 

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

0  823 

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

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

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

0  828 

1800  829 
(**** The following tactics all fail unless they solve one goal ****) 
0  830 

831 
(*Dumb but fast*) 

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

833 

834 
(*Slower but smarter than fast_tac*) 

835 
fun best_tac cs = 

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

837 

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

839 

840 
fun slow_best_tac cs = 

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

842 

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

843 

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

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

846 

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

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

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

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

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

851 

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

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

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

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

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

856 

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

858 
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

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

861 

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

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

863 
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

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

865 
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

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

867 

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

871 
(instp_step_tac cs APPEND' dup_step_tac cs); 

872 
in fun depth_tac cs m i state = SELECT_GOAL 

873 
(safe_steps_tac cs 1 THEN_ELSE 

874 
(DEPTH_SOLVE (depth_tac cs m 1), 

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

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

877 
)) i state; 

878 
end; 

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

879 

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

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

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

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

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

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

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

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

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

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

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

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

893 

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

894 
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

895 

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

896 

1724  897 

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

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

899 

7354  900 
(* theory data kind 'Provers/claset' *) 
1724  901 

7354  902 
structure GlobalClasetArgs = 
903 
struct 

904 
val name = "Provers/claset"; 

905 
type T = claset ref; 

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

906 

7354  907 
val empty = ref empty_cs; 
908 
fun copy (ref cs) = (ref cs): T; (*create new reference!*) 

6556  909 
val prep_ext = copy; 
7354  910 
fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2)); 
911 
fun print _ (ref cs) = print_cs cs; 

912 
end; 

1724  913 

7354  914 
structure GlobalClaset = TheoryDataFun(GlobalClasetArgs); 
915 
val print_claset = GlobalClaset.print; 

916 
val claset_ref_of_sg = GlobalClaset.get_sg; 

917 
val claset_ref_of = GlobalClaset.get; 

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

918 

1724  919 

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

920 
(* access claset *) 
1724  921 

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

922 
val claset_of_sg = ! o claset_ref_of_sg; 
6391  923 
val claset_of = claset_of_sg o Theory.sign_of; 
1800  924 

6391  925 
fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state; 
926 
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

927 

5028  928 
val claset = claset_of o Context.the_context; 
6391  929 
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

930 

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

931 

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

932 
(* change claset *) 
1800  933 

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

934 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  935 

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

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

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

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

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

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

941 
val AddSIs = change_claset (op addSIs); 
6955  942 
val AddXDs = change_claset (op addXDs); 
943 
val AddXEs = change_claset (op addXEs); 

944 
val AddXIs = change_claset (op addXIs); 

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

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

946 

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

947 

5841  948 
(* proof data kind 'Provers/claset' *) 
949 

950 
structure LocalClasetArgs = 

951 
struct 

952 
val name = "Provers/claset"; 

953 
type T = claset; 

954 
val init = claset_of; 

955 
fun print _ cs = print_cs cs; 

956 
end; 

957 

958 
structure LocalClaset = ProofDataFun(LocalClasetArgs); 

959 
val print_local_claset = LocalClaset.print; 

960 
val get_local_claset = LocalClaset.get; 

961 
val put_local_claset = LocalClaset.put; 

962 

963 

5885  964 
(* attributes *) 
965 

966 
fun change_global_cs f (thy, th) = 

967 
let val r = claset_ref_of thy 

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

970 
fun change_local_cs f (ctxt, th) = 

6096  971 
let val cs = f (get_local_claset ctxt, [th]) 
5885  972 
in (put_local_claset cs ctxt, th) end; 
973 

974 
val safe_dest_global = change_global_cs (op addSDs); 

975 
val safe_elim_global = change_global_cs (op addSEs); 

976 
val safe_intro_global = change_global_cs (op addSIs); 

6955  977 
val haz_dest_global = change_global_cs (op addDs); 
978 
val haz_elim_global = change_global_cs (op addEs); 

979 
val haz_intro_global = change_global_cs (op addIs); 

980 
val xtra_dest_global = change_global_cs (op addXDs); 

981 
val xtra_elim_global = change_global_cs (op addXEs); 

982 
val xtra_intro_global = change_global_cs (op addXIs); 

5885  983 
val delrule_global = change_global_cs (op delrules); 
984 

6955  985 
val safe_dest_local = change_local_cs (op addSDs); 
986 
val safe_elim_local = change_local_cs (op addSEs); 

987 
val safe_intro_local = change_local_cs (op addSIs); 

5885  988 
val haz_dest_local = change_local_cs (op addDs); 
989 
val haz_elim_local = change_local_cs (op addEs); 

990 
val haz_intro_local = change_local_cs (op addIs); 

6955  991 
val xtra_dest_local = change_local_cs (op addXDs); 
992 
val xtra_elim_local = change_local_cs (op addXEs); 

993 
val xtra_intro_local = change_local_cs (op addXIs); 

5885  994 
val delrule_local = change_local_cs (op delrules); 
995 

996 

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

997 
(* tactics referring to the implicit claset *) 
1800  998 

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

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

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

1001 
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

1002 
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

1003 
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

1004 
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

1005 
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

1006 
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

1007 
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

1008 
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

1009 
fun Deepen_tac m = deepen_tac (claset()) m; 
2066  1010 

1800  1011 

0  1012 
end; 
5841  1013 

1014 

1015 

5885  1016 
(** concrete syntax of attributes **) 
5841  1017 

1018 
(* add / del rules *) 

1019 

1020 
val introN = "intro"; 

1021 
val elimN = "elim"; 

1022 
val destN = "dest"; 

1023 
val delN = "del"; 

5885  1024 
val delruleN = "delrule"; 
5841  1025 

8382  1026 
val colon = Args.$$$ ":"; 
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8168
diff
changeset

1027 
val query = Args.$$$ "?"; 
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8168
diff
changeset

1028 
val qquery = Args.$$$ "??"; 
8382  1029 
val query_colon = Args.$$$ "?:"; 
1030 
val qquery_colon = Args.$$$ "??:"; 

5841  1031 

6955  1032 
fun cla_att change xtra haz safe = Attrib.syntax 
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8168
diff
changeset

1033 
(Scan.lift ((qquery >> K xtra  query >> K haz  Scan.succeed safe) >> change)); 
5841  1034 

6955  1035 
fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); 
5885  1036 
val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local); 
5841  1037 

1038 

1039 
(* setup_attrs *) 

1040 

9184  1041 
fun elimify x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x; 
1042 

5841  1043 
val setup_attrs = Attrib.add_attributes 
9184  1044 
[("elimify", (elimify, elimify), "turn destruct rule into elimination rule (classical)"), 
1045 
(destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declare destruction rule"), 

8470  1046 
(elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declare elimination rule"), 
1047 
(introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declare introduction rule"), 

8519  1048 
(delruleN, del_attr, "undeclare rule")]; 
5841  1049 

1050 

1051 

7230  1052 
(** proof methods **) 
1053 

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

1055 

1056 
local 

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

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

1059 
in 

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

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

1062 
end; 

1063 

1064 

1065 
(* METHOD_CLASET' *) 

5841  1066 

8098  1067 
fun METHOD_CLASET' tac ctxt = 
8671  1068 
Method.METHOD (HEADGOAL o tac (get_local_claset ctxt)); 
7230  1069 

1070 

1071 
val trace_rules = ref false; 

5841  1072 

7230  1073 
local 
1074 

1075 
fun trace rules i = 

1076 
if not (! trace_rules) then () 

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

1078 
(map Display.pretty_thm rules)); 

1079 

1080 

5841  1081 
fun order_rules xs = map snd (Tactic.orderlist xs); 
1082 

1083 
fun find_rules concl nets = 

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

1085 
in flat (map rules_of nets) end; 

1086 

1087 
fun find_erules [] _ = [] 

6955  1088 
 find_erules (fact :: _) nets = 
5841  1089 
let 
6502  1090 
fun may_unify net = Net.unify_term net o Logic.strip_assums_concl o #prop o Thm.rep_thm; 
6955  1091 
fun erules_of (_, enet) = order_rules (may_unify enet fact); 
6502  1092 
in flat (map erules_of nets) end; 
5841  1093 

1094 

7230  1095 
fun some_rule_tac cs facts = 
5841  1096 
let 
7230  1097 
val nets = get_nets cs; 
6492  1098 
val erules = find_erules facts nets; 
5841  1099 

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

1101 
let 

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

1103 
val rules = erules @ irules; 

7425  1104 
val ruleq = Method.multi_resolves facts rules; 
7230  1105 
in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end); 
5841  1106 
in tac end; 
1107 

7281  1108 
fun rule_tac [] cs facts = some_rule_tac cs facts 
1109 
 rule_tac rules _ facts = Method.rule_tac rules facts; 

1110 

7230  1111 
in 
7281  1112 
val rule = METHOD_CLASET' o rule_tac; 
7230  1113 
end; 
5841  1114 

1115 

7230  1116 
(* intro / elim methods *) 
1117 

1118 
local 

1119 

7329  1120 
fun intro_elim_tac netpair_of res_tac rules cs facts = 
1121 
let 

8342  1122 
val tac = 
7329  1123 
if null rules then FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs)) 
1124 
else res_tac rules; 

8342  1125 
in Method.insert_tac facts THEN' REPEAT_ALL_NEW tac end; 
6502  1126 

8699  1127 
val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) Tactic.match_tac; 
1128 
val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) Tactic.ematch_tac; 

7230  1129 

1130 
in 

1131 
val intro = METHOD_CLASET' o intro_tac; 

1132 
val elim = METHOD_CLASET' o elim_tac; 

1133 
end; 

1134 

1135 

1136 
(* contradiction method *) 

6502  1137 

7425  1138 
val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl]; 
6502  1139 

1140 

1141 
(* automatic methods *) 

5841  1142 

5927  1143 
val cla_modifiers = 
8382  1144 
[Args.$$$ destN  qquery_colon >> K ((I, xtra_dest_local):Method.modifier), 
1145 
Args.$$$ destN  query_colon >> K (I, haz_dest_local), 

1146 
Args.$$$ destN  colon >> K (I, safe_dest_local), 

1147 
Args.$$$ elimN  qquery_colon >> K (I, xtra_elim_local), 

1148 
Args.$$$ elimN  query_colon >> K (I, haz_elim_local), 

1149 
Args.$$$ elimN  colon >> K (I, safe_elim_local), 

1150 
Args.$$$ introN  qquery_colon >> K (I, xtra_intro_local), 

1151 
Args.$$$ introN  query_colon >> K (I, haz_intro_local), 

1152 
Args.$$$ introN  colon >> K (I, safe_intro_local), 

1153 
Args.$$$ delN  colon >> K (I, delrule_local)]; 

5927  1154 

7559  1155 
fun cla_meth tac prems ctxt = Method.METHOD (fn facts => 
1156 
ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt)); 

7132  1157 

7559  1158 
fun cla_meth' tac prems ctxt = Method.METHOD (fn facts => 
8168  1159 
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt))); 
5841  1160 

7559  1161 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1162 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1163 

1164 

1165 

1166 
(** setup_methods **) 

1167 

1168 
val setup_methods = Method.add_methods 

8098  1169 
[("default", Method.thms_ctxt_args rule, "apply some rule"), 
1170 
("rule", Method.thms_ctxt_args rule, "apply some rule"), 

6502  1171 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
8098  1172 
("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"), 
1173 
("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"), 

7132  1174 
("safe_tac", cla_method safe_tac, "safe_tac (improper!)"), 
1175 
("safe_step_tac", cla_method' safe_step_tac, "safe_step_tac (improper!)"), 

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

7004  1177 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
1178 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 

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

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

5841  1181 

1182 

1183 

1184 
(** theory setup **) 

1185 

7354  1186 
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; 
5841  1187 

1188 

8667  1189 

1190 
(** outer syntax **) 

1191 

1192 
val print_clasetP = 

1193 
OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" 

1194 
OuterSyntax.Keyword.diag 

9010  1195 
(Scan.succeed (Toplevel.no_timing o (Toplevel.keep 
1196 
(Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); 

8667  1197 

1198 
val _ = OuterSyntax.add_parsers [print_clasetP]; 

1199 

1200 

5841  1201 
end; 