doc-src/IsarRef/generic.tex
 changeset 10154 05d6ccb2f536 parent 10031 12fd0fcf755a child 10160 bb8f9412fec6
equal inserted replaced
10153:482899aff303 10154:05d6ccb2f536
    57 \begin{matharray}{rcl}
    57 \begin{matharray}{rcl}
    58   \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
    58   \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
    59   \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
    59   \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
    60   \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
    60   \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
    61   \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
    61   \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
    62   \isarcmd{print_trans_rules} & : & \isarkeep{theory~|~proof} \\
    62   \isarcmd{print_trans_rules}^* & : & \isarkeep{theory~|~proof} \\
    63   trans & : & \isaratt \\
    63   trans & : & \isaratt \\
    64 \end{matharray}
    64 \end{matharray}
    65
    65
    66 Calculational proof is forward reasoning with implicit application of
    66 Calculational proof is forward reasoning with implicit application of
    67 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
    67 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
   239   \quad \BG \\
   239   \quad \BG \\
   240   \qquad \FIX{thesis} \\
   240   \qquad \FIX{thesis} \\
   241   \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
   241   \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
   242   \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
   242   \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
   243   \quad \EN \\
   243   \quad \EN \\
   244   \quad \FIX{\vec x}~\ASSUMENAME^{\ast}~{a}~{\vec\phi} \\
   244   \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
   245 \end{matharray}
   245 \end{matharray}
   246
   246
   247 Typically, the soundness proof is relatively straight-forward, often just by
   247 Typically, the soundness proof is relatively straight-forward, often just by
   248 canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
   248 canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
   249 $\BY{blast}$ (see \S\ref{sec:classical-auto}).  Accordingly, the $that$''
   249 $\BY{blast}$ (see \S\ref{sec:classical-auto}).  Accordingly, the $that$''
   328 \begin{rail}
   328 \begin{rail}
   329   'tagged' (nameref+)
   329   'tagged' (nameref+)
   330   ;
   330   ;
   331   'untagged' name
   331   'untagged' name
   332   ;
   332   ;
   333   ('THEN' | 'COMP') nat? thmref
   333   ('THEN' | 'COMP') ('[' nat ']')? thmref
   334   ;
   334   ;
   335   'where' (name '=' term * 'and')
   335   'where' (name '=' term * 'and')
   336   ;
   336   ;
   337   ('unfolded' | 'folded') thmrefs
   337   ('unfolded' | 'folded') thmrefs
   338   ;
   338   ;
   568 \subsection{Declaring rules}
   568 \subsection{Declaring rules}
   569
   569
   570 \indexisarcmd{print-simpset}
   570 \indexisarcmd{print-simpset}
   571 \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
   571 \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
   572 \begin{matharray}{rcl}
   572 \begin{matharray}{rcl}
   573   print_simpset & : & \isarkeep{theory~|~proof} \\
   573   print_simpset^* & : & \isarkeep{theory~|~proof} \\
   574   simp & : & \isaratt \\
   574   simp & : & \isaratt \\
   575   cong & : & \isaratt \\
   575   cong & : & \isaratt \\
   576   split & : & \isaratt \\
   576   split & : & \isaratt \\
   577 \end{matharray}
   577 \end{matharray}
   578
   578
   788
   788
   789 \indexisarcmd{print-claset}
   789 \indexisarcmd{print-claset}
   790 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   790 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   791 \indexisaratt{iff}\indexisaratt{rule}
   791 \indexisaratt{iff}\indexisaratt{rule}
   792 \begin{matharray}{rcl}
   792 \begin{matharray}{rcl}
   793   print_claset & : & \isarkeep{theory~|~proof} \\
   793   print_claset^* & : & \isarkeep{theory~|~proof} \\
   794   intro & : & \isaratt \\
   794   intro & : & \isaratt \\
   795   elim & : & \isaratt \\
   795   elim & : & \isaratt \\
   796   dest & : & \isaratt \\
   796   dest & : & \isaratt \\
   797   rule & : & \isaratt \\
   797   rule & : & \isaratt \\
   798   iff & : & \isaratt \\
   798   iff & : & \isaratt \\