src/Pure/Isar/proof.ML
changeset 6950 ab6d35b7283f
parent 6932 77c14313af51
child 6982 4d2a3f35af93
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Jul 09 18:45:15 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Jul 09 18:46:51 1999 +0200
     1.3 @@ -72,8 +72,8 @@
     1.4    val at_bottom: state -> bool
     1.5    val local_qed: (state -> state Seq.seq) -> ({kind: string, name: string, thm: thm} -> unit)
     1.6      -> state -> state Seq.seq
     1.7 -  val global_qed: (state -> state Seq.seq) -> bstring option -> theory attribute list option
     1.8 -    -> state -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
     1.9 +  val global_qed: (state -> state Seq.seq) -> state
    1.10 +    -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
    1.11    val begin_block: state -> state
    1.12    val end_block: state -> state Seq.seq
    1.13    val next_block: state -> state
    1.14 @@ -395,10 +395,10 @@
    1.15  fun RANGE [] _ = all_tac
    1.16    | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
    1.17  
    1.18 -fun export_goal raw_rule inner_state state =
    1.19 +fun export_goal raw_rule inner state =
    1.20    let
    1.21      val (outer, (_, (result, (facts, thm)))) = find_goal 0 state;
    1.22 -    val (exp, tacs) = export_wrt (context_of inner_state) (Some outer);
    1.23 +    val (exp, tacs) = export_wrt inner (Some outer);
    1.24      val rule = exp raw_rule;
    1.25      val thmq = FIRSTGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm;
    1.26    in Seq.map (fn th => map_goal (K (result, (facts, th))) state) thmq end;
    1.27 @@ -575,7 +575,7 @@
    1.28      val casms = map #1 (assumptions state');
    1.29  
    1.30      val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl;
    1.31 -    fun cut_asm (casm, thm) = (Thm.assume casm COMP revcut_rl) RS thm;
    1.32 +    fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Thm.assume casm COMP revcut_rl) RS thm);
    1.33      val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
    1.34    in
    1.35      state'
    1.36 @@ -612,7 +612,7 @@
    1.37  
    1.38  (* current goal *)
    1.39  
    1.40 -fun current_goal (State ({goal = Some goal, ...}, _)) = goal
    1.41 +fun current_goal (State ({context, goal = Some goal, ...}, _)) = (context, goal)
    1.42    | current_goal state = raise STATE ("No current goal!", state);
    1.43  
    1.44  fun assert_current_goal true (state as State ({goal = None, ...}, _)) =
    1.45 @@ -641,11 +641,11 @@
    1.46  
    1.47  fun finish_local print_result state =
    1.48    let
    1.49 -    val ((kind, name, t), (_, raw_thm)) = current_goal state;
    1.50 +    val (ctxt, ((kind, name, t), (_, raw_thm))) = current_goal state;
    1.51      val result = prep_result state t raw_thm;
    1.52      val (atts, opt_solve) =
    1.53        (case kind of
    1.54 -        Goal atts => (atts, export_goal result state)
    1.55 +        Goal atts => (atts, export_goal result ctxt)
    1.56        | Aux atts => (atts, Seq.single)
    1.57        | _ => err_malformed "finish_local" state);
    1.58    in
    1.59 @@ -666,27 +666,26 @@
    1.60  
    1.61  (* global_qed *)
    1.62  
    1.63 -fun finish_global alt_name alt_atts state =
    1.64 +fun finish_global state =
    1.65    let
    1.66 -    val ((kind, def_name, t), (_, raw_thm)) = current_goal state;
    1.67 +    val (_, ((kind, name, t), (_, raw_thm))) = current_goal state;
    1.68      val result = final_result state (prep_result state t raw_thm);
    1.69  
    1.70 -    val name = if_none alt_name def_name;
    1.71      val atts =
    1.72        (case kind of
    1.73 -        Theorem atts => if_none alt_atts atts
    1.74 -      | Lemma atts => (if_none alt_atts atts) @ [Drule.tag_lemma]
    1.75 +        Theorem atts => atts
    1.76 +      | Lemma atts => atts @ [Drule.tag_lemma]
    1.77        | _ => err_malformed "finish_global" state);
    1.78  
    1.79      val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
    1.80    in (thy', {kind = kind_name kind, name = name, thm = result'}) end;
    1.81  
    1.82  (*Note: should inspect first result only, backtracking may destroy theory*)
    1.83 -fun global_qed finalize alt_name alt_atts state =
    1.84 +fun global_qed finalize state =
    1.85    state
    1.86    |> end_proof true
    1.87    |> finalize
    1.88 -  |> Seq.map (finish_global alt_name alt_atts);
    1.89 +  |> Seq.map finish_global;
    1.90  
    1.91  
    1.92