src/HOL/IMP/Denotation.thy
author nipkow
Tue, 20 Sep 2011 05:48:23 +0200
changeset 45015 fdac1e9880eb
parent 43144 631dd866b284
child 52046 bc01725d7918
permissions -rw-r--r--
Updated IMP to use new induction method
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
43143
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
     5
theory Denotation 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
27362
a6dc1769fdda modernized specifications;
wenzelm
parents: 23746
diff changeset
     9
definition
43143
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    10
  Gamma :: "bexp \<Rightarrow> com_den \<Rightarrow> (com_den \<Rightarrow> com_den)" where
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    11
  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> bval b s} \<union>
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    12
                       {(s,t). s=t \<and> \<not>bval b s})"
18372
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    13
43143
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    14
fun C :: "com \<Rightarrow> com_den" where
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    15
"C SKIP   = Id" |
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    16
"C (x ::= a) = {(s,t). t = s(x := aval a s)}" |
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    17
"C (c0;c1)   = C(c0) O C(c1)" |
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    18
"C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union>
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    19
                            {(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" |
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    20
"C(WHILE b DO c) = lfp (Gamma b (C c))"
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    21
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    22
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    23
lemma Gamma_mono: "mono (Gamma b c)"
43143
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    24
by (unfold Gamma_def mono_def) fast
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    25
43143
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    26
lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"
18372
2bffdf62fe7f tuned proofs;
wenzelm
parents: 16417
diff changeset
    27
apply simp
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 12434
diff changeset
    28
apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 12434
diff changeset
    29
apply (simp add: Gamma_def)
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    30
done
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    31
43144
631dd866b284 Made comments text
nipkow
parents: 43143
diff changeset
    32
text{* Equivalence of denotational and big-step semantics: *}
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    33
43143
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    34
lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43144
diff changeset
    35
apply (induction rule: big_step_induct)
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    36
apply auto
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    37
(* while *)
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    38
apply (unfold Gamma_def)
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    39
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    40
apply fast
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    41
apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 32235
diff changeset
    42
apply auto 
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    43
done
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    44
43143
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    45
lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43144
diff changeset
    46
apply (induction c arbitrary: s t)
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 32235
diff changeset
    47
apply auto 
fdf294ee08b2 streamlined proofs
paulson
parents: 32235
diff changeset
    48
apply blast
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    49
(* while *)
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21020
diff changeset
    50
apply (erule lfp_induct2 [OF _ Gamma_mono])
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    51
apply (unfold Gamma_def)
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 32235
diff changeset
    52
apply auto
12431
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    53
done
07ec657249e5 converted to Isar
kleing
parents: 9241
diff changeset
    54
43144
631dd866b284 Made comments text
nipkow
parents: 43143
diff changeset
    55
lemma denotational_is_big_step: "(s,t) \<in> C(c)  =  ((c,s) \<Rightarrow> t)"
43143
1aeafba76f21 Fixed denotational semantics
nipkow
parents: 42174
diff changeset
    56
by (fast elim: com2 dest: com1)
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    57
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    58
end