local goals: after_qed;
authorwenzelm
Thu Aug 05 22:08:53 1999 +0200 (1999-08-05)
changeset 7176a329a37ed91a
parent 7175 8263d0b50e12
child 7177 6bb7ad30f3da
local goals: after_qed;
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Aug 04 18:20:24 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Aug 05 22:08:53 1999 +0200
     1.3 @@ -295,14 +295,14 @@
     1.4  val presume_i   = local_statement_i Proof.presume_i I o Comment.ignore;
     1.5  val local_def   = local_statement LocalDefs.def I o Comment.ignore;
     1.6  val local_def_i = local_statement LocalDefs.def_i I o Comment.ignore;
     1.7 -val show        = local_statement Proof.show I o Comment.ignore;
     1.8 -val show_i      = local_statement_i Proof.show_i I o Comment.ignore;
     1.9 -val have        = local_statement Proof.have I o Comment.ignore;
    1.10 -val have_i      = local_statement_i Proof.have_i I o Comment.ignore;
    1.11 -val thus        = local_statement Proof.show Proof.chain o Comment.ignore;
    1.12 -val thus_i      = local_statement_i Proof.show_i Proof.chain o Comment.ignore;
    1.13 -val hence       = local_statement Proof.have Proof.chain o Comment.ignore;
    1.14 -val hence_i     = local_statement_i Proof.have_i Proof.chain o Comment.ignore;
    1.15 +val show        = local_statement (Proof.show Seq.single) I o Comment.ignore;
    1.16 +val show_i      = local_statement_i (Proof.show_i Seq.single) I o Comment.ignore;
    1.17 +val have        = local_statement (Proof.have Seq.single) I o Comment.ignore;
    1.18 +val have_i      = local_statement_i (Proof.have_i Seq.single) I o Comment.ignore;
    1.19 +val thus        = local_statement (Proof.show Seq.single) Proof.chain o Comment.ignore;
    1.20 +val thus_i      = local_statement_i (Proof.show_i Seq.single) Proof.chain o Comment.ignore;
    1.21 +val hence       = local_statement (Proof.have Seq.single) Proof.chain o Comment.ignore;
    1.22 +val hence_i     = local_statement_i (Proof.have_i Seq.single) Proof.chain o Comment.ignore;
    1.23  
    1.24  
    1.25  (* blocks *)
     2.1 --- a/src/Pure/Isar/proof.ML	Wed Aug 04 18:20:24 1999 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Thu Aug 05 22:08:53 1999 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    val sign_of: state -> Sign.sg
     2.5    val the_facts: state -> thm list
     2.6    val the_fact: state -> thm
     2.7 +  val get_goal: state -> thm list * thm
     2.8    val goal_facts: (state -> thm list) -> state -> state
     2.9    val use_facts: state -> state
    2.10    val reset_facts: state -> state
    2.11 @@ -64,14 +65,14 @@
    2.12    val chain: state -> state
    2.13    val export_chain: state -> state Seq.seq
    2.14    val from_facts: thm list -> state -> state
    2.15 -  val show: string -> context attribute list -> string * (string list * string list)
    2.16 -    -> state -> state
    2.17 -  val show_i: string -> context attribute list -> term * (term list * term list)
    2.18 -    -> state -> state
    2.19 -  val have: string -> context attribute list -> string * (string list * string list)
    2.20 -    -> state -> state
    2.21 -  val have_i: string -> context attribute list -> term * (term list * term list)
    2.22 -    -> state -> state
    2.23 +  val show: (state -> state Seq.seq) -> string -> context attribute list
    2.24 +    -> string * (string list * string list) -> state -> state
    2.25 +  val show_i: (state -> state Seq.seq) -> string -> context attribute list
    2.26 +    -> term * (term list * term list) -> state -> state
    2.27 +  val have: (state -> state Seq.seq) -> string -> context attribute list
    2.28 +    -> string * (string list * string list) -> state -> state
    2.29 +  val have_i: (state -> state Seq.seq) -> string -> context attribute list
    2.30 +    -> term * (term list * term list) -> state -> state
    2.31    val at_bottom: state -> bool
    2.32    val local_qed: (state -> state Seq.seq)
    2.33      -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) -> state -> state Seq.seq
    2.34 @@ -125,25 +126,23 @@
    2.35      (fn Forward => "state" | ForwardChain => "chain" | Backward => "prove");
    2.36  
    2.37  
    2.38 -(* type node *)
    2.39 -
    2.40 -type node =
    2.41 - {context: context,
    2.42 -  facts: thm list option,
    2.43 -  mode: mode,
    2.44 -  goal: goal option};
    2.45 -
    2.46 -fun make_node (context, facts, mode, goal) =
    2.47 -  {context = context, facts = facts, mode = mode, goal = goal}: node;
    2.48 -
    2.49 -
    2.50  (* datatype state *)
    2.51  
    2.52 -datatype state =
    2.53 +datatype node =
    2.54 +  Node of
    2.55 +   {context: context,
    2.56 +    facts: thm list option,
    2.57 +    mode: mode,
    2.58 +    goal: (goal * (state -> state Seq.seq)) option}
    2.59 +and state =
    2.60    State of
    2.61      node *              (*current*)
    2.62      node list;          (*parents wrt. block structure*)
    2.63  
    2.64 +fun make_node (context, facts, mode, goal) =
    2.65 +  Node {context = context, facts = facts, mode = mode, goal = goal};
    2.66 +
    2.67 +
    2.68  exception STATE of string * state;
    2.69  
    2.70  fun err_malformed name state =
    2.71 @@ -155,7 +154,7 @@
    2.72    | Some s_sq => Seq.cons s_sq);
    2.73  
    2.74  
    2.75 -fun map_current f (State ({context, facts, mode, goal}, nodes)) =
    2.76 +fun map_current f (State (Node {context, facts, mode, goal}, nodes)) =
    2.77    State (make_node (f (context, facts, mode, goal)), nodes);
    2.78  
    2.79  fun init_state thy =
    2.80 @@ -167,13 +166,13 @@
    2.81  
    2.82  (* context *)
    2.83  
    2.84 -fun context_of (State ({context, ...}, _)) = context;
    2.85 +fun context_of (State (Node {context, ...}, _)) = context;
    2.86  val theory_of = ProofContext.theory_of o context_of;
    2.87  val sign_of = ProofContext.sign_of o context_of;
    2.88  
    2.89  fun map_context f = map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
    2.90  
    2.91 -fun map_context_result f (state as State ({context, facts, mode, goal}, nodes)) =
    2.92 +fun map_context_result f (state as State (Node {context, facts, mode, goal}, nodes)) =
    2.93    let val (context', result) = f context
    2.94    in (State (make_node (context', facts, mode, goal), nodes), result) end;
    2.95  
    2.96 @@ -190,7 +189,7 @@
    2.97  
    2.98  (* facts *)
    2.99  
   2.100 -fun the_facts (State ({facts = Some facts, ...}, _)) = facts
   2.101 +fun the_facts (State (Node {facts = Some facts, ...}, _)) = facts
   2.102    | the_facts state = raise STATE ("No current facts available", state);
   2.103  
   2.104  fun the_fact state =
   2.105 @@ -199,7 +198,7 @@
   2.106    | _ => raise STATE ("Single fact expected", state));
   2.107  
   2.108  fun assert_facts state = (the_facts state; state);
   2.109 -fun get_facts (State ({facts, ...}, _)) = facts;
   2.110 +fun get_facts (State (Node {facts, ...}, _)) = facts;
   2.111  
   2.112  fun put_facts facts state =
   2.113    state
   2.114 @@ -218,14 +217,18 @@
   2.115  
   2.116  (* goal *)
   2.117  
   2.118 -fun find_goal i (state as State ({goal = Some goal, ...}, _)) = (context_of state, (i, goal))
   2.119 -  | find_goal i (State ({goal = None, ...}, node :: nodes)) =
   2.120 +fun find_goal i (state as State (Node {goal = Some goal, ...}, _)) = (context_of state, (i, goal))
   2.121 +  | find_goal i (State (Node {goal = None, ...}, node :: nodes)) =
   2.122        find_goal (i + 1) (State (node, nodes))
   2.123    | find_goal _ (state as State (_, [])) = err_malformed "find_goal" state;
   2.124  
   2.125 +fun get_goal state =
   2.126 +  let val (_, (_, ((_, goal), _))) = find_goal 0 state
   2.127 +  in goal end;
   2.128 +
   2.129  fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
   2.130  
   2.131 -fun map_goal f (State ({context, facts, mode, goal = Some goal}, nodes)) =
   2.132 +fun map_goal f (State (Node {context, facts, mode, goal = Some goal}, nodes)) =
   2.133        State (make_node (context, facts, mode, Some (f goal)), nodes)
   2.134    | map_goal f (State (nd, node :: nodes)) =
   2.135        let val State (node', nodes') = map_goal f (State (node, nodes))
   2.136 @@ -234,7 +237,7 @@
   2.137  
   2.138  fun goal_facts get state =
   2.139    state
   2.140 -  |> map_goal (fn (result, (_, thm)) => (result, (get state, thm)));
   2.141 +  |> map_goal (fn ((result, (_, thm)), f) => ((result, (get state, thm)), f));
   2.142  
   2.143  fun use_facts state =
   2.144    state
   2.145 @@ -244,7 +247,7 @@
   2.146  
   2.147  (* mode *)
   2.148  
   2.149 -fun get_mode (State ({mode, ...}, _)) = mode;
   2.150 +fun get_mode (State (Node {mode, ...}, _)) = mode;
   2.151  fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
   2.152  
   2.153  val enter_forward = put_mode Forward;
   2.154 @@ -292,7 +295,7 @@
   2.155    | print_facts s (Some ths) =
   2.156        Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths));
   2.157  
   2.158 -fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
   2.159 +fun print_state (state as State (Node {context, facts, mode, goal = _}, nodes)) =
   2.160    let
   2.161      val ref (_, _, begin_goal) = Goals.current_goals_markers;
   2.162  
   2.163 @@ -300,7 +303,7 @@
   2.164        | levels_up 1 = " (1 level up)"
   2.165        | levels_up i = " (" ^ string_of_int i ^ " levels up)";
   2.166  
   2.167 -    fun print_goal (_, (i, ((kind, name, _), (goal_facts, thm)))) =
   2.168 +    fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) =
   2.169        (print_facts "Using" (if null goal_facts then None else Some goal_facts);
   2.170          writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
   2.171          Locale.print_goals_marker begin_goal (! goals_limit) thm);
   2.172 @@ -335,15 +338,15 @@
   2.173    if Sign.subsig (sg, sign_of state) then state
   2.174    else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
   2.175  
   2.176 -fun refine meth_fun (state as State ({context, ...}, _)) =
   2.177 +fun refine meth_fun state =
   2.178    let
   2.179 -    val Method meth = meth_fun context;
   2.180 -    val (_, (_, (result, (facts, thm)))) = find_goal 0 state;
   2.181 +    val Method meth = meth_fun (context_of state);
   2.182 +    val (_, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
   2.183  
   2.184      fun refn thm' =
   2.185        state
   2.186        |> check_sign (Thm.sign_of_thm thm')
   2.187 -      |> map_goal (K (result, (facts, thm')));
   2.188 +      |> map_goal (K ((result, (facts, thm')), f));
   2.189    in Seq.map refn (meth facts thm) end;
   2.190  
   2.191  
   2.192 @@ -403,12 +406,12 @@
   2.193  
   2.194  fun export_goal print_rule raw_rule inner state =
   2.195    let
   2.196 -    val (outer, (_, (result, (facts, thm)))) = find_goal 0 state;
   2.197 +    val (outer, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
   2.198      val (exp, tacs) = export_wrt inner (Some outer);
   2.199      val rule = exp raw_rule;
   2.200      val _ = print_rule rule;
   2.201      val thmq = FIRSTGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm;
   2.202 -  in Seq.map (fn th => map_goal (K (result, (facts, th))) state) thmq end;
   2.203 +  in Seq.map (fn th => map_goal (K ((result, (facts, th)), f)) state) thmq end;
   2.204  
   2.205  
   2.206  fun export_thm inner thm =
   2.207 @@ -573,7 +576,7 @@
   2.208  
   2.209  (* setup goals *)
   2.210  
   2.211 -fun setup_goal opt_block prepp kind name atts raw_propp state =
   2.212 +fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
   2.213    let
   2.214      val (state', prop) =
   2.215        state
   2.216 @@ -589,7 +592,7 @@
   2.217      val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
   2.218    in
   2.219      state'
   2.220 -    |> put_goal (Some ((kind atts, (PureThy.default_name name), prop), ([], goal)))
   2.221 +    |> put_goal (Some (((kind atts, (PureThy.default_name name), prop), ([], goal)), after_qed))
   2.222      |> auto_bind_goal prop
   2.223      |> (if is_chain state then use_facts else reset_facts)
   2.224      |> new_block
   2.225 @@ -599,7 +602,7 @@
   2.226  
   2.227  (*global goals*)
   2.228  fun global_goal prep kind name atts x thy =
   2.229 -  setup_goal I prep kind name atts x (init_state thy);
   2.230 +  setup_goal I prep kind Seq.single name atts x (init_state thy);
   2.231  
   2.232  val theorem = global_goal ProofContext.bind_propp Theorem;
   2.233  val theorem_i = global_goal ProofContext.bind_propp_i Theorem;
   2.234 @@ -608,8 +611,8 @@
   2.235  
   2.236  
   2.237  (*local goals*)
   2.238 -fun local_goal prep kind name atts x =
   2.239 -  setup_goal open_block prep kind name atts x;
   2.240 +fun local_goal prep kind f name atts x =
   2.241 +  setup_goal open_block prep kind f name atts x;
   2.242  
   2.243  val show   = local_goal ProofContext.bind_propp Goal;
   2.244  val show_i = local_goal ProofContext.bind_propp_i Goal;
   2.245 @@ -622,12 +625,12 @@
   2.246  
   2.247  (* current goal *)
   2.248  
   2.249 -fun current_goal (State ({context, goal = Some goal, ...}, _)) = (context, goal)
   2.250 +fun current_goal (State (Node {context, goal = Some goal, ...}, _)) = (context, goal)
   2.251    | current_goal state = raise STATE ("No current goal!", state);
   2.252  
   2.253 -fun assert_current_goal true (state as State ({goal = None, ...}, _)) =
   2.254 +fun assert_current_goal true (state as State (Node {goal = None, ...}, _)) =
   2.255        raise STATE ("No goal in this block!", state)
   2.256 -  | assert_current_goal false (state as State ({goal = Some _, ...}, _)) =
   2.257 +  | assert_current_goal false (state as State (Node {goal = Some _, ...}, _)) =
   2.258        raise STATE ("Goal present in this block!", state)
   2.259    | assert_current_goal _ state = state;
   2.260  
   2.261 @@ -652,7 +655,7 @@
   2.262  
   2.263  fun finish_local (print_result, print_rule) state =
   2.264    let
   2.265 -    val (ctxt, ((kind, name, t), (_, raw_thm))) = current_goal state;
   2.266 +    val (ctxt, (((kind, name, t), (_, raw_thm)), after_qed)) = current_goal state;
   2.267      val result = prep_result state t raw_thm;
   2.268      val (atts, opt_solve) =
   2.269        (case kind of
   2.270 @@ -666,6 +669,7 @@
   2.271      |> auto_bind_facts name [t]
   2.272      |> have_thmss [] name atts [Thm.no_attributes [result]]
   2.273      |> opt_solve
   2.274 +    |> (Seq.flat o Seq.map after_qed)
   2.275    end;
   2.276  
   2.277  fun local_qed finalize print state =
   2.278 @@ -679,7 +683,7 @@
   2.279  
   2.280  fun finish_global state =
   2.281    let
   2.282 -    val (_, ((kind, name, t), (_, raw_thm))) = current_goal state;
   2.283 +    val (_, (((kind, name, t), (_, raw_thm)), _)) = current_goal state;   (*ignores after_qed!*)
   2.284      val result = final_result state (prep_result state t raw_thm);
   2.285  
   2.286      val atts =