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