--- a/doc-src/IsarRef/generic.tex Fri Feb 04 21:53:36 2000 +0100
+++ b/doc-src/IsarRef/generic.tex Sat Feb 05 16:54:27 2000 +0100
@@ -3,12 +3,14 @@
\section{Basic proof methods}\label{sec:pure-meth}
-\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
+\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}
+\indexisarmeth{assumption}\indexisarmeth{this}
\indexisarmeth{fold}\indexisarmeth{unfold}
\indexisarmeth{rule}\indexisarmeth{erule}
\begin{matharray}{rcl}
- & : & \isarmeth \\
assumption & : & \isarmeth \\
+ this & : & \isarmeth \\
rule & : & \isarmeth \\
erule^* & : & \isarmeth \\[0.5ex]
fold & : & \isarmeth \\
@@ -29,8 +31,9 @@
plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
$\PROOFNAME$ alone.
\item [$assumption$] solves some goal by assumption. Any facts given are
- guaranteed to participate in the refinement. Note that ``$\DOT$'' (dot)
- abbreviates $\BY{assumption}$.
+ guaranteed to participate in the refinement.
+\item [$this$] applies the current facts directly as rules. Note that
+ ``$\DOT$'' (dot) abbreviates $\BY{this}$.
\item [$rule~thms$] applies some rule given as argument in backward manner;
facts are used to reduce the rule before applying it to the goal. Thus
$rule$ without facts is plain \emph{introduction}, while with facts it
--- a/doc-src/IsarRef/pure.tex Fri Feb 04 21:53:36 2000 +0100
+++ b/doc-src/IsarRef/pure.tex Sat Feb 05 16:54:27 2000 +0100
@@ -718,7 +718,7 @@
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
abbreviates $\BY{default}$.
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
- abbreviates $\BY{assumption}$.
+ abbreviates $\BY{this}$.
\item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};
provided that the \texttt{quick_and_dirty} flag is enabled,
$\isarkeyword{sorry}$ pretends to solve the goal without further ado. Of
--- a/doc-src/IsarRef/refcard.tex Fri Feb 04 21:53:36 2000 +0100
+++ b/doc-src/IsarRef/refcard.tex Sat Feb 05 16:54:27 2000 +0100
@@ -41,7 +41,7 @@
\begin{matharray}{rcl}
\BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\
\DDOT & \equiv & \BY{rule} \\
- \DOT & \equiv & \BY{assumption} \\
+ \DOT & \equiv & \BY{this} \\
\HENCENAME & \equiv & \THEN~\HAVENAME \\
\THUSNAME & \equiv & \THEN~\SHOWNAME \\
\FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\
@@ -79,6 +79,7 @@
\begin{tabular}{ll}
\multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
$assumption$ & apply some assumption \\
+ $this$ & apply current facts \\
$rule~a@1\;\dots\;a@n$ & apply some rule \\
$rule$ & apply standard rule (default for $\PROOFNAME$) \\
$induct~x$ & apply induction rule \\
--- a/src/Pure/Isar/method.ML Fri Feb 04 21:53:36 2000 +0100
+++ b/src/Pure/Isar/method.ML Sat Feb 05 16:54:27 2000 +0100
@@ -41,6 +41,7 @@
val erule_tac: thm list -> thm list -> int -> tactic
val rule: thm list -> Proof.method
val erule: thm list -> Proof.method
+ val this: Proof.method
val assumption: Proof.context -> Proof.method
exception METHOD_FAIL of (string * Position.T) * exn
val help_methods: theory option -> unit
@@ -281,7 +282,12 @@
end;
-(* assumption / finish *)
+(* this *)
+
+val this = METHOD (EVERY o map (FINDGOAL o Tactic.rtac));
+
+
+(* assumption *)
fun assm_tac ctxt =
assume_tac APPEND' resolve_tac (filter Thm.no_prems (ProofContext.prems_of ctxt));
@@ -291,7 +297,6 @@
| assumption_tac _ _ = K no_tac;
fun assumption ctxt = METHOD (FINDGOAL o assumption_tac ctxt);
-fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac)));
@@ -458,6 +463,9 @@
(* structured proof steps *)
val default_text = Source (Args.src (("default", []), Position.none));
+val this_text = Basic (K this);
+
+fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac)));
fun finish_text None = Basic finish
| finish_text (Some txt) = Then [txt, Basic finish];
@@ -470,7 +478,7 @@
fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_text));
fun local_terminal_proof (text, opt_text) pr = Seq.THEN (proof (Some text), local_qed opt_text pr);
-val local_immediate_proof = local_terminal_proof (Basic assumption, None);
+val local_immediate_proof = local_terminal_proof (this_text, None);
val local_default_proof = local_terminal_proof (default_text, None);
@@ -490,7 +498,7 @@
|> Proof.check_result "Failed to finish proof (after successful terminal method)" state
|> Seq.hd;
-val global_immediate_proof = global_terminal_proof (Basic assumption, None);
+val global_immediate_proof = global_terminal_proof (this_text, None);
val global_default_proof = global_terminal_proof (default_text, None);
@@ -509,6 +517,7 @@
("default", thms_ctxt_args some_rule, "apply some rule"),
("rule", thms_ctxt_args some_rule, "apply some rule"),
("erule", thms_ctxt_args some_erule, "apply some erule (improper!)"),
+ ("this", no_args this, "apply current facts as rules"),
("assumption", ctxt_args assumption, "proof by assumption, preferring facts")];