author  wenzelm 
Wed, 08 Mar 2000 23:47:44 +0100  
changeset 8382  52d5fae273dd 
parent 8342  289ad8062cb5 
child 8470  f06fc940c61c 
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 
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset

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

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

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

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

35 
end; 
0  36 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

62 
val delWrapper : claset * string > claset 

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

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

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

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

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

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

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

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

74 

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

75 
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

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

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

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

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

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

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

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

83 

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

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

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

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

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

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

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

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

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

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

93 

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

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

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

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

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

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

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

100 
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

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

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

104 
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

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

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

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

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

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

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

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

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

114 
val instp_step_tac : claset > int > tactic 
1724  115 

116 
val AddDs : thm list > unit 

117 
val AddEs : thm list > unit 

118 
val AddIs : thm list > unit 

119 
val AddSDs : thm list > unit 

120 
val AddSEs : thm list > unit 

121 
val AddSIs : thm list > unit 

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

124 
val AddXIs : thm list > unit 

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

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

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

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

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

136 
end; 
1724  137 

5841  138 
signature CLASSICAL = 
139 
sig 

140 
include BASIC_CLASSICAL 

141 
val print_local_claset: Proof.context > unit 

142 
val get_local_claset: Proof.context > claset 

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

144 
val safe_dest_global: theory attribute 

145 
val safe_elim_global: theory attribute 

146 
val safe_intro_global: theory attribute 

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

149 
val haz_intro_global: theory attribute 

150 
val xtra_dest_global: theory attribute 

151 
val xtra_elim_global: theory attribute 

152 
val xtra_intro_global: theory attribute 

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

156 
val safe_intro_local: Proof.context attribute 

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

159 
val haz_intro_local: Proof.context attribute 

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

162 
val xtra_intro_local: Proof.context attribute 

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

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

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

171 

0  172 

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

7354  176 
local open Data in 
0  177 

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

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

0  182 

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

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

186 
val contr_tac = eresolve_tac [not_elim] THEN' 

187 
(eq_assume_tac ORELSE' assume_tac); 

0  188 

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

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

190 
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

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

193 
(*Like mp_tac but instantiates no variables*) 

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

194 
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

195 

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

0  198 

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

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

201 

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

203 
trying rules in order. *) 

204 
fun swap_res_tac rls = 

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

207 
contr_tac ORELSE' 

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

0  209 
end; 
210 

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

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

212 
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

213 

6967  214 
fun dup_elim th = 
215 
(case try 

216 
(rule_by_tactic (TRYALL (etac revcut_rl))) 

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

218 
Some th' => th' 

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

0  220 

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

221 

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

224 
datatype claset = 

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

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

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

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

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

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

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

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

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

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

0  238 

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

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

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

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

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

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

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

246 

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

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

248 
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

249 
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

250 
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

251 
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

252 
*) 
0  253 

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

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

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

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

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

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

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

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

6502  265 
safe0_netpair = empty_netpair, 
266 
safep_netpair = empty_netpair, 

267 
haz_netpair = empty_netpair, 

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

0  270 

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

4624  274 
Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs)); 
6955  275 
Pretty.writeln (Pretty.big_list "extra introduction rules:" (pretty_thms xtraIs)); 
4625  276 
Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs)); 
6955  277 
Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs)); 
278 
Pretty.writeln (Pretty.big_list "extra elimination rules:" (pretty_thms xtraEs)) 

3546  279 
end; 
0  280 

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

282 

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

285 
in 

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

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

288 
end; 

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

289 

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

290 

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

292 

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

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

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

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

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

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

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

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

301 

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

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

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

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

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

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

308 

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

310 

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

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

312 
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

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

314 
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

315 

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

317 

1800  318 
val delete = delete_tagged_list o joinrules; 
319 

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

320 
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

321 
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

322 

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

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

324 
is still allowed.*) 
6955  325 
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

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

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

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

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

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

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

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

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

336 
else if mem_thm (th, xtraEs) then 

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

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

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

339 

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

341 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

359 
hazEs = hazEs, 
6955  360 
xtraIs = xtraIs, 
361 
xtraEs = xtraEs, 

4651  362 
swrappers = swrappers, 
363 
uwrappers = uwrappers, 

2630  364 
haz_netpair = haz_netpair, 
6955  365 
dup_netpair = dup_netpair, 
366 
xtra_netpair = xtra_netpair} 

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

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

368 

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

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

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

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

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

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

376 
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

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

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

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

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

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

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

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

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

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

386 
hazEs = hazEs, 
6955  387 
xtraIs = xtraIs, 
388 
xtraEs = xtraEs, 

4651  389 
swrappers = swrappers, 
390 
uwrappers = uwrappers, 

2630  391 
haz_netpair = haz_netpair, 
6955  392 
dup_netpair = dup_netpair, 
393 
xtra_netpair = xtra_netpair} 

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

394 
end; 
0  395 

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

396 
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

397 

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

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

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

400 

0  401 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
402 

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

403 

1800  404 
(*** Hazardous (unsafe) rules ***) 
0  405 

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

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

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

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

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

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

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

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

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

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

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

418 
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

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

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

421 
hazEs = hazEs, 
6955  422 
xtraIs = xtraIs, 
423 
xtraEs = xtraEs, 

4651  424 
swrappers = swrappers, 
425 
uwrappers = uwrappers, 

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

426 
safe0_netpair = safe0_netpair, 
6955  427 
safep_netpair = safep_netpair, 
428 
xtra_netpair = xtra_netpair} 

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

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

430 

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

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

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

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

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

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

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

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

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

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

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

443 
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

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

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

446 
hazIs = hazIs, 
6955  447 
xtraIs = xtraIs, 
448 
xtraEs = xtraEs, 

4651  449 
swrappers = swrappers, 
450 
uwrappers = uwrappers, 

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

451 
safe0_netpair = safe0_netpair, 
6955  452 
safep_netpair = safep_netpair, 
453 
xtra_netpair = xtra_netpair} 

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

454 
end; 
0  455 

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

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

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

458 

0  459 
fun cs addDs ths = cs addEs (map make_elim ths); 
460 

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

461 

6955  462 
(*** Extra (single step) rules ***) 
463 

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

465 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 

466 
th)= 

467 
if mem_thm (th, xtraIs) then 

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

469 
cs) 

470 
else 

471 
let val nI = length xtraIs + 1 

472 
and nE = length xtraEs 

473 
in warn_dup th cs; 

474 
CS{xtraIs = th::xtraIs, 

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

476 
safeIs = safeIs, 

477 
safeEs = safeEs, 

478 
hazIs = hazIs, 

479 
hazEs = hazEs, 

480 
xtraEs = xtraEs, 

481 
swrappers = swrappers, 

482 
uwrappers = uwrappers, 

483 
safe0_netpair = safe0_netpair, 

484 
safep_netpair = safep_netpair, 

485 
haz_netpair = haz_netpair, 

486 
dup_netpair = dup_netpair} 

487 
end; 

488 

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

490 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, 

491 
th) = 

492 
if mem_thm (th, xtraEs) then 

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

494 
cs) 

495 
else 

496 
let val nI = length xtraIs 

497 
and nE = length xtraEs + 1 

498 
in warn_dup th cs; 

499 
CS{xtraEs = th::xtraEs, 

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

501 
safeIs = safeIs, 

502 
safeEs = safeEs, 

503 
hazIs = hazIs, 

504 
hazEs = hazEs, 

505 
xtraIs = xtraIs, 

506 
swrappers = swrappers, 

507 
uwrappers = uwrappers, 

508 
safe0_netpair = safe0_netpair, 

509 
safep_netpair = safep_netpair, 

510 
haz_netpair = haz_netpair, 

511 
dup_netpair = dup_netpair} 

512 
end; 

513 

514 
infix 4 addXIs addXEs addXDs; 

515 

516 
val op addXIs = rev_foldl addXI; 

517 
val op addXEs = rev_foldl addXE; 

518 

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

520 

521 

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

524 
to insert. 

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

525 
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

526 
searches in all the lists and chooses the relevant delXX functions. 
1800  527 
***) 
528 

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

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

532 
if mem_thm (th, safeIs) then 
7559  533 
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

534 
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

535 
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

536 
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

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

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

539 
hazEs = hazEs, 
6955  540 
xtraIs = xtraIs, 
541 
xtraEs = xtraEs, 

4651  542 
swrappers = swrappers, 
543 
uwrappers = uwrappers, 

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

544 
haz_netpair = haz_netpair, 
6955  545 
dup_netpair = dup_netpair, 
546 
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

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

548 
else cs; 
1800  549 

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

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

553 
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

554 
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

555 
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

556 
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

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

558 
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

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

560 
hazEs = hazEs, 
6955  561 
xtraIs = xtraIs, 
562 
xtraEs = xtraEs, 

4651  563 
swrappers = swrappers, 
564 
uwrappers = uwrappers, 

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

565 
haz_netpair = haz_netpair, 
6955  566 
dup_netpair = dup_netpair, 
567 
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

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

569 
else cs; 
1800  570 

571 

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

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

575 
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

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

579 
safeEs = safeEs, 

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

580 
hazIs = rem_thm (hazIs,th), 
1800  581 
hazEs = hazEs, 
6955  582 
xtraIs = xtraIs, 
583 
xtraEs = xtraEs, 

4651  584 
swrappers = swrappers, 
585 
uwrappers = uwrappers, 

1800  586 
safe0_netpair = safe0_netpair, 
6955  587 
safep_netpair = safep_netpair, 
588 
xtra_netpair = xtra_netpair} 

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

589 
else cs; 
1800  590 

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

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

594 
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

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

598 
safeEs = safeEs, 

599 
hazIs = hazIs, 

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

600 
hazEs = rem_thm (hazEs,th), 
6955  601 
xtraIs = xtraIs, 
602 
xtraEs = xtraEs, 

603 
swrappers = swrappers, 

604 
uwrappers = uwrappers, 

605 
safe0_netpair = safe0_netpair, 

606 
safep_netpair = safep_netpair, 

607 
xtra_netpair = xtra_netpair} 

608 
else cs; 

609 

610 

611 
fun delXI th 

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

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

614 
if mem_thm (th, xtraIs) then 

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

616 
safeIs = safeIs, 

617 
safeEs = safeEs, 

618 
hazIs = hazIs, 

619 
hazEs = hazEs, 

620 
xtraIs = rem_thm (xtraIs,th), 

621 
xtraEs = xtraEs, 

4651  622 
swrappers = swrappers, 
623 
uwrappers = uwrappers, 

1800  624 
safe0_netpair = safe0_netpair, 
6955  625 
safep_netpair = safep_netpair, 
626 
haz_netpair = haz_netpair, 

627 
dup_netpair = dup_netpair} 

628 
else cs; 

629 

630 
fun delXE th 

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

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

633 
if mem_thm (th, xtraEs) then 

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

635 
safeIs = safeIs, 

636 
safeEs = safeEs, 

637 
hazIs = hazIs, 

638 
hazEs = hazEs, 

639 
xtraIs = xtraIs, 

640 
xtraEs = rem_thm (xtraEs,th), 

641 
swrappers = swrappers, 

642 
uwrappers = uwrappers, 

643 
safe0_netpair = safe0_netpair, 

644 
safep_netpair = safep_netpair, 

645 
haz_netpair = haz_netpair, 

646 
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

647 
else cs; 
1800  648 

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

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

651 
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse 
6955  652 
mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse 
653 
mem_thm (th, xtraIs) orelse mem_thm (th, xtraEs) 

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

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

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

656 
cs); 
1800  657 

658 
val op delrules = foldl delrule; 

659 

660 

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

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

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

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

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

668 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  669 
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

670 

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

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

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

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

677 
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, 
6955  678 
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

679 

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

680 

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

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

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

685 
overwrite (swrappers, new_swrapper))); 
4651  686 

687 
(*Add/replace an unsafe wrapper*) 

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

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

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

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

692 

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

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

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

696 
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

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

698 

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

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

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

702 
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

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

704 

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

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

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

710 

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

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

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

716 

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

719 
fun cs addE2 (name, thm) = 

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

721 
fun cs addSD2 (name, thm) = 

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

723 
fun cs addSE2 (name, thm) = 

724 
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

725 

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

728 
treatment of priority might get muddled up.*) 

729 
fun merge_cs 

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

2630  735 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
736 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

6955  737 
val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs) 
738 
val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs) 

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

739 
val cs1 = cs addSIs safeIs' 
4765  740 
addSEs safeEs' 
741 
addIs hazIs' 

742 
addEs hazEs' 

6955  743 
addXIs xtraIs' 
744 
addXEs xtraEs' 

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

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

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

747 
in cs3 
1711  748 
end; 
749 

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

750 

1800  751 
(**** Simple tactics for theorem proving ****) 
0  752 

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

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

758 
bimatch_from_nets_tac safe0_netpair, 

759 
FIRST' hyp_subst_tacs, 

760 
bimatch_from_nets_tac safep_netpair]); 

0  761 

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

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

765 

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

768 

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

769 

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

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

771 

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

772 
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

773 

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

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

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

776 
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

777 
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

778 

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

779 
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

780 
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

781 

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

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

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

784 
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

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

786 

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

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

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

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

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

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

793 
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

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

795 

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

796 
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

797 

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

798 

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

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

800 

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

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

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

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

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

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

807 

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

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

810 
biresolve_from_nets_tac safep_netpair; 
0  811 

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

813 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  814 

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

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

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

817 

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

0  821 

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

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

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

0  826 

1800  827 
(**** The following tactics all fail unless they solve one goal ****) 
0  828 

829 
(*Dumb but fast*) 

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

831 

832 
(*Slower but smarter than fast_tac*) 

833 
fun best_tac cs = 

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

835 

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

837 

838 
fun slow_best_tac cs = 

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

840 

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

841 

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

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

844 

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

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

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

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

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

849 

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

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

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

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

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

854 

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

856 
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

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

859 

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

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

861 
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

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

863 
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

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

865 

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

869 
(instp_step_tac cs APPEND' dup_step_tac cs); 

870 
in fun depth_tac cs m i state = SELECT_GOAL 

871 
(safe_steps_tac cs 1 THEN_ELSE 

872 
(DEPTH_SOLVE (depth_tac cs m 1), 

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

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

875 
)) i state; 

876 
end; 

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

877 

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

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

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

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

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

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

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

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

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

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

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

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

891 

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

892 
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

893 

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

894 

1724  895 

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

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

897 

7354  898 
(* theory data kind 'Provers/claset' *) 
1724  899 

7354  900 
structure GlobalClasetArgs = 
901 
struct 

902 
val name = "Provers/claset"; 

903 
type T = claset ref; 

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

904 

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

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

910 
end; 

1724  911 

7354  912 
structure GlobalClaset = TheoryDataFun(GlobalClasetArgs); 
913 
val print_claset = GlobalClaset.print; 

914 
val claset_ref_of_sg = GlobalClaset.get_sg; 

915 
val claset_ref_of = GlobalClaset.get; 

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

916 

1724  917 

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

918 
(* access claset *) 
1724  919 

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

920 
val claset_of_sg = ! o claset_ref_of_sg; 
6391  921 
val claset_of = claset_of_sg o Theory.sign_of; 
1800  922 

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

925 

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

928 

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

929 

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

930 
(* change claset *) 
1800  931 

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

932 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  933 

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

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

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

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

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

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

939 
val AddSIs = change_claset (op addSIs); 
6955  940 
val AddXDs = change_claset (op addXDs); 
941 
val AddXEs = change_claset (op addXEs); 

942 
val AddXIs = change_claset (op addXIs); 

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

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

944 

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

945 

5841  946 
(* proof data kind 'Provers/claset' *) 
947 

948 
structure LocalClasetArgs = 

949 
struct 

950 
val name = "Provers/claset"; 

951 
type T = claset; 

952 
val init = claset_of; 

953 
fun print _ cs = print_cs cs; 

954 
end; 

955 

956 
structure LocalClaset = ProofDataFun(LocalClasetArgs); 

957 
val print_local_claset = LocalClaset.print; 

958 
val get_local_claset = LocalClaset.get; 

959 
val put_local_claset = LocalClaset.put; 

960 

961 

5885  962 
(* attributes *) 
963 

964 
fun change_global_cs f (thy, th) = 

965 
let val r = claset_ref_of thy 

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

968 
fun change_local_cs f (ctxt, th) = 

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

972 
val safe_dest_global = change_global_cs (op addSDs); 

973 
val safe_elim_global = change_global_cs (op addSEs); 

974 
val safe_intro_global = change_global_cs (op addSIs); 

6955  975 
val haz_dest_global = change_global_cs (op addDs); 
976 
val haz_elim_global = change_global_cs (op addEs); 

977 
val haz_intro_global = change_global_cs (op addIs); 

978 
val xtra_dest_global = change_global_cs (op addXDs); 

979 
val xtra_elim_global = change_global_cs (op addXEs); 

980 
val xtra_intro_global = change_global_cs (op addXIs); 

5885  981 
val delrule_global = change_global_cs (op delrules); 
982 

6955  983 
val safe_dest_local = change_local_cs (op addSDs); 
984 
val safe_elim_local = change_local_cs (op addSEs); 

985 
val safe_intro_local = change_local_cs (op addSIs); 

5885  986 
val haz_dest_local = change_local_cs (op addDs); 
987 
val haz_elim_local = change_local_cs (op addEs); 

988 
val haz_intro_local = change_local_cs (op addIs); 

6955  989 
val xtra_dest_local = change_local_cs (op addXDs); 
990 
val xtra_elim_local = change_local_cs (op addXEs); 

991 
val xtra_intro_local = change_local_cs (op addXIs); 

5885  992 
val delrule_local = change_local_cs (op delrules); 
993 

994 

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

995 
(* tactics referring to the implicit claset *) 
1800  996 

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

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

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

999 
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

1000 
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

1001 
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

1002 
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

1003 
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

1004 
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

1005 
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

1006 
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

1007 
fun Deepen_tac m = deepen_tac (claset()) m; 
2066  1008 

1800  1009 

0  1010 
end; 
5841  1011 

1012 

1013 

5885  1014 
(** concrete syntax of attributes **) 
5841  1015 

1016 
(* add / del rules *) 

1017 

1018 
val introN = "intro"; 

1019 
val elimN = "elim"; 

1020 
val destN = "dest"; 

1021 
val delN = "del"; 

5885  1022 
val delruleN = "delrule"; 
5841  1023 

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

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

1026 
val qquery = Args.$$$ "??"; 
8382  1027 
val query_colon = Args.$$$ "?:"; 
1028 
val qquery_colon = Args.$$$ "??:"; 

5841  1029 

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

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

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

1036 

1037 
(* setup_attrs *) 

1038 

1039 
val setup_attrs = Attrib.add_attributes 

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

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

5885  1043 
(delruleN, del_attr, "delete rule")]; 
5841  1044 

1045 

1046 

7230  1047 
(** proof methods **) 
1048 

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

1050 

1051 
local 

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

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

1054 
in 

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

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

1057 
end; 

1058 

1059 

1060 
(* METHOD_CLASET' *) 

5841  1061 

8098  1062 
fun METHOD_CLASET' tac ctxt = 
8154  1063 
Method.METHOD (FINDGOAL o tac (get_local_claset ctxt)); 
7230  1064 

1065 

1066 
val trace_rules = ref false; 

5841  1067 

7230  1068 
local 
1069 

1070 
fun trace rules i = 

1071 
if not (! trace_rules) then () 

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

1073 
(map Display.pretty_thm rules)); 

1074 

1075 

5841  1076 
fun order_rules xs = map snd (Tactic.orderlist xs); 
1077 

1078 
fun find_rules concl nets = 

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

1080 
in flat (map rules_of nets) end; 

1081 

1082 
fun find_erules [] _ = [] 

6955  1083 
 find_erules (fact :: _) nets = 
5841  1084 
let 
6502  1085 
fun may_unify net = Net.unify_term net o Logic.strip_assums_concl o #prop o Thm.rep_thm; 
6955  1086 
fun erules_of (_, enet) = order_rules (may_unify enet fact); 
6502  1087 
in flat (map erules_of nets) end; 
5841  1088 

1089 

7230  1090 
fun some_rule_tac cs facts = 
5841  1091 
let 
7230  1092 
val nets = get_nets cs; 
6492  1093 
val erules = find_erules facts nets; 
5841  1094 

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

1096 
let 

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

1098 
val rules = erules @ irules; 

7425  1099 
val ruleq = Method.multi_resolves facts rules; 
7230  1100 
in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end); 
5841  1101 
in tac end; 
1102 

7281  1103 
fun rule_tac [] cs facts = some_rule_tac cs facts 
1104 
 rule_tac rules _ facts = Method.rule_tac rules facts; 

1105 

7230  1106 
in 
7281  1107 
val rule = METHOD_CLASET' o rule_tac; 
7230  1108 
end; 
5841  1109 

1110 

7230  1111 
(* intro / elim methods *) 
1112 

1113 
local 

1114 

7329  1115 
fun intro_elim_tac netpair_of res_tac rules cs facts = 
1116 
let 

8342  1117 
val tac = 
7329  1118 
if null rules then FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs)) 
1119 
else res_tac rules; 

8342  1120 
in Method.insert_tac facts THEN' REPEAT_ALL_NEW tac end; 
6502  1121 

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

1124 

1125 
in 

1126 
val intro = METHOD_CLASET' o intro_tac; 

1127 
val elim = METHOD_CLASET' o elim_tac; 

1128 
end; 

1129 

1130 

1131 
(* contradiction method *) 

6502  1132 

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

1135 

1136 
(* automatic methods *) 

5841  1137 

5927  1138 
val cla_modifiers = 
8382  1139 
[Args.$$$ destN  qquery_colon >> K ((I, xtra_dest_local):Method.modifier), 
1140 
Args.$$$ destN  query_colon >> K (I, haz_dest_local), 

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

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

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

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

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

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

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

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

5927  1149 

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

7132  1152 

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

7559  1156 
val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; 
1157 
val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; 

5841  1158 

1159 

1160 

1161 
(** setup_methods **) 

1162 

1163 
val setup_methods = Method.add_methods 

8098  1164 
[("default", Method.thms_ctxt_args rule, "apply some rule"), 
1165 
("rule", Method.thms_ctxt_args rule, "apply some rule"), 

6502  1166 
("contradiction", Method.no_args contradiction, "proof by contradiction"), 
8098  1167 
("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"), 
1168 
("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"), 

7132  1169 
("safe_tac", cla_method safe_tac, "safe_tac (improper!)"), 
1170 
("safe_step_tac", cla_method' safe_step_tac, "safe_step_tac (improper!)"), 

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

7004  1172 
("fast", cla_method' fast_tac, "classical prover (depthfirst)"), 
1173 
("best", cla_method' best_tac, "classical prover (bestfirst)"), 

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

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

5841  1176 

1177 

1178 

1179 
(** theory setup **) 

1180 

7354  1181 
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; 
5841  1182 

1183 

1184 
end; 