'.' == by this;
authorwenzelm
Sat Feb 05 16:54:27 2000 +0100 (2000-02-05)
changeset 8195af2575a5c5ae
parent 8194 0c5d9d23b715
child 8196 ecb9decd38ac
'.' == by this;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/refcard.tex
src/Pure/Isar/method.ML
     1.1 --- a/doc-src/IsarRef/generic.tex	Fri Feb 04 21:53:36 2000 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sat Feb 05 16:54:27 2000 +0100
     1.3 @@ -3,12 +3,14 @@
     1.4  
     1.5  \section{Basic proof methods}\label{sec:pure-meth}
     1.6  
     1.7 -\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
     1.8 +\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}
     1.9 +\indexisarmeth{assumption}\indexisarmeth{this}
    1.10  \indexisarmeth{fold}\indexisarmeth{unfold}
    1.11  \indexisarmeth{rule}\indexisarmeth{erule}
    1.12  \begin{matharray}{rcl}
    1.13    - & : & \isarmeth \\
    1.14    assumption & : & \isarmeth \\
    1.15 +  this & : & \isarmeth \\
    1.16    rule & : & \isarmeth \\
    1.17    erule^* & : & \isarmeth \\[0.5ex]
    1.18    fold & : & \isarmeth \\
    1.19 @@ -29,8 +31,9 @@
    1.20    plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
    1.21    $\PROOFNAME$ alone.
    1.22  \item [$assumption$] solves some goal by assumption.  Any facts given are
    1.23 -  guaranteed to participate in the refinement.  Note that ``$\DOT$'' (dot)
    1.24 -  abbreviates $\BY{assumption}$.
    1.25 +  guaranteed to participate in the refinement.
    1.26 +\item [$this$] applies the current facts directly as rules.  Note that
    1.27 +  ``$\DOT$'' (dot) abbreviates $\BY{this}$.
    1.28  \item [$rule~thms$] applies some rule given as argument in backward manner;
    1.29    facts are used to reduce the rule before applying it to the goal.  Thus
    1.30    $rule$ without facts is plain \emph{introduction}, while with facts it
     2.1 --- a/doc-src/IsarRef/pure.tex	Fri Feb 04 21:53:36 2000 +0100
     2.2 +++ b/doc-src/IsarRef/pure.tex	Sat Feb 05 16:54:27 2000 +0100
     2.3 @@ -718,7 +718,7 @@
     2.4  \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
     2.5    abbreviates $\BY{default}$.
     2.6  \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
     2.7 -  abbreviates $\BY{assumption}$.
     2.8 +  abbreviates $\BY{this}$.
     2.9  \item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};
    2.10    provided that the \texttt{quick_and_dirty} flag is enabled,
    2.11    $\isarkeyword{sorry}$ pretends to solve the goal without further ado.  Of
     3.1 --- a/doc-src/IsarRef/refcard.tex	Fri Feb 04 21:53:36 2000 +0100
     3.2 +++ b/doc-src/IsarRef/refcard.tex	Sat Feb 05 16:54:27 2000 +0100
     3.3 @@ -41,7 +41,7 @@
     3.4  \begin{matharray}{rcl}
     3.5    \BYY{m@1}{m@2} & \equiv & \PROOF{m@1}~\QED{m@2} \\
     3.6    \DDOT & \equiv & \BY{rule} \\
     3.7 -  \DOT & \equiv & \BY{assumption} \\
     3.8 +  \DOT & \equiv & \BY{this} \\
     3.9    \HENCENAME & \equiv & \THEN~\HAVENAME \\
    3.10    \THUSNAME & \equiv & \THEN~\SHOWNAME \\
    3.11    \FROM{a@1\;\dots\;a@n} & \equiv & \NOTE{this}{a@1\;\dots\;a@n}~\THEN \\
    3.12 @@ -79,6 +79,7 @@
    3.13  \begin{tabular}{ll}
    3.14    \multicolumn{2}{l}{\textbf{Single steps (forward-chaining facts)}} \\[0.5ex]
    3.15    $assumption$ & apply some assumption \\
    3.16 +  $this$ & apply current facts \\
    3.17    $rule~a@1\;\dots\;a@n$ & apply some rule  \\
    3.18    $rule$ & apply standard rule (default for $\PROOFNAME$) \\
    3.19    $induct~x$ & apply induction rule \\
     4.1 --- a/src/Pure/Isar/method.ML	Fri Feb 04 21:53:36 2000 +0100
     4.2 +++ b/src/Pure/Isar/method.ML	Sat Feb 05 16:54:27 2000 +0100
     4.3 @@ -41,6 +41,7 @@
     4.4    val erule_tac: thm list -> thm list -> int -> tactic
     4.5    val rule: thm list -> Proof.method
     4.6    val erule: thm list -> Proof.method
     4.7 +  val this: Proof.method
     4.8    val assumption: Proof.context -> Proof.method
     4.9    exception METHOD_FAIL of (string * Position.T) * exn
    4.10    val help_methods: theory option -> unit
    4.11 @@ -281,7 +282,12 @@
    4.12  end;
    4.13  
    4.14  
    4.15 -(* assumption / finish *)
    4.16 +(* this *)
    4.17 +
    4.18 +val this = METHOD (EVERY o map (FINDGOAL o Tactic.rtac));
    4.19 +
    4.20 +
    4.21 +(* assumption *)
    4.22  
    4.23  fun assm_tac ctxt =
    4.24    assume_tac APPEND' resolve_tac (filter Thm.no_prems (ProofContext.prems_of ctxt));
    4.25 @@ -291,7 +297,6 @@
    4.26    | assumption_tac _ _ = K no_tac;
    4.27  
    4.28  fun assumption ctxt = METHOD (FINDGOAL o assumption_tac ctxt);
    4.29 -fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac)));
    4.30  
    4.31  
    4.32  
    4.33 @@ -458,6 +463,9 @@
    4.34  (* structured proof steps *)
    4.35  
    4.36  val default_text = Source (Args.src (("default", []), Position.none));
    4.37 +val this_text = Basic (K this);
    4.38 +
    4.39 +fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac)));
    4.40  
    4.41  fun finish_text None = Basic finish
    4.42    | finish_text (Some txt) = Then [txt, Basic finish];
    4.43 @@ -470,7 +478,7 @@
    4.44  
    4.45  fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_text));
    4.46  fun local_terminal_proof (text, opt_text) pr = Seq.THEN (proof (Some text), local_qed opt_text pr);
    4.47 -val local_immediate_proof = local_terminal_proof (Basic assumption, None);
    4.48 +val local_immediate_proof = local_terminal_proof (this_text, None);
    4.49  val local_default_proof = local_terminal_proof (default_text, None);
    4.50  
    4.51  
    4.52 @@ -490,7 +498,7 @@
    4.53    |> Proof.check_result "Failed to finish proof (after successful terminal method)" state
    4.54    |> Seq.hd;
    4.55  
    4.56 -val global_immediate_proof = global_terminal_proof (Basic assumption, None);
    4.57 +val global_immediate_proof = global_terminal_proof (this_text, None);
    4.58  val global_default_proof = global_terminal_proof (default_text, None);
    4.59  
    4.60  
    4.61 @@ -509,6 +517,7 @@
    4.62    ("default", thms_ctxt_args some_rule, "apply some rule"),
    4.63    ("rule", thms_ctxt_args some_rule, "apply some rule"),
    4.64    ("erule", thms_ctxt_args some_erule, "apply some erule (improper!)"),
    4.65 +  ("this", no_args this, "apply current facts as rules"),
    4.66    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts")];
    4.67  
    4.68