author  wenzelm 
Mon, 06 Nov 2000 22:52:35 +0100  
changeset 10405  9a23abbc81fa 
parent 10378  98c95ebf804f 
child 10417  42e6b8502d52 
permissions  rwrr 
5824  1 
(* Title: Pure/Isar/method.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

8807  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5824  5 

6 
Proof methods. 

7 
*) 

8 

9 
signature BASIC_METHOD = 

10 
sig 

11 
val print_methods: theory > unit 

12 
val Method: bstring > (Args.src > Proof.context > Proof.method) > string > unit 

13 
end; 

14 

15 
signature METHOD = 

16 
sig 

17 
include BASIC_METHOD 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

18 
val print_global_rules: theory > unit 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

19 
val print_local_rules: Proof.context > unit 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

20 
val dest_global: theory attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

21 
val elim_global: theory attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

22 
val intro_global: theory attribute 
9938  23 
val rule_del_global: theory attribute 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

24 
val dest_local: Proof.context attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

25 
val elim_local: Proof.context attribute 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

26 
val intro_local: Proof.context attribute 
9938  27 
val rule_del_local: Proof.context attribute 
6091  28 
val METHOD: (thm list > tactic) > Proof.method 
8372  29 
val METHOD_CASES: 
30 
(thm list > thm > (thm * (string * RuleCases.T) list) Seq.seq) > Proof.method 

9706  31 
val SIMPLE_METHOD: tactic > Proof.method 
32 
val SIMPLE_METHOD': ((int > tactic) > tactic) > (int > tactic) > Proof.method 

5824  33 
val fail: Proof.method 
34 
val succeed: Proof.method 

8167  35 
val defer: int option > Proof.method 
36 
val prefer: int > Proof.method 

7419  37 
val insert_tac: thm list > int > tactic 
7574  38 
val insert: thm list > Proof.method 
7555  39 
val insert_facts: Proof.method 
7601  40 
val unfold: thm list > Proof.method 
7419  41 
val fold: thm list > Proof.method 
10405  42 
val rewrite_goal_tac: thm list > int > tactic 
9484  43 
val atomize_tac: thm list > int > tactic 
9485  44 
val atomize_goal: thm list > int > thm > thm 
7419  45 
val multi_resolve: thm list > thm > thm Seq.seq 
46 
val multi_resolves: thm list > thm list > thm Seq.seq 

8335  47 
val resolveq_tac: thm Seq.seq > int > tactic 
10405  48 
val resolveq_cases_tac: (thm > string list > (string * RuleCases.T) list) 
49 
> (thm * string list) Seq.seq > int > thm > (thm * (string * RuleCases.T) list) Seq.seq 

6091  50 
val rule_tac: thm list > thm list > int > tactic 
9587  51 
val erule_tac: thm list > thm list > int > tactic 
10309  52 
val some_rule_tac: thm list > Proof.context > thm list > int > tactic 
6091  53 
val rule: thm list > Proof.method 
7130  54 
val erule: thm list > Proof.method 
8220  55 
val drule: thm list > Proof.method 
56 
val frule: thm list > Proof.method 

8195  57 
val this: Proof.method 
7555  58 
val assumption: Proof.context > Proof.method 
8351  59 
val set_tactic: (Proof.context > thm list > tactic) > unit 
60 
val tactic: string > Proof.context > Proof.method 

5916  61 
exception METHOD_FAIL of (string * Position.T) * exn 
5824  62 
val method: theory > Args.src > Proof.context > Proof.method 
9539  63 
val add_method: bstring * (Args.src > Proof.context > Proof.method) * string 
64 
> theory > theory 

5824  65 
val add_methods: (bstring * (Args.src > Proof.context > Proof.method) * string) list 
66 
> theory > theory 

5884  67 
val syntax: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list)) > 
8282  68 
Args.src > Proof.context > Proof.context * 'a 
8351  69 
val simple_args: (Args.T list > 'a * Args.T list) 
70 
> ('a > Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 

7555  71 
val ctxt_args: (Proof.context > Proof.method) > Args.src > Proof.context > Proof.method 
5884  72 
val no_args: Proof.method > Args.src > Proof.context > Proof.method 
7268  73 
type modifier 
7601  74 
val sectioned_args: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list)) > 
7268  75 
(Args.T list > modifier * Args.T list) list > 
9864  76 
('a > Proof.context > 'b) > Args.src > Proof.context > 'b 
7601  77 
val bang_sectioned_args: 
78 
(Args.T list > modifier * Args.T list) list > 

9864  79 
(thm list > Proof.context > 'a) > Args.src > Proof.context > 'a 
9777  80 
val bang_sectioned_args': 
81 
(Args.T list > modifier * Args.T list) list > 

82 
(Proof.context * Args.T list > 'a * (Proof.context * Args.T list)) > 

9864  83 
('a > thm list > Proof.context > 'b) > Args.src > Proof.context > 'b 
7601  84 
val only_sectioned_args: 
85 
(Args.T list > modifier * Args.T list) list > 

9864  86 
(Proof.context > 'a) > Args.src > Proof.context > 'a 
87 
val thms_ctxt_args: (thm list > Proof.context > 'a) > Args.src > Proof.context > 'a 

88 
val thms_args: (thm list > 'a) > Args.src > Proof.context > 'a 

89 
val thm_args: (thm > 'a) > Args.src > Proof.context > 'a 

5824  90 
datatype text = 
91 
Basic of (Proof.context > Proof.method)  

92 
Source of Args.src  

93 
Then of text list  

94 
Orelse of text list  

95 
Try of text  

96 
Repeat1 of text 

97 
val refine: text > Proof.state > Proof.state Seq.seq 

8238  98 
val refine_end: text > Proof.state > Proof.state Seq.seq 
5824  99 
val proof: text option > Proof.state > Proof.state Seq.seq 
8966  100 
val local_qed: bool > text option 
6981  101 
> ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 
6736  102 
> Proof.state > Proof.state Seq.seq 
6981  103 
val local_terminal_proof: text * text option 
104 
> ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 

6736  105 
> Proof.state > Proof.state Seq.seq 
6981  106 
val local_default_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 
6736  107 
> Proof.state > Proof.state Seq.seq 
8966  108 
val local_immediate_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 
109 
> Proof.state > Proof.state Seq.seq 

110 
val local_done_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 

111 
> Proof.state > Proof.state Seq.seq 

112 
val global_qed: bool > text option 

113 
> Proof.state > theory * {kind: string, name: string, thm: thm} 

6934  114 
val global_terminal_proof: text * text option 
115 
> Proof.state > theory * {kind: string, name: string, thm: thm} 

8966  116 
val global_default_proof: Proof.state > theory * {kind: string, name: string, thm: thm} 
6532  117 
val global_immediate_proof: Proof.state > theory * {kind: string, name: string, thm: thm} 
8966  118 
val global_done_proof: Proof.state > theory * {kind: string, name: string, thm: thm} 
9539  119 
val goal_args: (Args.T list > 'a * Args.T list) > ('a > int > tactic) 
120 
> Args.src > Proof.context > Proof.method 

121 
val goal_args': (Proof.context * Args.T list > 'a * (Proof.context * Args.T list)) 

122 
> ('a > int > tactic) > Args.src > Proof.context > Proof.method 

5824  123 
val setup: (theory > theory) list 
124 
end; 

125 

126 
structure Method: METHOD = 

127 
struct 

128 

129 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

130 
(** global and local rule data **) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

131 

10008  132 
local 
133 
fun prt_rules kind sg ths = 

134 
Pretty.writeln (Pretty.big_list ("standard " ^ kind ^ " rules:") 

135 
(map (Display.pretty_thm_sg sg) ths)); 

136 
in 

137 
fun print_rules sg (intro, elim) = 

138 
(prt_rules "introduction" sg intro; prt_rules "elimination" sg elim); 

139 
end; 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

140 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

141 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

142 
(* theory data kind 'Isar/rules' *) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

143 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

144 
structure GlobalRulesArgs = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

145 
struct 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

146 
val name = "Isar/rules"; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

147 
type T = thm list * thm list; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

148 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

149 
val empty = ([], []); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

150 
val copy = I; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

151 
val prep_ext = I; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

152 
fun merge ((intro1, elim1), (intro2, elim2)) = 
9418  153 
(Drule.merge_rules (intro1, intro2), Drule.merge_rules (elim1, elim2)); 
10008  154 
val print = print_rules; 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

155 
end; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

156 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

157 
structure GlobalRules = TheoryDataFun(GlobalRulesArgs); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

158 
val print_global_rules = GlobalRules.print; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

159 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

160 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

161 
(* proof data kind 'Isar/rules' *) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

162 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

163 
structure LocalRulesArgs = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

164 
struct 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

165 
val name = "Isar/rules"; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

166 
type T = thm list * thm list; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

167 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

168 
val init = GlobalRules.get; 
10008  169 
val print = print_rules o ProofContext.sign_of; 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

170 
end; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

171 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

172 
structure LocalRules = ProofDataFun(LocalRulesArgs); 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

173 
val print_local_rules = LocalRules.print; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

174 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

175 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

176 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

177 
(** attributes **) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

178 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

179 
(* add rules *) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

180 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

181 
local 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

182 

9938  183 
fun add_dest th (intro, elim) = (intro, Drule.add_rules [Tactic.make_elim th] elim); 
184 
fun add_elim th (intro, elim) = (intro, Drule.add_rules [th] elim); 

185 
fun add_intro th (intro, elim) = (Drule.add_rules [th] intro, elim); 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

186 

9938  187 
fun del_rule th (intro, elim) = 
188 
let 

189 
val th' = Tactic.make_elim th; 

190 
val del = Drule.del_rules [th'] o Drule.del_rules [th]; 

191 
in (del intro, del elim) end; 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

192 

9938  193 
fun mk_att f g (x, th) = (f (g th) x, th); 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

194 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

195 
in 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

196 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

197 
val dest_global = mk_att GlobalRules.map add_dest; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

198 
val elim_global = mk_att GlobalRules.map add_elim; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

199 
val intro_global = mk_att GlobalRules.map add_intro; 
9938  200 
val rule_del_global = mk_att GlobalRules.map del_rule; 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

201 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

202 
val dest_local = mk_att LocalRules.map add_dest; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

203 
val elim_local = mk_att LocalRules.map add_elim; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

204 
val intro_local = mk_att LocalRules.map add_intro; 
9938  205 
val rule_del_local = mk_att LocalRules.map del_rule; 
206 

10034  207 
fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att); 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

208 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

209 
end; 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

210 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

211 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

212 
(* concrete syntax *) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

213 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

214 
val rule_atts = 
9900  215 
[("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local), 
216 
"declaration of destruction rule"), 

217 
("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local), 

218 
"declaration of elimination rule"), 

219 
("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), 

220 
"declaration of introduction rule"), 

9938  221 
("rule", (del_args rule_del_global, del_args rule_del_local), 
9900  222 
"remove declaration of elim/intro rule")]; 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

223 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

224 

9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

225 

5824  226 
(** proof methods **) 
227 

8372  228 
(* make methods *) 
5824  229 

6849  230 
val METHOD = Proof.method; 
8372  231 
val METHOD_CASES = Proof.method_cases; 
232 

5824  233 

234 
(* primitive *) 

235 

236 
val fail = METHOD (K no_tac); 

237 
val succeed = METHOD (K all_tac); 

238 

239 

8167  240 
(* shuffle *) 
241 

8240  242 
fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1))); 
8167  243 
fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1))); 
244 

245 

7419  246 
(* insert *) 
247 

248 
local 

5824  249 

6981  250 
fun cut_rule_tac raw_rule = 
251 
let 

252 
val rule = Drule.forall_intr_vars raw_rule; 

253 
val revcut_rl = Drule.incr_indexes_wrt [] [] [] [rule] Drule.revcut_rl; 

7555  254 
in Tactic.rtac (rule COMP revcut_rl) end; 
6981  255 

7419  256 
in 
5824  257 

7419  258 
fun insert_tac [] i = all_tac 
259 
 insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); 

6981  260 

7555  261 
val insert_facts = METHOD (ALLGOALS o insert_tac); 
7664  262 
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); 
7419  263 

264 
end; 

5824  265 

266 

9706  267 
(* simple methods *) 
268 

269 
fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac); 

270 
fun SIMPLE_METHOD' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac)); 

271 

272 

7601  273 
(* unfold / fold definitions *) 
6532  274 

9706  275 
fun unfold thms = SIMPLE_METHOD (CHANGED (rewrite_goals_tac thms)); 
276 
fun fold thms = SIMPLE_METHOD (CHANGED (fold_goals_tac thms)); 

9484  277 

278 

279 
(* atomize metaconnectives *) 

280 

10405  281 
fun rewrite_goal_tac rews = 
282 
Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of rews); 

9485  283 

10405  284 
fun atomize_tac rews = 
285 
let val rew_tac = rewrite_goal_tac rews in 

286 
fn i => fn thm => 

287 
if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then rew_tac i thm 

288 
else all_tac thm 

289 
end; 

290 

291 
fun atomize_goal rews = 

292 
let val tac = atomize_tac rews 

293 
in fn i => fn thm => (case Seq.pull (tac i thm) of None => thm  Some (thm', _) => thm') end; 

6532  294 

295 

7419  296 
(* multi_resolve *) 
297 

298 
local 

299 

300 
fun res th i rule = 

301 
Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty; 

302 

303 
fun multi_res _ [] rule = Seq.single rule 

304 
 multi_res i (th :: ths) rule = Seq.flat (Seq.map (res th i) (multi_res (i + 1) ths rule)); 

305 

306 
in 

307 

308 
val multi_resolve = multi_res 1; 

8372  309 
fun multi_resolves facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules)); 
7419  310 

311 
end; 

312 

313 

8372  314 
(* general rule *) 
5824  315 

8335  316 
fun gen_resolveq_tac tac rules i st = 
8372  317 
Seq.flat (Seq.map (fn rule => tac rule i st) rules); 
318 

319 
val resolveq_tac = gen_resolveq_tac Tactic.rtac; 

8335  320 

10405  321 
fun resolveq_cases_tac make = gen_resolveq_tac (fn (rule, cases) => fn i => fn st => 
322 
Seq.map (rpair (make rule cases)) (Tactic.rtac rule i st)); 

8335  323 

324 

8372  325 
(* simple rule *) 
326 

7419  327 
local 
5824  328 

7130  329 
fun gen_rule_tac tac rules [] = tac rules 
8372  330 
 gen_rule_tac tac erules facts = gen_resolveq_tac (tac o single) (multi_resolves facts erules); 
7130  331 

10309  332 
fun gen_some_rule_tac tac arg_rules ctxt facts = 
8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

333 
let val rules = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

334 
if not (null arg_rules) then arg_rules 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

335 
else if null facts then #1 (LocalRules.get ctxt) 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

336 
else op @ (LocalRules.get ctxt); 
10309  337 
in tac rules facts end; 
338 

339 
fun gen_rule tac rules = METHOD (HEADGOAL o tac rules); 

340 
fun gen_rule' tac arg_rules ctxt = METHOD (HEADGOAL o gen_some_rule_tac tac arg_rules ctxt); 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

341 

8220  342 
fun setup raw_tac = 
343 
let val tac = gen_rule_tac raw_tac 

344 
in (tac, gen_rule tac, gen_rule' tac) end; 

345 

7419  346 
in 
347 

10309  348 
val some_rule_tac = gen_some_rule_tac (gen_rule_tac Tactic.resolve_tac); 
8220  349 
val (rule_tac, rule, some_rule) = setup Tactic.resolve_tac; 
350 
val (erule_tac, erule, some_erule) = setup Tactic.eresolve_tac; 

351 
val (drule_tac, drule, some_drule) = setup Tactic.dresolve_tac; 

352 
val (frule_tac, frule, some_frule) = setup Tactic.forward_tac; 

5824  353 

7419  354 
end; 
355 

356 

8195  357 
(* this *) 
358 

8671  359 
val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac)); 
8195  360 

361 

362 
(* assumption *) 

7555  363 

10378
98c95ebf804f
assumption / finish: handle nonatomic assumptions from context as well;
wenzelm
parents:
10309
diff
changeset

364 
fun asm_tac ths = 
98c95ebf804f
assumption / finish: handle nonatomic assumptions from context as well;
wenzelm
parents:
10309
diff
changeset

365 
foldr (op APPEND') (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths, K no_tac); 
98c95ebf804f
assumption / finish: handle nonatomic assumptions from context as well;
wenzelm
parents:
10309
diff
changeset

366 

10405  367 
fun assm_tac ctxt = 
368 
assume_tac APPEND' 

369 
asm_tac (ProofContext.prems_of ctxt) APPEND' 

370 
Tactic.rtac Drule.reflexive_thm; 

7419  371 

7555  372 
fun assumption_tac ctxt [] = assm_tac ctxt 
10378
98c95ebf804f
assumption / finish: handle nonatomic assumptions from context as well;
wenzelm
parents:
10309
diff
changeset

373 
 assumption_tac _ [fact] = asm_tac [fact] 
7555  374 
 assumption_tac _ _ = K no_tac; 
7419  375 

8671  376 
fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt); 
7419  377 

378 

9539  379 
(* res_inst_tac etc. *) 
8238  380 

9539  381 
(*Note: insts refer to the implicit (!!) goal context; use at your own risk*) 
9565
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

382 
fun gen_res_inst _ tac (quant, ([], thms)) = 
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

383 
METHOD (fn facts => (quant (insert_tac facts THEN' tac thms))) 
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

384 
 gen_res_inst tac _ (quant, (insts, [thm])) = 
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

385 
METHOD (fn facts => (quant (insert_tac facts THEN' tac insts thm))) 
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

386 
 gen_res_inst _ _ _ = error "Cannot have instantiations with multiple rules"; 
8238  387 

9565
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

388 
val res_inst = gen_res_inst Tactic.res_inst_tac Tactic.resolve_tac; 
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

389 
val eres_inst = gen_res_inst Tactic.eres_inst_tac Tactic.eresolve_tac; 
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

390 
val dres_inst = gen_res_inst Tactic.dres_inst_tac Tactic.dresolve_tac; 
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

391 
val forw_inst = gen_res_inst Tactic.forw_inst_tac Tactic.forward_tac; 
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

392 
val cut_inst = gen_res_inst Tactic.cut_inst_tac Tactic.cut_facts_tac; 
8238  393 

394 

8329  395 
(* simple Prolog interpreter *) 
396 

397 
fun prolog_tac rules facts = 

398 
DEPTH_SOLVE_1 (HEADGOAL (Tactic.assume_tac APPEND' Tactic.resolve_tac (facts @ rules))); 

399 

400 
val prolog = METHOD o prolog_tac; 

401 

402 

8351  403 
(* ML tactics *) 
404 

405 
val tactic_ref = ref ((fn _ => raise Match): Proof.context > thm list > tactic); 

406 
fun set_tactic f = tactic_ref := f; 

407 

408 
fun tactic txt ctxt = METHOD (fn facts => 

9631  409 
(Context.use_mltext 
410 
("let fun tactic (ctxt: PureIsar.Proof.context) (facts: thm list) : tactic = \ 

411 
\let val thm = PureIsar.ProofContext.get_thm_closure ctxt\n\ 

412 
\ and thms = PureIsar.ProofContext.get_thms_closure ctxt in\n" 

413 
^ txt ^ 

414 
"\nend in PureIsar.Method.set_tactic tactic end") 

415 
false None; 

416 
Context.setmp (Some (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts)); 

8351  417 

418 

5824  419 

420 
(** methods theory data **) 

421 

422 
(* data kind 'Isar/methods' *) 

423 

424 
structure MethodsDataArgs = 

425 
struct 

426 
val name = "Isar/methods"; 

427 
type T = 

428 
{space: NameSpace.T, 

429 
meths: (((Args.src > Proof.context > Proof.method) * string) * stamp) Symtab.table}; 

430 

431 
val empty = {space = NameSpace.empty, meths = Symtab.empty}; 

6546  432 
val copy = I; 
5824  433 
val prep_ext = I; 
434 
fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) = 

435 
{space = NameSpace.merge (space1, space2), 

436 
meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups => 

437 
error ("Attempt to merge different versions of methods " ^ commas_quote dups)}; 

438 

9222  439 
fun print _ {space, meths} = 
5824  440 
let 
441 
fun prt_meth (name, ((_, comment), _)) = Pretty.block 

6849  442 
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; 
5824  443 
in 
8720  444 
[Pretty.big_list "methods:" (map prt_meth (NameSpace.cond_extern_table space meths))] 
9222  445 
> Pretty.chunks > Pretty.writeln 
5824  446 
end; 
447 
end; 

448 

449 
structure MethodsData = TheoryDataFun(MethodsDataArgs); 

450 
val print_methods = MethodsData.print; 

7611  451 

5824  452 

453 
(* get methods *) 

454 

5916  455 
exception METHOD_FAIL of (string * Position.T) * exn; 
456 

5824  457 
fun method thy = 
458 
let 

459 
val {space, meths} = MethodsData.get thy; 

460 

5884  461 
fun meth src = 
462 
let 

463 
val ((raw_name, _), pos) = Args.dest_src src; 

464 
val name = NameSpace.intern space raw_name; 

465 
in 

5824  466 
(case Symtab.lookup (meths, name) of 
467 
None => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos) 

5916  468 
 Some ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src)) 
5824  469 
end; 
470 
in meth end; 

471 

472 

9194  473 
(* add_method(s) *) 
5824  474 

475 
fun add_methods raw_meths thy = 

476 
let 

477 
val full = Sign.full_name (Theory.sign_of thy); 

478 
val new_meths = 

479 
map (fn (name, f, comment) => (full name, ((f, comment), stamp ()))) raw_meths; 

480 

481 
val {space, meths} = MethodsData.get thy; 

482 
val space' = NameSpace.extend (space, map fst new_meths); 

483 
val meths' = Symtab.extend (meths, new_meths) handle Symtab.DUPS dups => 

484 
error ("Duplicate declaration of method(s) " ^ commas_quote dups); 

485 
in 

486 
thy > MethodsData.put {space = space', meths = meths'} 

487 
end; 

488 

9194  489 
val add_method = add_methods o Library.single; 
490 

5824  491 
(*implicit version*) 
492 
fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]); 

493 

494 

5884  495 

496 
(** method syntax **) 

5824  497 

5884  498 
(* basic *) 
499 

500 
fun syntax (scan: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list))) = 

501 
Args.syntax "method" scan; 

5824  502 

8351  503 
fun simple_args scan f src ctxt : Proof.method = 
504 
#2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt); 

505 

7555  506 
fun ctxt_args (f: Proof.context > Proof.method) src ctxt = 
8282  507 
#2 (syntax (Scan.succeed (f ctxt)) src ctxt); 
7555  508 

509 
fun no_args m = ctxt_args (K m); 

5884  510 

511 

8351  512 

5884  513 
(* sections *) 
5824  514 

7268  515 
type modifier = (Proof.context > Proof.context) * Proof.context attribute; 
516 

517 
local 

518 

8381  519 
fun sect ss = Scan.first (map Scan.lift ss); 
5884  520 
fun thms ss = Scan.unless (sect ss) Attrib.local_thms; 
521 
fun thmss ss = Scan.repeat (thms ss) >> flat; 

522 

7268  523 
fun apply (f, att) (ctxt, ths) = Thm.applys_attributes ((f ctxt, ths), [att]); 
5824  524 

7268  525 
fun section ss = (sect ss  thmss ss) : (fn (m, ths) => Scan.depend (fn ctxt => 
526 
Scan.succeed (apply m (ctxt, ths)))) >> #2; 

5884  527 

7601  528 
fun sectioned args ss = args  Scan.repeat (section ss); 
5884  529 

7268  530 
in 
5824  531 

5884  532 
fun sectioned_args args ss f src ctxt = 
8282  533 
let val (ctxt', (x, _)) = syntax (sectioned args ss) src ctxt 
5921  534 
in f x ctxt' end; 
5884  535 

7601  536 
fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f; 
9777  537 
fun bang_sectioned_args' ss scan f = 
538 
sectioned_args (Args.bang_facts  scan >> swap) ss (uncurry f); 

7601  539 
fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f); 
7268  540 

8093  541 
fun thms_ctxt_args f = sectioned_args (thmss []) [] f; 
542 
fun thms_args f = thms_ctxt_args (K o f); 

9706  543 
fun thm_args f = thms_args (fn [thm] => f thm  _ => error "Single theorem expected"); 
5824  544 

7268  545 
end; 
546 

5824  547 

9539  548 
(* tactic syntax *) 
8238  549 

550 
val insts = 

9539  551 
Scan.optional 
9565
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

552 
(Args.enum1 "and" (Scan.lift (Args.name  (Args.$$$ "="  Args.!!! Args.name)))  
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

553 
Scan.lift (Args.$$$ "in")) []  Attrib.local_thmss; 
8238  554 

8537  555 
fun inst_args f = f oo (#2 oo syntax (Args.goal_spec HEADGOAL  insts)); 
556 

557 

9539  558 
fun goal_args' args tac = #2 oo syntax (Args.goal_spec HEADGOAL  args >> 
9706  559 
(fn (quant, s) => SIMPLE_METHOD' quant (tac s))); 
8537  560 

9539  561 
fun goal_args args tac = goal_args' (Scan.lift args) tac; 
8238  562 

563 

5824  564 

565 
(** method text **) 

566 

567 
(* datatype text *) 

568 

569 
datatype text = 

570 
Basic of (Proof.context > Proof.method)  

571 
Source of Args.src  

572 
Then of text list  

573 
Orelse of text list  

574 
Try of text  

575 
Repeat1 of text; 

576 

577 

578 
(* refine *) 

579 

8238  580 
fun gen_refine f text state = 
5824  581 
let 
582 
val thy = Proof.theory_of state; 

583 

8238  584 
fun eval (Basic mth) = f mth 
585 
 eval (Source src) = f (method thy src) 

5824  586 
 eval (Then txts) = Seq.EVERY (map eval txts) 
587 
 eval (Orelse txts) = Seq.FIRST (map eval txts) 

588 
 eval (Try txt) = Seq.TRY (eval txt) 

589 
 eval (Repeat1 txt) = Seq.REPEAT1 (eval txt); 

590 
in eval text state end; 

591 

8238  592 
val refine = gen_refine Proof.refine; 
593 
val refine_end = gen_refine Proof.refine_end; 

6404  594 

5824  595 

6404  596 
(* structured proof steps *) 
5824  597 

7506  598 
val default_text = Source (Args.src (("default", []), Position.none)); 
8195  599 
val this_text = Basic (K this); 
9706  600 
val done_text = Basic (K (SIMPLE_METHOD all_tac)); 
7555  601 

8966  602 
fun close_text asm = Basic (fn ctxt => METHOD (K 
603 
(FILTER Thm.no_prems ((if asm then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac)))); 

604 

605 
fun finish_text asm None = close_text asm 

606 
 finish_text asm (Some txt) = Then [txt, close_text asm]; 

6872  607 

5824  608 
fun proof opt_text state = 
609 
state 

610 
> Proof.assert_backward 

6404  611 
> refine (if_none opt_text default_text) 
8242  612 
> Seq.map (Proof.goal_facts (K [])) 
5824  613 
> Seq.map Proof.enter_forward; 
614 

8966  615 
fun local_qed asm opt_text = Proof.local_qed (refine (finish_text asm opt_text)); 
616 
fun local_terminal_proof (text, opt_text) pr = 

617 
Seq.THEN (proof (Some text), local_qed true opt_text pr); 

618 
val local_default_proof = local_terminal_proof (default_text, None); 

8195  619 
val local_immediate_proof = local_terminal_proof (this_text, None); 
8966  620 
fun local_done_proof pr = Seq.THEN (proof (Some done_text), local_qed false None pr); 
5824  621 

6872  622 

8966  623 
fun global_qeds asm opt_text = Proof.global_qed (refine (finish_text asm opt_text)); 
5824  624 

8966  625 
fun global_qed asm opt_text state = 
6872  626 
state 
8966  627 
> global_qeds asm opt_text 
6872  628 
> Proof.check_result "Failed to finish proof" state 
629 
> Seq.hd; 

630 

8966  631 
fun global_term_proof asm (text, opt_text) state = 
6872  632 
state 
633 
> proof (Some text) 

634 
> Proof.check_result "Terminal proof method failed" state 

8966  635 
> (Seq.flat o Seq.map (global_qeds asm opt_text)) 
6872  636 
> Proof.check_result "Failed to finish proof (after successful terminal method)" state 
637 
> Seq.hd; 

638 

8966  639 
val global_terminal_proof = global_term_proof true; 
6934  640 
val global_default_proof = global_terminal_proof (default_text, None); 
8966  641 
val global_immediate_proof = global_terminal_proof (this_text, None); 
642 
val global_done_proof = global_term_proof false (done_text, None); 

5824  643 

644 

645 
(** theory setup **) 

646 

9539  647 
(* misc tactic emulations *) 
648 

649 
val subgoal_meth = goal_args (Scan.repeat1 Args.name) Tactic.subgoals_tac; 

650 
val thin_meth = goal_args Args.name Tactic.thin_tac; 

651 
val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac; 

9631  652 
val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac; 
9539  653 

654 

5824  655 
(* pure_methods *) 
656 

657 
val pure_methods = 

658 
[("fail", no_args fail, "force failure"), 

659 
("succeed", no_args succeed, "succeed"), 

9587  660 
("", no_args insert_facts, "do nothing (insert current facts only)"), 
9539  661 
("insert", thms_args insert, "insert theorems, ignoring facts (improper)"), 
7601  662 
("unfold", thms_args unfold, "unfold definitions"), 
663 
("fold", thms_args fold, "fold definitions"), 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

664 
("rule", thms_ctxt_args some_rule, "apply some rule"), 
9539  665 
("erule", thms_ctxt_args some_erule, "apply some rule in elimination manner (improper)"), 
666 
("drule", thms_ctxt_args some_drule, "apply some rule in destruct manner (improper)"), 

667 
("frule", thms_ctxt_args some_frule, "apply some rule in forward manner (improper)"), 

8195  668 
("this", no_args this, "apply current facts as rules"), 
8238  669 
("assumption", ctxt_args assumption, "proof by assumption, preferring facts"), 
9539  670 
("rule_tac", inst_args res_inst, "apply rule (dynamic instantiation!)"), 
671 
("erule_tac", inst_args eres_inst, "apply rule in elimination manner (dynamic instantiation!)"), 

672 
("drule_tac", inst_args dres_inst, "apply rule in destruct manner (dynamic instantiation!)"), 

673 
("frule_tac", inst_args forw_inst, "apply rule in forward manner (dynamic instantiation!)"), 

674 
("cut_tac", inst_args cut_inst, "cut rule (dynamic instantiation!)"), 

9565
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

675 
("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation!)"), 
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

676 
("thin_tac", thin_meth, "remove premise (dynamic instantiation!)"), 
9631  677 
("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation!)"), 
678 
("rotate_tac", rotate_meth, "rotate assumptions of goal"), 

8351  679 
("prolog", thms_args prolog, "simple prolog interpreter"), 
680 
("tactic", simple_args Args.name tactic, "ML tactic as proof method")]; 

5824  681 

682 

683 
(* setup *) 

684 

8153
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

685 
val setup = 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

686 
[GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts, 
9bdbcb71dc56
maintain standard rules (beware: classical provers provides another version!);
wenzelm
parents:
8093
diff
changeset

687 
MethodsData.init, add_methods pure_methods]; 
5824  688 

689 

690 
end; 

691 

692 

693 
structure BasicMethod: BASIC_METHOD = Method; 

694 
open BasicMethod; 