src/Pure/Isar/proof.ML
changeset 7412 35ebe1452c10
parent 7271 442456b2a8bb
child 7478 02291239d627
equal deleted inserted replaced
7411:4dbff71ac480 7412:35ebe1452c10
    14   val init_state: theory -> state
    14   val init_state: theory -> state
    15   val context_of: state -> context
    15   val context_of: state -> context
    16   val theory_of: state -> theory
    16   val theory_of: state -> theory
    17   val sign_of: state -> Sign.sg
    17   val sign_of: state -> Sign.sg
    18   val the_facts: state -> thm list
    18   val the_facts: state -> thm list
    19   val the_fact: state -> thm
       
    20   val get_goal: state -> thm list * thm
    19   val get_goal: state -> thm list * thm
    21   val goal_facts: (state -> thm list) -> state -> state
    20   val goal_facts: (state -> thm list) -> state -> state
    22   val use_facts: state -> state
    21   val use_facts: state -> state
    23   val reset_facts: state -> state
    22   val reset_facts: state -> state
    24   val assert_forward: state -> state
    23   val assert_forward: state -> state
    25   val assert_backward: state -> state
    24   val assert_backward: state -> state
    26   val enter_forward: state -> state
    25   val enter_forward: state -> state
    27   val show_hyps: bool ref
    26   val show_hyps: bool ref
    28   val pretty_thm: thm -> Pretty.T
    27   val pretty_thm: thm -> Pretty.T
       
    28   val pretty_thms: thm list -> Pretty.T
    29   val verbose: bool ref
    29   val verbose: bool ref
    30   val print_state: int -> state -> unit
    30   val print_state: int -> state -> unit
    31   val level: state -> int
    31   val level: state -> int
    32   type method
    32   type method
    33   val method: (thm list -> tactic) -> method
    33   val method: (thm list -> tactic) -> method
    38   val match_bind: (string list * string) list -> state -> state
    38   val match_bind: (string list * string) list -> state -> state
    39   val match_bind_i: (term list * term) list -> state -> state
    39   val match_bind_i: (term list * term) list -> state -> state
    40   val have_thmss: thm list -> string -> context attribute list ->
    40   val have_thmss: thm list -> string -> context attribute list ->
    41     (thm list * context attribute list) list -> state -> state
    41     (thm list * context attribute list) list -> state -> state
    42   val simple_have_thms: string -> thm list -> state -> state
    42   val simple_have_thms: string -> thm list -> state -> state
    43   val fix: (string * string option) list -> state -> state
    43   val fix: (string list * string option) list -> state -> state
    44   val fix_i: (string * typ) list -> state -> state
    44   val fix_i: (string list * typ) list -> state -> state
    45   val assm: (int -> tactic) * (int -> tactic)
    45   val assm: (int -> tactic) * (int -> tactic)
    46     -> (string * context attribute list * (string * (string list * string list)) list) list
    46     -> (string * context attribute list * (string * (string list * string list)) list) list
    47     -> state -> state
    47     -> state -> state
    48   val assm_i: (int -> tactic) * (int -> tactic)
    48   val assm_i: (int -> tactic) * (int -> tactic)
    49     -> (string * context attribute list * (term * (term list * term list)) list) list
    49     -> (string * context attribute list * (term * (term list * term list)) list) list
   189 (* facts *)
   189 (* facts *)
   190 
   190 
   191 fun the_facts (State (Node {facts = Some facts, ...}, _)) = facts
   191 fun the_facts (State (Node {facts = Some facts, ...}, _)) = facts
   192   | the_facts state = raise STATE ("No current facts available", state);
   192   | the_facts state = raise STATE ("No current facts available", state);
   193 
   193 
   194 fun the_fact state =
       
   195   (case the_facts state of
       
   196     [fact] => fact
       
   197   | _ => raise STATE ("Single fact expected", state));
       
   198 
       
   199 fun assert_facts state = (the_facts state; state);
   194 fun assert_facts state = (the_facts state; state);
   200 fun get_facts (State (Node {facts, ...}, _)) = facts;
   195 fun get_facts (State (Node {facts, ...}, _)) = facts;
   201 
   196 
   202 fun put_facts facts state =
   197 fun put_facts facts state =
   203   state
   198   state
   204   |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
   199   |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
   205   |> put_thms ("facts", if_none facts []);
   200   |> put_thms ("this", if_none facts []);
   206 
   201 
   207 val reset_facts = put_facts None;
   202 val reset_facts = put_facts None;
   208 
   203 
   209 fun have_facts (name, facts) state =
   204 fun have_facts (name, facts) state =
   210   state
   205   state
   286 (** print_state **)
   281 (** print_state **)
   287 
   282 
   288 val show_hyps = ProofContext.show_hyps;
   283 val show_hyps = ProofContext.show_hyps;
   289 val pretty_thm = ProofContext.pretty_thm;
   284 val pretty_thm = ProofContext.pretty_thm;
   290 
   285 
       
   286 fun pretty_thms [th] = pretty_thm th
       
   287   | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
       
   288 
       
   289 
   291 val verbose = ProofContext.verbose;
   290 val verbose = ProofContext.verbose;
   292 
   291 
   293 fun print_facts _ None = ()
   292 fun print_facts _ None = ()
   294   | print_facts s (Some ths) =
   293   | print_facts s (Some ths) =
   295       Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths));
   294       Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths));
   301     fun levels_up 0 = ""
   300     fun levels_up 0 = ""
   302       | levels_up 1 = " (1 level up)"
   301       | levels_up 1 = " (1 level up)"
   303       | levels_up i = " (" ^ string_of_int i ^ " levels up)";
   302       | levels_up i = " (" ^ string_of_int i ^ " levels up)";
   304 
   303 
   305     fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
   304     fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
   306       (print_facts "Using" (if null goal_facts then None else Some goal_facts);
   305       (print_facts "Using"
       
   306           (if mode <> Backward orelse null goal_facts then None else Some goal_facts);
   307         writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
   307         writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
   308         Locale.print_goals_marker begin_goal (! goals_limit) thm);
   308         Locale.print_goals_marker begin_goal (! goals_limit) thm);
   309 
   309 
   310     val ctxt_strings = ProofContext.strings_of_context context;
   310     val ctxt_strings = ProofContext.strings_of_context context;
   311   in
   311   in
   585   let
   585   let
   586     val (state', prop) =
   586     val (state', prop) =
   587       state
   587       state
   588       |> assert_forward_or_chain
   588       |> assert_forward_or_chain
   589       |> enter_forward
   589       |> enter_forward
   590       |> opt_block
       
   591       |> map_context_result (fn c => prepp (c, raw_propp));
   590       |> map_context_result (fn c => prepp (c, raw_propp));
   592     val cprop = Thm.cterm_of (sign_of state') prop;
   591     val cprop = Thm.cterm_of (sign_of state') prop;
   593     val casms = map #1 (assumptions state');
   592     val casms = map #1 (assumptions state');
   594 
   593 
   595     val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl;
   594     val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl;
   596     fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Drule.assume_goal casm COMP revcut_rl) RS thm);
   595     fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Drule.assume_goal casm COMP revcut_rl) RS thm);
   597     val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
   596     val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
   598   in
   597   in
   599     state'
   598     state'
       
   599     |> opt_block
   600     |> put_goal (Some (((kind atts, (PureThy.default_name name), prop), ([], goal)), after_qed))
   600     |> put_goal (Some (((kind atts, (PureThy.default_name name), prop), ([], goal)), after_qed))
   601     |> auto_bind_goal prop
   601     |> auto_bind_goal prop
   602     |> (if is_chain state then use_facts else reset_facts)
   602     |> (if is_chain state then use_facts else reset_facts)
   603     |> new_block
   603     |> new_block
   604     |> enter_backward
   604     |> enter_backward