| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Strong_Security/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 921 B |
|
Quelle Expr.thySprache: Isabelle |
|||||||||||||||
|
(* Title: Strong-Security Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer *) theory Expr imports Types begin ― ‹type parameters:› ― ‹'val: numbers, boolean constants....› ― ‹'id: identifier names› type_synonym ('val) operation = "'val list ==> 'val" datatype (dead 'id, dead 'val) Expr = Const "'val" | Var "'id" | Op "'val operation" "(('id, 'val) Expr) list" ― ‹defining a simple recursive evaluation function on this datatype› primrec ExprEval :: "(('id, 'val) Expr, 'id, 'val) Evalfunction" and ExprEvalL :: "(('id, 'val) Expr) list ==> ('id, 'val) State ==> 'val list" where "ExprEval (Const v) m = v" | "ExprEval (Var x) m = (m x)" | "ExprEval (Op f arglist) m = (f (ExprEvalL arglist m))" | "ExprEvalL [] m = []" | "ExprEvalL (e#V) m = (ExprEval e m)#(ExprEvalL V m)" end
¤ Dauer der Verarbeitung: 0.1 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09