src/HOL/IMP/Compiler0.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 18372 2bffdf62fe7f
child 23746 a455e69c31cc
permissions -rw-r--r--
adaptions to codegen_package
nipkow@13095
     1
(*  Title:      HOL/IMP/Compiler.thy
nipkow@13095
     2
    ID:         $Id$
nipkow@13095
     3
    Author:     Tobias Nipkow, TUM
nipkow@13095
     4
    Copyright   1996 TUM
nipkow@13095
     5
nipkow@13095
     6
This is an early version of the compiler, where the abstract machine
nipkow@13095
     7
has an explicit pc. This turned out to be awkward, and a second
nipkow@13095
     8
development was started. See Machines.thy and Compiler.thy.
nipkow@13095
     9
*)
nipkow@13095
    10
nipkow@13095
    11
header "A Simple Compiler"
nipkow@13095
    12
haftmann@16417
    13
theory Compiler0 imports Natural begin
nipkow@13095
    14
nipkow@13095
    15
subsection "An abstract, simplistic machine"
nipkow@13095
    16
nipkow@13095
    17
text {* There are only three instructions: *}
nipkow@13095
    18
datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
nipkow@13095
    19
nipkow@13095
    20
text {* We describe execution of programs in the machine by
nipkow@13095
    21
  an operational (small step) semantics:
nipkow@13095
    22
*}
nipkow@13095
    23
consts  stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
nipkow@13095
    24
nipkow@13095
    25
syntax
nipkow@13095
    26
  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
nipkow@13095
    27
               ("_ |- (3<_,_>/ -1-> <_,_>)" [50,0,0,0,0] 50)
nipkow@13095
    28
  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
nipkow@13095
    29
               ("_ |-/ (3<_,_>/ -*-> <_,_>)" [50,0,0,0,0] 50)
nipkow@13095
    30
nipkow@13095
    31
  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
nipkow@13095
    32
               ("_ |-/ (3<_,_>/ -(_)-> <_,_>)" [50,0,0,0,0,0] 50)
nipkow@13095
    33
nipkow@13095
    34
syntax (xsymbols)
nipkow@13095
    35
  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
nipkow@13095
    36
               ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
nipkow@13095
    37
  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
nipkow@13095
    38
               ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
nipkow@13095
    39
  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
nipkow@13095
    40
               ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
nipkow@13095
    41
kleing@14565
    42
syntax (HTML output)
kleing@14565
    43
  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
kleing@14565
    44
               ("_ |- (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
kleing@14565
    45
  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
kleing@14565
    46
               ("_ |-/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
kleing@14565
    47
  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
kleing@14565
    48
               ("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
kleing@14565
    49
wenzelm@18372
    50
translations
nipkow@13095
    51
  "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
nipkow@13095
    52
  "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
nipkow@13095
    53
  "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^i)"
nipkow@13095
    54
nipkow@13095
    55
inductive "stepa1 P"
nipkow@13095
    56
intros
nipkow@13095
    57
ASIN[simp]:
nipkow@13095
    58
  "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s[x\<mapsto> a s],Suc n\<rangle>"
nipkow@13095
    59
JMPFT[simp,intro]:
nipkow@13095
    60
  "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,Suc n\<rangle>"
nipkow@13095
    61
JMPFF[simp,intro]:
nipkow@13095
    62
  "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,m\<rangle>"
nipkow@13095
    63
JMPB[simp]:
nipkow@13095
    64
  "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,j\<rangle>"
nipkow@13095
    65
nipkow@13095
    66
subsection "The compiler"
nipkow@13095
    67
nipkow@13095
    68
consts compile :: "com \<Rightarrow> instr list"
nipkow@13095
    69
primrec
nipkow@13095
    70
"compile \<SKIP> = []"
nipkow@13095
    71
"compile (x:==a) = [ASIN x a]"
nipkow@13095
    72
"compile (c1;c2) = compile c1 @ compile c2"
nipkow@13095
    73
"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
nipkow@13095
    74
 [JMPF b (length(compile c1) + 2)] @ compile c1 @
nipkow@13095
    75
 [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
nipkow@13095
    76
"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
nipkow@13095
    77
 [JMPB (length(compile c)+1)]"
nipkow@13095
    78
nipkow@13095
    79
declare nth_append[simp]
nipkow@13095
    80
nipkow@13095
    81
subsection "Context lifting lemmas"
nipkow@13095
    82
wenzelm@18372
    83
text {*
nipkow@13095
    84
  Some lemmas for lifting an execution into a prefix and suffix
nipkow@13095
    85
  of instructions; only needed for the first proof.
nipkow@13095
    86
*}
nipkow@13095
    87
lemma app_right_1:
wenzelm@18372
    88
  assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
    89
  shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
    90
  using prems
wenzelm@18372
    91
  by induct auto
nipkow@13095
    92
nipkow@13095
    93
lemma app_left_1:
wenzelm@18372
    94
  assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
    95
  shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
wenzelm@18372
    96
  using prems
wenzelm@18372
    97
  by induct auto
nipkow@13095
    98
nipkow@13095
    99
declare rtrancl_induct2 [induct set: rtrancl]
nipkow@13095
   100
nipkow@13095
   101
lemma app_right:
wenzelm@18372
   102
  assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
   103
  shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
   104
  using prems
wenzelm@18372
   105
proof induct
wenzelm@18372
   106
  show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
wenzelm@18372
   107
next
wenzelm@18372
   108
  fix s1' i1' s2 i2
wenzelm@18372
   109
  assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
wenzelm@18372
   110
    and "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
   111
  thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
   112
    by (blast intro: app_right_1 rtrancl_trans)
nipkow@13095
   113
qed
nipkow@13095
   114
nipkow@13095
   115
lemma app_left:
wenzelm@18372
   116
  assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
   117
  shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
wenzelm@18372
   118
using prems
wenzelm@18372
   119
proof induct
wenzelm@18372
   120
  show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
wenzelm@18372
   121
next
wenzelm@18372
   122
  fix s1' i1' s2 i2
wenzelm@18372
   123
  assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
wenzelm@18372
   124
    and "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
   125
  thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
wenzelm@18372
   126
    by (blast intro: app_left_1 rtrancl_trans)
nipkow@13095
   127
qed
nipkow@13095
   128
nipkow@13095
   129
lemma app_left2:
nipkow@13095
   130
  "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
wenzelm@18372
   131
    is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
wenzelm@18372
   132
  by (simp add: app_left)
nipkow@13095
   133
nipkow@13095
   134
lemma app1_left:
wenzelm@18372
   135
  assumes "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
   136
  shows "instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
wenzelm@18372
   137
proof -
wenzelm@18372
   138
  from app_left [OF prems, of "[instr]"]
wenzelm@18372
   139
  show ?thesis by simp
wenzelm@18372
   140
qed
nipkow@13095
   141
nipkow@13095
   142
subsection "Compiler correctness"
nipkow@13095
   143
nipkow@13095
   144
declare rtrancl_into_rtrancl[trans]
nipkow@13095
   145
        converse_rtrancl_into_rtrancl[trans]
nipkow@13095
   146
        rtrancl_trans[trans]
nipkow@13095
   147
nipkow@13095
   148
text {*
nipkow@13095
   149
  The first proof; The statement is very intuitive,
nipkow@13095
   150
  but application of induction hypothesis requires the above lifting lemmas
nipkow@13095
   151
*}
wenzelm@18372
   152
theorem
wenzelm@18372
   153
  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
wenzelm@18372
   154
  shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
wenzelm@18372
   155
  using prems
wenzelm@18372
   156
proof induct
wenzelm@18372
   157
  show "\<And>s. ?P \<SKIP> s s" by simp
wenzelm@18372
   158
next
wenzelm@18372
   159
  show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
wenzelm@18372
   160
next
wenzelm@18372
   161
  fix c0 c1 s0 s1 s2
wenzelm@18372
   162
  assume "?P c0 s0 s1"
wenzelm@18372
   163
  hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
wenzelm@18372
   164
    by (rule app_right)
wenzelm@18372
   165
  moreover assume "?P c1 s1 s2"
wenzelm@18372
   166
  hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
wenzelm@18372
   167
    \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
wenzelm@18372
   168
  proof -
wenzelm@18372
   169
    show "\<And>is1 is2 s1 s2 i2.
wenzelm@18372
   170
      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
wenzelm@18372
   171
      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
wenzelm@18372
   172
      using app_left[of _ 0] by simp
nipkow@13095
   173
  qed
wenzelm@18372
   174
  ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
wenzelm@18372
   175
      \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
wenzelm@18372
   176
    by (rule rtrancl_trans)
wenzelm@18372
   177
  thus "?P (c0; c1) s0 s2" by simp
wenzelm@18372
   178
next
wenzelm@18372
   179
  fix b c0 c1 s0 s1
wenzelm@18372
   180
  let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
wenzelm@18372
   181
  assume "b s0" and IH: "?P c0 s0 s1"
wenzelm@18372
   182
  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
wenzelm@18372
   183
  also from IH
wenzelm@18372
   184
  have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
wenzelm@18372
   185
    by(auto intro:app1_left app_right)
wenzelm@18372
   186
  also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
wenzelm@18372
   187
    by(auto)
wenzelm@18372
   188
  finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
wenzelm@18372
   189
next
wenzelm@18372
   190
  fix b c0 c1 s0 s1
wenzelm@18372
   191
  let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
wenzelm@18372
   192
  assume "\<not>b s0" and IH: "?P c1 s0 s1"
wenzelm@18372
   193
  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
wenzelm@18372
   194
  also from IH
wenzelm@18372
   195
  have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
wenzelm@18372
   196
    by (force intro!: app_left2 app1_left)
wenzelm@18372
   197
  finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
wenzelm@18372
   198
next
wenzelm@18372
   199
  fix b c and s::state
wenzelm@18372
   200
  assume "\<not>b s"
wenzelm@18372
   201
  thus "?P (\<WHILE> b \<DO> c) s s" by force
wenzelm@18372
   202
next
wenzelm@18372
   203
  fix b c and s0::state and s1 s2
wenzelm@18372
   204
  let ?comp = "compile(\<WHILE> b \<DO> c)"
wenzelm@18372
   205
  assume "b s0" and
wenzelm@18372
   206
    IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
wenzelm@18372
   207
  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
wenzelm@18372
   208
  also from IHc
wenzelm@18372
   209
  have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
wenzelm@18372
   210
    by (auto intro: app1_left app_right)
wenzelm@18372
   211
  also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
wenzelm@18372
   212
  also note IHw
wenzelm@18372
   213
  finally show "?P (\<WHILE> b \<DO> c) s0 s2".
nipkow@13095
   214
qed
nipkow@13095
   215
nipkow@13095
   216
text {*
nipkow@13095
   217
  Second proof; statement is generalized to cater for prefixes and suffixes;
nipkow@13095
   218
  needs none of the lifting lemmas, but instantiations of pre/suffix.
nipkow@13095
   219
  *}
nipkow@13130
   220
(*
nipkow@13112
   221
theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13112
   222
shows "\<And>a z. a@compile c@z \<turnstile> \<langle>s,size a\<rangle> -*\<rightarrow> \<langle>t,size a + size(compile c)\<rangle>"
nipkow@13112
   223
      (is "\<And>a z. ?P c s t a z")
nipkow@13112
   224
proof -
nipkow@13112
   225
  from A show "\<And>a z. ?thesis a z"
nipkow@13112
   226
  proof induct
nipkow@13112
   227
    case Skip thus ?case by simp
nipkow@13112
   228
  next
nipkow@13112
   229
    case Assign thus ?case by (force intro!: ASIN)
nipkow@13112
   230
  next
nipkow@13112
   231
    fix c1 c2 s s' s'' a z
nipkow@13112
   232
    assume IH1: "\<And>a z. ?P c1 s s' a z" and IH2: "\<And>a z. ?P c2 s' s'' a z"
nipkow@13112
   233
    from IH1 IH2[of "a@compile c1"]
nipkow@13112
   234
    show "?P (c1;c2) s s'' a z"
nipkow@13112
   235
      by(simp add:add_assoc[THEN sym])(blast intro:rtrancl_trans)
nipkow@13112
   236
  next
nipkow@13112
   237
(* at this point I gave up converting to structured proofs *)
nipkow@13095
   238
(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
nipkow@13095
   239
   apply(intro strip)
nipkow@13095
   240
   (* instantiate assumption sufficiently for later: *)
nipkow@13095
   241
   apply(erule_tac x = "a@[?I]" in allE)
nipkow@13095
   242
   apply(simp)
nipkow@13095
   243
   (* execute JMPF: *)
nipkow@13095
   244
   apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   245
    apply(force intro!: JMPFT)
nipkow@13095
   246
   (* execute compile c0: *)
nipkow@13095
   247
   apply(rule rtrancl_trans)
nipkow@13095
   248
    apply(erule allE)
nipkow@13095
   249
    apply assumption
nipkow@13095
   250
   (* execute JMPF: *)
nipkow@13095
   251
   apply(rule r_into_rtrancl)
nipkow@13095
   252
   apply(force intro!: JMPFF)
nipkow@13095
   253
(* end of case b is true *)
nipkow@13095
   254
  apply(intro strip)
nipkow@13095
   255
  apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
nipkow@13095
   256
  apply(simp add:add_assoc)
nipkow@13095
   257
  apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   258
   apply(force intro!: JMPFF)
nipkow@13095
   259
  apply(blast)
nipkow@13095
   260
 apply(force intro: JMPFF)
nipkow@13095
   261
apply(intro strip)
nipkow@13095
   262
apply(erule_tac x = "a@[?I]" in allE)
nipkow@13095
   263
apply(erule_tac x = a in allE)
nipkow@13095
   264
apply(simp)
nipkow@13095
   265
apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   266
 apply(force intro!: JMPFT)
nipkow@13095
   267
apply(rule rtrancl_trans)
nipkow@13095
   268
 apply(erule allE)
nipkow@13095
   269
 apply assumption
nipkow@13095
   270
apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   271
 apply(force intro!: JMPB)
nipkow@13095
   272
apply(simp)
nipkow@13095
   273
done
nipkow@13130
   274
*)
nipkow@13095
   275
text {* Missing: the other direction! I did much of it, and although
nipkow@13095
   276
the main lemma is very similar to the one in the new development, the
nipkow@13095
   277
lemmas surrounding it seemed much more complicated. In the end I gave
nipkow@13095
   278
up. *}
nipkow@13095
   279
nipkow@13095
   280
end