src/HOL/IMP/Denotational.thy
author nipkow
Wed, 19 Jun 2013 17:16:45 +0200
changeset 52396 432777f2e372
parent 52395 7cc3f42930f3
child 52401 56e83c57f953
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43143
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
     1
(* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *)
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     2
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
     3
header "Denotational Semantics of Commands"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     4
52394
fe33d456b36c more canonical name (2)
nipkow
parents: 52393
diff changeset
     5
theory Denotational imports Big_Step begin
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
     6
42174
d0be2722ce9f modernized specifications;
wenzelm
parents: 41589
diff changeset
     7
type_synonym com_den = "(state \<times> state) set"
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
     8
52396
nipkow
parents: 52395
diff changeset
     9
definition W :: "(state \<Rightarrow> bool) \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where
nipkow
parents: 52395
diff changeset
    10
"W db dc = (\<lambda>dw. {(s,t). if db s then (s,t) \<in> dc O dw else s=t})"
18372
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    11
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    12
fun D :: "com \<Rightarrow> com_den" where
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    13
"D SKIP   = Id" |
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    14
"D (x ::= a) = {(s,t). t = s(x := aval a s)}" |
52395
nipkow
parents: 52394
diff changeset
    15
"D (c1;;c2)  = D(c1) O D(c2)" |
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    16
"D (IF b THEN c1 ELSE c2)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    17
 = {(s,t). if bval b s then (s,t) \<in> D c1 else (s,t) \<in> D c2}" |
52396
nipkow
parents: 52395
diff changeset
    18
"D (WHILE b DO c) = lfp (W (bval b) (D c))"
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    19
52387
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    20
lemma W_mono: "mono (W b r)"
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    21
by (unfold W_def mono_def) auto
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    22
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    23
lemma D_While_If:
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    24
  "D(WHILE b DO c) = D(IF b THEN c;;WHILE b DO c ELSE SKIP)"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    25
proof-
52396
nipkow
parents: 52395
diff changeset
    26
  let ?w = "WHILE b DO c" let ?f = "W (bval b) (D c)"
nipkow
parents: 52395
diff changeset
    27
  have "D ?w = lfp ?f" by simp
nipkow
parents: 52395
diff changeset
    28
  also have "\<dots> = ?f (lfp ?f)" by(rule lfp_unfold [OF W_mono])
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    29
  also have "\<dots> = D(IF b THEN c;;?w ELSE SKIP)" by (simp add: W_def)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    30
  finally show ?thesis .
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    31
qed
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    32
43144
631dd866b284 Made comments text
nipkow
parents: 43143
diff changeset
    33
text{* Equivalence of denotational and big-step semantics: *}
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    34
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    35
lemma D_if_big_step:  "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> D(c)"
52387
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    36
proof (induction rule: big_step_induct)
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    37
  case WhileFalse
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    38
  with D_While_If show ?case by auto
52387
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    39
next
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    40
  case WhileTrue
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    41
  show ?case unfolding D_While_If using WhileTrue by auto
52387
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    42
qed auto
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    43
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    44
abbreviation Big_step :: "com \<Rightarrow> com_den" where
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    45
"Big_step c \<equiv> {(s,t). (c,s) \<Rightarrow> t}"
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    46
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    47
lemma Big_step_if_D:  "(s,t) \<in> D(c) \<Longrightarrow> (s,t) : Big_step c"
52387
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    48
proof (induction c arbitrary: s t)
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    49
  case Seq thus ?case by fastforce
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    50
next
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    51
  case (While b c)
52396
nipkow
parents: 52395
diff changeset
    52
  let ?B = "Big_step (WHILE b DO c)" let ?f = "W (bval b) (D c)"
nipkow
parents: 52395
diff changeset
    53
  have "?f ?B \<subseteq> ?B" using While.IH by (auto simp: W_def)
nipkow
parents: 52395
diff changeset
    54
  from lfp_lowerbound[where ?f = "?f", OF this] While.prems
52387
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    55
  show ?case by auto
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    56
qed (auto split: if_splits)
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    57
52387
b5b510c686cb improved defs and proofs
nipkow
parents: 52046
diff changeset
    58
theorem denotational_is_big_step:
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    59
  "(s,t) \<in> D(c)  =  ((c,s) \<Rightarrow> t)"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    60
by (metis D_if_big_step Big_step_if_D[simplified])
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    61
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    62
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    63
subsection "Continuity"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    64
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    65
definition chain :: "(nat \<Rightarrow> 'a set) \<Rightarrow> bool" where
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    66
"chain S = (\<forall>i. S i \<subseteq> S(Suc i))"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    67
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    68
lemma chain_total: "chain S \<Longrightarrow> S i \<le> S j \<or> S j \<le> S i"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    69
by (metis chain_def le_cases lift_Suc_mono_le)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    70
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    71
definition cont :: "('a set \<Rightarrow> 'a set) \<Rightarrow> bool" where
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    72
"cont f = (\<forall>S. chain S \<longrightarrow> f(UN n. S n) = (UN n. f(S n)))"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    73
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    74
lemma mono_if_cont: fixes f :: "'a set \<Rightarrow> 'a set"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    75
  assumes "cont f" shows "mono f"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    76
proof
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    77
  fix a b :: "'a set" assume "a \<subseteq> b"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    78
  let ?S = "\<lambda>n::nat. if n=0 then a else b"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    79
  have "chain ?S" using `a \<subseteq> b` by(auto simp: chain_def)
52396
nipkow
parents: 52395
diff changeset
    80
  hence "f(UN n. ?S n) = (UN n. f(?S n))"
nipkow
parents: 52395
diff changeset
    81
    using assms by(simp add: cont_def)
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    82
  moreover have "(UN n. ?S n) = b" using `a \<subseteq> b` by (auto split: if_splits)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    83
  moreover have "(UN n. f(?S n)) = f a \<union> f b" by (auto split: if_splits)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    84
  ultimately show "f a \<subseteq> f b" by (metis Un_upper1)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    85
qed
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    86
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    87
lemma chain_iterates: fixes f :: "'a set \<Rightarrow> 'a set"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    88
  assumes "mono f" shows "chain(\<lambda>n. (f^^n) {})"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    89
proof-
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    90
  { fix n have "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" using assms
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    91
    by(induction n) (auto simp: mono_def) }
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    92
  thus ?thesis by(auto simp: chain_def)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    93
qed
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    94
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    95
theorem lfp_if_cont:
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    96
  assumes "cont f" shows "lfp f = (UN n. (f^^n) {})" (is "_ = ?U")
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    97
proof
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    98
  show "lfp f \<subseteq> ?U"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
    99
  proof (rule lfp_lowerbound)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   100
    have "f ?U = (UN n. (f^^Suc n){})"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   101
      using chain_iterates[OF mono_if_cont[OF assms]] assms
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   102
      by(simp add: cont_def)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   103
    also have "\<dots> = (f^^0){} \<union> \<dots>" by simp
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   104
    also have "\<dots> = ?U"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   105
      by(auto simp del: funpow.simps) (metis not0_implies_Suc)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   106
    finally show "f ?U \<subseteq> ?U" by simp
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   107
  qed
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   108
next
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   109
  { fix n p assume "f p \<subseteq> p"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   110
    have "(f^^n){} \<subseteq> p"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   111
    proof(induction n)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   112
      case 0 show ?case by simp
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   113
    next
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   114
      case Suc
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   115
      from monoD[OF mono_if_cont[OF assms] Suc] `f p \<subseteq> p`
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   116
      show ?case by simp
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   117
    qed
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   118
  }
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   119
  thus "?U \<subseteq> lfp f" by(auto simp: lfp_def)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   120
qed
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   121
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   122
lemma cont_W: "cont(W b r)"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   123
by(auto simp: cont_def W_def)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   124
52392
ee996ca08de3 added lemma
nipkow
parents: 52389
diff changeset
   125
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   126
subsection{*The denotational semantics is deterministic*}
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   127
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   128
lemma single_valued_UN_chain:
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   129
  assumes "chain S" "(\<And>n. single_valued (S n))"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   130
  shows "single_valued(UN n. S n)"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   131
proof(auto simp: single_valued_def)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   132
  fix m n x y z assume "(x, y) \<in> S m" "(x, z) \<in> S n"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   133
  with chain_total[OF assms(1), of m n] assms(2)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   134
  show "y = z" by (auto simp: single_valued_def)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   135
qed
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   136
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   137
lemma single_valued_lfp: fixes f :: "com_den \<Rightarrow> com_den"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   138
assumes "cont f" "\<And>r. single_valued r \<Longrightarrow> single_valued (f r)"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   139
shows "single_valued(lfp f)"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   140
unfolding lfp_if_cont[OF assms(1)]
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   141
proof(rule single_valued_UN_chain[OF chain_iterates[OF mono_if_cont[OF assms(1)]]])
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   142
  fix n show "single_valued ((f ^^ n) {})"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   143
  by(induction n)(auto simp: assms(2))
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   144
qed
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   145
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   146
lemma single_valued_D: "single_valued (D c)"
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   147
proof(induction c)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   148
  case Seq thus ?case by(simp add: single_valued_relcomp)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   149
next
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   150
  case (While b c)
52396
nipkow
parents: 52395
diff changeset
   151
  let ?f = "W (bval b) (D c)"
nipkow
parents: 52395
diff changeset
   152
  have "single_valued (lfp ?f)"
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   153
  proof(rule single_valued_lfp[OF cont_W])
52396
nipkow
parents: 52395
diff changeset
   154
    show "\<And>r. single_valued r \<Longrightarrow> single_valued (?f r)"
52389
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   155
      using While.IH by(force simp: single_valued_def W_def)
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   156
  qed
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   157
  thus ?case by simp
3971dd9ca831 Added continuity and determinism proof
nipkow
parents: 52387
diff changeset
   158
qed (auto simp add: single_valued_def)
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   159
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
   160
end