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