# Theory Denotation

Up to index of Isabelle/HOL/HOL-IMP

theory Denotation
imports Big_Step
`(* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *)header "Denotational Semantics of Commands"theory Denotation imports Big_Step begintype_synonym com_den = "(state × state) set"definition  Gamma :: "bexp => com_den => (com_den => com_den)" where  "Gamma b cd = (λphi. {(s,t). (s,t) ∈ (cd O phi) ∧ bval b s} ∪                       {(s,t). s=t ∧ ¬bval b s})"fun C :: "com => com_den" where"C SKIP   = Id" |"C (x ::= a) = {(s,t). t = s(x := aval a s)}" |"C (c0;c1)   = C(c0) O C(c1)" |"C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) ∈ C c1 ∧ bval b s} ∪                            {(s,t). (s,t) ∈ C c2 ∧ ¬bval b s}" |"C(WHILE b DO c) = lfp (Gamma b (C c))"lemma Gamma_mono: "mono (Gamma b c)"by (unfold Gamma_def mono_def) fastlemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"apply simpapply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}apply (simp add: Gamma_def)donetext{* Equivalence of denotational and big-step semantics: *}lemma com1: "(c,s) => t ==> (s,t) ∈ C(c)"apply (induction rule: big_step_induct)apply auto(* while *)apply (unfold Gamma_def)apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])apply fastapply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])apply auto donelemma com2: "(s,t) ∈ C(c) ==> (c,s) => t"apply (induction c arbitrary: s t)apply auto apply blast(* while *)apply (erule lfp_induct2 [OF _ Gamma_mono])apply (unfold Gamma_def)apply autodonelemma denotational_is_big_step: "(s,t) ∈ C(c)  =  ((c,s) => t)"by (fast elim: com2 dest: com1)end`