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


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


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


29 
> theory > theory


30 
datatype text =


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


32 
Source of Args.src 


33 
Then of text list 


34 
Orelse of text list 


35 
Try of text 


36 
Repeat of text 


37 
Repeat1 of text


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


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


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


41 
val etac: text > Proof.state > Proof.state Seq.seq


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


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


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


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


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


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


48 
> theory * (string * string * tthm)


49 
val syntax: (Args.T list > 'a * Args.T list) > ('a > 'b) > Args.src > 'b


50 
val no_args: 'a > Args.src > Proof.context > 'a


51 
val thm_args: (tthm list > 'a) > Args.src > Proof.context > 'a


52 
val sectioned_args: (Proof.context > 'a) > ('a * tthm list > 'b) >


53 
(string * ('b * tthm list > 'b)) list > ('b > 'c) > Args.src > Proof.context > 'c


54 
val setup: (theory > theory) list


55 
end;


56 


57 
structure Method: METHOD =


58 
struct


59 


60 


61 
(** proof methods **)


62 


63 
(* method from tactic *)


64 


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


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


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


68 


69 


70 
(* primitive *)


71 


72 
val fail = METHOD (K no_tac);


73 
val succeed = METHOD (K all_tac);


74 


75 


76 
(* trivial, assumption *)


77 


78 
fun trivial_tac [] = K all_tac


79 
 trivial_tac facts =


80 
let


81 
val thms = map Attribute.thm_of facts;


82 
val r = ~ (length facts);


83 
in metacuts_tac thms THEN' rotate_tac r end;


84 


85 
val trivial = METHOD (ALLGOALS o trivial_tac);


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


87 


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


89 


90 


91 
(* rule *)


92 


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


94 


95 
fun multi_resolve facts rule =


96 
let


97 
fun multi_res i [] = Seq.single rule


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


99 
in multi_res 1 facts end;


100 


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


102 


103 
fun rule_tac rules [] = resolve_tac (map Attribute.thm_of rules)


104 
 rule_tac erules facts =


105 
let


106 
val rules = forward_chain (map Attribute.thm_of facts) (map Attribute.thm_of erules);


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


108 
in tac end;


109 


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


111 


112 


113 


114 
(** methods theory data **)


115 


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


117 


118 
structure MethodsDataArgs =


119 
struct


120 
val name = "Isar/methods";


121 
type T =


122 
{space: NameSpace.T,


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


124 


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


126 
val prep_ext = I;


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


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


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


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


131 


132 
fun print _ {space, meths} =


133 
let


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


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


136 
in


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


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


139 
end;


140 
end;


141 


142 
structure MethodsData = TheoryDataFun(MethodsDataArgs);


143 
val print_methods = MethodsData.print;


144 


145 


146 
(* get methods *)


147 


148 
fun method thy =


149 
let


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


151 


152 
fun meth ((raw_name, args), pos) =


153 
let val name = NameSpace.intern space raw_name in


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


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


156 
 Some ((mth, _), _) => mth ((name, args), pos))


157 
end;


158 
in meth end;


159 


160 


161 
(* add_methods *)


162 


163 
fun add_methods raw_meths thy =


164 
let


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


166 
val new_meths =


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


168 


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


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


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


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


173 
in


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


175 
end;


176 


177 
(*implicit version*)


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


179 


180 


181 
(* argument syntax *)


182 


183 
val methodN = "method";


184 
fun syntax scan = Args.syntax methodN scan;


185 


186 
fun no_args x = syntax (Scan.succeed (fn (_: Proof.context) => x)) I;


187 


188 
(* FIXME move? *)


189 
fun thm_args f = syntax (Scan.repeat Args.name)


190 
(fn names => fn ctxt => f (ProofContext.get_tthmss ctxt names));


191 


192 
fun sectioned_args get_data def_sect sects f =


193 
syntax (Args.sectioned (map fst sects))


194 
(fn (names, sect_names) => fn ctxt =>


195 
let


196 
val get_thms = ProofContext.get_tthmss ctxt;


197 
val thms = get_thms names;


198 
val sect_thms = map (apsnd get_thms) sect_names;


199 


200 
fun apply_sect (data, (s, ths)) =


201 
(case assoc (sects, s) of


202 
Some add => add (data, ths)


203 
 None => error ("Unknown argument section " ^ quote s));


204 
in f (foldl apply_sect (def_sect (get_data ctxt, thms), sect_thms)) end);


205 


206 


207 


208 
(** method text **)


209 


210 
(* datatype text *)


211 


212 
datatype text =


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


214 
Source of Args.src 


215 
Then of text list 


216 
Orelse of text list 


217 
Try of text 


218 
Repeat of text 


219 
Repeat1 of text;


220 


221 


222 
(* dynamic methods *)


223 


224 
fun dynamic_method name = (fn ctxt =>


225 
method (ProofContext.theory_of ctxt) ((name, []), Position.none) ctxt);


226 


227 


228 
(* refine *)


229 


230 
fun refine text state =


231 
let


232 
val thy = Proof.theory_of state;


233 


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


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


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


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


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


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


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


241 
in eval text state end;


242 


243 


244 
(* unstructured steps *)


245 


246 
fun tac text state =


247 
state


248 
> Proof.goal_facts (K [])


249 
> refine text;


250 


251 
fun etac text state =


252 
state


253 
> Proof.goal_facts Proof.the_facts


254 
> refine text;


255 


256 


257 
(* proof steps *)


258 


259 
val default_txt = Source (("default", []), Position.none);


260 
val finishN = "finish";


261 


262 
fun proof opt_text state =


263 
state


264 
> Proof.assert_backward


265 
> refine (if_none opt_text default_txt)


266 
> Seq.map Proof.enter_forward;


267 


268 


269 
(* conclusions *)


270 


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


272 


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


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


275 
val default_proof = terminal_proof default_txt;


276 


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


278 


279 


280 


281 
(** theory setup **)


282 


283 
(* pure_methods *)


284 


285 
val pure_methods =


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


287 
("succeed", no_args succeed, "succeed"),


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


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


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


291 
("rule", thm_args rule, "apply primitive rule")];


292 


293 


294 
(* setup *)


295 


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


297 


298 


299 
end;


300 


301 


302 
structure BasicMethod: BASIC_METHOD = Method;


303 
open BasicMethod;
