src/Pure/Isar/proof.ML
author wenzelm
Sun Jun 07 20:03:40 2015 +0200 (2015-06-07)
changeset 60379 51d9dcd71ad7
parent 60377 234b7da8542e
child 60381 b568b98fa000
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/Isar/proof.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 The Isar/VM proof language interpreter: maintains a structured flow of
     5 context elements, goals, refinements, and facts.
     6 *)
     7 
     8 signature PROOF =
     9 sig
    10   type context = Proof.context
    11   type method = Method.method
    12   type state
    13   val init: context -> state
    14   val level: state -> int
    15   val assert_bottom: bool -> state -> state
    16   val context_of: state -> context
    17   val theory_of: state -> theory
    18   val map_context: (context -> context) -> state -> state
    19   val map_context_result : (context -> 'a * context) -> state -> 'a * state
    20   val map_contexts: (context -> context) -> state -> state
    21   val propagate_ml_env: state -> state
    22   val bind_terms: (indexname * term option) list -> state -> state
    23   val put_thms: bool -> string * thm list option -> state -> state
    24   val the_facts: state -> thm list
    25   val the_fact: state -> thm
    26   val set_facts: thm list -> state -> state
    27   val reset_facts: state -> state
    28   val assert_forward: state -> state
    29   val assert_chain: state -> state
    30   val assert_forward_or_chain: state -> state
    31   val assert_backward: state -> state
    32   val assert_no_chain: state -> state
    33   val enter_forward: state -> state
    34   val enter_chain: state -> state
    35   val enter_backward: state -> state
    36   val has_bottom_goal: state -> bool
    37   val pretty_state: int -> state -> Pretty.T list
    38   val refine: Method.text -> state -> state Seq.seq
    39   val refine_end: Method.text -> state -> state Seq.seq
    40   val refine_insert: thm list -> state -> state
    41   val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
    42   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
    43   val goal: state -> {context: context, facts: thm list, goal: thm}
    44   val simple_goal: state -> {context: context, goal: thm}
    45   val status_markup: state -> Markup.T
    46   val let_bind: (term list * term) list -> state -> state
    47   val let_bind_cmd: (string list * string) list -> state -> state
    48   val write: Syntax.mode -> (term * mixfix) list -> state -> state
    49   val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state
    50   val fix: (binding * typ option * mixfix) list -> state -> state
    51   val fix_cmd: (binding * string option * mixfix) list -> state -> state
    52   val assm: Assumption.export ->
    53     (Thm.binding * (term * term list) list) list -> state -> state
    54   val assm_cmd: Assumption.export ->
    55     (Attrib.binding * (string * string list) list) list -> state -> state
    56   val assume: (Thm.binding * (term * term list) list) list -> state -> state
    57   val assume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
    58   val presume: (Thm.binding * (term * term list) list) list -> state -> state
    59   val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
    60   val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
    61   val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
    62   val chain: state -> state
    63   val chain_facts: thm list -> state -> state
    64   val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
    65   val note_thmss_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list -> state -> state
    66   val from_thmss: ((thm list * attribute list) list) list -> state -> state
    67   val from_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
    68   val with_thmss: ((thm list * attribute list) list) list -> state -> state
    69   val with_thmss_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
    70   val supply: (Thm.binding * (thm list * attribute list) list) list -> state -> state
    71   val supply_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list -> state -> state
    72   val using: ((thm list * attribute list) list) list -> state -> state
    73   val using_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
    74   val unfolding: ((thm list * attribute list) list) list -> state -> state
    75   val unfolding_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
    76   val invoke_case: (string * Position.T) * binding option list * attribute list ->
    77     state -> state
    78   val invoke_case_cmd: (string * Position.T) * binding option list * Token.src list ->
    79     state -> state
    80   val begin_block: state -> state
    81   val next_block: state -> state
    82   val end_block: state -> state
    83   val begin_notepad: context -> state
    84   val end_notepad: state -> context
    85   val proof: Method.text option -> state -> state Seq.seq
    86   val proof_results: Method.text_range option -> state -> state Seq.result Seq.seq
    87   val defer: int -> state -> state
    88   val prefer: int -> state -> state
    89   val apply: Method.text -> state -> state Seq.seq
    90   val apply_end: Method.text -> state -> state Seq.seq
    91   val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
    92   val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
    93   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
    94     (context -> 'a -> attribute) ->
    95     ('b list -> context -> (term list list * (context -> context)) * context) ->
    96     string -> Method.text option -> (thm list list -> state -> state) ->
    97     ((binding * 'a list) * 'b) list -> state -> state
    98   val local_qed: Method.text_range option * bool -> state -> state
    99   val theorem: Method.text option -> (thm list list -> context -> context) ->
   100     (term * term list) list list -> context -> state
   101   val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
   102     (string * string list) list list -> context -> state
   103   val global_qed: Method.text_range option * bool -> state -> context
   104   val local_terminal_proof: Method.text_range * Method.text_range option -> state -> state
   105   val local_default_proof: state -> state
   106   val local_immediate_proof: state -> state
   107   val local_skip_proof: bool -> state -> state
   108   val local_done_proof: state -> state
   109   val global_terminal_proof: Method.text_range * Method.text_range option -> state -> context
   110   val global_default_proof: state -> context
   111   val global_immediate_proof: state -> context
   112   val global_skip_proof: bool -> state -> context
   113   val global_done_proof: state -> context
   114   val have: Method.text option -> (thm list list -> state -> state) ->
   115     (Thm.binding * (term * term list) list) list -> bool -> state -> state
   116   val have_cmd: Method.text option -> (thm list list -> state -> state) ->
   117     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   118   val show: Method.text option -> (thm list list -> state -> state) ->
   119     (Thm.binding * (term * term list) list) list -> bool -> state -> state
   120   val show_cmd: Method.text option -> (thm list list -> state -> state) ->
   121     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   122   val schematic_goal: state -> bool
   123   val is_relevant: state -> bool
   124   val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
   125   val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
   126     state -> state
   127   val global_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
   128     state -> context
   129 end;
   130 
   131 structure Proof: PROOF =
   132 struct
   133 
   134 type context = Proof.context;
   135 type method = Method.method;
   136 
   137 
   138 (** proof state **)
   139 
   140 (* datatype state *)
   141 
   142 datatype mode = Forward | Chain | Backward;
   143 
   144 datatype state =
   145   State of node Stack.T
   146 and node =
   147   Node of
   148    {context: context,
   149     facts: thm list option,
   150     mode: mode,
   151     goal: goal option}
   152 and goal =
   153   Goal of
   154    {statement: (string * Position.T) * term list list * term,
   155       (*goal kind and statement (starting with vars), initial proposition*)
   156     using: thm list,                      (*goal facts*)
   157     goal: thm,                            (*subgoals ==> statement*)
   158     before_qed: Method.text option,
   159     after_qed:
   160       (thm list list -> state -> state) *
   161       (thm list list -> context -> context)};
   162 
   163 fun make_goal (statement, using, goal, before_qed, after_qed) =
   164   Goal {statement = statement, using = using, goal = goal,
   165     before_qed = before_qed, after_qed = after_qed};
   166 
   167 fun make_node (context, facts, mode, goal) =
   168   Node {context = context, facts = facts, mode = mode, goal = goal};
   169 
   170 fun map_node f (Node {context, facts, mode, goal}) =
   171   make_node (f (context, facts, mode, goal));
   172 
   173 val init_context =
   174   Proof_Context.set_stmt true #>
   175   Proof_Context.map_naming (K Name_Space.local_naming);
   176 
   177 fun init ctxt =
   178   State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
   179 
   180 fun top (State stack) = Stack.top stack |> (fn Node node => node);
   181 fun map_top f (State stack) = State (Stack.map_top (map_node f) stack);
   182 fun map_all f (State stack) = State (Stack.map_all (map_node f) stack);
   183 
   184 
   185 
   186 (** basic proof state operations **)
   187 
   188 (* block structure *)
   189 
   190 fun open_block (State stack) = State (Stack.push stack);
   191 
   192 fun close_block (State stack) = State (Stack.pop stack)
   193   handle List.Empty => error "Unbalanced block parentheses";
   194 
   195 fun level (State stack) = Stack.level stack;
   196 
   197 fun assert_bottom b state =
   198   let val b' = level state <= 2 in
   199     if b andalso not b' then error "Not at bottom of proof"
   200     else if not b andalso b' then error "Already at bottom of proof"
   201     else state
   202   end;
   203 
   204 
   205 (* context *)
   206 
   207 val context_of = #context o top;
   208 val theory_of = Proof_Context.theory_of o context_of;
   209 
   210 fun map_node_context f =
   211   map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
   212 
   213 fun map_context f =
   214   map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
   215 
   216 fun map_context_result f state =
   217   f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
   218 
   219 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
   220 
   221 fun propagate_ml_env state = map_contexts
   222   (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
   223 
   224 val bind_terms = map_context o Proof_Context.bind_terms;
   225 val put_thms = map_context oo Proof_Context.put_thms;
   226 
   227 
   228 (* facts *)
   229 
   230 val get_facts = #facts o top;
   231 
   232 fun the_facts state =
   233   (case get_facts state of SOME facts => facts
   234   | NONE => error "No current facts available");
   235 
   236 fun the_fact state =
   237   (case the_facts state of [thm] => thm
   238   | _ => error "Single theorem expected");
   239 
   240 fun put_facts facts =
   241   map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
   242   put_thms true (Auto_Bind.thisN, facts);
   243 
   244 val set_facts = put_facts o SOME;
   245 val reset_facts = put_facts NONE;
   246 
   247 fun these_factss more_facts (named_factss, state) =
   248   (named_factss, state |> set_facts (maps snd named_factss @ more_facts));
   249 
   250 fun export_facts inner outer =
   251   (case get_facts inner of
   252     NONE => reset_facts outer
   253   | SOME thms =>
   254       thms
   255       |> Proof_Context.export (context_of inner) (context_of outer)
   256       |> (fn ths => set_facts ths outer));
   257 
   258 
   259 (* mode *)
   260 
   261 val get_mode = #mode o top;
   262 fun put_mode mode = map_top (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
   263 
   264 val mode_name = (fn Forward => "state" | Chain => "chain" | Backward => "prove");
   265 
   266 fun assert_mode pred state =
   267   let val mode = get_mode state in
   268     if pred mode then state
   269     else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode")
   270   end;
   271 
   272 val assert_forward = assert_mode (fn mode => mode = Forward);
   273 val assert_chain = assert_mode (fn mode => mode = Chain);
   274 val assert_forward_or_chain = assert_mode (fn mode => mode = Forward orelse mode = Chain);
   275 val assert_backward = assert_mode (fn mode => mode = Backward);
   276 val assert_no_chain = assert_mode (fn mode => mode <> Chain);
   277 
   278 val enter_forward = put_mode Forward;
   279 val enter_chain = put_mode Chain;
   280 val enter_backward = put_mode Backward;
   281 
   282 
   283 (* current goal *)
   284 
   285 fun current_goal state =
   286   (case top state of
   287     {context, goal = SOME (Goal goal), ...} => (context, goal)
   288   | _ => error "No current goal");
   289 
   290 fun assert_current_goal g state =
   291   let val g' = can current_goal state in
   292     if g andalso not g' then error "No goal in this block"
   293     else if not g andalso g' then error "Goal present in this block"
   294     else state
   295   end;
   296 
   297 fun put_goal goal = map_top (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
   298 
   299 val set_goal = put_goal o SOME;
   300 val reset_goal = put_goal NONE;
   301 
   302 val before_qed = #before_qed o #2 o current_goal;
   303 
   304 
   305 (* bottom goal *)
   306 
   307 fun has_bottom_goal (State stack) =
   308   let
   309     fun bottom [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = true
   310       | bottom [Node {goal, ...}] = is_some goal
   311       | bottom [] = false
   312       | bottom (_ :: rest) = bottom rest;
   313   in bottom (op :: (Stack.dest stack)) end;
   314 
   315 
   316 (* nested goal *)
   317 
   318 fun map_goal f g h (State stack) =
   319   (case Stack.dest stack of
   320     (Node {context, facts, mode, goal = SOME goal}, node :: nodes) =>
   321       let
   322         val Goal {statement, using, goal, before_qed, after_qed} = goal;
   323         val goal' = make_goal (g (statement, using, goal, before_qed, after_qed));
   324         val node' = map_node_context h node;
   325         val stack' = Stack.make (make_node (f context, facts, mode, SOME goal')) (node' :: nodes);
   326       in State stack' end
   327   | (nd, node :: nodes) =>
   328       let
   329         val nd' = map_node_context f nd;
   330         val State stack' = map_goal f g h (State (Stack.make node nodes));
   331         val (node', nodes') = Stack.dest stack';
   332       in State (Stack.make nd' (node' :: nodes')) end
   333   | _ => State stack);
   334 
   335 fun provide_goal goal = map_goal I (fn (statement, using, _, before_qed, after_qed) =>
   336   (statement, using, goal, before_qed, after_qed)) I;
   337 
   338 fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) =>
   339   (statement, using, goal, before_qed, after_qed)) I;
   340 
   341 local
   342   fun find i state =
   343     (case try current_goal state of
   344       SOME (ctxt, goal) => (ctxt, (i, goal))
   345     | NONE => find (i + 1) (close_block state handle ERROR _ => error "No proof goal"));
   346 in val find_goal = find 0 end;
   347 
   348 fun get_goal state =
   349   let val (ctxt, (_, {using, goal, ...})) = find_goal state
   350   in (ctxt, (using, goal)) end;
   351 
   352 
   353 
   354 (** pretty_state **)
   355 
   356 local
   357 
   358 fun pretty_facts _ _ NONE = []
   359   | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths];
   360 
   361 fun pretty_sep prts [] = prts
   362   | pretty_sep [] prts = prts
   363   | pretty_sep prts1 prts2 = prts1 @ [Pretty.str ""] @ prts2;
   364 
   365 in
   366 
   367 fun pretty_state nr state =
   368   let
   369     val {context = ctxt, facts, mode, goal = _} = top state;
   370     val verbose = Config.get ctxt Proof_Context.verbose;
   371 
   372     fun prt_goal (SOME (_, (_,
   373       {statement = ((_, pos), _, _), using, goal, before_qed = _, after_qed = _}))) =
   374           pretty_sep
   375             (pretty_facts ctxt "using"
   376               (if mode <> Backward orelse null using then NONE else SOME using))
   377             ([Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal)
   378       | prt_goal NONE = [];
   379 
   380     val prt_ctxt =
   381       if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
   382       else if mode = Backward then Proof_Context.pretty_ctxt ctxt
   383       else [];
   384 
   385     val position_markup = Position.markup (Position.thread_data ()) Markup.position;
   386   in
   387     [Pretty.block
   388       [Pretty.mark_str (position_markup, "proof"),
   389         Pretty.str (" (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1))],
   390       Pretty.str ""] @
   391     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
   392     (if verbose orelse mode = Forward then
   393        pretty_sep (pretty_facts ctxt "" facts) (prt_goal (try find_goal state))
   394      else if mode = Chain then pretty_facts ctxt "picking" facts
   395      else prt_goal (try find_goal state))
   396   end;
   397 
   398 end;
   399 
   400 
   401 
   402 (** proof steps **)
   403 
   404 (* refine via method *)
   405 
   406 local
   407 
   408 fun goalN i = "goal" ^ string_of_int i;
   409 fun goals st = map goalN (1 upto Thm.nprems_of st);
   410 
   411 fun no_goal_cases st = map (rpair NONE) (goals st);
   412 
   413 fun goal_cases ctxt st =
   414   Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
   415 
   416 fun apply_method text ctxt state =
   417   #2 (#2 (find_goal state)) |> (fn {statement, using, goal, before_qed, after_qed} =>
   418     Method.evaluate text ctxt using goal
   419     |> Seq.map (fn (meth_cases, goal') =>
   420       state
   421       |> map_goal
   422           (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases ctxt goal') #>
   423            Proof_Context.update_cases true meth_cases)
   424           (K (statement, using, goal', before_qed, after_qed)) I));
   425 
   426 in
   427 
   428 fun refine text state = apply_method text (context_of state) state;
   429 fun refine_end text state = apply_method text (#1 (find_goal state)) state;
   430 
   431 fun refine_insert ths =
   432   Seq.hd o refine (Method.Basic (K (Method.insert ths)));
   433 
   434 end;
   435 
   436 
   437 (* refine via sub-proof *)
   438 
   439 local
   440 
   441 fun finish_tac _ 0 = K all_tac
   442   | finish_tac ctxt n =
   443       Goal.norm_hhf_tac ctxt THEN'
   444       SUBGOAL (fn (goal, i) =>
   445         if can Logic.unprotect (Logic.strip_assums_concl goal) then
   446           eresolve_tac ctxt [Drule.protectI] i THEN finish_tac ctxt (n - 1) i
   447         else finish_tac ctxt (n - 1) (i + 1));
   448 
   449 fun goal_tac ctxt rule =
   450   Goal.norm_hhf_tac ctxt THEN'
   451   resolve_tac ctxt [rule] THEN'
   452   finish_tac ctxt (Thm.nprems_of rule);
   453 
   454 fun FINDGOAL tac st =
   455   let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
   456   in find 1 (Thm.nprems_of st) st end;
   457 
   458 in
   459 
   460 fun refine_goals print_rule inner raw_rules state =
   461   let
   462     val (outer, (_, goal)) = get_goal state;
   463     fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac outer rule) st);
   464   in
   465     raw_rules
   466     |> Proof_Context.goal_export inner outer
   467     |> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
   468   end;
   469 
   470 end;
   471 
   472 
   473 (* conclude goal *)
   474 
   475 fun conclude_goal ctxt goal propss =
   476   let
   477     val thy = Proof_Context.theory_of ctxt;
   478 
   479     val _ =
   480       Theory.subthy (Thm.theory_of_thm goal, thy) orelse
   481         error "Bad background theory of goal state";
   482     val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
   483 
   484     fun lost_structure () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
   485 
   486     val th =
   487       (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
   488         handle THM _ => lost_structure ())
   489       |> Drule.flexflex_unique (SOME ctxt)
   490       |> Thm.check_shyps (Variable.sorts_of ctxt)
   491       |> Thm.check_hyps (Context.Proof ctxt);
   492 
   493     val goal_propss = filter_out null propss;
   494     val results =
   495       Conjunction.elim_balanced (length goal_propss) th
   496       |> map2 Conjunction.elim_balanced (map length goal_propss)
   497       handle THM _ => lost_structure ();
   498     val _ =
   499       Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results))
   500         orelse error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
   501 
   502     fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
   503       | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
   504       | recover_result [] [] = []
   505       | recover_result _ _ = lost_structure ();
   506   in recover_result propss results end;
   507 
   508 val finished_goal_error = "Failed to finish proof";
   509 
   510 fun finished_goal pos state =
   511   let val (ctxt, (_, goal)) = get_goal state in
   512     if Thm.no_prems goal then Seq.Result state
   513     else
   514       Seq.Error (fn () =>
   515         finished_goal_error ^ Position.here pos ^ ":\n" ^
   516           Proof_Display.string_of_goal ctxt goal)
   517   end;
   518 
   519 
   520 (* goal views -- corresponding to methods *)
   521 
   522 fun raw_goal state =
   523   let val (ctxt, (facts, goal)) = get_goal state
   524   in {context = ctxt, facts = facts, goal = goal} end;
   525 
   526 val goal = raw_goal o refine_insert [];
   527 
   528 fun simple_goal state =
   529   let
   530     val (_, (facts, _)) = get_goal state;
   531     val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
   532   in {context = ctxt, goal = goal} end;
   533 
   534 fun status_markup state =
   535   (case try goal state of
   536     SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
   537   | NONE => Markup.empty);
   538 
   539 fun method_error kind pos state =
   540   Seq.single (Proof_Display.method_error kind pos (raw_goal state));
   541 
   542 
   543 
   544 (*** structured proof commands ***)
   545 
   546 (** context elements **)
   547 
   548 (* let bindings *)
   549 
   550 local
   551 
   552 fun gen_bind bind args state =
   553   state
   554   |> assert_forward
   555   |> map_context (bind true args #> snd)
   556   |> reset_facts;
   557 
   558 in
   559 
   560 val let_bind = gen_bind Proof_Context.match_bind;
   561 val let_bind_cmd = gen_bind Proof_Context.match_bind_cmd;
   562 
   563 end;
   564 
   565 
   566 (* concrete syntax *)
   567 
   568 local
   569 
   570 fun gen_write prep_arg mode args =
   571   assert_forward
   572   #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
   573   #> reset_facts;
   574 
   575 fun read_arg ctxt (c, mx) =
   576   (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
   577     Free (x, _) =>
   578       let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx)
   579       in (Free (x, T), mx) end
   580   | t => (t, mx));
   581 
   582 in
   583 
   584 val write = gen_write (K I);
   585 val write_cmd = gen_write read_arg;
   586 
   587 end;
   588 
   589 
   590 (* fix *)
   591 
   592 local
   593 
   594 fun gen_fix prep_var args =
   595   assert_forward
   596   #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (fold_map prep_var args ctxt)) ctxt))
   597   #> reset_facts;
   598 
   599 in
   600 
   601 val fix = gen_fix Proof_Context.cert_var;
   602 val fix_cmd = gen_fix Proof_Context.read_var;
   603 
   604 end;
   605 
   606 
   607 (* assume etc. *)
   608 
   609 local
   610 
   611 fun gen_assume asm prep_att exp args state =
   612   state
   613   |> assert_forward
   614   |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args))
   615   |> these_factss [] |> #2;
   616 
   617 in
   618 
   619 val assm = gen_assume Proof_Context.add_assms (K I);
   620 val assm_cmd = gen_assume Proof_Context.add_assms_cmd Attrib.attribute_cmd;
   621 val assume = assm Assumption.assume_export;
   622 val assume_cmd = assm_cmd Assumption.assume_export;
   623 val presume = assm Assumption.presume_export;
   624 val presume_cmd = assm_cmd Assumption.presume_export;
   625 
   626 end;
   627 
   628 
   629 (* def *)
   630 
   631 local
   632 
   633 fun gen_def prep_att prep_var prep_binds args state =
   634   let
   635     val _ = assert_forward state;
   636     val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
   637     val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
   638   in
   639     state
   640     |> map_context_result (fold_map (fn (x, mx) => prep_var (x, NONE, mx)) raw_vars)
   641     |>> map (fn (x, _, mx) => (x, mx))
   642     |-> (fn vars =>
   643       map_context_result (prep_binds false (map swap raw_rhss))
   644       #-> (fn rhss =>
   645         let
   646           val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
   647             ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
   648         in map_context_result (Local_Defs.add_defs defs) end))
   649     |-> (set_facts o map (#2 o #2))
   650   end;
   651 
   652 in
   653 
   654 val def = gen_def (K I) Proof_Context.cert_var Proof_Context.match_bind;
   655 val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_var Proof_Context.match_bind_cmd;
   656 
   657 end;
   658 
   659 
   660 
   661 (** facts **)
   662 
   663 (* chain *)
   664 
   665 fun clean_facts ctxt =
   666   set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt;
   667 
   668 val chain =
   669   assert_forward
   670   #> clean_facts
   671   #> enter_chain;
   672 
   673 fun chain_facts facts =
   674   set_facts facts
   675   #> chain;
   676 
   677 
   678 (* note etc. *)
   679 
   680 fun no_binding args = map (pair (Binding.empty, [])) args;
   681 
   682 local
   683 
   684 fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
   685   state
   686   |> assert_forward
   687   |> map_context_result (fn ctxt => ctxt |> Proof_Context.note_thmss ""
   688     (Attrib.map_facts_refs (map (prep_atts ctxt)) (prep_fact ctxt) args))
   689   |> these_factss (more_facts state)
   690   ||> opt_chain
   691   |> opt_result;
   692 
   693 in
   694 
   695 val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
   696 val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
   697 
   698 val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
   699 val from_thmss_cmd =
   700   gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
   701 
   702 val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
   703 val with_thmss_cmd =
   704   gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
   705 
   706 val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
   707 
   708 end;
   709 
   710 
   711 (* facts during goal refinement *)
   712 
   713 local
   714 
   715 fun gen_supply prep_att prep_fact args state =
   716   state
   717   |> assert_backward
   718   |> map_context (fn ctxt => ctxt |> Proof_Context.note_thmss ""
   719        (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) args) |> snd);
   720 
   721 in
   722 
   723 val supply = gen_supply (K I) (K I);
   724 val supply_cmd = gen_supply Attrib.attribute_cmd Proof_Context.get_fact;
   725 
   726 end;
   727 
   728 
   729 (* using/unfolding *)
   730 
   731 local
   732 
   733 fun gen_using f g prep_att prep_fact args state =
   734   state
   735   |> assert_backward
   736   |> map_context_result
   737     (fn ctxt => ctxt |> Proof_Context.note_thmss ""
   738       (Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
   739   |> (fn (named_facts, state') =>
   740     state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) =>
   741       let
   742         val ctxt = context_of state';
   743         val ths = maps snd named_facts;
   744       in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I);
   745 
   746 fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
   747 fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths);
   748 val unfold_goals = Local_Defs.unfold_goals;
   749 
   750 in
   751 
   752 val using = gen_using append_using (K (K I)) (K I) (K I);
   753 val using_cmd = gen_using append_using (K (K I)) Attrib.attribute_cmd Proof_Context.get_fact;
   754 val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
   755 val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact;
   756 
   757 end;
   758 
   759 
   760 (* case *)
   761 
   762 local
   763 
   764 fun gen_invoke_case internal prep_att ((name, pos), xs, raw_atts) state =
   765   let
   766     val atts = map (prep_att (context_of state)) raw_atts;
   767     val (asms, state') = state |> map_context_result (fn ctxt =>
   768       ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt internal (name, pos) xs));
   769     val assumptions =
   770       asms |> map (fn (b, ts) => ((Binding.set_pos pos b, atts), map (rpair []) ts));
   771   in
   772     state'
   773     |> assume assumptions
   774     |> bind_terms Auto_Bind.no_facts
   775     |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
   776   end;
   777 
   778 in
   779 
   780 val invoke_case = gen_invoke_case true (K I);
   781 val invoke_case_cmd = gen_invoke_case false Attrib.attribute_cmd;
   782 
   783 end;
   784 
   785 
   786 
   787 (** proof structure **)
   788 
   789 (* blocks *)
   790 
   791 val begin_block =
   792   assert_forward
   793   #> open_block
   794   #> reset_goal
   795   #> open_block;
   796 
   797 val next_block =
   798   assert_forward
   799   #> close_block
   800   #> open_block
   801   #> reset_goal
   802   #> reset_facts;
   803 
   804 fun end_block state =
   805   state
   806   |> assert_forward
   807   |> assert_bottom false
   808   |> close_block
   809   |> assert_current_goal false
   810   |> close_block
   811   |> export_facts state;
   812 
   813 
   814 (* global notepad *)
   815 
   816 val begin_notepad =
   817   init
   818   #> open_block
   819   #> map_context (Variable.set_body true)
   820   #> open_block;
   821 
   822 val end_notepad =
   823   assert_forward
   824   #> assert_bottom true
   825   #> close_block
   826   #> assert_current_goal false
   827   #> close_block
   828   #> context_of;
   829 
   830 
   831 (* sub-proofs *)
   832 
   833 fun proof opt_text =
   834   assert_backward
   835   #> refine (the_default Method.default_text opt_text)
   836   #> Seq.map (using_facts [] #> enter_forward);
   837 
   838 fun proof_results arg =
   839   Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
   840     method_error "initial" (Method.position arg));
   841 
   842 fun end_proof bot (prev_pos, (opt_text, immed)) =
   843   let
   844     val (finish_text, terminal_pos, finished_pos) =
   845       (case opt_text of
   846         NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
   847       | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
   848   in
   849     Seq.APPEND (fn state =>
   850       state
   851       |> assert_forward
   852       |> assert_bottom bot
   853       |> close_block
   854       |> assert_current_goal true
   855       |> using_facts []
   856       |> `before_qed |-> (refine o the_default Method.succeed_text)
   857       |> Seq.maps (refine finish_text)
   858       |> Seq.make_results, method_error "terminal" terminal_pos)
   859     #> Seq.maps_results (Seq.single o finished_goal finished_pos)
   860   end;
   861 
   862 fun check_result msg sq =
   863   (case Seq.pull sq of
   864     NONE => error msg
   865   | SOME (s, _) => s);
   866 
   867 
   868 (* unstructured refinement *)
   869 
   870 fun defer i =
   871   assert_no_chain #>
   872   refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd;
   873 
   874 fun prefer i =
   875   assert_no_chain #>
   876   refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd;
   877 
   878 fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
   879 
   880 fun apply_end text = assert_forward #> refine_end text;
   881 
   882 fun apply_results (text, (pos, _)) =
   883   Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
   884 
   885 fun apply_end_results (text, (pos, _)) =
   886   Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
   887 
   888 
   889 
   890 (** goals **)
   891 
   892 (* generic goals *)
   893 
   894 local
   895 
   896 val is_var =
   897   can (dest_TVar o Logic.dest_type o Logic.dest_term) orf
   898   can (dest_Var o Logic.dest_term);
   899 
   900 fun implicit_vars props =
   901   let
   902     val (var_props, _) = take_prefix is_var props;
   903     val explicit_vars = fold Term.add_vars var_props [];
   904     val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
   905   in map (Logic.mk_term o Var) vars end;
   906 
   907 fun refine_terms n =
   908   refine (Method.Basic (fn ctxt => EMPTY_CASES o
   909     K (HEADGOAL (PRECISE_CONJUNCTS n
   910       (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))))
   911   #> Seq.hd;
   912 
   913 in
   914 
   915 fun generic_goal prepp kind before_qed after_qed raw_propp state =
   916   let
   917     val ctxt = context_of state;
   918     val chaining = can assert_chain state;
   919     val pos = Position.thread_data ();
   920 
   921     val ((propss, after_ctxt), goal_state) =
   922       state
   923       |> assert_forward_or_chain
   924       |> enter_forward
   925       |> open_block
   926       |> map_context_result (prepp raw_propp);
   927     val props = flat propss;
   928 
   929     val vars = implicit_vars props;
   930     val propss' = vars :: propss;
   931     val goal_propss = filter_out null propss';
   932     val goal =
   933       Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
   934       |> Thm.cterm_of ctxt
   935       |> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
   936     val statement = ((kind, pos), propss', Thm.term_of goal);
   937     val after_qed' = after_qed |>> (fn after_local =>
   938       fn results => map_context after_ctxt #> after_local results);
   939   in
   940     goal_state
   941     |> map_context (init_context #> Variable.set_body true)
   942     |> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed'))
   943     |> map_context (Proof_Context.auto_bind_goal props)
   944     |> chaining ? (`the_facts #-> using_facts)
   945     |> reset_facts
   946     |> open_block
   947     |> reset_goal
   948     |> enter_backward
   949     |> not (null vars) ? refine_terms (length goal_propss)
   950     |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
   951   end;
   952 
   953 fun generic_qed after_ctxt state =
   954   let
   955     val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state;
   956     val outer_state = state |> close_block;
   957     val outer_ctxt = context_of outer_state;
   958 
   959     val props =
   960       flat (tl stmt)
   961       |> Variable.exportT_terms goal_ctxt outer_ctxt;
   962     val results =
   963       tl (conclude_goal goal_ctxt goal stmt)
   964       |> burrow (Proof_Context.export goal_ctxt outer_ctxt);
   965   in
   966     outer_state
   967     |> map_context (after_ctxt props)
   968     |> pair (after_qed, results)
   969   end;
   970 
   971 end;
   972 
   973 
   974 (* local goals *)
   975 
   976 fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state =
   977   let
   978     val ((names, attss), propp) =
   979       Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
   980 
   981     fun after_qed' results =
   982       local_results ((names ~~ attss) ~~ results)
   983       #-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
   984       #> after_qed results;
   985   in
   986     state
   987     |> generic_goal prepp kind before_qed (after_qed', K I) propp
   988     |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   989   end;
   990 
   991 fun local_qeds arg =
   992   end_proof false arg
   993   #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
   994     (fn ((after_qed, _), results) => after_qed results));
   995 
   996 fun local_qed arg =
   997   local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
   998 
   999 
  1000 (* global goals *)
  1001 
  1002 fun prepp_auto_fixes prepp args =
  1003   prepp args #>
  1004   (fn ((propss, a), ctxt) => ((propss, a), (fold o fold) Variable.auto_fixes propss ctxt));
  1005 
  1006 fun global_goal prepp before_qed after_qed propp =
  1007   init #>
  1008   generic_goal (prepp_auto_fixes prepp) "" before_qed (K I, after_qed) propp;
  1009 
  1010 val theorem = global_goal Proof_Context.bind_propp_schematic;
  1011 val theorem_cmd = global_goal Proof_Context.bind_propp_schematic_cmd;
  1012 
  1013 fun global_qeds arg =
  1014   end_proof true arg
  1015   #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
  1016     after_qed results (context_of state)));
  1017 
  1018 fun global_qed arg =
  1019   global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
  1020 
  1021 
  1022 (* terminal proof steps *)
  1023 
  1024 local
  1025 
  1026 fun terminal_proof qeds initial terminal =
  1027   proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
  1028   #> Seq.the_result "";
  1029 
  1030 in
  1031 
  1032 fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
  1033 val local_default_proof = local_terminal_proof ((Method.default_text, Position.no_range), NONE);
  1034 val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE);
  1035 val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (NONE, false);
  1036 
  1037 fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
  1038 val global_default_proof = global_terminal_proof ((Method.default_text, Position.no_range), NONE);
  1039 val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
  1040 val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);
  1041 
  1042 end;
  1043 
  1044 
  1045 (* skip proofs *)
  1046 
  1047 fun local_skip_proof int state =
  1048   local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
  1049   Skip_Proof.report (context_of state);
  1050 
  1051 fun global_skip_proof int state =
  1052   global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
  1053   Skip_Proof.report (context_of state);
  1054 
  1055 
  1056 (* common goal statements *)
  1057 
  1058 local
  1059 
  1060 fun gen_have prep_att prepp before_qed after_qed stmt int =
  1061   local_goal (Proof_Display.print_results int (Position.thread_data ()))
  1062     prep_att prepp "have" before_qed after_qed stmt;
  1063 
  1064 fun gen_show prep_att prepp before_qed after_qed stmt int state =
  1065   let
  1066     val testing = Unsynchronized.ref false;
  1067     val rule = Unsynchronized.ref (NONE: thm option);
  1068     fun fail_msg ctxt =
  1069       "Local statement fails to refine any pending goal" ::
  1070       (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
  1071       |> cat_lines;
  1072 
  1073     val pos = Position.thread_data ();
  1074     fun print_results ctxt res =
  1075       if ! testing then ()
  1076       else Proof_Display.print_results int pos ctxt res;
  1077     fun print_rule ctxt th =
  1078       if ! testing then rule := SOME th
  1079       else if int then
  1080         Proof_Display.string_of_rule ctxt "Successful" th
  1081         |> Markup.markup Markup.text_fold
  1082         |> Output.state
  1083       else ();
  1084     val test_proof =
  1085       local_skip_proof true
  1086       |> Unsynchronized.setmp testing true
  1087       |> Exn.interruptible_capture;
  1088 
  1089     fun after_qed' results =
  1090       refine_goals print_rule (context_of state) (flat results)
  1091       #> check_result "Failed to refine any pending goal"
  1092       #> after_qed results;
  1093   in
  1094     state
  1095     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
  1096     |> int ? (fn goal_state =>
  1097       (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
  1098         Exn.Res _ => goal_state
  1099       | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
  1100   end;
  1101 
  1102 in
  1103 
  1104 val have = gen_have (K I) Proof_Context.bind_propp;
  1105 val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp_cmd;
  1106 val show = gen_show (K I) Proof_Context.bind_propp;
  1107 val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp_cmd;
  1108 
  1109 end;
  1110 
  1111 
  1112 
  1113 (** future proofs **)
  1114 
  1115 (* relevant proof states *)
  1116 
  1117 fun schematic_goal state =
  1118   let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state
  1119   in Goal.is_schematic prop end;
  1120 
  1121 fun is_relevant state =
  1122   (case try find_goal state of
  1123     NONE => true
  1124   | SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
  1125       Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
  1126 
  1127 
  1128 (* full proofs *)
  1129 
  1130 local
  1131 
  1132 structure Result = Proof_Data
  1133 (
  1134   type T = thm option;
  1135   fun init _ = NONE;
  1136 );
  1137 
  1138 fun the_result ctxt =
  1139   (case Result.get ctxt of
  1140     NONE => error "No result of forked proof"
  1141   | SOME th => th);
  1142 
  1143 val set_result = Result.put o SOME;
  1144 val reset_result = Result.put NONE;
  1145 
  1146 in
  1147 
  1148 fun future_proof fork_proof state =
  1149   let
  1150     val _ = assert_backward state;
  1151     val (goal_ctxt, (_, goal)) = find_goal state;
  1152     val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal;
  1153     val goal_tfrees =
  1154       fold Term.add_tfrees
  1155         (prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) [];
  1156 
  1157     val _ = is_relevant state andalso error "Cannot fork relevant proof";
  1158 
  1159     val prop' = Logic.protect prop;
  1160     val statement' = (kind, [[], [prop']], prop');
  1161     val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) (Goal.protect (Thm.nprems_of goal) goal);
  1162     val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th);
  1163 
  1164     val result_ctxt =
  1165       state
  1166       |> map_context reset_result
  1167       |> map_goal I (K (statement', using, goal', before_qed, after_qed'))
  1168         (fold (Variable.declare_typ o TFree) goal_tfrees)
  1169       |> fork_proof;
  1170 
  1171     val future_thm = Future.map (the_result o snd) result_ctxt;
  1172     val finished_goal = Goal.future_result goal_ctxt future_thm prop';
  1173     val state' =
  1174       state
  1175       |> map_goal I (K (statement, using, finished_goal, NONE, after_qed)) I;
  1176   in (Future.map fst result_ctxt, state') end;
  1177 
  1178 end;
  1179 
  1180 
  1181 (* terminal proofs *)  (* FIXME avoid toplevel imitation -- include in PIDE/document *)
  1182 
  1183 local
  1184 
  1185 fun future_terminal_proof proof1 proof2 done int state =
  1186   if Goal.future_enabled 3 andalso not (is_relevant state) then
  1187     state |> future_proof (fn state' =>
  1188       let
  1189         val pos = Position.thread_data ();
  1190         val props = Markup.command_timing :: (Markup.nameN, "by") :: Position.properties_of pos;
  1191       in
  1192         Execution.fork {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
  1193           (fn () => ((), Timing.protocol props proof2 state'))
  1194       end) |> snd |> done
  1195   else proof1 state;
  1196 
  1197 in
  1198 
  1199 fun local_future_terminal_proof meths =
  1200   future_terminal_proof
  1201     (local_terminal_proof meths)
  1202     (local_terminal_proof meths #> context_of) local_done_proof;
  1203 
  1204 fun global_future_terminal_proof meths =
  1205   future_terminal_proof
  1206     (global_terminal_proof meths)
  1207     (global_terminal_proof meths) global_done_proof;
  1208 
  1209 end;
  1210 
  1211 end;
  1212