--- a/NEWS Tue Jun 30 10:40:42 2015 +0200
+++ b/NEWS Tue Jun 30 15:20:56 2015 +0200
@@ -97,6 +97,11 @@
INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
and always put attributes in front.
+* The standard proof method of commands 'proof' and '..' is now called
+"standard" to make semantically clear what it is; the old name "default"
+is still available as legacy for some time. Documentation now explains
+'..' more accurately as "by standard" instead of "by rule".
+
* Proof method "goals" turns the current subgoals into cases within the
context; the conclusion is bound to variable ?case in each case.
For example:
--- a/src/Doc/Isar_Ref/Framework.thy Tue Jun 30 10:40:42 2015 +0200
+++ b/src/Doc/Isar_Ref/Framework.thy Tue Jun 30 15:20:56 2015 +0200
@@ -531,13 +531,13 @@
@{attribute (Pure) dest}, followed by those declared as @{attribute
(Pure) intro}.
- The default method for @{command proof} is ``@{method (Pure) rule}''
+ The default method for @{command proof} is ``@{method standard}''
(arguments picked from the context), for @{command qed} it is
- ``@{method "-"}''. Further abbreviations for terminal proof steps
+ ``@{method "succeed"}''. Further abbreviations for terminal proof steps
are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for
``@{command proof}~@{text "method\<^sub>1"}~@{command qed}~@{text
"method\<^sub>2"}'', and ``@{command ".."}'' for ``@{command
- "by"}~@{method (Pure) rule}, and ``@{command "."}'' for ``@{command
+ "by"}~@{method standard}, and ``@{command "."}'' for ``@{command
"by"}~@{method this}''. The @{command unfolding} element operates
directly on the current facts and goal by applying equalities.
--- a/src/Doc/Isar_Ref/Proof.thy Tue Jun 30 10:40:42 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Tue Jun 30 15:20:56 2015 +0200
@@ -706,6 +706,7 @@
@{command_def ".."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
@{command_def "."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
@{command_def "sorry"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
+ @{method_def standard} & : & @{text method} \\
\end{matharray}
Arbitrary goal refinement via tactics is considered harmful.
@@ -740,11 +741,11 @@
an intelligible manner.
Unless given explicitly by the user, the default initial method is
- @{method_ref (Pure) rule} (or its classical variant @{method_ref
- rule}), which applies a single standard elimination or introduction
- rule according to the topmost symbol involved. There is no separate
- default terminal method. Any remaining goals are always solved by
- assumption in the very last step.
+ @{method standard}, which subsumes at least @{method_ref (Pure) rule} or
+ its classical variant @{method_ref (HOL) rule}. These methods apply a
+ single standard elimination or introduction rule according to the topmost
+ logical connective involved. There is no separate default terminal method.
+ Any remaining goals are always solved by assumption in the very last step.
@{rail \<open>
@@{command proof} method?
@@ -784,9 +785,9 @@
@{text "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
problem.
- \item ``@{command ".."}'' is a \emph{default
- proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
- "rule"}.
+ \item ``@{command ".."}'' is a \emph{standard
+ proof}\index{proof!standard}; it abbreviates @{command "by"}~@{text
+ "standard"}.
\item ``@{command "."}'' is a \emph{trivial
proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
@@ -803,6 +804,19 @@
The most important application of @{command "sorry"} is to support
experimentation and top-down proof development.
+ \item @{method standard} refers to the default refinement step of some
+ Isar language elements (notably @{command proof} and ``@{command ".."}'').
+ It is \emph{dynamically scoped}, so the behaviour depends on the
+ application environment.
+
+ In Isabelle/Pure, @{method standard} performs elementary introduction~/
+ elimination steps (@{method_ref (Pure) rule}), introduction of type
+ classes (@{method_ref intro_classes}) and locales (@{method_ref
+ intro_locales}).
+
+ In Isabelle/HOL, @{method standard} also takes classical rules into
+ account (cf.\ \secref{sec:classical}).
+
\end{description}
\<close>
@@ -910,12 +924,12 @@
before applying it to the goal. Thus @{method (Pure) rule} without facts
is plain introduction, while with facts it becomes elimination.
- When no arguments are given, the @{method (Pure) rule} method tries to pick
- appropriate rules automatically, as declared in the current context
- using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
- @{attribute (Pure) dest} attributes (see below). This is the
- default behavior of @{command "proof"} and ``@{command ".."}''
- (double-dot) steps (see \secref{sec:proof-steps}).
+ When no arguments are given, the @{method (Pure) rule} method tries to
+ pick appropriate rules automatically, as declared in the current context
+ using the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute
+ (Pure) dest} attributes (see below). This is included in the standard
+ behaviour of @{command "proof"} and ``@{command ".."}'' (double-dot) steps
+ (see \secref{sec:proof-steps}).
\item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
@{attribute (Pure) dest} declare introduction, elimination, and
--- a/src/Doc/Isar_Ref/Quick_Reference.thy Tue Jun 30 10:40:42 2015 +0200
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy Tue Jun 30 15:20:56 2015 +0200
@@ -53,7 +53,7 @@
\begin{tabular}{rcl}
@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} & @{text "\<equiv>"} &
@{command "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"} \\
- @{command ".."} & @{text "\<equiv>"} & @{command "by"}~@{text rule} \\
+ @{command ".."} & @{text "\<equiv>"} & @{command "by"}~@{text standard} \\
@{command "."} & @{text "\<equiv>"} & @{command "by"}~@{text this} \\
@{command "hence"} & @{text "\<equiv>"} & @{command "then"}~@{command "have"} \\
@{command "thus"} & @{text "\<equiv>"} & @{command "then"}~@{command "show"} \\
@@ -116,7 +116,7 @@
@{method assumption} & apply some assumption \\
@{method this} & apply current facts \\
@{method rule}~@{text a} & apply some rule \\
- @{method rule} & apply standard rule (default for @{command "proof"}) \\
+ @{method standard} & apply standard rule (default for @{command "proof"}) \\
@{method contradiction} & apply @{text "\<not>"} elimination rule (any order) \\
@{method cases}~@{text t} & case analysis (provides cases) \\
@{method induct}~@{text x} & proof by induction (provides cases) \\[2ex]
--- a/src/Provers/classical.ML Tue Jun 30 10:40:42 2015 +0200
+++ b/src/Provers/classical.ML Tue Jun 30 15:20:56 2015 +0200
@@ -917,9 +917,16 @@
fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
| rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts;
-fun default_tac ctxt rules facts =
+fun standard_tac ctxt rules facts =
HEADGOAL (rule_tac ctxt rules facts) ORELSE
- Class.default_intro_tac ctxt facts;
+ Class.standard_intro_classes_tac ctxt facts;
+
+fun default_tac rules ctxt facts st =
+ (if Method.detect_closure_state st then
+ legacy_feature
+ ("Old method \"default\"; use \"standard\" instead" ^ Position.here (Position.thread_data ()))
+ else ();
+ standard_tac rules ctxt facts st);
end;
@@ -944,9 +951,12 @@
val _ =
Theory.setup
- (Method.setup @{binding default}
+ (Method.setup @{binding standard}
+ (Attrib.thms >> (fn rules => fn ctxt => METHOD (standard_tac ctxt rules)))
+ "standard proof step: classical intro/elim rule or class introduction" #>
+ Method.setup @{binding default}
(Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
- "apply some intro/elim rule (potentially classical)" #>
+ "standard proof step: classical intro/elim rule or class introduction (legacy)" #>
Method.setup @{binding rule}
(Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
"apply some intro/elim rule (potentially classical)" #>
--- a/src/Pure/Isar/class.ML Tue Jun 30 10:40:42 2015 +0200
+++ b/src/Pure/Isar/class.ML Tue Jun 30 15:20:56 2015 +0200
@@ -48,7 +48,7 @@
(*tactics*)
val intro_classes_tac: Proof.context -> thm list -> tactic
- val default_intro_tac: Proof.context -> thm list -> tactic
+ val standard_intro_classes_tac: Proof.context -> thm list -> tactic
(*diagnostics*)
val pretty_specification: theory -> class -> Pretty.T list
@@ -743,6 +743,7 @@
end;
+
(** tactics and methods **)
fun intro_classes_tac ctxt facts st =
@@ -756,20 +757,29 @@
Method.intros_tac ctxt (class_trivs @ class_intros @ assm_intros) facts st
end;
-fun default_intro_tac ctxt [] =
- COND Thm.no_prems no_tac
- (intro_classes_tac ctxt [] ORELSE Locale.intro_locales_tac true ctxt [])
- | default_intro_tac _ _ = no_tac;
+fun standard_intro_classes_tac ctxt facts st =
+ if null facts andalso not (Thm.no_prems st) then
+ (intro_classes_tac ctxt [] ORELSE Locale.intro_locales_tac true ctxt []) st
+ else no_tac st;
-fun default_tac rules ctxt facts =
+fun standard_tac rules ctxt facts =
HEADGOAL (Method.some_rule_tac ctxt rules facts) ORELSE
- default_intro_tac ctxt facts;
+ standard_intro_classes_tac ctxt facts;
+
+fun default_tac rules ctxt facts st =
+ (if Method.detect_closure_state st then
+ legacy_feature
+ ("Old method \"default\"; use \"standard\" instead" ^ Position.here (Position.thread_data ()))
+ else ();
+ standard_tac rules ctxt facts st);
val _ = Theory.setup
(Method.setup @{binding intro_classes} (Scan.succeed (METHOD o intro_classes_tac))
"back-chain introduction rules of classes" #>
+ Method.setup @{binding standard} (Attrib.thms >> (METHOD oo standard_tac))
+ "standard proof step: Pure intro/elim rule or class introduction" #>
Method.setup @{binding default} (Attrib.thms >> (METHOD oo default_tac))
- "apply some intro/elim rule");
+ "standard proof step: Pure intro/elim rule or class introduction (legacy)");
--- a/src/Pure/Isar/method.ML Tue Jun 30 10:40:42 2015 +0200
+++ b/src/Pure/Isar/method.ML Tue Jun 30 15:20:56 2015 +0200
@@ -50,7 +50,7 @@
val map_source: (Token.src -> Token.src) -> text -> text
val primitive_text: (Proof.context -> thm -> thm) -> text
val succeed_text: text
- val default_text: text
+ val standard_text: text
val this_text: text
val done_text: text
val sorry_text: bool -> text
@@ -335,7 +335,7 @@
fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
val succeed_text = Basic (K succeed);
-val default_text = Source (Token.src ("default", Position.none) []);
+val standard_text = Source (Token.src ("standard", Position.none) []);
val this_text = Basic this;
val done_text = Basic (K (SIMPLE_METHOD all_tac));
fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
--- a/src/Pure/Isar/proof.ML Tue Jun 30 10:40:42 2015 +0200
+++ b/src/Pure/Isar/proof.ML Tue Jun 30 15:20:56 2015 +0200
@@ -845,7 +845,7 @@
fun proof opt_text =
assert_backward
- #> refine (the_default Method.default_text opt_text)
+ #> refine (the_default Method.standard_text opt_text)
#> Seq.map
(using_facts []
#> enter_forward
@@ -1109,12 +1109,12 @@
in
fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
-val local_default_proof = local_terminal_proof ((Method.default_text, Position.no_range), NONE);
+val local_default_proof = local_terminal_proof ((Method.standard_text, Position.no_range), NONE);
val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE);
val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (NONE, false);
fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
-val global_default_proof = global_terminal_proof ((Method.default_text, Position.no_range), NONE);
+val global_default_proof = global_terminal_proof ((Method.standard_text, Position.no_range), NONE);
val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);