src/HOL/IMP/Compiler.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 61147 263a354329e9
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
kleing@51259
     1
(* Author: Tobias Nipkow and Gerwin Klein *)
nipkow@43141
     2
wenzelm@58889
     3
section "Compiler for IMP"
nipkow@10343
     4
kleing@52915
     5
theory Compiler imports Big_Step Star
nipkow@43141
     6
begin
kleing@12429
     7
kleing@43438
     8
subsection "List setup"
kleing@43438
     9
kleing@51259
    10
text {* 
kleing@51259
    11
  In the following, we use the length of lists as integers 
kleing@51259
    12
  instead of natural numbers. Instead of converting @{typ nat}
kleing@51259
    13
  to @{typ int} explicitly, we tell Isabelle to coerce @{typ nat}
kleing@51259
    14
  automatically when necessary.
kleing@43438
    15
*}
kleing@51259
    16
declare [[coercion_enabled]] 
kleing@51259
    17
declare [[coercion "int :: nat \<Rightarrow> int"]]
kleing@43438
    18
kleing@51259
    19
text {* 
kleing@51259
    20
  Similarly, we will want to access the ith element of a list, 
kleing@51259
    21
  where @{term i} is an @{typ int}.
kleing@51259
    22
*}
nipkow@45637
    23
fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
nipkow@53869
    24
"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"
kleing@43438
    25
kleing@43438
    26
text {*
kleing@51259
    27
  The only additional lemma we need about this function 
kleing@51259
    28
  is indexing over append:
kleing@43438
    29
*}
kleing@43438
    30
lemma inth_append [simp]:
nipkow@53869
    31
  "0 \<le> i \<Longrightarrow>
nipkow@53869
    32
  (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
nipkow@53869
    33
by (induction xs arbitrary: i) (auto simp: algebra_simps)
kleing@43438
    34
nipkow@53958
    35
text{* We hide coercion @{const int} applied to @{const length}: *}
nipkow@53958
    36
nipkow@53958
    37
abbreviation (output)
nipkow@53958
    38
  "isize xs == int (length xs)"
nipkow@53958
    39
nipkow@53958
    40
notation isize ("size")
nipkow@53958
    41
nipkow@53958
    42
nipkow@43141
    43
subsection "Instructions and Stack Machine"
nipkow@10342
    44
kleing@52906
    45
text_raw{*\snip{instrdef}{0}{1}{% *}
blanchet@58310
    46
datatype instr = 
kleing@52906
    47
  LOADI int | LOAD vname | ADD | STORE vname |
kleing@52906
    48
  JMP int | JMPLESS int | JMPGE int
kleing@52906
    49
text_raw{*}%endsnip*}
nipkow@10342
    50
kleing@43438
    51
type_synonym stack = "val list"
nipkow@45637
    52
type_synonym config = "int \<times> state \<times> stack"
nipkow@43141
    53
nipkow@43141
    54
abbreviation "hd2 xs == hd(tl xs)"
nipkow@43141
    55
abbreviation "tl2 xs == tl(tl xs)"
nipkow@11275
    56
nipkow@50060
    57
fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where
nipkow@50060
    58
"iexec instr (i,s,stk) = (case instr of
nipkow@50060
    59
  LOADI n \<Rightarrow> (i+1,s, n#stk) |
nipkow@50060
    60
  LOAD x \<Rightarrow> (i+1,s, s x # stk) |
nipkow@50060
    61
  ADD \<Rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk) |
nipkow@50060
    62
  STORE x \<Rightarrow> (i+1,s(x := hd stk),tl stk) |
nipkow@50060
    63
  JMP n \<Rightarrow>  (i+1+n,s,stk) |
nipkow@50060
    64
  JMPLESS n \<Rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk) |
nipkow@50060
    65
  JMPGE n \<Rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk))"
kleing@43438
    66
kleing@44000
    67
definition
nipkow@50060
    68
  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
nipkow@50060
    69
     ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
kleing@44000
    70
where
kleing@43438
    71
  "P \<turnstile> c \<rightarrow> c' = 
kleing@51259
    72
  (\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < size P)"
kleing@44000
    73
kleing@44000
    74
lemma exec1I [intro, code_pred_intro]:
kleing@51259
    75
  "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
nipkow@50060
    76
  \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
kleing@52915
    77
by (simp add: exec1_def)
nipkow@43141
    78
kleing@52915
    79
abbreviation 
kleing@52915
    80
  exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
nipkow@43141
    81
where
kleing@52915
    82
  "exec P \<equiv> star (exec1 P)"
kleing@52915
    83
kleing@52915
    84
lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]
nipkow@43141
    85
kleing@52915
    86
code_pred exec1 by (metis exec1_def)
nipkow@43141
    87
nipkow@43141
    88
values
nipkow@43141
    89
  "{(i,map t [''x'',''y''],stk) | i t stk.
nipkow@43141
    90
    [LOAD ''y'', STORE ''x''] \<turnstile>
kleing@44036
    91
    (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
nipkow@43141
    92
nipkow@43141
    93
nipkow@43141
    94
subsection{* Verification infrastructure *}
nipkow@43141
    95
nipkow@43141
    96
text{* Below we need to argue about the execution of code that is embedded in
nipkow@43141
    97
larger programs. For this purpose we show that execution is preserved by
nipkow@43141
    98
appending code to the left or right of a program. *}
nipkow@43141
    99
nipkow@50060
   100
lemma iexec_shift [simp]: 
nipkow@50060
   101
  "((n+i',s',stk') = iexec x (n+i,s,stk)) = ((i',s',stk') = iexec x (i,s,stk))"
nipkow@50060
   102
by(auto split:instr.split)
nipkow@50060
   103
kleing@43438
   104
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
kleing@52915
   105
by (auto simp: exec1_def)
nipkow@11275
   106
nipkow@43141
   107
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
nipkow@61147
   108
by (induction rule: star.induct) (fastforce intro: star.step exec1_appendR)+
nipkow@13095
   109
nipkow@43141
   110
lemma exec1_appendL:
kleing@51259
   111
  fixes i i' :: int 
kleing@51259
   112
  shows
kleing@43438
   113
  "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
kleing@51259
   114
   P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
kleing@52915
   115
  unfolding exec1_def
kleing@52952
   116
  by (auto simp del: iexec.simps)
nipkow@13095
   117
nipkow@43141
   118
lemma exec_appendL:
kleing@51259
   119
  fixes i i' :: int 
kleing@51259
   120
  shows
nipkow@43141
   121
 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')  \<Longrightarrow>
kleing@51259
   122
  P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
nipkow@61147
   123
  by (induction rule: exec_induct) (blast intro: star.step exec1_appendL)+
nipkow@13095
   124
nipkow@43141
   125
text{* Now we specialise the above lemmas to enable automatic proofs of
nipkow@43141
   126
@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
nipkow@43141
   127
pieces of code that we already know how they execute (by induction), combined
nipkow@43141
   128
by @{text "@"} and @{text "#"}. Backward jumps are not supported.
nipkow@43141
   129
The details should be skipped on a first reading.
nipkow@13095
   130
kleing@43438
   131
If we have just executed the first instruction of the program, drop it: *}
nipkow@43141
   132
kleing@43438
   133
lemma exec_Cons_1 [intro]:
kleing@43438
   134
  "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
kleing@43438
   135
  instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
nipkow@50060
   136
by (drule exec_appendL[where P'="[instr]"]) simp
nipkow@13095
   137
nipkow@43141
   138
lemma exec_appendL_if[intro]:
nipkow@54428
   139
  fixes i i' j :: int
kleing@51259
   140
  shows
kleing@51259
   141
  "size P' <= i
nipkow@54428
   142
   \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (j,s',stk')
nipkow@54428
   143
   \<Longrightarrow> i' = size P' + j
nipkow@54428
   144
   \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')"
nipkow@50060
   145
by (drule exec_appendL[where P'=P']) simp
nipkow@10342
   146
blanchet@60542
   147
text{* Split the execution of a compound program up into the execution of its
nipkow@43141
   148
parts: *}
nipkow@13095
   149
nipkow@43141
   150
lemma exec_append_trans[intro]:
kleing@51259
   151
  fixes i' i'' j'' :: int
kleing@51259
   152
  shows
nipkow@43141
   153
"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
kleing@51259
   154
 size P \<le> i' \<Longrightarrow>
kleing@51259
   155
 P' \<turnstile>  (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
kleing@51259
   156
 j'' = size P + i''
nipkow@43141
   157
 \<Longrightarrow>
nipkow@43141
   158
 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
kleing@52915
   159
by(metis star_trans[OF exec_appendR exec_appendL_if])
nipkow@13095
   160
nipkow@43141
   161
nipkow@50060
   162
declare Let_def[simp]
nipkow@13095
   163
nipkow@13095
   164
nipkow@43141
   165
subsection "Compilation"
nipkow@13095
   166
nipkow@43141
   167
fun acomp :: "aexp \<Rightarrow> instr list" where
nipkow@43141
   168
"acomp (N n) = [LOADI n]" |
nipkow@43141
   169
"acomp (V x) = [LOAD x]" |
nipkow@43141
   170
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
nipkow@43141
   171
nipkow@43141
   172
lemma acomp_correct[intro]:
kleing@51259
   173
  "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
nipkow@50060
   174
by (induction a arbitrary: stk) fastforce+
nipkow@10342
   175
kleing@43438
   176
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
nipkow@53880
   177
"bcomp (Bc v) f n = (if v=f then [JMP n] else [])" |
nipkow@53880
   178
"bcomp (Not b) f n = bcomp b (\<not>f) n" |
nipkow@53880
   179
"bcomp (And b1 b2) f n =
nipkow@53880
   180
 (let cb2 = bcomp b2 f n;
kleing@55582
   181
        m = if f then size cb2 else (size cb2::int)+n;
nipkow@43141
   182
      cb1 = bcomp b1 False m
nipkow@43141
   183
  in cb1 @ cb2)" |
nipkow@53880
   184
"bcomp (Less a1 a2) f n =
nipkow@53880
   185
 acomp a1 @ acomp a2 @ (if f then [JMPLESS n] else [JMPGE n])"
nipkow@43141
   186
nipkow@43141
   187
value
nipkow@43141
   188
  "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
nipkow@43141
   189
     False 3"
nipkow@43141
   190
nipkow@43141
   191
lemma bcomp_correct[intro]:
kleing@51259
   192
  fixes n :: int
kleing@51259
   193
  shows
kleing@43438
   194
  "0 \<le> n \<Longrightarrow>
nipkow@53880
   195
  bcomp b f n \<turnstile>
nipkow@53880
   196
 (0,s,stk)  \<rightarrow>*  (size(bcomp b f n) + (if f = bval b s then n else 0),s,stk)"
nipkow@53880
   197
proof(induction b arbitrary: f n)
nipkow@43141
   198
  case Not
nipkow@53880
   199
  from Not(1)[where f="~f"] Not(2) show ?case by fastforce
nipkow@13095
   200
next
nipkow@43141
   201
  case (And b1 b2)
nipkow@53880
   202
  from And(1)[of "if f then size(bcomp b2 f n) else size(bcomp b2 f n) + n" 
kleing@43438
   203
                 "False"] 
nipkow@53880
   204
       And(2)[of n f] And(3) 
nipkow@44890
   205
  show ?case by fastforce
nipkow@44890
   206
qed fastforce+
nipkow@43141
   207
nipkow@43141
   208
fun ccomp :: "com \<Rightarrow> instr list" where
nipkow@43141
   209
"ccomp SKIP = []" |
nipkow@43141
   210
"ccomp (x ::= a) = acomp a @ [STORE x]" |
wenzelm@53015
   211
"ccomp (c\<^sub>1;;c\<^sub>2) = ccomp c\<^sub>1 @ ccomp c\<^sub>2" |
wenzelm@53015
   212
"ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
wenzelm@53015
   213
  (let cc\<^sub>1 = ccomp c\<^sub>1; cc\<^sub>2 = ccomp c\<^sub>2; cb = bcomp b False (size cc\<^sub>1 + 1)
wenzelm@53015
   214
   in cb @ cc\<^sub>1 @ JMP (size cc\<^sub>2) # cc\<^sub>2)" |
nipkow@43141
   215
"ccomp (WHILE b DO c) =
kleing@51259
   216
 (let cc = ccomp c; cb = bcomp b False (size cc + 1)
kleing@51259
   217
  in cb @ cc @ [JMP (-(size cb + size cc + 1))])"
kleing@44004
   218
nipkow@43141
   219
nipkow@43141
   220
value "ccomp
nipkow@43141
   221
 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
nipkow@43141
   222
  ELSE ''v'' ::= V ''u'')"
nipkow@43141
   223
nipkow@43141
   224
value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
nipkow@43141
   225
nipkow@43141
   226
Jean@45114
   227
subsection "Preservation of semantics"
nipkow@43141
   228
kleing@43438
   229
lemma ccomp_bigstep:
kleing@51259
   230
  "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
nipkow@45015
   231
proof(induction arbitrary: stk rule: big_step_induct)
nipkow@43141
   232
  case (Assign x a s)
nipkow@44890
   233
  show ?case by (fastforce simp:fun_upd_def cong: if_cong)
nipkow@13095
   234
next
nipkow@47818
   235
  case (Seq c1 s1 s2 c2 s3)
nipkow@43141
   236
  let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
kleing@51259
   237
  have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
nipkow@47818
   238
    using Seq.IH(1) by fastforce
nipkow@43141
   239
  moreover
kleing@51259
   240
  have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
nipkow@47818
   241
    using Seq.IH(2) by fastforce
kleing@52915
   242
  ultimately show ?case by simp (blast intro: star_trans)
nipkow@43141
   243
next
nipkow@43141
   244
  case (WhileTrue b s1 c s2 s3)
nipkow@43141
   245
  let ?cc = "ccomp c"
kleing@51259
   246
  let ?cb = "bcomp b False (size ?cc + 1)"
nipkow@43141
   247
  let ?cw = "ccomp(WHILE b DO c)"
kleing@51259
   248
  have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb,s1,stk)"
nipkow@50133
   249
    using `bval b s1` by fastforce
nipkow@50133
   250
  moreover
kleing@51259
   251
  have "?cw \<turnstile> (size ?cb,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)"
nipkow@50133
   252
    using WhileTrue.IH(1) by fastforce
nipkow@43141
   253
  moreover
kleing@51259
   254
  have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
nipkow@44890
   255
    by fastforce
nipkow@43141
   256
  moreover
kleing@51259
   257
  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2))
kleing@52915
   258
  ultimately show ?case by(blast intro: star_trans)
nipkow@44890
   259
qed fastforce+
nipkow@13095
   260
webertj@20217
   261
end