doc-src/IsarRef/pure.tex

 
 
 \subsection{Facts and forward chaining}
 
 \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
-\indexisarcmd{using}
+\indexisarcmd{using}\indexisarcmd{unfolding}
 \begin{matharray}{rcl}
   \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
   \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
   \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
   \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
   \isarcmd{using} & : & \isartrans{proof(prove)}{proof(prove)} \\
+  \isarcmd{unfolding} & : & \isartrans{proof(prove)}{proof(prove)} \\
 \end{matharray}
 
 New facts are established either by assumption or proof of local statements.
 Any fact will usually be involved in further proofs, either as explicit
 arguments of proof methods, or when forward chaining towards the next goal via

 but only \emph{before} issuing a follow-up claim.
 
 \begin{rail}
   'note' (thmdef? thmrefs + 'and')
   ;
-  ('from' | 'with' | 'using') (thmrefs + 'and')
+  ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
   ;
 \end{rail}
 
 \begin{descr}
 

 \item [$\WITH{\vec b}$] abbreviates ``$\FROM{\vec b~\AND~this}$''; thus the
   forward chaining is from earlier facts together with the current ones.
   
 \item [$\USING{\vec b}$] augments the facts being currently indicated for use
   by a subsequent refinement step (such as $\APPLYNAME$ or $\PROOFNAME$).
+  
+\item [$\UNFOLDING{\vec b}$] is structurally similar to $\USINGNAME$,
+  but unfolds meta-level equations {\vec b} throughout the goal state
+  and facts.
 
 \end{descr}
 
 Forward chaining with an empty list of theorems is the same as not chaining at
 all.  Thus ``$\FROM{nothing}$'' has no effect apart from entering