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