--- a/src/Doc/IsarImplementation/Tactic.thy Wed Jun 26 09:58:39 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy Wed Jun 26 11:54:45 2013 +0200
@@ -53,8 +53,10 @@
with protected propositions:
\[
- \infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad
- \infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}
+ \infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}
+ \]
+ \[
+ \infer[@{text "(conclude)"}]{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> C"}}{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> #C"}}
\]
*}
@@ -62,7 +64,7 @@
\begin{mldecls}
@{index_ML Goal.init: "cterm -> thm"} \\
@{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
- @{index_ML Goal.protect: "thm -> thm"} \\
+ @{index_ML Goal.protect: "int -> thm -> thm"} \\
@{index_ML Goal.conclude: "thm -> thm"} \\
\end{mldecls}
@@ -76,8 +78,9 @@
result by removing the goal protection. The context is only
required for printing error messages.
- \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement
- of theorem @{text "thm"}.
+ \item @{ML "Goal.protect"}~@{text "n thm"} protects the statement
+ of theorem @{text "thm"}. The parameter @{text n} indicates the
+ number of premises to be retained.
\item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
protection, even if there are pending subgoals.
--- a/src/HOL/Tools/Function/function_core.ML Wed Jun 26 09:58:39 2013 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Wed Jun 26 11:54:45 2013 +0200
@@ -425,7 +425,7 @@
val goalstate = Conjunction.intr graph_is_function complete
|> Thm.close_derivation
- |> Goal.protect
+ |> Goal.protect 0
|> fold_rev (Thm.implies_intr o cprop_of) compat
|> Thm.implies_intr (cprop_of complete)
in
--- a/src/Pure/Isar/obtain.ML Wed Jun 26 09:58:39 2013 +0200
+++ b/src/Pure/Isar/obtain.ML Wed Jun 26 11:54:45 2013 +0200
@@ -301,7 +301,7 @@
fun print_result ctxt' (k, [(s, [_, th])]) =
Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
- (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
+ (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
fun after_qed [[_, res]] =
Proof.end_block #> guess_context (check_result ctxt thesis res);
in
--- a/src/Pure/Isar/proof.ML Wed Jun 26 09:58:39 2013 +0200
+++ b/src/Pure/Isar/proof.ML Wed Jun 26 11:54:45 2013 +0200
@@ -1133,8 +1133,7 @@
val prop' = Logic.protect prop;
val statement' = (kind, [[], [prop']], prop');
- val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
- (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
+ val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) (Goal.protect (Thm.nprems_of goal) goal);
val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th);
val result_ctxt =
--- a/src/Pure/goal.ML Wed Jun 26 09:58:39 2013 +0200
+++ b/src/Pure/goal.ML Wed Jun 26 11:54:45 2013 +0200
@@ -19,7 +19,7 @@
sig
include BASIC_GOAL
val init: cterm -> thm
- val protect: thm -> thm
+ val protect: int -> thm -> thm
val conclude: thm -> thm
val check_finished: Proof.context -> thm -> thm
val finish: Proof.context -> thm -> thm
@@ -73,11 +73,11 @@
in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end;
(*
- C
- --- (protect)
- #C
+ A1 ==> ... ==> An ==> C
+ ------------------------ (protect n)
+ A1 ==> ... ==> An ==> #C
*)
-fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI;
+fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI;
(*
A ==> ... ==> #C