src/HOL/IMP/Denotational.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 52402 c2f30ba4bb98
child 62217 527488dc8b90
permissions -rw-r--r--
modernized header uniformly as section;
     1 (* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *)
     2 
     3 section "Denotational Semantics of Commands"
     4 
     5 theory Denotational imports Big_Step begin
     6 
     7 type_synonym com_den = "(state \<times> state) set"
     8 
     9 definition W :: "(state \<Rightarrow> bool) \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where
    10 "W db dc = (\<lambda>dw. {(s,t). if db s then (s,t) \<in> dc O dw else s=t})"
    11 
    12 fun D :: "com \<Rightarrow> com_den" where
    13 "D SKIP   = Id" |
    14 "D (x ::= a) = {(s,t). t = s(x := aval a s)}" |
    15 "D (c1;;c2)  = D(c1) O D(c2)" |
    16 "D (IF b THEN c1 ELSE c2)
    17  = {(s,t). if bval b s then (s,t) \<in> D c1 else (s,t) \<in> D c2}" |
    18 "D (WHILE b DO c) = lfp (W (bval b) (D c))"
    19 
    20 lemma W_mono: "mono (W b r)"
    21 by (unfold W_def mono_def) auto
    22 
    23 lemma D_While_If:
    24   "D(WHILE b DO c) = D(IF b THEN c;;WHILE b DO c ELSE SKIP)"
    25 proof-
    26   let ?w = "WHILE b DO c" let ?f = "W (bval b) (D c)"
    27   have "D ?w = lfp ?f" by simp
    28   also have "\<dots> = ?f (lfp ?f)" by(rule lfp_unfold [OF W_mono])
    29   also have "\<dots> = D(IF b THEN c;;?w ELSE SKIP)" by (simp add: W_def)
    30   finally show ?thesis .
    31 qed
    32 
    33 text{* Equivalence of denotational and big-step semantics: *}
    34 
    35 lemma D_if_big_step:  "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> D(c)"
    36 proof (induction rule: big_step_induct)
    37   case WhileFalse
    38   with D_While_If show ?case by auto
    39 next
    40   case WhileTrue
    41   show ?case unfolding D_While_If using WhileTrue by auto
    42 qed auto
    43 
    44 abbreviation Big_step :: "com \<Rightarrow> com_den" where
    45 "Big_step c \<equiv> {(s,t). (c,s) \<Rightarrow> t}"
    46 
    47 lemma Big_step_if_D:  "(s,t) \<in> D(c) \<Longrightarrow> (s,t) : Big_step c"
    48 proof (induction c arbitrary: s t)
    49   case Seq thus ?case by fastforce
    50 next
    51   case (While b c)
    52   let ?B = "Big_step (WHILE b DO c)" let ?f = "W (bval b) (D c)"
    53   have "?f ?B \<subseteq> ?B" using While.IH by (auto simp: W_def)
    54   from lfp_lowerbound[where ?f = "?f", OF this] While.prems
    55   show ?case by auto
    56 qed (auto split: if_splits)
    57 
    58 theorem denotational_is_big_step:
    59   "(s,t) \<in> D(c)  =  ((c,s) \<Rightarrow> t)"
    60 by (metis D_if_big_step Big_step_if_D[simplified])
    61 
    62 corollary equiv_c_iff_equal_D: "(c1 \<sim> c2) \<longleftrightarrow> D c1 = D c2"
    63 by(simp add: denotational_is_big_step[symmetric] set_eq_iff)
    64 
    65 
    66 subsection "Continuity"
    67 
    68 definition chain :: "(nat \<Rightarrow> 'a set) \<Rightarrow> bool" where
    69 "chain S = (\<forall>i. S i \<subseteq> S(Suc i))"
    70 
    71 lemma chain_total: "chain S \<Longrightarrow> S i \<le> S j \<or> S j \<le> S i"
    72 by (metis chain_def le_cases lift_Suc_mono_le)
    73 
    74 definition cont :: "('a set \<Rightarrow> 'b set) \<Rightarrow> bool" where
    75 "cont f = (\<forall>S. chain S \<longrightarrow> f(UN n. S n) = (UN n. f(S n)))"
    76 
    77 lemma mono_if_cont: fixes f :: "'a set \<Rightarrow> 'b set"
    78   assumes "cont f" shows "mono f"
    79 proof
    80   fix a b :: "'a set" assume "a \<subseteq> b"
    81   let ?S = "\<lambda>n::nat. if n=0 then a else b"
    82   have "chain ?S" using `a \<subseteq> b` by(auto simp: chain_def)
    83   hence "f(UN n. ?S n) = (UN n. f(?S n))"
    84     using assms by(simp add: cont_def)
    85   moreover have "(UN n. ?S n) = b" using `a \<subseteq> b` by (auto split: if_splits)
    86   moreover have "(UN n. f(?S n)) = f a \<union> f b" by (auto split: if_splits)
    87   ultimately show "f a \<subseteq> f b" by (metis Un_upper1)
    88 qed
    89 
    90 lemma chain_iterates: fixes f :: "'a set \<Rightarrow> 'a set"
    91   assumes "mono f" shows "chain(\<lambda>n. (f^^n) {})"
    92 proof-
    93   { fix n have "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" using assms
    94     by(induction n) (auto simp: mono_def) }
    95   thus ?thesis by(auto simp: chain_def)
    96 qed
    97 
    98 theorem lfp_if_cont:
    99   assumes "cont f" shows "lfp f = (UN n. (f^^n) {})" (is "_ = ?U")
   100 proof
   101   show "lfp f \<subseteq> ?U"
   102   proof (rule lfp_lowerbound)
   103     have "f ?U = (UN n. (f^^Suc n){})"
   104       using chain_iterates[OF mono_if_cont[OF assms]] assms
   105       by(simp add: cont_def)
   106     also have "\<dots> = (f^^0){} \<union> \<dots>" by simp
   107     also have "\<dots> = ?U"
   108       by(auto simp del: funpow.simps) (metis not0_implies_Suc)
   109     finally show "f ?U \<subseteq> ?U" by simp
   110   qed
   111 next
   112   { fix n p assume "f p \<subseteq> p"
   113     have "(f^^n){} \<subseteq> p"
   114     proof(induction n)
   115       case 0 show ?case by simp
   116     next
   117       case Suc
   118       from monoD[OF mono_if_cont[OF assms] Suc] `f p \<subseteq> p`
   119       show ?case by simp
   120     qed
   121   }
   122   thus "?U \<subseteq> lfp f" by(auto simp: lfp_def)
   123 qed
   124 
   125 lemma cont_W: "cont(W b r)"
   126 by(auto simp: cont_def W_def)
   127 
   128 
   129 subsection{*The denotational semantics is deterministic*}
   130 
   131 lemma single_valued_UN_chain:
   132   assumes "chain S" "(\<And>n. single_valued (S n))"
   133   shows "single_valued(UN n. S n)"
   134 proof(auto simp: single_valued_def)
   135   fix m n x y z assume "(x, y) \<in> S m" "(x, z) \<in> S n"
   136   with chain_total[OF assms(1), of m n] assms(2)
   137   show "y = z" by (auto simp: single_valued_def)
   138 qed
   139 
   140 lemma single_valued_lfp: fixes f :: "com_den \<Rightarrow> com_den"
   141 assumes "cont f" "\<And>r. single_valued r \<Longrightarrow> single_valued (f r)"
   142 shows "single_valued(lfp f)"
   143 unfolding lfp_if_cont[OF assms(1)]
   144 proof(rule single_valued_UN_chain[OF chain_iterates[OF mono_if_cont[OF assms(1)]]])
   145   fix n show "single_valued ((f ^^ n) {})"
   146   by(induction n)(auto simp: assms(2))
   147 qed
   148 
   149 lemma single_valued_D: "single_valued (D c)"
   150 proof(induction c)
   151   case Seq thus ?case by(simp add: single_valued_relcomp)
   152 next
   153   case (While b c)
   154   let ?f = "W (bval b) (D c)"
   155   have "single_valued (lfp ?f)"
   156   proof(rule single_valued_lfp[OF cont_W])
   157     show "\<And>r. single_valued r \<Longrightarrow> single_valued (?f r)"
   158       using While.IH by(force simp: single_valued_def W_def)
   159   qed
   160   thus ?case by simp
   161 qed (auto simp add: single_valued_def)
   162 
   163 end