Quelle  Isar.thy

(*:maxLineLen=78:*)

theory Isar
imports Base
begin

chapter ‹Isar language elements›

text ‹
 The Isar proof language (see also cite‹‹\S2› in "isabelle-isar-ref"›)
 consists of three main categories of language elements:

 🪙 Proof 🪙‹commands› define the primary language of transactions of the
 underlying Isar/VM interpreter. Typical examples are @{command "fix"},
 @{command "assume"}, @{command "show"}, @{command "proof"}, and @{command
 "qed"}.

 Composing proof commands according to the rules of the Isar/VM leads to
 expressions of structured proof text, such that both the machine and the
 human reader can give it a meaning as formal reasoning.

 🪙 Proof 🪙‹methods› define a secondary language of mixed forward-backward
 refinement steps involving facts and goals. Typical examples are @{method
 rule}, @{method unfold}, and @{method simp}.

 Methods can occur in certain well-defined parts of the Isar proof language,
 say as arguments to @{command "proof"}, @{command "qed"}, or @{command
 "by"}.

 🪙 🪙‹Attributes› define a tertiary language of small annotations to theorems
 being defined or referenced. Attributes can modify both the context and the
 theorem.

 Typical examples are @{attribute intro} (which affects the context), and
 @{attribute symmetric} (which affects the theorem).
 ›


section ‹Proof commands›

text ‹
 A 🪙‹proof command› is state transition of the Isar/VM proof interpreter.

 In principle, Isar proof commands could be defined in user-space as well.
 The system is built like that in the first place: one part of the commands
 are primitive, the other part is defined as derived elements. Adding to the
 genuine structured proof language requires profound understanding of the
 Isar/VM machinery, though, so this is beyond the scope of this manual.

 What can be done realistically is to define some diagnostic commands that
 inspect the general state of the Isar/VM, and report some feedback to the
 user. Typically this involves checking of the linguistic 🪙‹mode› of a proof
 state, or peeking at the pending goals (if available).

 Another common application is to define a toplevel command that poses a
 problem to the user as Isar proof state and processes the final result
 relatively to the context. Thus a proof can be incorporated into the context
 of some user-space tool, without modifying the Isar proof language itself.
 ›

text %mlref ‹
 \begin{mldecls}
 @{define_ML_type Proof.state} \\
 @{define_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\
 @{define_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\
 @{define_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\
 @{define_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\
 @{define_ML Proof.goal: "Proof.state ->
 {context: Proof.context, facts: thm list, goal: thm}"} \\
 @{define_ML Proof.raw_goal: "Proof.state ->
 {context: Proof.context, facts: thm list, goal: thm}"} \\
 @{define_ML Proof.theorem: "Method.text option ->
 (thm list list -> Proof.context -> Proof.context) ->
 (term * term list) list list -> Proof.context -> Proof.state"} \\
 \end{mldecls}

 🪙 Type 🪙‹Proof.state› represents Isar proof states. This is a
 block-structured configuration with proof context, linguistic mode, and
 optional goal. The latter consists of goal context, goal facts
 (``‹using›''), and tactical goal state (see \secref{sec:tactical-goals}).

 The general idea is that the facts shall contribute to the refinement of
 some parts of the tactical goal --- how exactly is defined by the proof
 method that is applied in that situation.

 🪙 🪙‹Proof.assert_forward›, 🪙‹Proof.assert_chain›, 🪙‹Proof.assert_backward› are partial identity functions that fail unless a
 certain linguistic mode is active, namely ``‹proof(state)›'',
 ``‹proof(chain)›'', ``‹proof(prove)›'', respectively (using the terminology
 of cite‹"isabelle-isar-ref"›).

 It is advisable study the implementations of existing proof commands for
 suitable modes to be asserted.

 🪙 🪙‹Proof.simple_goal›~‹state› returns the structured Isar goal (if
 available) in the form seen by ``simple'' methods (like @{method simp} or
 @{method blast}). The Isar goal facts are already inserted as premises into
 the subgoals, which are presented individually as in 🪙‹Proof.goal›.

 🪙 🪙‹Proof.goal›~‹state› returns the structured Isar goal (if available)
 in the form seen by regular methods (like @{method rule}). The auxiliary
 internal encoding of Pure conjunctions is split into individual subgoals as
 usual.

 🪙 🪙‹Proof.raw_goal›~‹state› returns the structured Isar goal (if
 available) in the raw internal form seen by ``raw'' methods (like @{method
 induct}). This form is rarely appropriate for diagnostic tools; 🪙‹Proof.simple_goal› or 🪙‹Proof.goal› should be used in most situations.

 🪙 🪙‹Proof.theorem›~‹before_qed after_qed statement ctxt› initializes a
 toplevel Isar proof state within a given context.

 The optional ‹before_qed› method is applied at the end of the proof, just
 before extracting the result (this feature is rarely used).

 The ‹after_qed› continuation receives the extracted result in order to apply
 it to the final context in a suitable way (e.g.\ storing named facts). Note
 that at this generic level the target context is specified as 🪙‹Proof.context›, but the usual wrapping of toplevel proofs into command
 transactions will provide a 🪙‹local_theory› here
 (\chref{ch:local-theory}). This affects the way how results are stored.

 The ‹statement› is given as a nested list of terms, each associated with
 optional @{keyword "is"} patterns as usual in the Isar source language. The
 original nested list structure over terms is turned into one over theorems
 when ‹after_qed› is invoked.
 ›


text %mlantiq ‹
 \begin{matharray}{rcl}
 @{ML_antiquotation_def "Isar.goal"} & : & ‹ML_antiquotation› \\
 \end{matharray}

 🪙 ‹@{Isar.goal}› refers to the regular goal state (if available) of the
 current proof state managed by the Isar toplevel --- as abstract value.

 This only works for diagnostic ML commands, such as @{command ML_val} or
 @{command ML_command}.
 ›

text %mlex ‹
 The following example peeks at a certain goal configuration.
 ›

notepad
begin
  have A and B and C
    ML_val
     ‹val n = Thm.nprems_of (#goal @{Isar.goal});
 🍋 (n = 3);›
    sorry
end

text ‹
 Here we see 3 individual subgoals in the same way as regular proof methods
 would do.
 ›


section ‹Proof methods›

text ‹
 A ‹method› is a function ‹thm^* → context * goal → (context × goal)^**›
 that operates on the full Isar goal configuration with context, goal facts,
 and tactical goal state and enumerates possible follow-up goal states. Under
 normal circumstances, the goal context remains unchanged, but it is also
 possible to declare named extensions of the proof context (🪙‹cases›).

java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 \secref{sec:tactics}). The well-formedness conditions for tactics need to
 hold for methods accordingly, with the following additions.

 ▪ Goal addressing is further limited either to operate uniformly on 🪙‹all›
 subgoals, or specifically on the 🪙‹first› subgoal.

 Exception: old-style tactic emulations that are embedded into the method
 space, e.g.\ @{method rule_tac}.

 ▪ A non-trivial method always needs to make progress: an identical follow-up
 goal state has to be avoided.🪙‹This enables the user to write method
 expressions like ‹meth⁺› without looping, while the trivial do-nothing case
 can be recovered via ‹meth^?›.›

 Exception: trivial stuttering steps, such as ``@{method -}'' or @{method
 succeed}.

 ▪ Goal facts passed to the method must not be ignored. If there is no
 sensible use of facts outside the goal state, facts should be inserted into
 the subgoals that are addressed by the method.


 🪙
 Syntactically, the language of proof methods appears as arguments to Isar
 commands like @{command "by"} or @{command apply}. User-space additions are
 reasonably easy by plugging suitable method-valued parser functions into the
 framework, using the @{command method_setup} command, for example.

 To get a better idea about the range of possibilities, consider the
 following Isar proof schemes. This is the general form of structured proof
 text:

 🪙
 \begin{tabular}{l}
 @{command from}~‹facts₁›~@{command have}~‹props›~@{command using}~‹facts₂› \\
 @{command proof}~‹(initial_method)› \\
 \quad‹body› \\
 @{command qed}~‹(terminal_method)› \\
 \end{tabular}
 🪙

 The goal configuration consists of ‹facts₁› and ‹facts₂› appended in that
 order, and various ‹props› being claimed. The ‹initial_method› is invoked
 with facts and goals together and refines the problem to something that is
 handled recursively in the proof ‹body›. The ‹terminal_method› has another
 chance to finish any remaining subgoals, but it does not see the facts of
 the initial step.

 🪙
 This pattern illustrates unstructured proof scripts:

 🪙
 \begin{tabular}{l}
 @{command have}~‹props› \\
 \quad@{command using}~‹facts₁›~@{command apply}~‹method₁› \\
 \quad@{command apply}~‹method₂› \\
 \quad@{command using}~‹facts₃›~@{command apply}~‹method₃› \\
 \quad@{command done} \\
 \end{tabular}
 🪙

 The ‹method₁› operates on the original claim while using ‹facts₁›. Since
 the @{command apply} command structurally resets the facts, the ‹method₂›
 will operate on the remaining goal state without facts. The ‹method₃› will
 see again a collection of ‹facts₃› that has been inserted into the script
 explicitly.

 🪙
 Empirically, any Isar proof method can be categorized as follows.

 🪙 🪙‹Special method with cases› with named context additions associated
 with the follow-up goal state.

 Example: @{method "induct"}, which is also a ``raw'' method since it
 operates on the internal representation of simultaneous claims as Pure
 conjunction (\secref{sec:logic-aux}), instead of separate subgoals
 (\secref{sec:tactical-goals}).

 🪙 🪙‹Structured method› with strong emphasis on facts outside the goal
 state.

 Example: @{method "rule"}, which captures the key ideas behind structured
 reasoning in Isar in its purest form.

 🪙 🪙‹Simple method› with weaker emphasis on facts, which are inserted into
 subgoals to emulate old-style tactical ``premises''.

 Examples: @{method "simp"}, @{method "blast"}, @{method "auto"}.

 🪙 🪙‹Old-style tactic emulation› with detailed numeric goal addressing and
 explicit references to entities of the internal goal state (which are
 otherwise invisible from proper Isar proof text). The naming convention
 ‹foo_tac› makes this special non-standard status clear.

 Example: @{method "rule_tac"}.

 When implementing proof methods, it is advisable to study existing
 implementations carefully and imitate the typical ``boiler plate'' for
 context-sensitive parsing and further combinators to wrap-up tactic
 expressions as methods.🪙‹Aliases or abbreviations of the standard method
 combinators should be avoided.›
 ›

text %mlref ‹
 \begin{mldecls}
 @{define_ML_type Proof.method} \\
 @{define_ML CONTEXT_METHOD: "(thm list -> context_tactic) -> Proof.method"} \\
 @{define_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\
 @{define_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\
 @{define_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\
 @{define_ML Method.insert_tac: "Proof.context -> thm list -> int -> tactic"} \\
 @{define_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser ->
 string -> theory -> theory"} \\
 \end{mldecls}

 🪙 Type 🪙‹Proof.method› represents proof methods as abstract type.

 🪙 🪙‹CONTEXT_METHOD›~‹(fn facts => context_tactic)› wraps ‹context_tactic›
 depending on goal facts as a general proof method that may change the proof
 context dynamically. A typical operation is 🪙‹Proof_Context.update_cases›, which is wrapped up as combinator @{define_ML
 CONTEXT_CASES} for convenience.

 🪙 🪙‹METHOD›~‹(fn facts => tactic)› wraps ‹tactic› depending on goal facts
 as regular proof method; the goal context is passed via method syntax.

 🪙 🪙‹SIMPLE_METHOD›~‹tactic› wraps a tactic that addresses all subgoals
 uniformly as simple proof method. Goal facts are already inserted into all
 subgoals before ‹tactic› is applied.

 🪙 🪙‹SIMPLE_METHOD'›~‹tactic› wraps a tactic that addresses a specific
 subgoal as simple proof method that operates on subgoal 1. Goal facts are
 inserted into the subgoal then the ‹tactic› is applied.

 🪙 🪙‹Method.insert_tac›~‹ctxt facts i› inserts ‹facts› into subgoal ‹i›.
 This is convenient to reproduce part of the 🪙‹SIMPLE_METHOD› or 🪙‹SIMPLE_METHOD'› wrapping within regular 🪙‹METHOD›, for example.

 🪙 🪙‹Method.setup›~‹name parser description› provides the functionality of
 the Isar command @{command method_setup} as ML function.
 ›

text %mlex ‹
 See also @{command method_setup} in cite‹"isabelle-isar-ref"› which
 includes some abstract examples.

 🪙
 The following toy examples illustrate how the goal facts and state are
 passed to proof methods. The predefined proof method called ``@{method
 tactic}'' wraps ML source of type 🪙‹tactic› (abstracted over
 🪙‹facts›). This allows immediate experimentation without parsing of
 concrete syntax.
 ›

notepad
begin
  fix A B :: bool
  assume a: A and b: B

  have "A ∧ B"
    apply (tactic ‹resolve_tac 🍋 @{thms conjI} 1›)
    using a apply (tactic ‹resolve_tac 🍋 facts 1›)
    using b apply (tactic ‹resolve_tac 🍋 facts 1›)
    done

  have "A ∧ B"
    using a and b
    ML_val ‹@{Isar.goal}›
    apply (tactic ‹Method.insert_tac 🍋 facts 1›)
    apply (tactic ‹(resolve_tac 🍋 @{thms conjI} THEN_ALL_NEW assume_tac 🍋) 1›)
    done
end

text ‹
 🪙
 The next example implements a method that simplifies the first subgoal by
 rewrite rules that are given as arguments.
 ›

method_setup my_simp =
  ‹Attrib.thms >> (fn thms => fn ctxt =>
 SIMPLE_METHOD' (fn i =>
 CHANGED (asm_full_simp_tac
 (put_simpset HOL_basic_ss ctxt addsimps thms) i)))›
  "rewrite subgoal by given rules"

text ‹
 The concrete syntax wrapping of @{command method_setup} always
 passes-through the proof context at the end of parsing, but it is not used
 in this example.

 The 🪙‹Attrib.thms› parser produces a list of theorems from the usual Isar
 syntax involving attribute expressions etc.\ (syntax category @{syntax
 thms}) cite‹"isabelle-isar-ref"›. The resulting 🪙‹thms› are
 added to 🪙‹HOL_basic_ss› which already contains the basic Simplifier
 setup for HOL.

 The tactic 🪙‹asm_full_simp_tac› is the one that is also used in method
 @{method simp} by default. The extra wrapping by the 🪙‹CHANGED› tactical
 ensures progress of simplification: identical goal states are filtered out
 explicitly to make the raw tactic conform to standard Isar method behaviour.

 🪙
 Method @{method my_simp} can be used in Isar proofs like this:
 ›

notepad
begin
  fix a b c :: 'a
  assume a: "a = b"
  assume b: "b = c"
  have "a = c" by (my_simp a b)
end

text ‹
 Here is a similar method that operates on all subgoals, instead of just the
 first one.›

method_setup my_simp_all =
  ‹Attrib.thms >> (fn thms => fn ctxt =>
 SIMPLE_METHOD
 (CHANGED
 (ALLGOALS (asm_full_simp_tac
 (put_simpset HOL_basic_ss ctxt addsimps thms)))))›
  "rewrite all subgoals by given rules"

notepad
begin
  fix a b c :: 'a
  assume a: "a = b"
  assume b: "b = c"
  have "a = c" and "c = b" by (my_simp_all a b)
end

text ‹
 🪙
 Apart from explicit arguments, common proof methods typically work with a
 default configuration provided by the context. As a shortcut to rule
 management we use a cheap solution via the @{command named_theorems} command
 to declare a dynamic fact in the context.
 ›

named_theorems my_simp

text ‹
 The proof method is now defined as before, but we append the explicit
 arguments and the rules from the context.
 ›

method_setup my_simp' =
  ‹Attrib.thms >> (fn thms => fn ctxt =>
 let
 val my_simps = Named_Theorems.get ctxt 🍋‹my_simp›
 in
 SIMPLE_METHOD' (fn i =>
 CHANGED (asm_full_simp_tac
 (put_simpset HOL_basic_ss ctxt
 addsimps (thms @ my_simps)) i))
 end)›
  "rewrite subgoal by given rules and my_simp rules from the context"

text ‹
 🪙
 Method @{method my_simp'} can be used in Isar proofs like this:
 ›

notepad
begin
  fix a b c :: 'a
  assume [my_simp]: "a ≡ b"
  assume [my_simp]: "b ≡ c"
  have "a ≡ c" by my_simp'
end

text ‹
 🪙
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 the goal facts are merely inserted as goal premises by the 🪙‹SIMPLE_METHOD'› or 🪙‹SIMPLE_METHOD› wrapper. For proof methods that are
 similar to the standard collection of @{method simp}, @{method blast},
 @{method fast}, @{method auto} there is little more that can be done.

 Note that using the primary goal facts in the same manner as the method
 arguments obtained via concrete syntax or the context does not meet the
 requirement of ``strong emphasis on facts'' of regular proof methods,
 because rewrite rules as used above can be easily ignored. A proof text
 ``@{command using}~‹foo›~@{command "by"}~‹my_simp›'' where ‹foo› is not used
 would deceive the reader.

 🪙
 The technical treatment of rules from the context requires further
 attention. Above we rebuild a fresh 🪙‹simpset› from the arguments
 and 🪙‹all› rules retrieved from the context on every invocation of the
 method. This does not scale to really large collections of rules, which
 easily emerges in the context of a big theory library, for example.

 This is an inherent limitation of the simplistic rule management via
 @{command named_theorems}, because it lacks tool-specific storage and
 retrieval. More realistic applications require efficient index-structures
 that organize theorems in a customized manner, such as a discrimination net
 that is indexed by the left-hand sides of rewrite rules. For variations on
 the Simplifier, re-use of the existing type 🪙‹simpset› is adequate,
 but scalability would require it be maintained statically within the context
 data, not dynamically on each tool invocation.
 ›


section ‹Attributes \label{sec:attributes}›

text ‹
 An 🪙‹attribute› is a function ‹context × thm → context × thm›, which means
 both a (generic) context and a theorem can be modified simultaneously. In
 practice this mixed form is very rare, instead attributes are presented
 either as 🪙‹declaration attribute:› ‹thm → context → context› or 🪙‹rule
 attribute:› ‹context → thm → thm›.

 Attributes can have additional arguments via concrete syntax. There is a
 collection of context-sensitive parsers for various logical entities (types,
 terms, theorems). These already take care of applying morphisms to the
 arguments when attribute expressions are moved into a different context (see
 also \secref{sec:morphisms}).

 When implementing declaration attributes, it is important to operate exactly
 on the variant of the generic context that is provided by the system, which
 is either global theory context or local proof context. In particular, the
 background theory of a local context must not be modified in this
 situation!
 ›

text %mlref ‹
 \begin{mldecls}
 @{define_ML_type attribute} \\
 @{define_ML Thm.rule_attribute: "thm list ->
 (Context.generic -> thm -> thm) -> attribute"} \\
 @{define_ML Thm.declaration_attribute: "
 (thm -> Context.generic -> Context.generic) -> attribute"} \\
 @{define_ML Attrib.setup: "binding -> attribute context_parser ->
 string -> theory -> theory"} \\
 \end{mldecls}

 🪙 Type 🪙‹attribute› represents attributes as concrete type alias.

 🪙 🪙‹Thm.rule_attribute›~‹thms (fn context => rule)› wraps a
 context-dependent rule (mapping on 🪙‹thm›) as attribute.

 The ‹thms› are additional parameters: when forming an abstract closure, the
 system may provide dummy facts that are propagated according to strict
 evaluation discipline. In that case, ‹rule› is bypassed.

 🪙 🪙‹Thm.declaration_attribute›~‹(fn thm => decl)› wraps a
 theorem-dependent declaration (mapping on 🪙‹Context.generic›) as
 attribute.

 When forming an abstract closure, the system may provide a dummy fact as
 ‹thm›. In that case, ‹decl› is bypassed.

 🪙 🪙‹Attrib.setup›~‹name parser description› provides the functionality of
 the Isar command @{command attribute_setup} as ML function.
 ›

text %mlantiq ‹
 \begin{matharray}{rcl}
 @{ML_antiquotation_def attributes} & : & ‹ML_antiquotation› \\
 \end{matharray}

 🪙‹
 @@{ML_antiquotation attributes} attributes
 ›

 🪙 ‹@{attributes […]}› embeds attribute source representation into the ML
 text, which is particularly useful with declarations like 🪙‹Local_Theory.note›. Attribute names are internalized at compile time, but
 the source is unevaluated. This means attributes with formal arguments
 (types, terms, theorems) may be subject to odd effects of dynamic scoping!
 ›

text %mlex ‹
 See also @{command attribute_setup} in cite‹"isabelle-isar-ref"› which
 includes some abstract examples.
 ›

end