Theory IsaFoR_Outline

section ‹IsaFoR Basics›

text ‹We present basic notions of IsaFoR.›

(*<*)
theory IsaFoR_Outline
  imports LS_Extras
begin
(*>*)
subsection ‹Types›

text ‹
  \begin{itemize}
  \setlength{\itemsep}{0pt}
  \item \textbf{type\textunderscore synonym} @{typ "'f sig"} $=$ @{typeof "x :: 'f sig"}\\
    Note that IsaFoR regards arities as part of the function symbol.
  \item @{datatype [names_short] term}\\
    In the definition of terms, the arity is implicit in the length of the argument list.
  \item @{datatype pos}
  \item @{datatype [names_short] ctxt}
  \item \textbf{type\textunderscore synonym} @{typ "('f,'v) rule"} $=$ @{typeof [names_short] "x :: ('f,'v) rule"}
  \item \textbf{type\textunderscore synonym} @{typ "('f,'v) trs"} $=$ @{typ "('f,'v) rule set"}
  \item @{datatype mctxt}
  \end{itemize}
›

subsection ‹Functions›

text ‹
  \begin{itemize}
  \setlength{\itemsep}{0pt}
  \item @{term_type [names_short] "subt_at"}\\
    Return subterm at given position.
  \item @{term [source] "replace_at"}@{text "::"}@{typeof [names_short] "replace_at"}
  \item @{term [names_short] "poss"}, @{term [names_short] "funposs"}, @{term_type [names_short] "varposs"}
  \item @{term_type [names_short] "funas_term"}, @{term_type [names_short] "vars_term"}
  \item @{term_type [names_short] "vars_term_ms"}
  \item @{term_type [names_short] "mctxt_of_term"}
  \item @{term_type [names_short] "subm_at"}
  \item @{term_type [names_short] "mreplace_at"}
  \item @{term_type [names_short] "poss_mctxt"}
  \item @{term_type [names_short] "hole_poss"}
  \item @{term_type [names_short] "mctxt_term_conv"},\\ @{term_type [names_short] "term_mctxt_conv"}\\
    These two functions define a bijection between multi-hole contexts and terms with an extra variable
    (represented by @{term None}).
  \item @{term_type [names_short] "rstep_r_p_s'"}\\
    @{term "(s,t) ∈ rstep_r_p_s' ℛ (l,r) p σ"} is a rewrite step with explicit rule, position and substitution.
  \end{itemize}
›

subsection ‹Definitions›
text ‹
  \begin{itemize}
  \setlength{\itemsep}{0pt}
  \item @{term_type [names_short] "left_linear_trs"}
  \end{itemize}
›

(*<*)
print_antiquotations

end
(*>*)