text‹We introduce a syntactic variant of the let-expression so that we can
unfold it during verification condition generation. With the new
attribute ‹vcg_simp› we can declare equalities to be used
the verification condition generator, while simplifying assertions. ›
syntax "_Let'" :: "[letbinds, basicblock] => basicblock"
(‹(‹notation=‹mixfix LET expression››LET (_)/ IN (_))› 23)
syntax_consts "_Let'" == Let'
translations "_Let' (_binds b bs) e" == "_Let' b (_Let' bs e)" "_Let' (_bind x a) e" == "CONST Let' a (%x. e)"
lemmaLet'_unfold [vcg_simp]: "Let' x f = f x" by (simp add: Let'_def Let_def)
lemmaLet'_split_conv [vcg_simp]: "(Let' x (λp. (case_prod (f p) (g p)))) = (Let' x (λp. (f p) (fst (g p)) (snd (g p))))" by (simp add: split_def)
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet am 2026-07-02)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
