src/Pure/Isar/proof.ML
changeset 8234 36a85a6c4852
parent 8206 e50a130ec9af
child 8239 07f25f7d2218
equal deleted inserted replaced
8233:85169951d515 8234:36a85a6c4852
    40   val print_state: int -> state -> unit
    40   val print_state: int -> state -> unit
    41   val level: state -> int
    41   val level: state -> int
    42   type method
    42   type method
    43   val method: (thm list -> tactic) -> method
    43   val method: (thm list -> tactic) -> method
    44   val refine: (context -> method) -> state -> state Seq.seq
    44   val refine: (context -> method) -> state -> state Seq.seq
       
    45   val refine_end: (context -> method) -> state -> state Seq.seq
    45   val find_free: term -> string -> term option
    46   val find_free: term -> string -> term option
    46   val export_thm: context -> thm -> thm
    47   val export_thm: context -> thm -> thm
    47   val match_bind: (string list * string) list -> state -> state
    48   val match_bind: (string list * string) list -> state -> state
    48   val match_bind_i: (term list * term) list -> state -> state
    49   val match_bind_i: (term list * term) list -> state -> state
    49   val have_thmss: thm list -> string -> context attribute list ->
    50   val have_thmss: thm list -> string -> context attribute list ->
   344 val method = Method;
   345 val method = Method;
   345 
   346 
   346 
   347 
   347 (* refine goal *)
   348 (* refine goal *)
   348 
   349 
       
   350 local
       
   351 
   349 fun check_sign sg state =
   352 fun check_sign sg state =
   350   if Sign.subsig (sg, sign_of state) then state
   353   if Sign.subsig (sg, sign_of state) then state
   351   else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
   354   else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
   352 
   355 
   353 fun refine meth_fun state =
   356 fun gen_refine current_context meth_fun state =
   354   let
   357   let
   355     val Method meth = meth_fun (context_of state);
   358     val (goal_ctxt, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
   356     val (_, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
   359     val Method meth = meth_fun (if current_context then context_of state else goal_ctxt);
   357 
   360 
   358     fun refn thm' =
   361     fun refn thm' =
   359       state
   362       state
   360       |> check_sign (Thm.sign_of_thm thm')
   363       |> check_sign (Thm.sign_of_thm thm')
   361       |> map_goal (K ((result, (facts, thm')), f));
   364       |> map_goal (K ((result, (facts, thm')), f));
   362   in Seq.map refn (meth facts thm) end;
   365   in Seq.map refn (meth facts thm) end;
       
   366 
       
   367 in
       
   368 
       
   369 val refine = gen_refine true;
       
   370 val refine_end = gen_refine false;
       
   371 
       
   372 end;
   363 
   373 
   364 
   374 
   365 (* export *)
   375 (* export *)
   366 
   376 
   367 fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None
   377 fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None