# HG changeset patch # User wenzelm # Date 1434984507 -7200 # Node ID 2b8342b0d98cbb5c1d059be46b25778d73f86cba # Parent a31374738b7d6a4a3bc1446947fefe3f9a97ce4b clarified nesting of Isar goal structure; tuned message; diff -r a31374738b7d -r 2b8342b0d98c NEWS --- a/NEWS Mon Jun 22 11:35:30 2015 +0200 +++ b/NEWS Mon Jun 22 16:48:27 2015 +0200 @@ -62,6 +62,19 @@ then show ?thesis qed +* Nesting of Isar goal structure has been clarified: the context after +the initial backwards refinement is retained for the whole proof, within +all its context sections (as indicated via 'next'). This is e.g. +relevant for 'using', 'including', 'supply': + + have "A \ A" if a: A for A + supply [simp] = a + proof + show A by simp + next + show A by simp + qed + *** Pure *** diff -r a31374738b7d -r 2b8342b0d98c src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Jun 22 11:35:30 2015 +0200 +++ b/src/Pure/Isar/proof.ML Mon Jun 22 16:48:27 2015 +0200 @@ -392,9 +392,7 @@ val position_markup = Position.markup (Position.thread_data ()) Markup.position; in [Pretty.block - [Pretty.mark_str (position_markup, "proof"), - Pretty.str (" (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1))], - Pretty.str ""] @ + [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @ (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @ (if verbose orelse mode = Forward then pretty_sep (pretty_facts ctxt "" facts) (prt_goal (try find_goal state)) @@ -841,7 +839,11 @@ fun proof opt_text = assert_backward #> refine (the_default Method.default_text opt_text) - #> Seq.map (using_facts [] #> enter_forward); + #> Seq.map + (using_facts [] + #> enter_forward + #> open_block + #> reset_goal); fun proof_results arg = Seq.APPEND (proof (Method.text arg) #> Seq.make_results, @@ -925,17 +927,11 @@ val chaining = can assert_chain state; val pos = Position.thread_data (); - val goal_state = - state - |> assert_forward_or_chain - |> enter_forward - |> open_block - |> map_context (K goal_ctxt); val goal_props = flat goal_propss; - val vars = implicit_vars goal_props; val propss' = vars :: goal_propss; val goal_propss = filter_out null propss'; + val goal = Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss) |> Thm.cterm_of goal_ctxt @@ -945,15 +941,19 @@ val after_qed' = after_qed |>> (fn after_local => fn results => map_context (fold Variable.maybe_bind_term result_binds) #> after_local results); in - goal_state - |> map_context (init_context #> Variable.set_body true) + state + |> assert_forward_or_chain + |> enter_forward + |> open_block + |> enter_backward + |> map_context + (K goal_ctxt + #> init_context + #> Variable.set_body true + #> Proof_Context.auto_bind_goal goal_props) |> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed')) - |> map_context (Proof_Context.auto_bind_goal goal_props) |> chaining ? (`the_facts #-> using_facts) |> reset_facts - |> open_block - |> reset_goal - |> enter_backward |> not (null vars) ? refine_terms (length goal_propss) |> null goal_props ? (refine (Method.Basic Method.assumption) #> Seq.hd) end;