author  oheimb 
Wed, 25 Feb 1998 15:51:24 +0100  
changeset 4651  70dd492a1698 
parent 4646  f6298426f5a7 
child 4653  d60f76680bf4 
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 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

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

21 

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 
(*should be a type abbreviation in signature CLASSICAL*) 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

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

26 

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

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

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

29 
val clasetK: string 
4124  30 
exception ClasetData of object ref 
31 
val thy_data: string * (object * (object > object) * 

4259  32 
(object * object > object) * (Sign.sg > object > unit)) 
4124  33 
val fix_methods: object * (object > object) * 
4259  34 
(object * object > object) * (Sign.sg > object > unit) > unit 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

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

36 

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

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

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

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

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

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

44 
end; 
0  45 

46 
signature CLASSICAL = 

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

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

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

50 
val print_cs: claset > unit 
4380  51 
val print_claset: theory > unit 
4651  52 
val rep_claset: (* 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

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

54 
hazIs: thm list, hazEs: thm list, 
4651  55 
swrappers: (string * wrapper) list, 
56 
uwrappers: (string * wrapper) list, 

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

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

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

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

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

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

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

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

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

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

70 
val delWrapper : claset * string > claset 

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

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

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

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

75 
val appWrappers : claset > wrapper 

76 
val appSWrappers : claset > wrapper 

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

77 

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

78 
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

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

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

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

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

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

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

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

86 

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

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

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

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

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

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

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

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

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

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

96 

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

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

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

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

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

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

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

103 
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

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

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

106 
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

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

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

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

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

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

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

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

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

116 
val instp_step_tac : claset > int > tactic 
1724  117 

118 
val AddDs : thm list > unit 

119 
val AddEs : thm list > unit 

120 
val AddIs : thm list > unit 

121 
val AddSDs : thm list > unit 

122 
val AddSEs : thm list > unit 

123 
val AddSIs : thm list > unit 

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

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

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

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

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

135 
end; 
1724  136 

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

137 

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

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

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

140 

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

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

142 

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

143 
val clasetK = "claset"; 
4124  144 
exception ClasetData of object ref; 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

145 

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

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

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

148 

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

149 
val empty_ref = ref ERROR; 
4124  150 
val prep_ext_fn = ref (undef: object > object); 
151 
val merge_fn = ref (undef: object * object > object); 

4259  152 
val print_fn = ref (undef: Sign.sg > object > unit); 
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

153 

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

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

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

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

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

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

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

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

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

163 

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

164 

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

165 
end; 
0  166 

167 

168 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 

169 
struct 

170 

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

171 
local open ClasetThyData Data in 
0  172 

1800  173 
(*** Useful tactics for classical reasoning ***) 
0  174 

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

0  177 

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

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

181 
val contr_tac = eresolve_tac [not_elim] THEN' 

182 
(eq_assume_tac ORELSE' assume_tac); 

0  183 

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

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

185 
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

186 
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; 
0  187 

188 
(*Like mp_tac but instantiates no variables*) 

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

189 
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

190 

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

0  193 

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

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

196 

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

198 
trying rules in order. *) 

199 
fun swap_res_tac rls = 

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

202 
contr_tac ORELSE' 

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

0  204 
end; 
205 

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

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

207 
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

208 

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

211 
rule_by_tactic (TRYALL (etac revcut_rl)) 

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

0  213 

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

214 

1800  215 
(**** Classical rule sets ****) 
0  216 

217 
datatype claset = 

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

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

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

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

221 
hazEs : thm list, (*unsafe elimination rules*) 
4651  222 
swrappers : (string * wrapper) list, (*for transf. safe_step_tac*) 
223 
uwrappers : (string * wrapper) list, (*for transforming step_tac*) 

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

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

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

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

227 
dup_netpair : netpair}; (*nets for duplication*) 
0  228 

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

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

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

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

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

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

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

235 

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

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

237 
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

238 
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

239 
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

240 
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

241 
*) 
0  242 

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

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

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

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

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

247 
hazEs = [], 
4651  248 
swrappers = [], 
249 
uwrappers = [], 

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

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

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

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

253 
dup_netpair = (Net.empty,Net.empty)}; 
0  254 

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

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

4624  258 
Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs)); 
4625  259 
Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs)); 
260 
Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs)) 

3546  261 
end; 
0  262 

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

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

264 

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

267 
in 

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

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

270 
end; 

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

271 

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

272 

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

274 

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

275 
In case of overlap, new rules are tried BEFORE old ones!! 
1800  276 
***) 
0  277 

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

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

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

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

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

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

283 

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

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

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

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

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

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

290 

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

292 

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

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

294 
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

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

296 
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

297 

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

299 

1800  300 
val delete = delete_tagged_list o joinrules; 
301 

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

302 
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

303 
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

304 

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

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

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

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

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

309 
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

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

311 
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

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

313 
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

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

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

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

317 

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

319 

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

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

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

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

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

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

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

327 
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

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

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

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

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

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

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

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

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

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

337 
hazEs = hazEs, 
4651  338 
swrappers = swrappers, 
339 
uwrappers = uwrappers, 

2630  340 
haz_netpair = haz_netpair, 
341 
dup_netpair = dup_netpair} 

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

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

343 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

361 
hazEs = hazEs, 
4651  362 
swrappers = swrappers, 
363 
uwrappers = uwrappers, 

2630  364 
haz_netpair = haz_netpair, 
365 
dup_netpair = dup_netpair} 

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

366 
end; 
0  367 

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

368 
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

369 

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

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

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

372 

0  373 
fun cs addSDs ths = cs addSEs (map make_elim ths); 
374 

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

375 

1800  376 
(*** Hazardous (unsafe) rules ***) 
0  377 

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

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

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

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

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

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

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

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

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

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

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

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

390 
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

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

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

393 
hazEs = hazEs, 
4651  394 
swrappers = swrappers, 
395 
uwrappers = uwrappers, 

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

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

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

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

399 

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

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

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

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

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

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

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

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

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

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

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

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

412 
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

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

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

415 
hazIs = hazIs, 
4651  416 
swrappers = swrappers, 
417 
uwrappers = uwrappers, 

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

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

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

420 
end; 
0  421 

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

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

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

424 

0  425 
fun cs addDs ths = cs addEs (map make_elim ths); 
426 

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

427 

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

430 
to insert. 

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

431 
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

432 
searches in all the lists and chooses the relevant delXX functions. 
1800  433 
***) 
434 

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

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

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

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

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

440 
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

441 
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

442 
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

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

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

445 
hazEs = hazEs, 
4651  446 
swrappers = swrappers, 
447 
uwrappers = uwrappers, 

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

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

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

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

451 
else cs; 
1800  452 

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

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

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

456 
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

457 
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

458 
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

459 
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

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

461 
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

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

463 
hazEs = hazEs, 
4651  464 
swrappers = swrappers, 
465 
uwrappers = uwrappers, 

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

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

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

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

469 
else cs; 
1800  470 

471 

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

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

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

475 
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

476 
CS{haz_netpair = delete ([th], []) haz_netpair, 
1800  477 
dup_netpair = delete ([dup_intr th], []) dup_netpair, 
478 
safeIs = safeIs, 

479 
safeEs = safeEs, 

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

480 
hazIs = rem_thm (hazIs,th), 
1800  481 
hazEs = hazEs, 
4651  482 
swrappers = swrappers, 
483 
uwrappers = uwrappers, 

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

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

486 
else cs; 
1800  487 

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

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

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

491 
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

492 
CS{haz_netpair = delete ([], [th]) haz_netpair, 
1800  493 
dup_netpair = delete ([], [dup_elim th]) dup_netpair, 
494 
safeIs = safeIs, 

495 
safeEs = safeEs, 

496 
hazIs = hazIs, 

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

497 
hazEs = rem_thm (hazEs,th), 
4651  498 
swrappers = swrappers, 
499 
uwrappers = uwrappers, 

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

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

502 
else cs; 
1800  503 

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

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

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

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

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

509 
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

510 
cs); 
1800  511 

512 
val op delrules = foldl delrule; 

513 

514 

2630  515 
(*** Setting or modifying the wrapper tacticals ***) 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

516 

4651  517 
(*Add/replace a safe wrapper*) 
518 
fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

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

519 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
4651  520 
addSWrapper new_swrapper = 
2630  521 
CS{safeIs = safeIs, 
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset

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

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

524 
hazEs = hazEs, 
4651  525 
swrappers = (case assoc_string (swrappers,(fst new_swrapper)) of None =>() 
526 
 Some x => warning("overwriting safe wrapper "^fst new_swrapper); 

527 
overwrite (swrappers, new_swrapper)), 

528 
uwrappers = uwrappers, 

529 
safe0_netpair = safe0_netpair, 

530 
safep_netpair = safep_netpair, 

531 
haz_netpair = haz_netpair, 

532 
dup_netpair = dup_netpair}; 

533 

534 
(*Add/replace an unsafe wrapper*) 

535 
fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

536 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 

537 
addWrapper new_uwrapper = 

538 
CS{safeIs = safeIs, 

539 
safeEs = safeEs, 

540 
hazIs = hazIs, 

541 
hazEs = hazEs, 

542 
swrappers = swrappers, 

543 
uwrappers = (case assoc_string (uwrappers,(fst new_uwrapper)) of None =>() 

544 
 Some x => warning ("overwriting unsafe wrapper "^fst new_uwrapper); 

545 
overwrite (uwrappers, new_uwrapper)), 

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

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

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

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

549 
dup_netpair = dup_netpair}; 
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset

550 

4651  551 
(*Remove a safe wrapper*) 
552 
fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

2630  553 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
4651  554 
delSWrapper name = 
2630  555 
CS{safeIs = safeIs, 
556 
safeEs = safeEs, 

557 
hazIs = hazIs, 

558 
hazEs = hazEs, 

4651  559 
swrappers = (case assoc_string (swrappers, name) of None => 
560 
warning("safe wrapper "^ name ^" not in claset")  Some x => (); 

561 
filter_out (fn (n,f) => n = name) swrappers), 

562 
uwrappers = uwrappers, 

2630  563 
safe0_netpair = safe0_netpair, 
564 
safep_netpair = safep_netpair, 

565 
haz_netpair = haz_netpair, 

566 
dup_netpair = dup_netpair}; 

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

567 

4651  568 
(*Remove an unsafe wrapper*) 
569 
fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 

570 
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 

571 
delWrapper name = 

572 
CS{safeIs = safeIs, 

573 
safeEs = safeEs, 

574 
hazIs = hazIs, 

575 
hazEs = hazEs, 

576 
swrappers = swrappers, 

577 
uwrappers = (case assoc_string (uwrappers, name) of None => 

578 
warning("unsafe wrapper "^ name ^" not in claset")  Some x => (); 

579 
filter_out (fn (n,f) => n = name) uwrappers), 

580 
safe0_netpair = safe0_netpair, 

581 
safep_netpair = safep_netpair, 

582 
haz_netpair = haz_netpair, 

583 
dup_netpair = dup_netpair}; 

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

584 

2630  585 
(*compose a safe tactic sequentially before/alternatively after safe_step_tac*) 
4651  586 
fun cs addSbefore (name,tac1) = cs addSWrapper (name, 
587 
fn tac2 => tac1 THEN_MAYBE' tac2); 

588 
fun cs addSaltern (name,tac2) = cs addSWrapper (name, 

589 
fn tac1 => tac1 ORELSE' tac2); 

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

590 

2630  591 
(*compose a tactic sequentially before/alternatively after the step tactic*) 
4651  592 
fun cs addbefore (name,tac1) = cs addWrapper (name, 
593 
fn tac2 => tac1 THEN_MAYBE' tac2); 

594 
fun cs addaltern (name,tac2) = cs addWrapper (name, 

595 
fn tac1 => tac1 APPEND' tac2); 

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

596 

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

599 
treatment of priority might get muddled up.*) 

600 
fun merge_cs 

2630  601 
(cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, 
1711  602 
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,...}) = 
603 
let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) 

604 
val safeEs' = gen_rems eq_thm (safeEs2,safeEs) 

2630  605 
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) 
606 
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) 

1711  607 
in cs addSIs safeIs' 
608 
addSEs safeEs' 

609 
addIs hazIs' 

610 
addEs hazEs' 

611 
end; 

612 

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

613 

1800  614 
(**** Simple tactics for theorem proving ****) 
0  615 

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

2630  617 
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
4651  618 
appSWrappers cs (FIRST' [ 
2630  619 
eq_assume_tac, 
620 
eq_mp_tac, 

621 
bimatch_from_nets_tac safe0_netpair, 

622 
FIRST' hyp_subst_tacs, 

623 
bimatch_from_nets_tac safep_netpair]); 

0  624 

625 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 

2630  626 
fun safe_tac cs = REPEAT_DETERM_FIRST 
627 
(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); 

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

628 

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

629 

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

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

631 

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

632 
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

633 

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

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

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

636 
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

637 
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

638 

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

639 
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

640 
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

641 

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

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

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

644 
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

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

646 

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

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

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

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

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

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

653 
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

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

655 

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

656 
fun 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

657 

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

658 

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

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

660 

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

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

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

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

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

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

667 

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

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

670 
biresolve_from_nets_tac safep_netpair; 
0  671 

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

673 
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; 
0  674 

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

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

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

677 

0  678 
(*Single step for the prover. FAILS unless it makes progress. *) 
4651  679 
fun step_tac cs i = appWrappers cs 
2630  680 
(K (safe_tac cs) ORELSE' (inst_step_tac cs ORELSE' haz_step_tac cs)) i; 
0  681 

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

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

4651  684 
fun slow_step_tac cs i = appWrappers cs 
2630  685 
(K (safe_tac cs) ORELSE' (inst_step_tac cs APPEND' haz_step_tac cs)) i; 
0  686 

1800  687 
(**** The following tactics all fail unless they solve one goal ****) 
0  688 

689 
(*Dumb but fast*) 

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

691 

692 
(*Slower but smarter than fast_tac*) 

693 
fun best_tac cs = 

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

695 

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

697 

698 
fun slow_best_tac cs = 

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

700 

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

701 

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

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

704 

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

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

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

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

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

709 

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

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

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

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

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

714 

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

716 
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

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

719 

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

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

721 
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

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

723 
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

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

725 

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

726 
(*Searching to depth m.*) 
3537  727 
fun depth_tac cs m i state = 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

728 
SELECT_GOAL 
4651  729 
(appWrappers cs 
3204
c1653e2e146d
corrected depth_tac: no call for safe_step_tac if subgoal not present
oheimb
parents:
2868
diff
changeset

730 
(fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac 
c1653e2e146d
corrected depth_tac: no call for safe_step_tac if subgoal not present
oheimb
parents:
2868
diff
changeset

731 
(safe_step_tac cs i)) THEN_ELSE 
2630  732 
(DEPTH_SOLVE (depth_tac cs m i), 
733 
inst0_step_tac cs i APPEND 

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

734 
COND (K(m=0)) no_tac 
2630  735 
((instp_step_tac cs i APPEND dup_step_tac cs i) 
736 
THEN DEPTH_SOLVE (depth_tac cs (m1) i)))) 1) 

3537  737 
i state; 
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset

738 

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

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

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

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

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

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

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

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

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

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

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

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

752 

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

753 
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

754 

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

755 

1724  756 

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

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

758 

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

759 
(* init data kind claset *) 
1724  760 

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

761 
exception CSData of claset ref; 
1724  762 

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

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

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

765 

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

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

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

768 
ClasetData (ref (CSData (ref cs))); 
1724  769 

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

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

771 
ClasetData (ref (CSData (ref (merge_cs (cs1, cs2))))); 
1724  772 

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

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

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

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

777 

1724  778 

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

779 
(* access claset *) 
1724  780 

4380  781 
fun print_claset thy = Display.print_data thy clasetK; 
782 

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

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

784 
(case Sign.get_data sg clasetK of 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

785 
ClasetData (ref (CSData r)) => r 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

786 
 _ => sys_error "claset_ref_of_sg"); 
1807  787 

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

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

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

790 
val claset_of = claset_of_sg o sign_of; 
1800  791 

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

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

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

794 

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

795 
val claset = claset_of o Context.get_context; 
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset

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

797 

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

798 

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

799 
(* change claset *) 
1800  800 

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

801 
fun change_claset f x = claset_ref () := (f (claset (), x)); 
1724  802 

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

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

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

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

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

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

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

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

810 

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

811 

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

812 
(* tactics referring to the implicit claset *) 
1800  813 

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

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

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

816 
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

817 
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

818 
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

819 
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

820 
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

821 
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

822 
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

823 
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

824 
fun Deepen_tac m = deepen_tac (claset()) m; 
2066  825 

1800  826 

0  827 
end; 
828 
end; 