src/HOL/IMP/Compiler.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45637 5f85efcb50c1
child 47818 151d137f1095
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
     3
header "A 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))"
45616
nipkow
parents: 45323
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
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    48
inductive iexec1 :: "instr \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"
44004
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
    49
    ("(_/ \<turnstile>i (_ \<rightarrow>/ _))" [59,0,59] 60)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    50
where
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    51
"LOADI n \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, n#stk)" |
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    52
"LOAD x  \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, s x # stk)" |
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    53
"ADD     \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s, (hd2 stk + hd stk) # tl2 stk)" |
45616
nipkow
parents: 45323
diff changeset
    54
"STORE x \<turnstile>i (i,s,stk) \<rightarrow> (i+1,s(x := hd stk),tl stk)" |
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    55
"JMP n   \<turnstile>i (i,s,stk) \<rightarrow> (i+1+n,s,stk)" |
45322
654cc47f6115 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents: 45200
diff changeset
    56
"JMPLESS n \<turnstile>i (i,s,stk) \<rightarrow> (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" |
654cc47f6115 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents: 45200
diff changeset
    57
"JMPGE n \<turnstile>i (i,s,stk) \<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
    58
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    59
code_pred iexec1 .
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    60
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    61
declare iexec1.intros
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    62
44000
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    63
definition
44004
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
    64
  exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool"  ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60) 
44000
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    65
where
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    66
  "P \<turnstile> c \<rightarrow> c' = 
44004
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
    67
  (\<exists>i s stk. c = (i,s,stk) \<and> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c' \<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
    68
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    69
declare exec1_def [simp] 
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    70
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    71
lemma exec1I [intro, code_pred_intro]:
44004
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
    72
  assumes "P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'" "0 \<le> i" "i < isize P" 
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
    73
  shows "P \<turnstile> (i,s,stk) \<rightarrow> c'"
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
    74
  using assms by simp
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    75
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    76
inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    77
where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    78
refl: "P \<turnstile> c \<rightarrow>* c" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    79
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
    80
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    81
declare refl[intro] step[intro]
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    82
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    83
lemmas exec_induct = exec.induct[split_format(complete)]
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    84
44000
ab4d8499815c resolved code_pred FIXME in IMP; clearer notation for exec_n
kleing
parents: 43438
diff changeset
    85
code_pred exec by force
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    86
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    87
values
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    88
  "{(i,map t [''x'',''y''],stk) | i t stk.
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    89
    [LOAD ''y'', STORE ''x''] \<turnstile>
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 44004
diff changeset
    90
    (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
43141
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
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
    93
subsection{* Verification infrastructure *}
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
lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
45616
nipkow
parents: 45323
diff changeset
    96
  by (induction rule: exec.induct) fastforce+
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    97
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    98
inductive_cases iexec1_cases [elim!]:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
    99
  "LOADI n \<turnstile>i c \<rightarrow> c'" 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   100
  "LOAD x  \<turnstile>i c \<rightarrow> c'"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   101
  "ADD     \<turnstile>i c \<rightarrow> c'"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   102
  "STORE n \<turnstile>i c \<rightarrow> c'" 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   103
  "JMP n   \<turnstile>i c \<rightarrow> c'"
45322
654cc47f6115 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents: 45200
diff changeset
   104
  "JMPLESS n \<turnstile>i c \<rightarrow> c'"
654cc47f6115 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents: 45200
diff changeset
   105
  "JMPGE n \<turnstile>i c \<rightarrow> c'"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   106
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   107
text {* Simplification rules for @{const iexec1}. *}
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   108
lemma iexec1_simps [simp]:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   109
  "LOADI n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, n # stk))"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   110
  "LOAD x \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, s x # stk))"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   111
  "ADD \<turnstile>i c \<rightarrow> c' = 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   112
  (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s, (hd2 stk + hd stk) # tl2 stk))"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   113
  "STORE x \<turnstile>i c \<rightarrow> c' = 
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 44004
diff changeset
   114
  (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1, s(x := hd stk), tl stk))"
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   115
  "JMP n \<turnstile>i c \<rightarrow> c' = (\<exists>i s stk. c = (i, s, stk) \<and> c' = (i + 1 + n, s, stk))"
45322
654cc47f6115 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents: 45200
diff changeset
   116
   "JMPLESS n \<turnstile>i c \<rightarrow> c' = 
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   117
  (\<exists>i s stk. c = (i, s, stk) \<and> 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   118
             c' = (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk))"  
45322
654cc47f6115 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents: 45200
diff changeset
   119
  "JMPGE n \<turnstile>i c \<rightarrow> c' = 
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   120
  (\<exists>i s stk. c = (i, s, stk) \<and> 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   121
             c' = (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk))"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   122
  by (auto split del: split_if intro!: iexec1.intros)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   123
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   124
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   125
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
   126
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
   127
appending code to the left or right of a program. *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   128
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   129
lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   130
  by auto
11275
71498de45241 new proof
nipkow
parents: 10425
diff changeset
   131
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   132
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
45616
nipkow
parents: 45323
diff changeset
   133
  by (induction rule: exec.induct) (fastforce intro: exec1_appendR)+
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   134
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   135
lemma iexec1_shiftI:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   136
  assumes "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   137
  shows "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   138
  using assms by cases auto
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   139
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   140
lemma iexec1_shiftD:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   141
  assumes "X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   142
  shows "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   143
  using assms by cases auto
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   144
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   145
lemma iexec_shift [simp]: 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   146
  "(X \<turnstile>i (n+i,s,stk) \<rightarrow> (n+i',s',stk')) = (X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk'))"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   147
  by (blast intro: iexec1_shiftI dest: iexec1_shiftD)
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   148
  
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   149
lemma exec1_appendL:
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   150
  "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   151
   P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   152
  by simp
13095
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
lemma exec_appendL:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   155
 "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
   156
  P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')"
45616
nipkow
parents: 45323
diff changeset
   157
  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
   158
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   159
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
   160
@{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
   161
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
   162
by @{text "@"} and @{text "#"}. Backward jumps are not supported.
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   163
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
   164
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   165
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
   166
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   167
lemma exec_Cons_1 [intro]:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   168
  "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   169
  instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   170
  by (drule exec_appendL[where P'="[instr]"]) simp
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   171
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   172
lemma exec_appendL_if[intro]:
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   173
 "isize P' <= i
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   174
  \<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
   175
  \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')"
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   176
  by (drule exec_appendL[where P'=P']) simp
10342
b124d59f7b61 *** empty log message ***
nipkow
parents:
diff changeset
   177
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   178
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
   179
parts: *}
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   180
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   181
lemma exec_append_trans[intro]:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   182
"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
   183
 isize P \<le> i' \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   184
 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
   185
 j'' = isize P + i''
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   186
 \<Longrightarrow>
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   187
 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   188
  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
   189
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   190
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   191
declare Let_def[simp] 
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   192
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   193
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   194
subsection "Compilation"
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   195
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   196
fun acomp :: "aexp \<Rightarrow> instr list" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   197
"acomp (N n) = [LOADI n]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   198
"acomp (V x) = [LOAD x]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   199
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   200
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   201
lemma acomp_correct[intro]:
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   202
  "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)"
45616
nipkow
parents: 45323
diff changeset
   203
  by (induction a arbitrary: stk) fastforce+
10342
b124d59f7b61 *** empty log message ***
nipkow
parents:
diff changeset
   204
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   205
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
45200
1f1897ac7877 renamed B to Bc
nipkow
parents: 45129
diff changeset
   206
"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
   207
"bcomp (Not b) c n = bcomp b (\<not>c) n" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   208
"bcomp (And b1 b2) c n =
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   209
 (let cb2 = bcomp b2 c n;
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   210
        m = (if c then isize cb2 else isize cb2+n);
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   211
      cb1 = bcomp b1 False m
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   212
  in cb1 @ cb2)" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   213
"bcomp (Less a1 a2) c n =
45322
654cc47f6115 JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
kleing
parents: 45200
diff changeset
   214
 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
   215
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   216
value
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   217
  "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
   218
     False 3"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   219
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   220
lemma bcomp_correct[intro]:
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   221
  "0 \<le> n \<Longrightarrow>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   222
  bcomp b c n \<turnstile>
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   223
 (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
   224
proof(induction b arbitrary: c n)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   225
  case Not
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   226
  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
   227
next
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   228
  case (And b1 b2)
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   229
  from And(1)[of "if c then isize (bcomp b2 c n) else isize (bcomp b2 c n) + n" 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   230
                 "False"] 
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   231
       And(2)[of n  "c"] And(3) 
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   232
  show ?case by fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   233
qed fastforce+
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   234
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   235
fun ccomp :: "com \<Rightarrow> instr list" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   236
"ccomp SKIP = []" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   237
"ccomp (x ::= a) = acomp a @ [STORE x]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   238
"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
   239
"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
   240
  (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
   241
   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
   242
"ccomp (WHILE b DO c) =
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   243
 (let cc = ccomp c; cb = bcomp b False (isize cc + 1)
44004
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
   244
  in cb @ cc @ [JMP (-(isize cb + isize cc + 1))])"
a9fcbafdf208 compiler proof cleanup
kleing
parents: 44000
diff changeset
   245
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   246
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   247
value "ccomp
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   248
 (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
   249
  ELSE ''v'' ::= V ''u'')"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   250
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   251
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
   252
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   253
45114
fa3715b35370 fixed typos in IMP
Jean Pichon
parents: 45015
diff changeset
   254
subsection "Preservation of semantics"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   255
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   256
lemma ccomp_bigstep:
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   257
  "(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
   258
proof(induction arbitrary: stk rule: big_step_induct)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   259
  case (Assign x a s)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   260
  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
   261
next
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   262
  case (Semi c1 s1 s2 c2 s3)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   263
  let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   264
  have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   265
    using Semi.IH(1) by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   266
  moreover
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   267
  have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   268
    using Semi.IH(2) by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   269
  ultimately show ?case by simp (blast intro: exec_trans)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   270
next
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   271
  case (WhileTrue b s1 c s2 s3)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   272
  let ?cc = "ccomp c"
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   273
  let ?cb = "bcomp b False (isize ?cc + 1)"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   274
  let ?cw = "ccomp(WHILE b DO c)"
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   275
  have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   276
    using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   277
  moreover
43438
a666b8d11252 IMP compiler with int, added reverse soundness direction
kleing
parents: 43158
diff changeset
   278
  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
   279
    by fastforce
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 32960
diff changeset
   280
  moreover
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   281
  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
   282
  ultimately show ?case by(blast intro: exec_trans)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44036
diff changeset
   283
qed fastforce+
13095
8ed413a57bdc New machine architecture and other direction of compiler proof.
nipkow
parents: 12566
diff changeset
   284
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 16417
diff changeset
   285
end