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