src/HOL/IMP/Types.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 58889 5b7a9633cfa8
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
wenzelm@58889
     1
section "A Typed Language"
nipkow@43150
     2
nipkow@43150
     3
theory Types imports Star Complex_Main begin
nipkow@43150
     4
kleing@52405
     5
text {* We build on @{theory Complex_Main} instead of @{theory Main} to access
kleing@52405
     6
the real numbers. *}
kleing@52405
     7
nipkow@43150
     8
subsection "Arithmetic Expressions"
nipkow@43150
     9
blanchet@58310
    10
datatype val = Iv int | Rv real
nipkow@43150
    11
nipkow@45212
    12
type_synonym vname = string
nipkow@45212
    13
type_synonym state = "vname \<Rightarrow> val"
nipkow@43150
    14
kleing@51461
    15
text_raw{*\snip{aexptDef}{0}{2}{% *}
blanchet@58310
    16
datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
kleing@51461
    17
text_raw{*}%endsnip*}
nipkow@43150
    18
nipkow@43150
    19
inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
nipkow@43150
    20
"taval (Ic i) s (Iv i)" |
nipkow@43150
    21
"taval (Rc r) s (Rv r)" |
nipkow@43150
    22
"taval (V x) s (s x)" |
nipkow@43150
    23
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2)
nipkow@43150
    24
 \<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))" |
kleing@44020
    25
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
nipkow@43150
    26
 \<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))"
nipkow@43150
    27
nipkow@43150
    28
inductive_cases [elim!]:
nipkow@43150
    29
  "taval (Ic i) s v"  "taval (Rc i) s v"
nipkow@43150
    30
  "taval (V x) s v"
nipkow@43150
    31
  "taval (Plus a1 a2) s v"
nipkow@43150
    32
nipkow@43150
    33
subsection "Boolean Expressions"
nipkow@43150
    34
blanchet@58310
    35
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
nipkow@43150
    36
nipkow@43150
    37
inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
nipkow@45200
    38
"tbval (Bc v) s v" |
nipkow@43150
    39
"tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
kleing@44020
    40
"tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
kleing@44020
    41
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
kleing@44020
    42
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
nipkow@43150
    43
nipkow@43150
    44
subsection "Syntax of Commands"
nipkow@43150
    45
(* a copy of Com.thy - keep in sync! *)
nipkow@43150
    46
blanchet@58310
    47
datatype
nipkow@43150
    48
  com = SKIP 
nipkow@47818
    49
      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
nipkow@52046
    50
      | Seq    com  com         ("_;; _"  [60, 61] 60)
nipkow@43150
    51
      | If     bexp com com     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
nipkow@43150
    52
      | While  bexp com         ("WHILE _ DO _"  [0, 61] 61)
nipkow@43150
    53
nipkow@43150
    54
nipkow@43150
    55
subsection "Small-Step Semantics of Commands"
nipkow@43150
    56
nipkow@43150
    57
inductive
nipkow@43150
    58
  small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
nipkow@43150
    59
where
nipkow@43150
    60
Assign:  "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" |
nipkow@43150
    61
nipkow@52046
    62
Seq1:   "(SKIP;;c,s) \<rightarrow> (c,s)" |
nipkow@52046
    63
Seq2:   "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;;c2,s) \<rightarrow> (c1';;c2,s')" |
nipkow@43150
    64
nipkow@43150
    65
IfTrue:  "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" |
nipkow@43150
    66
IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
nipkow@43150
    67
nipkow@52046
    68
While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
nipkow@43150
    69
nipkow@43150
    70
lemmas small_step_induct = small_step.induct[split_format(complete)]
nipkow@43150
    71
nipkow@43150
    72
subsection "The Type System"
nipkow@43150
    73
blanchet@58310
    74
datatype ty = Ity | Rty
nipkow@43150
    75
nipkow@45212
    76
type_synonym tyenv = "vname \<Rightarrow> ty"
nipkow@43150
    77
nipkow@43150
    78
inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
nipkow@43150
    79
  ("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
nipkow@43150
    80
where
nipkow@43150
    81
Ic_ty: "\<Gamma> \<turnstile> Ic i : Ity" |
nipkow@43150
    82
Rc_ty: "\<Gamma> \<turnstile> Rc r : Rty" |
nipkow@43150
    83
V_ty: "\<Gamma> \<turnstile> V x : \<Gamma> x" |
nipkow@43150
    84
Plus_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Plus a1 a2 : \<tau>"
nipkow@43150
    85
kleing@55572
    86
declare atyping.intros [intro!]
kleing@55572
    87
inductive_cases [elim!]:
kleing@55572
    88
  "\<Gamma> \<turnstile> V x : \<tau>" "\<Gamma> \<turnstile> Ic i : \<tau>" "\<Gamma> \<turnstile> Rc r : \<tau>" "\<Gamma> \<turnstile> Plus a1 a2 : \<tau>"
kleing@55572
    89
nipkow@43150
    90
text{* Warning: the ``:'' notation leads to syntactic ambiguities,
nipkow@43150
    91
i.e. multiple parse trees, because ``:'' also stands for set membership.
nipkow@43150
    92
In most situations Isabelle's type system will reject all but one parse tree,
nipkow@43150
    93
but will still inform you of the potential ambiguity. *}
nipkow@43150
    94
nipkow@43150
    95
inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
nipkow@43150
    96
where
nipkow@45200
    97
B_ty: "\<Gamma> \<turnstile> Bc v" |
nipkow@43150
    98
Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
nipkow@43150
    99
And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
nipkow@43150
   100
Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"
nipkow@43150
   101
kleing@55572
   102
declare btyping.intros [intro!]
kleing@55572
   103
inductive_cases [elim!]: "\<Gamma> \<turnstile> Not b" "\<Gamma> \<turnstile> And b1 b2" "\<Gamma> \<turnstile> Less a1 a2"
kleing@55572
   104
nipkow@43150
   105
inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
nipkow@43150
   106
Skip_ty: "\<Gamma> \<turnstile> SKIP" |
nipkow@43150
   107
Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
nipkow@52046
   108
Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;;c2" |
nipkow@43150
   109
If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
nipkow@43150
   110
While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"
nipkow@43150
   111
kleing@55572
   112
declare ctyping.intros [intro!]
nipkow@43150
   113
inductive_cases [elim!]:
nipkow@52046
   114
  "\<Gamma> \<turnstile> x ::= a"  "\<Gamma> \<turnstile> c1;;c2"
nipkow@43150
   115
  "\<Gamma> \<turnstile> IF b THEN c1 ELSE c2"
nipkow@43150
   116
  "\<Gamma> \<turnstile> WHILE b DO c"
nipkow@43150
   117
nipkow@43150
   118
subsection "Well-typed Programs Do Not Get Stuck"
nipkow@43150
   119
nipkow@43150
   120
fun type :: "val \<Rightarrow> ty" where
nipkow@43150
   121
"type (Iv i) = Ity" |
nipkow@43150
   122
"type (Rv r) = Rty"
nipkow@43150
   123
nipkow@54610
   124
lemma type_eq_Ity[simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
nipkow@43150
   125
by (cases v) simp_all
nipkow@43150
   126
nipkow@54610
   127
lemma type_eq_Rty[simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)"
nipkow@43150
   128
by (cases v) simp_all
nipkow@43150
   129
nipkow@43150
   130
definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>" 50)
nipkow@43150
   131
where "\<Gamma> \<turnstile> s  \<longleftrightarrow>  (\<forall>x. type (s x) = \<Gamma> x)"
nipkow@43150
   132
nipkow@43150
   133
lemma apreservation:
nipkow@43150
   134
  "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
nipkow@45015
   135
apply(induction arbitrary: v rule: atyping.induct)
nipkow@44890
   136
apply (fastforce simp: styping_def)+
nipkow@43150
   137
done
nipkow@43150
   138
nipkow@43150
   139
lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
nipkow@45015
   140
proof(induction rule: atyping.induct)
nipkow@43150
   141
  case (Plus_ty \<Gamma> a1 t a2)
nipkow@43150
   142
  then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast
nipkow@43150
   143
  show ?case
nipkow@43150
   144
  proof (cases v1)
nipkow@43150
   145
    case Iv
nipkow@45015
   146
    with Plus_ty v show ?thesis
nipkow@44890
   147
      by(fastforce intro: taval.intros(4) dest!: apreservation)
nipkow@43150
   148
  next
nipkow@43150
   149
    case Rv
nipkow@45015
   150
    with Plus_ty v show ?thesis
nipkow@44890
   151
      by(fastforce intro: taval.intros(5) dest!: apreservation)
nipkow@43150
   152
  qed
nipkow@43150
   153
qed (auto intro: taval.intros)
nipkow@43150
   154
nipkow@43150
   155
lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v"
nipkow@45015
   156
proof(induction rule: btyping.induct)
nipkow@43150
   157
  case (Less_ty \<Gamma> a1 t a2)
nipkow@43150
   158
  then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
nipkow@43150
   159
    by (metis aprogress)
nipkow@43150
   160
  show ?case
nipkow@43150
   161
  proof (cases v1)
nipkow@43150
   162
    case Iv
nipkow@43150
   163
    with Less_ty v show ?thesis
nipkow@44890
   164
      by (fastforce intro!: tbval.intros(4) dest!:apreservation)
nipkow@43150
   165
  next
nipkow@43150
   166
    case Rv
nipkow@43150
   167
    with Less_ty v show ?thesis
nipkow@44890
   168
      by (fastforce intro!: tbval.intros(5) dest!:apreservation)
nipkow@43150
   169
  qed
nipkow@43150
   170
qed (auto intro: tbval.intros)
nipkow@43150
   171
nipkow@43150
   172
theorem progress:
nipkow@43150
   173
  "\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
nipkow@45015
   174
proof(induction rule: ctyping.induct)
nipkow@43150
   175
  case Skip_ty thus ?case by simp
nipkow@43150
   176
next
nipkow@43150
   177
  case Assign_ty 
nipkow@43150
   178
  thus ?case by (metis Assign aprogress)
nipkow@43150
   179
next
nipkow@47818
   180
  case Seq_ty thus ?case by simp (metis Seq1 Seq2)
nipkow@43150
   181
next
nipkow@43150
   182
  case (If_ty \<Gamma> b c1 c2)
nipkow@43150
   183
  then obtain bv where "tbval b s bv" by (metis bprogress)
nipkow@43150
   184
  show ?case
nipkow@43150
   185
  proof(cases bv)
nipkow@43150
   186
    assume "bv"
nipkow@43150
   187
    with `tbval b s bv` show ?case by simp (metis IfTrue)
nipkow@43150
   188
  next
nipkow@43150
   189
    assume "\<not>bv"
nipkow@43150
   190
    with `tbval b s bv` show ?case by simp (metis IfFalse)
nipkow@43150
   191
  qed
nipkow@43150
   192
next
nipkow@43150
   193
  case While_ty show ?case by (metis While)
nipkow@43150
   194
qed
nipkow@43150
   195
nipkow@43150
   196
theorem styping_preservation:
nipkow@43150
   197
  "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'"
nipkow@45015
   198
proof(induction rule: small_step_induct)
nipkow@43150
   199
  case Assign thus ?case
nipkow@43150
   200
    by (auto simp: styping_def) (metis Assign(1,3) apreservation)
nipkow@43150
   201
qed auto
nipkow@43150
   202
nipkow@43150
   203
theorem ctyping_preservation:
nipkow@43150
   204
  "(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> c'"
nipkow@43150
   205
by (induct rule: small_step_induct) (auto simp: ctyping.intros)
nipkow@43150
   206
nipkow@43150
   207
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
nipkow@43150
   208
where "x \<rightarrow>* y == star small_step x y"
nipkow@43150
   209
nipkow@43150
   210
theorem type_sound:
nipkow@43150
   211
  "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP
nipkow@43150
   212
   \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
nipkow@45015
   213
apply(induction rule:star_induct)
nipkow@43150
   214
apply (metis progress)
nipkow@43150
   215
by (metis styping_preservation ctyping_preservation)
nipkow@43150
   216
nipkow@43150
   217
end