Theory SlideSnippets

theory SlideSnippets
  imports
    Semantics.TreeToGraphThms
    Snippets.Snipping
begin

notation (latex)
  kind ("_⟪_⟫")

notation (latex)
  IRTreeEval.ord_IRExpr_inst.less_eq_IRExpr ("_ ⟼ _")

snipbegin ‹abstract-syntax-tree›
text ‹@{datatype[display,margin=40] IRExpr}›
snipend -

snipbegin ‹tree-semantics›
text ‹
\induct{@{thm[mode=Rule] evaltree.ConstantExpr [no_vars]}}{semantics:constant}
\induct{@{thm[mode=Rule] evaltree.ParameterExpr [no_vars]}}{semantics:parameter}
\induct{@{thm[mode=Rule] evaltree.UnaryExpr [no_vars]}}{semantics:unary}
\induct{@{thm[mode=Rule] evaltree.BinaryExpr [no_vars]}}{semantics:binary}
\induct{@{thm[mode=Rule] evaltree.LeafExpr [no_vars]}}{semantics:leaf}
›
snipend -

snipbegin ‹expression-refinement›
text ‹
\begin{center}
@{thm le_expr_def [no_vars]} 
\end{center}
›
snipend -

snipbegin ‹graph2tree›
text ‹
\induct{@{thm[mode=Rule] rep.ConstantNode [no_vars]}}{semantics:constant}
\induct{@{thm[mode=Rule] rep.AbsNode [no_vars]}}{semantics:unary}
\induct{@{thm[mode=Rule] rep.AddNode [no_vars]}}{semantics:binary}
›
snipend -

snipbegin ‹graph-semantics›
text ‹
\begin{center}
@{thm encodeeval.intros}
\end{center}
›
snipend -

snipbegin ‹graph-refinement›
text ‹
\begin{center}
@{thm[display, margin=60] graph_refinement_def [no_vars]}
\end{center}
›
snipend -

(* hide as_set, should treat IRGraph as a set of pairs in paper *)
translations
  "n" <= "CONST as_set n"

snipbegin ‹graph-semantics-preservation›
text ‹
\begin{center}
@{thm[display, margin=30] graph_semantics_preservation [no_vars]}
\end{center}
›
snipend -

snipbegin ‹maximal-sharing›
text ‹@{thm[display, margin=50] maximal_sharing [no_vars]}›
snipend -

snipbegin ‹tree-to-graph-rewriting›
text ‹
\begin{center}
@{thm[display, margin=40] tree_to_graph_rewriting [no_vars]}
\end{center}
›
snipend -

snipbegin ‹graph-represents-expression›
text ‹
\begin{center}
@{thm[display] graph_represents_expression_def [no_vars]}
\end{center}
›
snipend -

snipbegin ‹graph-construction›
text ‹
\begin{center}
@{thm[display, margin=40] graph_construction [no_vars]}
\end{center}
›
snipend -

end