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


17 
val LIFT: tactic > thm > (thm * (indexname * term) list * (string * tthm list) list) Seq.seq


18 
val METHOD: (tthm list > tactic) > Proof.method


19 
val METHOD0: tactic > Proof.method


20 
val fail: Proof.method


21 
val succeed: Proof.method


22 
val trivial: Proof.method


23 
val assumption: Proof.method


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


25 
val rule_tac: tthm list > tthm list > int > tactic


26 
val rule: tthm list > Proof.method

5916

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

5824

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


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


30 
> theory > theory

5884

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


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


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


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


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


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


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


38 
val default_sectioned_args: Proof.context attribute >


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


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


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


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


43 
val thms_args: (tthm list > Proof.method) > Args.src > Proof.context > Proof.method

5824

44 
datatype text =


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


46 
Source of Args.src 


47 
Then of text list 


48 
Orelse of text list 


49 
Try of text 


50 
Repeat of text 


51 
Repeat1 of text


52 
val dynamic_method: string > (Proof.context > Proof.method)


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


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

5884

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

5824

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


57 
val end_block: Proof.state > Proof.state Seq.seq


58 
val terminal_proof: text > Proof.state > Proof.state Seq.seq


59 
val trivial_proof: Proof.state > Proof.state Seq.seq


60 
val default_proof: Proof.state > Proof.state Seq.seq


61 
val qed: bstring option > theory attribute list option > Proof.state


62 
> theory * (string * string * tthm)


63 
val setup: (theory > theory) list


64 
end;


65 


66 
structure Method: METHOD =


67 
struct


68 


69 


70 
(** proof methods **)


71 


72 
(* method from tactic *)


73 


74 
fun LIFT tac goal = Seq.map (fn x => (x, [], [])) (tac goal);


75 
fun METHOD tacf = Proof.method (LIFT o tacf);


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


77 


78 


79 
(* primitive *)


80 


81 
val fail = METHOD (K no_tac);


82 
val succeed = METHOD (K all_tac);


83 


84 


85 
(* trivial, assumption *)


86 


87 
fun trivial_tac [] = K all_tac


88 
 trivial_tac facts =


89 
let

5884

90 
val thms = Attribute.thms_of facts;

5824

91 
val r = ~ (length facts);


92 
in metacuts_tac thms THEN' rotate_tac r end;


93 


94 
val trivial = METHOD (ALLGOALS o trivial_tac);


95 
val assumption = METHOD (fn facts => FIRSTGOAL (trivial_tac facts THEN' assume_tac));


96 


97 
val asm_finish = METHOD (K (TRYALL assume_tac));


98 


99 


100 
(* rule *)


101 


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


103 


104 
fun multi_resolve facts rule =


105 
let


106 
fun multi_res i [] = Seq.single rule


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


108 
in multi_res 1 facts end;


109 


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


111 

5884

112 
fun rule_tac rules [] = resolve_tac (Attribute.thms_of rules)

5824

113 
 rule_tac erules facts =


114 
let

5884

115 
val rules = forward_chain (Attribute.thms_of facts) (Attribute.thms_of erules);

5824

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


117 
in tac end;


118 


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


120 


121 


122 


123 
(** methods theory data **)


124 


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


126 


127 
structure MethodsDataArgs =


128 
struct


129 
val name = "Isar/methods";


130 
type T =


131 
{space: NameSpace.T,


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


133 


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


135 
val prep_ext = I;


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


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


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


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


140 


141 
fun print _ {space, meths} =


142 
let


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


144 
[Pretty.str (NameSpace.cond_extern space name ^ ":"), Pretty.brk 2, Pretty.str comment];


145 
in


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


147 
Pretty.writeln (Pretty.big_list "methods:" (map prt_meth (Symtab.dest meths)))


148 
end;


149 
end;


150 


151 
structure MethodsData = TheoryDataFun(MethodsDataArgs);


152 
val print_methods = MethodsData.print;


153 


154 


155 
(* get methods *)


156 

5916

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


158 

5824

159 
fun method thy =


160 
let


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


162 

5884

163 
fun meth src =


164 
let


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


166 
val name = NameSpace.intern space raw_name;


167 
in

5824

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


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

5916

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

5824

171 
end;


172 
in meth end;


173 


174 


175 
(* add_methods *)


176 


177 
fun add_methods raw_meths thy =


178 
let


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


180 
val new_meths =


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


182 


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


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


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


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


187 
in


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


189 
end;


190 


191 
(*implicit version*)


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


193 


194 

5884

195 


196 
(** method syntax **)

5824

197 

5884

198 
(* basic *)


199 


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


201 
Args.syntax "method" scan;

5824

202 

5884

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


204 


205 


206 
(* sections *)

5824

207 

5884

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


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


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


211 


212 
fun apply att (ctxt, ths) = Attribute.applys ((ctxt, ths), [att]);

5824

213 

5884

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


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


216 


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


218 

5824

219 

5884

220 
fun sectioned_args args ss f src ctxt =

5921

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


222 
in f x ctxt' end;

5884

223 


224 
fun default_sectioned_args att ss f src ctxt =


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


226 


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


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

5824

229 


230 


231 


232 
(** method text **)


233 


234 
(* datatype text *)


235 


236 
datatype text =


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


238 
Source of Args.src 


239 
Then of text list 


240 
Orelse of text list 


241 
Try of text 


242 
Repeat of text 


243 
Repeat1 of text;


244 


245 


246 
(* dynamic methods *)


247 


248 
fun dynamic_method name = (fn ctxt =>

5884

249 
method (ProofContext.theory_of ctxt) (Args.src ((name, []), Position.none)) ctxt);

5824

250 


251 


252 
(* refine *)


253 


254 
fun refine text state =


255 
let


256 
val thy = Proof.theory_of state;


257 


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


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


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


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


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


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


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


265 
in eval text state end;


266 


267 


268 
(* unstructured steps *)


269 


270 
fun tac text state =


271 
state


272 
> Proof.goal_facts (K [])


273 
> refine text;


274 

5884

275 
fun then_tac text state =

5824

276 
state


277 
> Proof.goal_facts Proof.the_facts


278 
> refine text;


279 


280 


281 
(* proof steps *)


282 

5884

283 
val default_txt = Source (Args.src (("default", []), Position.none));

5824

284 
val finishN = "finish";


285 


286 
fun proof opt_text state =


287 
state


288 
> Proof.assert_backward


289 
> refine (if_none opt_text default_txt)


290 
> Seq.map Proof.enter_forward;


291 


292 


293 
(* conclusions *)


294 


295 
val end_block = Proof.end_block (dynamic_method finishN);


296 


297 
fun terminal_proof text = Seq.THEN (proof (Some text), end_block);


298 
val trivial_proof = terminal_proof (Basic (K trivial));


299 
val default_proof = terminal_proof default_txt;


300 


301 
val qed = Proof.qed (dynamic_method finishN);


302 


303 


304 


305 
(** theory setup **)


306 


307 
(* pure_methods *)


308 


309 
val pure_methods =


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


311 
("succeed", no_args succeed, "succeed"),


312 
("trivial", no_args trivial, "proof all goals trivially"),


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


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

5884

315 
("rule", thms_args rule, "apply primitive rule")];

5824

316 


317 


318 
(* setup *)


319 


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


321 


322 


323 
end;


324 


325 


326 
structure BasicMethod: BASIC_METHOD = Method;


327 
open BasicMethod;
