Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/HOLCF/IMP/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

Quelle Denotational.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/IMP/Denotational.thy
    Author:     Tobias Nipkow and Robert Sandner, TUM
    Copyright   1996 TUM
*)

section "Denotational Semantics of Commands in HOLCF"

theory Denotational imports HOLCF "HOL-IMP.Big_Step" begin

subsection "Definition"

definition
  dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" where
  "dlift f = (LAM x. case x of UU \ UU | Def y \ f\(Discr y))"

primrec D :: "com \ state discr \ state lift"
where
  "D(SKIP) = (LAM s. Def(undiscr s))"
| "D(X ::= a) = (LAM s. Def((undiscr s)(X := aval a (undiscr s))))"
| "D(c0 ;; c1) = (dlift(D c1) oo (D c0))"
| "D(IF b THEN c1 ELSE c2) =
        (LAM s. if bval b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
| "D(WHILE b DO c) =
        fix\<cdot>(LAM w s. if bval b (undiscr s) then (dlift w)\<cdot>((D c)\<cdot>s)
                      else Def(undiscr s))"

subsection
  "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL"

lemma dlift_Def [simp]: "dlift f\(Def x) = f\(Discr x)"
  by (simp add: dlift_def)

lemma cont_dlift [iff]: "cont (%f. dlift f)"
  by (simp add: dlift_def)

lemma dlift_is_Def [simp]:
    "(dlift f\l = Def y) = (\x. l = Def x \ f\(Discr x) = Def y)"
  by (simp add: dlift_def split: lift.split)

lemma eval_implies_D: "(c,s) \ t \ D c\(Discr s) = (Def t)"
apply (induct rule: big_step_induct)
      apply (auto)
apply (subst fix_eq)
apply simp
apply (subst fix_eq)
apply simp
done

lemma D_implies_eval: "\s t. D c\(Discr s) = (Def t) \ (c,s) \ t"
apply (induct c)
    apply fastforce
   apply fastforce
  apply force
apply (simp (no_asm))
apply force
apply (simp (no_asm))
apply (rule fix_ind)
  apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
apply (simp (no_asm))
apply (simp (no_asm))
apply force
done

theorem D_is_eval: "(D c\(Discr s) = (Def t)) = ((c,s) \ t)"
by (fast elim!: D_implies_eval [rule_format] eval_implies_D)

end

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.