src/HOL/IMP/Compiler.thy
author blanchet
Mon, 22 Jun 2015 16:56:03 +0200
changeset 60542 c5953e3a1e4f
parent 58889 5b7a9633cfa8
child 61147 263a354329e9
permissions -rw-r--r--
fixed typo
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
     1
(* Author: Tobias Nipkow and Gerwin Klein *)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
     2
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 58310
diff changeset
     3
section "Compiler for IMP"
10343
24c87e1366d8 *** empty log message ***
nipkow
parents: 10342
diff changeset
     4
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
     5
theory Compiler imports Big_Step Star
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
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    10
text {* 
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    11
  In the following, we use the length of lists as integers 
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    12
  instead of natural numbers. Instead of converting @{typ nat}
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    13
  to @{typ int} explicitly, we tell Isabelle to coerce @{typ nat}
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    14
  automatically when necessary.
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    15
*}
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    16
declare [[coercion_enabled]] 
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    17
declare [[coercion "int :: nat \<Rightarrow> int"]]
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    18
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    19
text {* 
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    20
  Similarly, we will want to access the ith element of a list, 
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    21
  where @{term i} is an @{typ int}.
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    22
*}
45637
nipkow
parents: 45616
diff changeset
    23
fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
53869
nipkow
parents: 53015
diff changeset
    24
"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"
43438
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
text {*
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    27
  The only additional lemma we need about this function 
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    28
  is indexing over append:
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    29
*}
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    30
lemma inth_append [simp]:
53869
nipkow
parents: 53015
diff changeset
    31
  "0 \<le> i \<Longrightarrow>
nipkow
parents: 53015
diff changeset
    32
  (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
nipkow
parents: 53015
diff changeset
    33
by (induction xs arbitrary: i) (auto simp: algebra_simps)
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    34
53958
50673b362324 hide coercion
nipkow
parents: 53880
diff changeset
    35
text{* We hide coercion @{const int} applied to @{const length}: *}
50673b362324 hide coercion
nipkow
parents: 53880
diff changeset
    36
50673b362324 hide coercion
nipkow
parents: 53880
diff changeset
    37
abbreviation (output)
50673b362324 hide coercion
nipkow
parents: 53880
diff changeset
    38
  "isize xs == int (length xs)"
50673b362324 hide coercion
nipkow
parents: 53880
diff changeset
    39
50673b362324 hide coercion
nipkow
parents: 53880
diff changeset
    40
notation isize ("size")
50673b362324 hide coercion
nipkow
parents: 53880
diff changeset
    41
50673b362324 hide coercion
nipkow
parents: 53880
diff changeset
    42
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    43
subsection "Instructions and Stack Machine"
10342
b124d59f7b61 *** empty log message ***
nipkow
parents:
diff changeset
    44
52906
ba514b5aa809 snippet for instr type
kleing
parents: 52046
diff changeset
    45
text_raw{*\snip{instrdef}{0}{1}{% *}
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    46
datatype instr = 
52906
ba514b5aa809 snippet for instr type
kleing
parents: 52046
diff changeset
    47
  LOADI int | LOAD vname | ADD | STORE vname |
ba514b5aa809 snippet for instr type
kleing
parents: 52046
diff changeset
    48
  JMP int | JMPLESS int | JMPGE int
ba514b5aa809 snippet for instr type
kleing
parents: 52046
diff changeset
    49
text_raw{*}%endsnip*}
10342
b124d59f7b61 *** empty log message ***
nipkow
parents:
diff changeset
    50
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    51
type_synonym stack = "val list"
45637
nipkow
parents: 45616
diff changeset
    52
type_synonym config = "int \<times> state \<times> stack"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    53
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    54
abbreviation "hd2 xs == hd(tl xs)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    55
abbreviation "tl2 xs == tl(tl xs)"
11275
71498de45241 new proof
nipkow
parents: 10425
diff changeset
    56
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    57
fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    58
"iexec instr (i,s,stk) = (case instr of
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    59
  LOADI n \<Rightarrow> (i+1,s, n#stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    60
  LOAD x \<Rightarrow> (i+1,s, s x # stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    61
  ADD \<Rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    62
  STORE x \<Rightarrow> (i+1,s(x := hd stk),tl stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    63
  JMP n \<Rightarrow>  (i+1+n,s,stk) |
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    64
  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
    65
  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
    66
44000
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    67
definition
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    68
  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    69
     ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
44000
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    70
where
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    71
  "P \<turnstile> c \<rightarrow> c' = 
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    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)"
44000
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    73
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    74
lemma exec1I [intro, code_pred_intro]:
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
    75
  "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
    76
  \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
    77
by (simp add: exec1_def)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    78
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
    79
abbreviation 
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
    80
  exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" 50)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    81
where
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
    82
  "exec P \<equiv> star (exec1 P)"
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
    83
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
    84
declare star.step[intro]
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    85
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
    86
lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    87
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
    88
code_pred exec1 by (metis exec1_def)
43141
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
values
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    91
  "{(i,map t [''x'',''y''],stk) | i t stk.
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    92
    [LOAD ''y'', STORE ''x''] \<turnstile>
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 44004
diff changeset
    93
    (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
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
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    96
subsection{* Verification infrastructure *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    97
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    98
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
    99
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
   100
appending code to the left or right of a program. *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   101
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   102
lemma iexec_shift [simp]: 
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   103
  "((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
   104
by(auto split:instr.split)
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   105
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   106
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
   107
by (auto simp: exec1_def)
11275
71498de45241 new proof
nipkow
parents: 10425
diff changeset
   108
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   109
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
   110
by (induction rule: star.induct) (fastforce intro: exec1_appendR)+
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   111
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   112
lemma exec1_appendL:
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   113
  fixes i i' :: int 
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   114
  shows
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   115
  "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   116
   P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
   117
  unfolding exec1_def
52952
07423b37bc22 avoid unnecessary case distinction
kleing
parents: 52924
diff changeset
   118
  by (auto simp del: iexec.simps)
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   119
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   120
lemma exec_appendL:
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   121
  fixes i i' :: int 
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   122
  shows
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   123
 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')  \<Longrightarrow>
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   124
  P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   125
  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
   126
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   127
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
   128
@{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
   129
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
   130
by @{text "@"} and @{text "#"}. Backward jumps are not supported.
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   131
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
   132
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   133
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
   134
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   135
lemma exec_Cons_1 [intro]:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   136
  "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   137
  instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   138
by (drule exec_appendL[where P'="[instr]"]) simp
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   139
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   140
lemma exec_appendL_if[intro]:
54428
6ccc6130140c tuned to improve automation (for REPEAT)
nipkow
parents: 53958
diff changeset
   141
  fixes i i' j :: int
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   142
  shows
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   143
  "size P' <= i
54428
6ccc6130140c tuned to improve automation (for REPEAT)
nipkow
parents: 53958
diff changeset
   144
   \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (j,s',stk')
6ccc6130140c tuned to improve automation (for REPEAT)
nipkow
parents: 53958
diff changeset
   145
   \<Longrightarrow> i' = size P' + j
6ccc6130140c tuned to improve automation (for REPEAT)
nipkow
parents: 53958
diff changeset
   146
   \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   147
by (drule exec_appendL[where P'=P']) simp
10342
b124d59f7b61 *** empty log message ***
nipkow
parents:
diff changeset
   148
60542
c5953e3a1e4f fixed typo
blanchet
parents: 58889
diff changeset
   149
text{* Split the execution of a compound program up into the execution of its
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   150
parts: *}
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   151
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   152
lemma exec_append_trans[intro]:
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   153
  fixes i' i'' j'' :: int
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   154
  shows
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   155
"P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   156
 size P \<le> i' \<Longrightarrow>
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   157
 P' \<turnstile>  (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   158
 j'' = size P + i''
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   159
 \<Longrightarrow>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   160
 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
   161
by(metis star_trans[OF exec_appendR exec_appendL_if])
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   162
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   163
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   164
declare Let_def[simp]
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   165
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   166
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   167
subsection "Compilation"
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   168
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   169
fun acomp :: "aexp \<Rightarrow> instr list" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   170
"acomp (N n) = [LOADI n]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   171
"acomp (V x) = [LOAD x]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   172
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   173
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   174
lemma acomp_correct[intro]:
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   175
  "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
50060
43753eca324a replaced relation by function - simplifies development
nipkow
parents: 47818
diff changeset
   176
by (induction a arbitrary: stk) fastforce+
10342
b124d59f7b61 *** empty log message ***
nipkow
parents:
diff changeset
   177
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   178
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
53880
nipkow
parents: 53869
diff changeset
   179
"bcomp (Bc v) f n = (if v=f then [JMP n] else [])" |
nipkow
parents: 53869
diff changeset
   180
"bcomp (Not b) f n = bcomp b (\<not>f) n" |
nipkow
parents: 53869
diff changeset
   181
"bcomp (And b1 b2) f n =
nipkow
parents: 53869
diff changeset
   182
 (let cb2 = bcomp b2 f n;
55582
20054fc56d17 tuned definition
kleing
parents: 54428
diff changeset
   183
        m = if f then size cb2 else (size cb2::int)+n;
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   184
      cb1 = bcomp b1 False m
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   185
  in cb1 @ cb2)" |
53880
nipkow
parents: 53869
diff changeset
   186
"bcomp (Less a1 a2) f n =
nipkow
parents: 53869
diff changeset
   187
 acomp a1 @ acomp a2 @ (if f then [JMPLESS n] else [JMPGE n])"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   188
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   189
value
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   190
  "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
   191
     False 3"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   192
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   193
lemma bcomp_correct[intro]:
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   194
  fixes n :: int
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   195
  shows
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   196
  "0 \<le> n \<Longrightarrow>
53880
nipkow
parents: 53869
diff changeset
   197
  bcomp b f n \<turnstile>
nipkow
parents: 53869
diff changeset
   198
 (0,s,stk)  \<rightarrow>*  (size(bcomp b f n) + (if f = bval b s then n else 0),s,stk)"
nipkow
parents: 53869
diff changeset
   199
proof(induction b arbitrary: f n)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   200
  case Not
53880
nipkow
parents: 53869
diff changeset
   201
  from Not(1)[where f="~f"] Not(2) show ?case by fastforce
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   202
next
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   203
  case (And b1 b2)
53880
nipkow
parents: 53869
diff changeset
   204
  from And(1)[of "if f then size(bcomp b2 f n) else size(bcomp b2 f n) + n" 
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   205
                 "False"] 
53880
nipkow
parents: 53869
diff changeset
   206
       And(2)[of n f] And(3) 
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   207
  show ?case by fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   208
qed fastforce+
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   209
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   210
fun ccomp :: "com \<Rightarrow> instr list" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   211
"ccomp SKIP = []" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   212
"ccomp (x ::= a) = acomp a @ [STORE x]" |
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52952
diff changeset
   213
"ccomp (c\<^sub>1;;c\<^sub>2) = ccomp c\<^sub>1 @ ccomp c\<^sub>2" |
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52952
diff changeset
   214
"ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52952
diff changeset
   215
  (let cc\<^sub>1 = ccomp c\<^sub>1; cc\<^sub>2 = ccomp c\<^sub>2; cb = bcomp b False (size cc\<^sub>1 + 1)
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52952
diff changeset
   216
   in cb @ cc\<^sub>1 @ JMP (size cc\<^sub>2) # cc\<^sub>2)" |
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   217
"ccomp (WHILE b DO c) =
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   218
 (let cc = ccomp c; cb = bcomp b False (size cc + 1)
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   219
  in cb @ cc @ [JMP (-(size cb + size cc + 1))])"
44004
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
   220
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   221
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   222
value "ccomp
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   223
 (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
   224
  ELSE ''v'' ::= V ''u'')"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   225
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   226
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
   227
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   228
45114
fa3715b35370 fixed typos in IMP
Jean Pichon
parents: 45015
diff changeset
   229
subsection "Preservation of semantics"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   230
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   231
lemma ccomp_bigstep:
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   232
  "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   233
proof(induction arbitrary: stk rule: big_step_induct)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   234
  case (Assign x a s)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   235
  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
   236
next
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45637
diff changeset
   237
  case (Seq c1 s1 s2 c2 s3)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   238
  let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   239
  have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45637
diff changeset
   240
    using Seq.IH(1) by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   241
  moreover
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   242
  have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45637
diff changeset
   243
    using Seq.IH(2) by fastforce
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
   244
  ultimately show ?case by simp (blast intro: star_trans)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   245
next
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   246
  case (WhileTrue b s1 c s2 s3)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   247
  let ?cc = "ccomp c"
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   248
  let ?cb = "bcomp b False (size ?cc + 1)"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   249
  let ?cw = "ccomp(WHILE b DO c)"
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   250
  have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb,s1,stk)"
50133
5b43abaf8415 tuned proof
nipkow
parents: 50061
diff changeset
   251
    using `bval b s1` by fastforce
5b43abaf8415 tuned proof
nipkow
parents: 50061
diff changeset
   252
  moreover
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   253
  have "?cw \<turnstile> (size ?cb,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)"
50133
5b43abaf8415 tuned proof
nipkow
parents: 50061
diff changeset
   254
    using WhileTrue.IH(1) by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   255
  moreover
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   256
  have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   257
    by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   258
  moreover
51259
1491459df114 eliminated isize in favour of size + type coercion
kleing
parents: 50133
diff changeset
   259
  have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2))
52915
c10bd1f49ff5 avoid re-inventing transitive closure
kleing
parents: 52906
diff changeset
   260
  ultimately show ?case by(blast intro: star_trans)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   261
qed fastforce+
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   262
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 16417
diff changeset
   263
end