src/HOL/IMP/Compiler0.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 23746 a455e69c31cc
child 27363 6d93bbe5633e
permissions -rw-r--r--
avoid rebinding of existing facts;
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
berghofe@23746
    24
inductive_set
berghofe@23746
    25
  stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
berghofe@23746
    26
  and stepa1' :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
berghofe@23746
    27
    ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
berghofe@23746
    28
  for P :: "instr list"
berghofe@23746
    29
where
berghofe@23746
    30
  "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : stepa1 P"
berghofe@23746
    31
| ASIN[simp]:
berghofe@23746
    32
  "\<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>"
berghofe@23746
    33
| JMPFT[simp,intro]:
berghofe@23746
    34
  "\<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>"
berghofe@23746
    35
| JMPFF[simp,intro]:
berghofe@23746
    36
  "\<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>"
berghofe@23746
    37
| JMPB[simp]:
berghofe@23746
    38
  "\<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>"
kleing@14565
    39
berghofe@23746
    40
abbreviation
berghofe@23746
    41
  stepa :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
berghofe@23746
    42
    ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)  where
berghofe@23746
    43
  "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^*)"
nipkow@13095
    44
berghofe@23746
    45
abbreviation
berghofe@23746
    46
  stepan :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
berghofe@23746
    47
    ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)  where
berghofe@23746
    48
  "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^i)"
nipkow@13095
    49
nipkow@13095
    50
subsection "The compiler"
nipkow@13095
    51
nipkow@13095
    52
consts compile :: "com \<Rightarrow> instr list"
nipkow@13095
    53
primrec
nipkow@13095
    54
"compile \<SKIP> = []"
nipkow@13095
    55
"compile (x:==a) = [ASIN x a]"
nipkow@13095
    56
"compile (c1;c2) = compile c1 @ compile c2"
nipkow@13095
    57
"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
nipkow@13095
    58
 [JMPF b (length(compile c1) + 2)] @ compile c1 @
nipkow@13095
    59
 [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
nipkow@13095
    60
"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
nipkow@13095
    61
 [JMPB (length(compile c)+1)]"
nipkow@13095
    62
nipkow@13095
    63
declare nth_append[simp]
nipkow@13095
    64
nipkow@13095
    65
subsection "Context lifting lemmas"
nipkow@13095
    66
wenzelm@18372
    67
text {*
nipkow@13095
    68
  Some lemmas for lifting an execution into a prefix and suffix
nipkow@13095
    69
  of instructions; only needed for the first proof.
nipkow@13095
    70
*}
nipkow@13095
    71
lemma app_right_1:
wenzelm@18372
    72
  assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
    73
  shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
    74
  using prems
wenzelm@18372
    75
  by induct auto
nipkow@13095
    76
nipkow@13095
    77
lemma app_left_1:
wenzelm@18372
    78
  assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
    79
  shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
wenzelm@18372
    80
  using prems
wenzelm@18372
    81
  by induct auto
nipkow@13095
    82
nipkow@13095
    83
declare rtrancl_induct2 [induct set: rtrancl]
nipkow@13095
    84
nipkow@13095
    85
lemma app_right:
wenzelm@18372
    86
  assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
    87
  shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
    88
  using prems
wenzelm@18372
    89
proof induct
wenzelm@18372
    90
  show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
wenzelm@18372
    91
next
wenzelm@18372
    92
  fix s1' i1' s2 i2
wenzelm@18372
    93
  assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
wenzelm@18372
    94
    and "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
    95
  thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
    96
    by (blast intro: app_right_1 rtrancl_trans)
nipkow@13095
    97
qed
nipkow@13095
    98
nipkow@13095
    99
lemma app_left:
wenzelm@18372
   100
  assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
   101
  shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
wenzelm@18372
   102
using prems
wenzelm@18372
   103
proof induct
wenzelm@18372
   104
  show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
wenzelm@18372
   105
next
wenzelm@18372
   106
  fix s1' i1' s2 i2
wenzelm@18372
   107
  assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
wenzelm@18372
   108
    and "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
   109
  thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
wenzelm@18372
   110
    by (blast intro: app_left_1 rtrancl_trans)
nipkow@13095
   111
qed
nipkow@13095
   112
nipkow@13095
   113
lemma app_left2:
nipkow@13095
   114
  "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
wenzelm@18372
   115
    is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
wenzelm@18372
   116
  by (simp add: app_left)
nipkow@13095
   117
nipkow@13095
   118
lemma app1_left:
wenzelm@18372
   119
  assumes "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
wenzelm@18372
   120
  shows "instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
wenzelm@18372
   121
proof -
wenzelm@18372
   122
  from app_left [OF prems, of "[instr]"]
wenzelm@18372
   123
  show ?thesis by simp
wenzelm@18372
   124
qed
nipkow@13095
   125
nipkow@13095
   126
subsection "Compiler correctness"
nipkow@13095
   127
nipkow@13095
   128
declare rtrancl_into_rtrancl[trans]
nipkow@13095
   129
        converse_rtrancl_into_rtrancl[trans]
nipkow@13095
   130
        rtrancl_trans[trans]
nipkow@13095
   131
nipkow@13095
   132
text {*
nipkow@13095
   133
  The first proof; The statement is very intuitive,
nipkow@13095
   134
  but application of induction hypothesis requires the above lifting lemmas
nipkow@13095
   135
*}
wenzelm@18372
   136
theorem
wenzelm@18372
   137
  assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
wenzelm@18372
   138
  shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
wenzelm@18372
   139
  using prems
wenzelm@18372
   140
proof induct
wenzelm@18372
   141
  show "\<And>s. ?P \<SKIP> s s" by simp
wenzelm@18372
   142
next
wenzelm@18372
   143
  show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
wenzelm@18372
   144
next
wenzelm@18372
   145
  fix c0 c1 s0 s1 s2
wenzelm@18372
   146
  assume "?P c0 s0 s1"
wenzelm@18372
   147
  hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
wenzelm@18372
   148
    by (rule app_right)
wenzelm@18372
   149
  moreover assume "?P c1 s1 s2"
wenzelm@18372
   150
  hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
wenzelm@18372
   151
    \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
wenzelm@18372
   152
  proof -
wenzelm@18372
   153
    show "\<And>is1 is2 s1 s2 i2.
wenzelm@18372
   154
      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
wenzelm@18372
   155
      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
wenzelm@18372
   156
      using app_left[of _ 0] by simp
nipkow@13095
   157
  qed
wenzelm@18372
   158
  ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
wenzelm@18372
   159
      \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
wenzelm@18372
   160
    by (rule rtrancl_trans)
wenzelm@18372
   161
  thus "?P (c0; c1) s0 s2" by simp
wenzelm@18372
   162
next
wenzelm@18372
   163
  fix b c0 c1 s0 s1
wenzelm@18372
   164
  let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
wenzelm@18372
   165
  assume "b s0" and IH: "?P c0 s0 s1"
wenzelm@18372
   166
  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
wenzelm@18372
   167
  also from IH
wenzelm@18372
   168
  have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
wenzelm@18372
   169
    by(auto intro:app1_left app_right)
wenzelm@18372
   170
  also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
wenzelm@18372
   171
    by(auto)
wenzelm@18372
   172
  finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
wenzelm@18372
   173
next
wenzelm@18372
   174
  fix b c0 c1 s0 s1
wenzelm@18372
   175
  let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
wenzelm@18372
   176
  assume "\<not>b s0" and IH: "?P c1 s0 s1"
wenzelm@18372
   177
  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
wenzelm@18372
   178
  also from IH
wenzelm@18372
   179
  have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
wenzelm@18372
   180
    by (force intro!: app_left2 app1_left)
wenzelm@18372
   181
  finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
wenzelm@18372
   182
next
wenzelm@18372
   183
  fix b c and s::state
wenzelm@18372
   184
  assume "\<not>b s"
wenzelm@18372
   185
  thus "?P (\<WHILE> b \<DO> c) s s" by force
wenzelm@18372
   186
next
wenzelm@18372
   187
  fix b c and s0::state and s1 s2
wenzelm@18372
   188
  let ?comp = "compile(\<WHILE> b \<DO> c)"
wenzelm@18372
   189
  assume "b s0" and
wenzelm@18372
   190
    IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
wenzelm@18372
   191
  hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
wenzelm@18372
   192
  also from IHc
wenzelm@18372
   193
  have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
wenzelm@18372
   194
    by (auto intro: app1_left app_right)
wenzelm@18372
   195
  also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
wenzelm@18372
   196
  also note IHw
wenzelm@18372
   197
  finally show "?P (\<WHILE> b \<DO> c) s0 s2".
nipkow@13095
   198
qed
nipkow@13095
   199
nipkow@13095
   200
text {*
nipkow@13095
   201
  Second proof; statement is generalized to cater for prefixes and suffixes;
nipkow@13095
   202
  needs none of the lifting lemmas, but instantiations of pre/suffix.
nipkow@13095
   203
  *}
nipkow@13130
   204
(*
nipkow@13112
   205
theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13112
   206
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
   207
      (is "\<And>a z. ?P c s t a z")
nipkow@13112
   208
proof -
nipkow@13112
   209
  from A show "\<And>a z. ?thesis a z"
nipkow@13112
   210
  proof induct
nipkow@13112
   211
    case Skip thus ?case by simp
nipkow@13112
   212
  next
nipkow@13112
   213
    case Assign thus ?case by (force intro!: ASIN)
nipkow@13112
   214
  next
nipkow@13112
   215
    fix c1 c2 s s' s'' a z
nipkow@13112
   216
    assume IH1: "\<And>a z. ?P c1 s s' a z" and IH2: "\<And>a z. ?P c2 s' s'' a z"
nipkow@13112
   217
    from IH1 IH2[of "a@compile c1"]
nipkow@13112
   218
    show "?P (c1;c2) s s'' a z"
nipkow@13112
   219
      by(simp add:add_assoc[THEN sym])(blast intro:rtrancl_trans)
nipkow@13112
   220
  next
nipkow@13112
   221
(* at this point I gave up converting to structured proofs *)
nipkow@13095
   222
(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
nipkow@13095
   223
   apply(intro strip)
nipkow@13095
   224
   (* instantiate assumption sufficiently for later: *)
nipkow@13095
   225
   apply(erule_tac x = "a@[?I]" in allE)
nipkow@13095
   226
   apply(simp)
nipkow@13095
   227
   (* execute JMPF: *)
nipkow@13095
   228
   apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   229
    apply(force intro!: JMPFT)
nipkow@13095
   230
   (* execute compile c0: *)
nipkow@13095
   231
   apply(rule rtrancl_trans)
nipkow@13095
   232
    apply(erule allE)
nipkow@13095
   233
    apply assumption
nipkow@13095
   234
   (* execute JMPF: *)
nipkow@13095
   235
   apply(rule r_into_rtrancl)
nipkow@13095
   236
   apply(force intro!: JMPFF)
nipkow@13095
   237
(* end of case b is true *)
nipkow@13095
   238
  apply(intro strip)
nipkow@13095
   239
  apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
nipkow@13095
   240
  apply(simp add:add_assoc)
nipkow@13095
   241
  apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   242
   apply(force intro!: JMPFF)
nipkow@13095
   243
  apply(blast)
nipkow@13095
   244
 apply(force intro: JMPFF)
nipkow@13095
   245
apply(intro strip)
nipkow@13095
   246
apply(erule_tac x = "a@[?I]" in allE)
nipkow@13095
   247
apply(erule_tac x = a in allE)
nipkow@13095
   248
apply(simp)
nipkow@13095
   249
apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   250
 apply(force intro!: JMPFT)
nipkow@13095
   251
apply(rule rtrancl_trans)
nipkow@13095
   252
 apply(erule allE)
nipkow@13095
   253
 apply assumption
nipkow@13095
   254
apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   255
 apply(force intro!: JMPB)
nipkow@13095
   256
apply(simp)
nipkow@13095
   257
done
nipkow@13130
   258
*)
nipkow@13095
   259
text {* Missing: the other direction! I did much of it, and although
nipkow@13095
   260
the main lemma is very similar to the one in the new development, the
nipkow@13095
   261
lemmas surrounding it seemed much more complicated. In the end I gave
nipkow@13095
   262
up. *}
nipkow@13095
   263
nipkow@13095
   264
end