5824

1 
(* Title: Pure/Isar/method.ML


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen


4 


5 
Proof methods.


6 
*)


7 


8 
signature BASIC_METHOD =


9 
sig


10 
val print_methods: theory > unit


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


12 
end;


13 


14 
signature METHOD =


15 
sig


16 
include BASIC_METHOD

6775

17 
val multi_resolve: thm list > thm > thm Seq.seq

6500

18 
val FINISHED: tactic > tactic

6091

19 
val METHOD: (thm list > tactic) > Proof.method

5824

20 
val METHOD0: tactic > Proof.method


21 
val fail: Proof.method


22 
val succeed: Proof.method

6500

23 
val same_tac: thm list > int > tactic

6108

24 
val same: Proof.method

6981

25 
val assumption_tac: thm list > int > tactic

5824

26 
val assumption: Proof.method


27 
val forward_chain: thm list > thm list > thm Seq.seq

6091

28 
val rule_tac: thm list > thm list > int > tactic


29 
val rule: thm list > Proof.method

5916

30 
exception METHOD_FAIL of (string * Position.T) * exn

5824

31 
val method: theory > Args.src > Proof.context > Proof.method


32 
val add_methods: (bstring * (Args.src > Proof.context > Proof.method) * string) list


33 
> theory > theory

5884

34 
val syntax: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list)) >


35 
Proof.context > Args.src > Proof.context * 'a


36 
val no_args: Proof.method > Args.src > Proof.context > Proof.method


37 
val sectioned_args: ((Args.T list > Proof.context attribute * Args.T list) list >


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


39 
(Args.T list > Proof.context attribute * Args.T list) list >


40 
('a > Proof.context > Proof.method) > Args.src > Proof.context > Proof.method


41 
val default_sectioned_args: Proof.context attribute >


42 
(Args.T list > Proof.context attribute * Args.T list) list >


43 
(Proof.context > Proof.method) > Args.src > Proof.context > Proof.method


44 
val only_sectioned_args: (Args.T list > Proof.context attribute * Args.T list) list >


45 
(Proof.context > Proof.method) > Args.src > Proof.context > Proof.method

6091

46 
val thms_args: (thm list > Proof.method) > Args.src > Proof.context > Proof.method

5824

47 
datatype text =


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


49 
Source of Args.src 


50 
Then of text list 


51 
Orelse of text list 


52 
Try of text 


53 
Repeat of text 


54 
Repeat1 of text


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


56 
val tac: text > Proof.state > Proof.state Seq.seq

5884

57 
val then_tac: text > Proof.state > Proof.state Seq.seq

5824

58 
val proof: text option > Proof.state > Proof.state Seq.seq

6981

59 
val local_qed: text option


60 
> ({kind: string, name: string, thm: thm} > unit) * (thm > unit)

6736

61 
> Proof.state > Proof.state Seq.seq

6981

62 
val local_terminal_proof: text * text option


63 
> ({kind: string, name: string, thm: thm} > unit) * (thm > unit)

6736

64 
> Proof.state > Proof.state Seq.seq

6981

65 
val local_immediate_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit)


66 
> Proof.state > Proof.state Seq.seq


67 
val local_default_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit)

6736

68 
> Proof.state > Proof.state Seq.seq

6951

69 
val global_qed: text option > Proof.state > theory * {kind: string, name: string, thm: thm}

6934

70 
val global_terminal_proof: text * text option


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

6532

72 
val global_immediate_proof: Proof.state > theory * {kind: string, name: string, thm: thm}


73 
val global_default_proof: Proof.state > theory * {kind: string, name: string, thm: thm}

5824

74 
val setup: (theory > theory) list


75 
end;


76 


77 
structure Method: METHOD =


78 
struct


79 


80 

6500

81 
(** utils **)


82 


83 
val FINISHED = FILTER (equal 0 o Thm.nprems_of);


84 


85 


86 

5824

87 
(** proof methods **)


88 


89 
(* method from tactic *)


90 

6849

91 
val METHOD = Proof.method;

5824

92 
fun METHOD0 tac = METHOD (fn [] => tac  _ => error "Method may not be used with facts");


93 


94 


95 
(* primitive *)


96 


97 
val fail = METHOD (K no_tac);


98 
val succeed = METHOD (K all_tac);


99 


100 

6981

101 
(* same *)

5824

102 

6981

103 
fun cut_rule_tac raw_rule =


104 
let


105 
val rule = Drule.forall_intr_vars raw_rule;


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


107 
in Tactic.rtac (rule COMP revcut_rl) THEN' Tactic.rotate_tac ~1 end;


108 


109 
fun same_tac [] i = all_tac


110 
 same_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);

5824

111 

6108

112 
val same = METHOD (ALLGOALS o same_tac);

6981

113 

5824

114 

6981

115 
(* assumption *)


116 


117 
fun assumption_tac facts = same_tac facts THEN' assume_tac;


118 
val assumption = METHOD (FIRSTGOAL o assumption_tac);

6500

119 
val asm_finish = METHOD (K (FINISHED (ALLGOALS assume_tac)));

5824

120 


121 

6532

122 
(* fold / unfold definitions *)


123 


124 
val fold = METHOD0 o fold_goals_tac;


125 
val unfold = METHOD0 o rewrite_goals_tac;


126 


127 

5824

128 
(* rule *)


129 


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


131 


132 
fun multi_resolve facts rule =


133 
let


134 
fun multi_res i [] = Seq.single rule


135 
 multi_res i (th :: ths) = Seq.flat (Seq.map (res th i) (multi_res (i + 1) ths))


136 
in multi_res 1 facts end;


137 


138 
fun forward_chain facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));


139 

6091

140 
fun rule_tac rules [] = resolve_tac rules

5824

141 
 rule_tac erules facts =


142 
let

6091

143 
val rules = forward_chain facts erules;

5824

144 
fun tac i state = Seq.flat (Seq.map (fn rule => Tactic.rtac rule i state) rules);


145 
in tac end;


146 


147 
fun rule rules = METHOD (FIRSTGOAL o rule_tac rules);


148 


149 


150 


151 
(** methods theory data **)


152 


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


154 


155 
structure MethodsDataArgs =


156 
struct


157 
val name = "Isar/methods";


158 
type T =


159 
{space: NameSpace.T,


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


161 


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

6546

163 
val copy = I;

5824

164 
val prep_ext = I;


165 
fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) =


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


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


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


169 


170 
fun print _ {space, meths} =


171 
let


172 
fun prt_meth (name, ((_, comment), _)) = Pretty.block

6849

173 
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];

5824

174 
in


175 
Pretty.writeln (Display.pretty_name_space ("method name space", space));

6849

176 
Pretty.writeln (Pretty.big_list "methods:"


177 
(map prt_meth (NameSpace.cond_extern_table space meths)))

5824

178 
end;


179 
end;


180 


181 
structure MethodsData = TheoryDataFun(MethodsDataArgs);


182 
val print_methods = MethodsData.print;


183 


184 


185 
(* get methods *)


186 

5916

187 
exception METHOD_FAIL of (string * Position.T) * exn;


188 

5824

189 
fun method thy =


190 
let


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


192 

5884

193 
fun meth src =


194 
let


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


196 
val name = NameSpace.intern space raw_name;


197 
in

5824

198 
(case Symtab.lookup (meths, name) of


199 
None => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)

5916

200 
 Some ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src))

5824

201 
end;


202 
in meth end;


203 


204 


205 
(* add_methods *)


206 


207 
fun add_methods raw_meths thy =


208 
let


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


210 
val new_meths =


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


212 


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


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


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


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


217 
in


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


219 
end;


220 


221 
(*implicit version*)


222 
fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]);


223 


224 

5884

225 


226 
(** method syntax **)

5824

227 

5884

228 
(* basic *)


229 


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


231 
Args.syntax "method" scan;

5824

232 

5884

233 
fun no_args (x: Proof.method) src ctxt = #2 (syntax (Scan.succeed x) ctxt src);


234 


235 


236 
(* sections *)

5824

237 

5884

238 
fun sect ss = Scan.first (map (fn s => Scan.lift (s  Args.$$$ ":")) ss);


239 
fun thms ss = Scan.unless (sect ss) Attrib.local_thms;


240 
fun thmss ss = Scan.repeat (thms ss) >> flat;


241 

6091

242 
fun apply att (ctxt, ths) = Thm.applys_attributes ((ctxt, ths), [att]);

5824

243 

5884

244 
fun section ss = (sect ss  thmss ss) : (fn (att, ths) => Scan.depend (fn ctxt =>


245 
Scan.succeed (apply att (ctxt, ths)))) >> #2;


246 


247 
fun sectioned args ss = args ss  Scan.repeat (section ss);


248 

5824

249 

5884

250 
fun sectioned_args args ss f src ctxt =

5921

251 
let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src


252 
in f x ctxt' end;

5884

253 


254 
fun default_sectioned_args att ss f src ctxt =


255 
sectioned_args thmss ss (fn ths => fn ctxt' => f (#1 (apply att (ctxt', ths)))) src ctxt;


256 


257 
fun only_sectioned_args ss f = sectioned_args (K (Scan.succeed ())) ss (fn () => f);


258 
fun thms_args f = sectioned_args thmss [] (fn ths => fn _ => f ths);

5824

259 


260 


261 


262 
(** method text **)


263 


264 
(* datatype text *)


265 


266 
datatype text =


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


268 
Source of Args.src 


269 
Then of text list 


270 
Orelse of text list 


271 
Try of text 


272 
Repeat of text 


273 
Repeat1 of text;


274 


275 


276 
(* refine *)


277 


278 
fun refine text state =


279 
let


280 
val thy = Proof.theory_of state;


281 


282 
fun eval (Basic mth) = Proof.refine mth


283 
 eval (Source src) = Proof.refine (method thy src)


284 
 eval (Then txts) = Seq.EVERY (map eval txts)


285 
 eval (Orelse txts) = Seq.FIRST (map eval txts)


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


287 
 eval (Repeat txt) = Seq.REPEAT (eval txt)


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


289 
in eval text state end;


290 

6404

291 
fun named_method name = Source (Args.src ((name, []), Position.none));


292 

5824

293 


294 
(* unstructured steps *)


295 


296 
fun tac text state =


297 
state


298 
> Proof.goal_facts (K [])


299 
> refine text;


300 

5884

301 
fun then_tac text state =

5824

302 
state


303 
> Proof.goal_facts Proof.the_facts


304 
> refine text;


305 


306 

6404

307 
(* structured proof steps *)

5824

308 

6404

309 
val default_text = named_method "default";


310 
val finish_text = named_method "finish";

5824

311 

6872

312 

5824

313 
fun proof opt_text state =


314 
state


315 
> Proof.assert_backward

6404

316 
> refine (if_none opt_text default_text)

5824

317 
> Seq.map Proof.enter_forward;


318 

6404

319 
fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text));

6934

320 
fun local_terminal_proof (text, opt_text) pr = Seq.THEN (proof (Some text), local_qed opt_text pr);


321 
val local_immediate_proof = local_terminal_proof (Basic (K same), None);


322 
val local_default_proof = local_terminal_proof (default_text, None);

5824

323 

6872

324 

6951

325 
fun global_qeds opt_text = Proof.global_qed (refine (if_none opt_text finish_text));

5824

326 

6951

327 
fun global_qed opt_text state =

6872

328 
state

6951

329 
> global_qeds opt_text

6872

330 
> Proof.check_result "Failed to finish proof" state


331 
> Seq.hd;


332 

6934

333 
fun global_terminal_proof (text, opt_text) state =

6872

334 
state


335 
> proof (Some text)


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

6951

337 
> (Seq.flat o Seq.map (global_qeds opt_text))

6872

338 
> Proof.check_result "Failed to finish proof (after successful terminal method)" state


339 
> Seq.hd;


340 

6934

341 
val global_immediate_proof = global_terminal_proof (Basic (K same), None);


342 
val global_default_proof = global_terminal_proof (default_text, None);

5824

343 


344 


345 


346 
(** theory setup **)


347 


348 
(* pure_methods *)


349 


350 
val pure_methods =


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


352 
("succeed", no_args succeed, "succeed"),

6108

353 
("same", no_args same, "insert facts, nothing else"),

5824

354 
("assumption", no_args assumption, "proof by assumption"),


355 
("finish", no_args asm_finish, "finish proof by assumption"),

6532

356 
("fold", thms_args fold, "fold definitions"),


357 
("unfold", thms_args unfold, "unfold definitions"),

6849

358 
("rule", thms_args rule, "apply some rule")];

5824

359 


360 


361 
(* setup *)


362 


363 
val setup = [MethodsData.init, add_methods pure_methods];


364 


365 


366 
end;


367 


368 


369 
structure BasicMethod: BASIC_METHOD = Method;


370 
open BasicMethod;
