src/Pure/Isar/method.ML
author wenzelm
Fri Mar 19 11:24:00 1999 +0100 (1999-03-19)
changeset 6404 2daaf2943c79
parent 6108 2c9ed58c30ba
child 6500 68ba555ac59a
permissions -rw-r--r--
common qed and end of proofs;
     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 * thm list) list) Seq.seq
    18   val METHOD: (thm list -> tactic) -> Proof.method
    19   val METHOD0: tactic -> Proof.method
    20   val fail: Proof.method
    21   val succeed: Proof.method
    22   val same: Proof.method
    23   val assumption: Proof.method
    24   val forward_chain: thm list -> thm list -> thm Seq.seq
    25   val rule_tac: thm list -> thm list -> int -> tactic
    26   val rule: thm list -> Proof.method
    27   exception METHOD_FAIL of (string * Position.T) * exn
    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
    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: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    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 refine: text -> Proof.state -> Proof.state Seq.seq
    53   val tac: text -> Proof.state -> Proof.state Seq.seq
    54   val then_tac: text -> Proof.state -> Proof.state Seq.seq
    55   val proof: text option -> Proof.state -> Proof.state Seq.seq
    56   val local_qed: text option -> Proof.state -> Proof.state Seq.seq
    57   val local_terminal_proof: text -> Proof.state -> Proof.state Seq.seq
    58   val local_immediate_proof: Proof.state -> Proof.state Seq.seq
    59   val local_default_proof: Proof.state -> Proof.state Seq.seq
    60   val global_qed: bstring option -> theory attribute list option -> text option
    61     -> Proof.state -> theory * (string * string * thm)
    62   val global_terminal_proof: text -> Proof.state -> theory * (string * string * thm)
    63   val global_immediate_proof: Proof.state -> theory * (string * string * thm)
    64   val global_default_proof: Proof.state -> theory * (string * string * thm)
    65   val setup: (theory -> theory) list
    66 end;
    67 
    68 structure Method: METHOD =
    69 struct
    70 
    71 
    72 (** proof methods **)
    73 
    74 (* method from tactic *)
    75 
    76 fun LIFT tac goal = Seq.map (fn x => (x, [], [])) (tac goal);
    77 fun METHOD tacf = Proof.method (LIFT o tacf);
    78 fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Method may not be used with facts");
    79 
    80 
    81 (* primitive *)
    82 
    83 val fail = METHOD (K no_tac);
    84 val succeed = METHOD (K all_tac);
    85 
    86 
    87 (* same, assumption *)
    88 
    89 fun same_tac [] = K all_tac
    90   | same_tac facts =
    91       let val r = ~ (length facts);
    92       in metacuts_tac facts THEN' rotate_tac r end;
    93 
    94 val same = METHOD (ALLGOALS o same_tac);
    95 val assumption = METHOD (fn facts => FIRSTGOAL (same_tac facts THEN' assume_tac));
    96 
    97 val asm_finish = METHOD (K (FILTER (equal 0 o Thm.nprems_of) (ALLGOALS 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 
   112 fun rule_tac rules [] = resolve_tac rules
   113   | rule_tac erules facts =
   114       let
   115         val rules = forward_chain facts erules;
   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 
   157 exception METHOD_FAIL of (string * Position.T) * exn;
   158 
   159 fun method thy =
   160   let
   161     val {space, meths} = MethodsData.get thy;
   162 
   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
   168         (case Symtab.lookup (meths, name) of
   169           None => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
   170         | Some ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src))
   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 
   195 
   196 (** method syntax **)
   197 
   198 (* basic *)
   199 
   200 fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
   201   Args.syntax "method" scan;
   202 
   203 fun no_args (x: Proof.method) src ctxt = #2 (syntax (Scan.succeed x) ctxt src);
   204 
   205 
   206 (* sections *)
   207 
   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) = Thm.applys_attributes ((ctxt, ths), [att]);
   213 
   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 
   219 
   220 fun sectioned_args args ss f src ctxt =
   221   let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src
   222   in f x ctxt' end;
   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);
   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 (* refine *)
   247 
   248 fun refine text state =
   249   let
   250     val thy = Proof.theory_of state;
   251 
   252     fun eval (Basic mth) = Proof.refine mth
   253       | eval (Source src) = Proof.refine (method thy src)
   254       | eval (Then txts) = Seq.EVERY (map eval txts)
   255       | eval (Orelse txts) = Seq.FIRST (map eval txts)
   256       | eval (Try txt) = Seq.TRY (eval txt)
   257       | eval (Repeat txt) = Seq.REPEAT (eval txt)
   258       | eval (Repeat1 txt) = Seq.REPEAT1 (eval txt);
   259   in eval text state end;
   260 
   261 fun named_method name = Source (Args.src ((name, []), Position.none));
   262 
   263 
   264 (* unstructured steps *)
   265 
   266 fun tac text state =
   267   state
   268   |> Proof.goal_facts (K [])
   269   |> refine text;
   270 
   271 fun then_tac text state =
   272   state
   273   |> Proof.goal_facts Proof.the_facts
   274   |> refine text;
   275 
   276 
   277 (* structured proof steps *)
   278 
   279 val default_text = named_method "default";
   280 val finish_text = named_method "finish";
   281 
   282 fun proof opt_text state =
   283   state
   284   |> Proof.assert_backward
   285   |> refine (if_none opt_text default_text)
   286   |> Seq.map Proof.enter_forward;
   287 
   288 fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text));
   289 fun local_terminal_proof text = Seq.THEN (proof (Some text), local_qed None);
   290 val local_immediate_proof = local_terminal_proof (Basic (K same));
   291 val local_default_proof = local_terminal_proof default_text;
   292 
   293 fun global_qed alt_name alt_atts opt_text =
   294   Proof.global_qed (refine (if_none opt_text finish_text)) alt_name alt_atts;
   295 
   296 fun global_terminal_proof text = Seq.hd o Seq.map (global_qed None None None) o proof (Some text);
   297 val global_immediate_proof = global_terminal_proof (Basic (K same));
   298 val global_default_proof = global_terminal_proof default_text;
   299 
   300 
   301 
   302 (** theory setup **)
   303 
   304 (* pure_methods *)
   305 
   306 val pure_methods =
   307  [("fail", no_args fail, "force failure"),
   308   ("succeed", no_args succeed, "succeed"),
   309   ("same", no_args same, "insert facts, nothing else"),
   310   ("assumption", no_args assumption, "proof by assumption"),
   311   ("finish", no_args asm_finish, "finish proof by assumption"),
   312   ("rule", thms_args rule, "apply primitive rule")];
   313 
   314 
   315 (* setup *)
   316 
   317 val setup = [MethodsData.init, add_methods pure_methods];
   318 
   319 
   320 end;
   321 
   322 
   323 structure BasicMethod: BASIC_METHOD = Method;
   324 open BasicMethod;