# HG changeset patch # User wenzelm # Date 1435670456 -7200 # Node ID 4c79543cc376e047f601ba9bedaa53e8e8ead3ed # Parent 0eb41780449bf9e6a285c5df42d7e64b991d551b renamed "default" to "standard", to make semantically clear what it is; diff -r 0eb41780449b -r 4c79543cc376 NEWS --- 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: diff -r 0eb41780449b -r 4c79543cc376 src/Doc/Isar_Ref/Framework.thy --- 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. diff -r 0eb41780449b -r 4c79543cc376 src/Doc/Isar_Ref/Proof.thy --- 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) \ proof(state) | local_theory | theory"} \\ @{command_def "."} & : & @{text "proof(prove) \ proof(state) | local_theory | theory"} \\ @{command_def "sorry"} & : & @{text "proof(prove) \ 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 \ @@{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} \ @@ -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 diff -r 0eb41780449b -r 4c79543cc376 src/Doc/Isar_Ref/Quick_Reference.thy --- 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 "\"} & @{command "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"} \\ - @{command ".."} & @{text "\"} & @{command "by"}~@{text rule} \\ + @{command ".."} & @{text "\"} & @{command "by"}~@{text standard} \\ @{command "."} & @{text "\"} & @{command "by"}~@{text this} \\ @{command "hence"} & @{text "\"} & @{command "then"}~@{command "have"} \\ @{command "thus"} & @{text "\"} & @{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 "\"} elimination rule (any order) \\ @{method cases}~@{text t} & case analysis (provides cases) \\ @{method induct}~@{text x} & proof by induction (provides cases) \\[2ex] diff -r 0eb41780449b -r 4c79543cc376 src/Provers/classical.ML --- 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)" #> diff -r 0eb41780449b -r 4c79543cc376 src/Pure/Isar/class.ML --- 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)"); diff -r 0eb41780449b -r 4c79543cc376 src/Pure/Isar/method.ML --- 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); diff -r 0eb41780449b -r 4c79543cc376 src/Pure/Isar/proof.ML --- 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);