src/HOL/IMP/Compiler0.thy
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 13130 423ce375bf65
child 16417 9bc16273c2d4
permissions -rw-r--r--
use more symbols in HTML output
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
nipkow@13095
    13
theory Compiler0 = Natural:
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
nipkow@13095
    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
nipkow@13095
    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:
nipkow@13095
    88
  assumes A: "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>"
nipkow@13095
    90
proof -
nipkow@13095
    91
 from A show ?thesis
nipkow@13095
    92
 by induct force+
nipkow@13095
    93
qed
nipkow@13095
    94
nipkow@13095
    95
lemma app_left_1:
nipkow@13095
    96
  assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
    97
  shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
nipkow@13095
    98
proof -
nipkow@13095
    99
 from A show ?thesis
nipkow@13095
   100
 by induct force+
nipkow@13095
   101
qed
nipkow@13095
   102
nipkow@13095
   103
declare rtrancl_induct2 [induct set: rtrancl]
nipkow@13095
   104
nipkow@13095
   105
lemma app_right:
nipkow@13095
   106
assumes A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
   107
shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
   108
proof -
nipkow@13095
   109
 from A show ?thesis
nipkow@13095
   110
 proof induct
nipkow@13095
   111
   show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
nipkow@13095
   112
 next
nipkow@13095
   113
   fix s1' i1' s2 i2
nipkow@13095
   114
   assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
nipkow@13095
   115
          "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
   116
   thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
   117
     by(blast intro:app_right_1 rtrancl_trans)
nipkow@13095
   118
 qed
nipkow@13095
   119
qed
nipkow@13095
   120
nipkow@13095
   121
lemma app_left:
nipkow@13095
   122
assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
   123
shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
nipkow@13095
   124
proof -
nipkow@13095
   125
  from A show ?thesis
nipkow@13095
   126
  proof induct
nipkow@13095
   127
    show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
nipkow@13095
   128
  next
nipkow@13095
   129
    fix s1' i1' s2 i2
nipkow@13095
   130
    assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
nipkow@13095
   131
           "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
nipkow@13095
   132
    thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
nipkow@13095
   133
      by(blast intro:app_left_1 rtrancl_trans)
nipkow@13095
   134
 qed
nipkow@13095
   135
qed
nipkow@13095
   136
nipkow@13095
   137
lemma app_left2:
nipkow@13095
   138
  "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
nipkow@13095
   139
   is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
nipkow@13095
   140
  by (simp add:app_left)
nipkow@13095
   141
nipkow@13095
   142
lemma app1_left:
nipkow@13095
   143
  "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
nipkow@13095
   144
   instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
nipkow@13095
   145
  by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
nipkow@13095
   146
nipkow@13095
   147
subsection "Compiler correctness"
nipkow@13095
   148
nipkow@13095
   149
declare rtrancl_into_rtrancl[trans]
nipkow@13095
   150
        converse_rtrancl_into_rtrancl[trans]
nipkow@13095
   151
        rtrancl_trans[trans]
nipkow@13095
   152
nipkow@13095
   153
text {*
nipkow@13095
   154
  The first proof; The statement is very intuitive,
nipkow@13095
   155
  but application of induction hypothesis requires the above lifting lemmas
nipkow@13095
   156
*}
nipkow@13095
   157
theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13095
   158
shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
nipkow@13095
   159
proof -
nipkow@13095
   160
  from A show ?thesis
nipkow@13095
   161
  proof induct
nipkow@13095
   162
    show "\<And>s. ?P \<SKIP> s s" by simp
nipkow@13095
   163
  next
nipkow@13095
   164
    show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
nipkow@13095
   165
  next
nipkow@13095
   166
    fix c0 c1 s0 s1 s2
nipkow@13095
   167
    assume "?P c0 s0 s1"
nipkow@13095
   168
    hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
nipkow@13095
   169
      by(rule app_right)
nipkow@13095
   170
    moreover assume "?P c1 s1 s2"
nipkow@13095
   171
    hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
nipkow@13095
   172
           \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
nipkow@13095
   173
    proof -
nipkow@13095
   174
      show "\<And>is1 is2 s1 s2 i2.
nipkow@13095
   175
	      is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
nipkow@13095
   176
	      is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
nipkow@13095
   177
	using app_left[of _ 0] by simp
nipkow@13095
   178
    qed
nipkow@13095
   179
    ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
nipkow@13095
   180
                       \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
nipkow@13095
   181
      by (rule rtrancl_trans)
nipkow@13095
   182
    thus "?P (c0; c1) s0 s2" by simp
nipkow@13095
   183
  next
nipkow@13095
   184
    fix b c0 c1 s0 s1
nipkow@13095
   185
    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
nipkow@13095
   186
    assume "b s0" and IH: "?P c0 s0 s1"
nipkow@13095
   187
    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
nipkow@13095
   188
    also from IH
nipkow@13095
   189
    have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
nipkow@13095
   190
      by(auto intro:app1_left app_right)
nipkow@13095
   191
    also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
nipkow@13095
   192
      by(auto)
nipkow@13095
   193
    finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
nipkow@13095
   194
  next
nipkow@13095
   195
    fix b c0 c1 s0 s1
nipkow@13095
   196
    let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
nipkow@13095
   197
    assume "\<not>b s0" and IH: "?P c1 s0 s1"
nipkow@13095
   198
    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
nipkow@13095
   199
    also from IH
nipkow@13095
   200
    have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
nipkow@13095
   201
      by(force intro!:app_left2 app1_left)
nipkow@13095
   202
    finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
nipkow@13095
   203
  next
nipkow@13095
   204
    fix b c and s::state
nipkow@13095
   205
    assume "\<not>b s"
nipkow@13095
   206
    thus "?P (\<WHILE> b \<DO> c) s s" by force
nipkow@13095
   207
  next
nipkow@13095
   208
    fix b c and s0::state and s1 s2
nipkow@13095
   209
    let ?comp = "compile(\<WHILE> b \<DO> c)"
nipkow@13095
   210
    assume "b s0" and
nipkow@13095
   211
      IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
nipkow@13095
   212
    hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
nipkow@13095
   213
    also from IHc
nipkow@13095
   214
    have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
nipkow@13095
   215
      by(auto intro:app1_left app_right)
nipkow@13095
   216
    also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
nipkow@13095
   217
    also note IHw
nipkow@13095
   218
    finally show "?P (\<WHILE> b \<DO> c) s0 s2".
nipkow@13095
   219
  qed
nipkow@13095
   220
qed
nipkow@13095
   221
nipkow@13095
   222
text {*
nipkow@13095
   223
  Second proof; statement is generalized to cater for prefixes and suffixes;
nipkow@13095
   224
  needs none of the lifting lemmas, but instantiations of pre/suffix.
nipkow@13095
   225
  *}
nipkow@13130
   226
(*
nipkow@13112
   227
theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
nipkow@13112
   228
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
   229
      (is "\<And>a z. ?P c s t a z")
nipkow@13112
   230
proof -
nipkow@13112
   231
  from A show "\<And>a z. ?thesis a z"
nipkow@13112
   232
  proof induct
nipkow@13112
   233
    case Skip thus ?case by simp
nipkow@13112
   234
  next
nipkow@13112
   235
    case Assign thus ?case by (force intro!: ASIN)
nipkow@13112
   236
  next
nipkow@13112
   237
    fix c1 c2 s s' s'' a z
nipkow@13112
   238
    assume IH1: "\<And>a z. ?P c1 s s' a z" and IH2: "\<And>a z. ?P c2 s' s'' a z"
nipkow@13112
   239
    from IH1 IH2[of "a@compile c1"]
nipkow@13112
   240
    show "?P (c1;c2) s s'' a z"
nipkow@13112
   241
      by(simp add:add_assoc[THEN sym])(blast intro:rtrancl_trans)
nipkow@13112
   242
  next
nipkow@13112
   243
(* at this point I gave up converting to structured proofs *)
nipkow@13095
   244
(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
nipkow@13095
   245
   apply(intro strip)
nipkow@13095
   246
   (* instantiate assumption sufficiently for later: *)
nipkow@13095
   247
   apply(erule_tac x = "a@[?I]" in allE)
nipkow@13095
   248
   apply(simp)
nipkow@13095
   249
   (* execute JMPF: *)
nipkow@13095
   250
   apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   251
    apply(force intro!: JMPFT)
nipkow@13095
   252
   (* execute compile c0: *)
nipkow@13095
   253
   apply(rule rtrancl_trans)
nipkow@13095
   254
    apply(erule allE)
nipkow@13095
   255
    apply assumption
nipkow@13095
   256
   (* execute JMPF: *)
nipkow@13095
   257
   apply(rule r_into_rtrancl)
nipkow@13095
   258
   apply(force intro!: JMPFF)
nipkow@13095
   259
(* end of case b is true *)
nipkow@13095
   260
  apply(intro strip)
nipkow@13095
   261
  apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
nipkow@13095
   262
  apply(simp add:add_assoc)
nipkow@13095
   263
  apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   264
   apply(force intro!: JMPFF)
nipkow@13095
   265
  apply(blast)
nipkow@13095
   266
 apply(force intro: JMPFF)
nipkow@13095
   267
apply(intro strip)
nipkow@13095
   268
apply(erule_tac x = "a@[?I]" in allE)
nipkow@13095
   269
apply(erule_tac x = a in allE)
nipkow@13095
   270
apply(simp)
nipkow@13095
   271
apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   272
 apply(force intro!: JMPFT)
nipkow@13095
   273
apply(rule rtrancl_trans)
nipkow@13095
   274
 apply(erule allE)
nipkow@13095
   275
 apply assumption
nipkow@13095
   276
apply(rule converse_rtrancl_into_rtrancl)
nipkow@13095
   277
 apply(force intro!: JMPB)
nipkow@13095
   278
apply(simp)
nipkow@13095
   279
done
nipkow@13130
   280
*)
nipkow@13095
   281
text {* Missing: the other direction! I did much of it, and although
nipkow@13095
   282
the main lemma is very similar to the one in the new development, the
nipkow@13095
   283
lemmas surrounding it seemed much more complicated. In the end I gave
nipkow@13095
   284
up. *}
nipkow@13095
   285
nipkow@13095
   286
end