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