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