src/HOL/IMP/Compiler.thy
author nipkow
Tue, 20 Nov 2012 17:49:26 +0100
changeset 50133 5b43abaf8415
parent 50061 7110422d4cb3
child 51259 1491459df114
permissions -rw-r--r--
tuned proof
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
     1
(* Author: Tobias Nipkow *)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
     2
50061
7110422d4cb3 tuned text
nipkow
parents: 50060
diff changeset
     3
header "Compiler for IMP"
10343
24c87e1366d8 *** empty log message ***
nipkow
parents: 10342
diff changeset
     4
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
     5
theory Compiler imports Big_Step 
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
     6
begin
12429
15c13bdc94c8 tuned for latex output
kleing
parents: 12275
diff changeset
     7
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
     8
subsection "List setup"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
     9
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    10
text {*
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    11
  We are going to define a small machine language where programs are
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    12
  lists of instructions. For nicer algebraic properties in our lemmas
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    13
  later, we prefer @{typ int} to @{term nat} as program counter.
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    14
  
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    15
  Therefore, we define notation for size and indexing for lists 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    16
  on @{typ int}:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    17
*}
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    18
abbreviation "isize xs == int (length xs)" 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    19
45637
nipkow
parents: 45616
diff changeset
    20
fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
nipkow
parents: 45616
diff changeset
    21
"(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    22
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    23
text {*
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    24
  The only additional lemma we need is indexing over append:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    25
*}
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    26
lemma inth_append [simp]:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    27
  "0 \<le> n \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    28
  (xs @ ys) !! n = (if n < isize xs then xs !! n else ys !! (n - isize xs))"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    29
by (induction xs arbitrary: n) (auto simp: algebra_simps)
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    30
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    31
subsection "Instructions and Stack Machine"
10342
b124d59f7b61 *** empty log message ***
nipkow
parents:
diff changeset
    32
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    33
datatype instr = 
45323
df7554ebe024 string -> vname
kleing
parents: 45322
diff changeset
    34
  LOADI int |
df7554ebe024 string -> vname
kleing
parents: 45322
diff changeset
    35
  LOAD vname |
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    36
  ADD |
45323
df7554ebe024 string -> vname
kleing
parents: 45322
diff changeset
    37
  STORE vname |
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    38
  JMP int |
45322
654cc47f6115 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents: 45200
diff changeset
    39
  JMPLESS int |
654cc47f6115 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents: 45200
diff changeset
    40
  JMPGE int
10342
b124d59f7b61 *** empty log message ***
nipkow
parents:
diff changeset
    41
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    42
type_synonym stack = "val list"
45637
nipkow
parents: 45616
diff changeset
    43
type_synonym config = "int \<times> state \<times> stack"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    44
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    45
abbreviation "hd2 xs == hd(tl xs)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    46
abbreviation "tl2 xs == tl(tl xs)"
11275
71498de45241 new proof
nipkow
parents: 10425
diff changeset
    47
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    48
fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    49
"iexec instr (i,s,stk) = (case instr of
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    50
  LOADI n \<Rightarrow> (i+1,s, n#stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    51
  LOAD x \<Rightarrow> (i+1,s, s x # stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    52
  ADD \<Rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    53
  STORE x \<Rightarrow> (i+1,s(x := hd stk),tl stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    54
  JMP n \<Rightarrow>  (i+1+n,s,stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    55
  JMPLESS n \<Rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    56
  JMPGE n \<Rightarrow> (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk))"
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    57
44000
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    58
definition
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    59
  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    60
     ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
44000
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    61
where
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    62
  "P \<turnstile> c \<rightarrow> c' = 
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    63
  (\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < isize P)"
44000
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    64
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    65
declare exec1_def [simp]
44000
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    66
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    67
lemma exec1I [intro, code_pred_intro]:
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    68
  "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < isize P
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    69
  \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    70
by simp
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    71
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    72
inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    73
   ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    74
where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    75
refl: "P \<turnstile> c \<rightarrow>* c" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    76
step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    77
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    78
declare refl[intro] step[intro]
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    79
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    80
lemmas exec_induct = exec.induct[split_format(complete)]
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    81
50133
5b43abaf8415 tuned proof
nipkow
parents: 50061
diff changeset
    82
code_pred exec by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    83
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    84
values
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    85
  "{(i,map t [''x'',''y''],stk) | i t stk.
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    86
    [LOAD ''y'', STORE ''x''] \<turnstile>
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 44004
diff changeset
    87
    (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    88
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    89
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    90
subsection{* Verification infrastructure *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    91
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    92
lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    93
by (induction rule: exec.induct) fastforce+
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    94
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    95
text{* Below we need to argue about the execution of code that is embedded in
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    96
larger programs. For this purpose we show that execution is preserved by
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    97
appending code to the left or right of a program. *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    98
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    99
lemma iexec_shift [simp]: 
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   100
  "((n+i',s',stk') = iexec x (n+i,s,stk)) = ((i',s',stk') = iexec x (i,s,stk))"
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   101
by(auto split:instr.split)
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   102
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   103
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   104
by auto
11275
71498de45241 new proof
nipkow
parents: 10425
diff changeset
   105
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   106
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   107
by (induction rule: exec.induct) (fastforce intro: exec1_appendR)+
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   108
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   109
lemma exec1_appendL:
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   110
  "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   111
   P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   112
by (auto split: instr.split)
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   113
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   114
lemma exec_appendL:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   115
 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')  \<Longrightarrow>
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   116
  P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   117
by (induction rule: exec_induct) (blast intro!: exec1_appendL)+
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   118
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   119
text{* Now we specialise the above lemmas to enable automatic proofs of
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   120
@{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   121
pieces of code that we already know how they execute (by induction), combined
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   122
by @{text "@"} and @{text "#"}. Backward jumps are not supported.
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   123
The details should be skipped on a first reading.
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   124
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   125
If we have just executed the first instruction of the program, drop it: *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   126
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   127
lemma exec_Cons_1 [intro]:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   128
  "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   129
  instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   130
by (drule exec_appendL[where P'="[instr]"]) simp
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   131
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   132
lemma exec_appendL_if[intro]:
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   133
 "isize P' <= i
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   134
  \<Longrightarrow> P \<turnstile> (i - isize P',s,stk) \<rightarrow>* (i',s',stk')
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   135
  \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   136
by (drule exec_appendL[where P'=P']) simp
10342
b124d59f7b61 *** empty log message ***
nipkow
parents:
diff changeset
   137
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   138
text{* Split the execution of a compound program up into the excution of its
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   139
parts: *}
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   140
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   141
lemma exec_append_trans[intro]:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   142
"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   143
 isize P \<le> i' \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   144
 P' \<turnstile>  (i' - isize P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   145
 j'' = isize P + i''
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   146
 \<Longrightarrow>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   147
 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   148
by(metis exec_trans[OF exec_appendR exec_appendL_if])
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   149
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   150
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   151
declare Let_def[simp]
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   152
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   153
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   154
subsection "Compilation"
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   155
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   156
fun acomp :: "aexp \<Rightarrow> instr list" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   157
"acomp (N n) = [LOADI n]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   158
"acomp (V x) = [LOAD x]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   159
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   160
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   161
lemma acomp_correct[intro]:
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   162
  "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   163
by (induction a arbitrary: stk) fastforce+
10342
b124d59f7b61 *** empty log message ***
nipkow
parents:
diff changeset
   164
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   165
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
45200
1f1897ac7877 renamed B to Bc
nipkow
parents: 45129
diff changeset
   166
"bcomp (Bc v) c n = (if v=c then [JMP n] else [])" |
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   167
"bcomp (Not b) c n = bcomp b (\<not>c) n" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   168
"bcomp (And b1 b2) c n =
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   169
 (let cb2 = bcomp b2 c n;
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   170
        m = (if c then isize cb2 else isize cb2+n);
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   171
      cb1 = bcomp b1 False m
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   172
  in cb1 @ cb2)" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   173
"bcomp (Less a1 a2) c n =
45322
654cc47f6115 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents: 45200
diff changeset
   174
 acomp a1 @ acomp a2 @ (if c then [JMPLESS n] else [JMPGE n])"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   175
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   176
value
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   177
  "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   178
     False 3"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   179
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   180
lemma bcomp_correct[intro]:
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   181
  "0 \<le> n \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   182
  bcomp b c n \<turnstile>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   183
 (0,s,stk)  \<rightarrow>*  (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
45129
1fce03e3e8ad tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
wenzelm
parents: 45114
diff changeset
   184
proof(induction b arbitrary: c n)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   185
  case Not
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   186
  from Not(1)[where c="~c"] Not(2) show ?case by fastforce
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   187
next
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   188
  case (And b1 b2)
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   189
  from And(1)[of "if c then isize(bcomp b2 c n) else isize(bcomp b2 c n) + n" 
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   190
                 "False"] 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   191
       And(2)[of n  "c"] And(3) 
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   192
  show ?case by fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   193
qed fastforce+
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   194
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   195
fun ccomp :: "com \<Rightarrow> instr list" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   196
"ccomp SKIP = []" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   197
"ccomp (x ::= a) = acomp a @ [STORE x]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   198
"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   199
"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   200
  (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (isize cc\<^isub>1 + 1)
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   201
   in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" |
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   202
"ccomp (WHILE b DO c) =
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   203
 (let cc = ccomp c; cb = bcomp b False (isize cc + 1)
44004
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
   204
  in cb @ cc @ [JMP (-(isize cb + isize cc + 1))])"
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
   205
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   206
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   207
value "ccomp
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   208
 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   209
  ELSE ''v'' ::= V ''u'')"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   210
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   211
value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   212
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   213
45114
fa3715b35370 fixed typos in IMP
Jean Pichon
parents: 45015
diff changeset
   214
subsection "Preservation of semantics"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   215
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   216
lemma ccomp_bigstep:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   217
  "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   218
proof(induction arbitrary: stk rule: big_step_induct)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   219
  case (Assign x a s)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   220
  show ?case by (fastforce simp:fun_upd_def cong: if_cong)
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   221
next
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45637
diff changeset
   222
  case (Seq c1 s1 s2 c2 s3)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   223
  let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   224
  have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45637
diff changeset
   225
    using Seq.IH(1) by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   226
  moreover
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   227
  have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45637
diff changeset
   228
    using Seq.IH(2) by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   229
  ultimately show ?case by simp (blast intro: exec_trans)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   230
next
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   231
  case (WhileTrue b s1 c s2 s3)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   232
  let ?cc = "ccomp c"
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   233
  let ?cb = "bcomp b False (isize ?cc + 1)"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   234
  let ?cw = "ccomp(WHILE b DO c)"
50133
5b43abaf8415 tuned proof
nipkow
parents: 50061
diff changeset
   235
  have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb,s1,stk)"
5b43abaf8415 tuned proof
nipkow
parents: 50061
diff changeset
   236
    using `bval b s1` by fastforce
5b43abaf8415 tuned proof
nipkow
parents: 50061
diff changeset
   237
  moreover
5b43abaf8415 tuned proof
nipkow
parents: 50061
diff changeset
   238
  have "?cw \<turnstile> (isize ?cb,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
5b43abaf8415 tuned proof
nipkow
parents: 50061
diff changeset
   239
    using WhileTrue.IH(1) by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   240
  moreover
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   241
  have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   242
    by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   243
  moreover
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   244
  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2))
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   245
  ultimately show ?case by(blast intro: exec_trans)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   246
qed fastforce+
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   247
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 16417
diff changeset
   248
end