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

5824

25 
val assumption: Proof.method


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

6091

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


28 
val rule: thm list > Proof.method

5916

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

5824

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


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


32 
> theory > theory

5884

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


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


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


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


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


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


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


40 
val default_sectioned_args: Proof.context attribute >


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


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


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


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

6091

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

5824

46 
datatype text =


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


48 
Source of Args.src 


49 
Then of text list 


50 
Orelse of text list 


51 
Try of text 


52 
Repeat of text 


53 
Repeat1 of text


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


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

5884

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

5824

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

6736

58 
val local_qed: text option > ({kind: string, name: string, thm: thm} > unit)


59 
> Proof.state > Proof.state Seq.seq


60 
val local_terminal_proof: text > ({kind: string, name: string, thm: thm} > unit)


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


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


63 
> Proof.state > Proof.state Seq.seq


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


65 
> Proof.state > Proof.state Seq.seq

6404

66 
val global_qed: bstring option > theory attribute list option > text option

6532

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


68 
val global_terminal_proof: text > Proof.state > theory * {kind: string, name: string, thm: thm}


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


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

5824

71 
val setup: (theory > theory) list


72 
end;


73 


74 
structure Method: METHOD =


75 
struct


76 


77 

6500

78 
(** utils **)


79 


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


81 


82 


83 

5824

84 
(** proof methods **)


85 


86 
(* method from tactic *)


87 

6849

88 
val METHOD = Proof.method;

5824

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


90 


91 


92 
(* primitive *)


93 


94 
val fail = METHOD (K no_tac);


95 
val succeed = METHOD (K all_tac);


96 


97 

6108

98 
(* same, assumption *)

5824

99 

6108

100 
fun same_tac [] = K all_tac


101 
 same_tac facts =

6091

102 
let val r = ~ (length facts);


103 
in metacuts_tac facts THEN' rotate_tac r end;

5824

104 

6108

105 
val same = METHOD (ALLGOALS o same_tac);


106 
val assumption = METHOD (fn facts => FIRSTGOAL (same_tac facts THEN' assume_tac));

5824

107 

6500

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

5824

109 


110 

6532

111 
(* fold / unfold definitions *)


112 


113 
val fold = METHOD0 o fold_goals_tac;


114 
val unfold = METHOD0 o rewrite_goals_tac;


115 


116 

5824

117 
(* rule *)


118 


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


120 


121 
fun multi_resolve facts rule =


122 
let


123 
fun multi_res i [] = Seq.single rule


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


125 
in multi_res 1 facts end;


126 


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


128 

6091

129 
fun rule_tac rules [] = resolve_tac rules

5824

130 
 rule_tac erules facts =


131 
let

6091

132 
val rules = forward_chain facts erules;

5824

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


134 
in tac end;


135 


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


137 


138 


139 


140 
(** methods theory data **)


141 


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


143 


144 
structure MethodsDataArgs =


145 
struct


146 
val name = "Isar/methods";


147 
type T =


148 
{space: NameSpace.T,


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


150 


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

6546

152 
val copy = I;

5824

153 
val prep_ext = I;


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


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


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


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


158 


159 
fun print _ {space, meths} =


160 
let


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

6849

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

5824

163 
in


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

6849

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


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

5824

167 
end;


168 
end;


169 


170 
structure MethodsData = TheoryDataFun(MethodsDataArgs);


171 
val print_methods = MethodsData.print;


172 


173 


174 
(* get methods *)


175 

5916

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


177 

5824

178 
fun method thy =


179 
let


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


181 

5884

182 
fun meth src =


183 
let


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


185 
val name = NameSpace.intern space raw_name;


186 
in

5824

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


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

5916

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

5824

190 
end;


191 
in meth end;


192 


193 


194 
(* add_methods *)


195 


196 
fun add_methods raw_meths thy =


197 
let


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


199 
val new_meths =


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


201 


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


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


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


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


206 
in


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


208 
end;


209 


210 
(*implicit version*)


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


212 


213 

5884

214 


215 
(** method syntax **)

5824

216 

5884

217 
(* basic *)


218 


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


220 
Args.syntax "method" scan;

5824

221 

5884

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


223 


224 


225 
(* sections *)

5824

226 

5884

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


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


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


230 

6091

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

5824

232 

5884

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


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


235 


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


237 

5824

238 

5884

239 
fun sectioned_args args ss f src ctxt =

5921

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


241 
in f x ctxt' end;

5884

242 


243 
fun default_sectioned_args att ss f src ctxt =


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


245 


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


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

5824

248 


249 


250 


251 
(** method text **)


252 


253 
(* datatype text *)


254 


255 
datatype text =


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


257 
Source of Args.src 


258 
Then of text list 


259 
Orelse of text list 


260 
Try of text 


261 
Repeat of text 


262 
Repeat1 of text;


263 


264 


265 
(* refine *)


266 


267 
fun refine text state =


268 
let


269 
val thy = Proof.theory_of state;


270 


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


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


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


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


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


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


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


278 
in eval text state end;


279 

6404

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


281 

5824

282 


283 
(* unstructured steps *)


284 


285 
fun tac text state =


286 
state


287 
> Proof.goal_facts (K [])


288 
> refine text;


289 

5884

290 
fun then_tac text state =

5824

291 
state


292 
> Proof.goal_facts Proof.the_facts


293 
> refine text;


294 


295 

6404

296 
(* structured proof steps *)

5824

297 

6404

298 
val default_text = named_method "default";


299 
val finish_text = named_method "finish";

5824

300 

6872

301 

5824

302 
fun proof opt_text state =


303 
state


304 
> Proof.assert_backward

6404

305 
> refine (if_none opt_text default_text)

5824

306 
> Seq.map Proof.enter_forward;


307 

6404

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

6736

309 
fun local_terminal_proof text pr = Seq.THEN (proof (Some text), local_qed None pr);

6404

310 
val local_immediate_proof = local_terminal_proof (Basic (K same));


311 
val local_default_proof = local_terminal_proof default_text;

5824

312 

6872

313 


314 
fun global_qeds alt_name alt_atts opt_text =

6404

315 
Proof.global_qed (refine (if_none opt_text finish_text)) alt_name alt_atts;

5824

316 

6872

317 
fun global_qed alt_name alt_atts opt_text state =


318 
state


319 
> global_qeds alt_name alt_atts opt_text


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


321 
> Seq.hd;


322 


323 
fun global_terminal_proof text state =


324 
state


325 
> proof (Some text)


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


327 
> (Seq.flat o Seq.map (global_qeds None None None))


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


329 
> Seq.hd;


330 

6404

331 
val global_immediate_proof = global_terminal_proof (Basic (K same));


332 
val global_default_proof = global_terminal_proof default_text;

5824

333 


334 


335 


336 
(** theory setup **)


337 


338 
(* pure_methods *)


339 


340 
val pure_methods =


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


342 
("succeed", no_args succeed, "succeed"),

6108

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

5824

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


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

6532

346 
("fold", thms_args fold, "fold definitions"),


347 
("unfold", thms_args unfold, "unfold definitions"),

6849

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

5824

349 


350 


351 
(* setup *)


352 


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


354 


355 


356 
end;


357 


358 


359 
structure BasicMethod: BASIC_METHOD = Method;


360 
open BasicMethod;
