src/HOL/IMP/Compiler.thy
author nipkow
Fri Aug 28 18:52:41 2009 +0200 (2009-08-28)
changeset 32436 10cd49e0c067
parent 31969 09524788a6b9
child 32960 69916a850301
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 
     7 theory Compiler imports Machines begin
     8 
     9 subsection "The compiler"
    10 
    11 primrec compile :: "com \<Rightarrow> instr list"
    12 where
    13   "compile \<SKIP> = []"
    14 | "compile (x:==a) = [SET x a]"
    15 | "compile (c1;c2) = compile c1 @ compile c2"
    16 | "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
    17     [JMPF b (length(compile c1) + 1)] @ compile c1 @
    18     [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
    19 | "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
    20     [JMPB (length(compile c)+1)]"
    21 
    22 subsection "Compiler correctness"
    23 
    24 theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    25 shows "\<And>p q. \<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle>"
    26   (is "\<And>p q. ?P c s t p q")
    27 proof -
    28   from A show "\<And>p q. ?thesis p q"
    29   proof induct
    30     case Skip thus ?case by simp
    31   next
    32     case Assign thus ?case by force
    33   next
    34     case Semi thus ?case by simp (blast intro:rtrancl_trans)
    35   next
    36     fix b c0 c1 s0 s1 p q
    37     assume IH: "\<And>p q. ?P c0 s0 s1 p q"
    38     assume "b s0"
    39     thus "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1 p q"
    40       by(simp add: IH[THEN rtrancl_trans])
    41   next
    42     case IfFalse thus ?case by(simp)
    43   next
    44     case WhileFalse thus ?case by simp
    45   next
    46     fix b c and s0::state and s1 s2 p q
    47     assume b: "b s0" and
    48       IHc: "\<And>p q. ?P c s0 s1 p q" and
    49       IHw: "\<And>p q. ?P (\<WHILE> b \<DO> c) s1 s2 p q"
    50     show "?P (\<WHILE> b \<DO> c) s0 s2 p q"
    51       using b  IHc[THEN rtrancl_trans] IHw by(simp)
    52   qed
    53 qed
    54 
    55 text {* The other direction! *}
    56 
    57 inductive_cases [elim!]: "(([],p,s),(is',p',s')) : stepa1"
    58 
    59 lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
    60 apply(rule iffI)
    61  apply(erule rel_pow_E2, simp, fast)
    62 apply simp
    63 done
    64 
    65 lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
    66 by(simp add: rtrancl_is_UN_rel_pow)
    67 
    68 definition
    69   forws :: "instr \<Rightarrow> nat set" where
    70   "forws instr = (case instr of
    71      SET x a \<Rightarrow> {0} |
    72      JMPF b n \<Rightarrow> {0,n} |
    73      JMPB n \<Rightarrow> {})"
    74 
    75 definition
    76   backws :: "instr \<Rightarrow> nat set" where
    77   "backws instr = (case instr of
    78      SET x a \<Rightarrow> {} |
    79      JMPF b n \<Rightarrow> {} |
    80      JMPB n \<Rightarrow> {n})"
    81 
    82 primrec closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
    83 where
    84   "closed m n [] = True"
    85 | "closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
    86                           (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
    87 
    88 lemma [simp]:
    89  "\<And>m n. closed m n (C1@C2) =
    90          (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
    91 by(induct C1) (simp, simp add:add_ac)
    92 
    93 theorem [simp]: "\<And>m n. closed m n (compile c)"
    94 by(induct c) (simp_all add:backws_def forws_def)
    95 
    96 lemma drop_lem: "n \<le> size(p1@p2)
    97  \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =
    98     (n \<le> size p1 & p1' = drop n p1)"
    99 apply(rule iffI)
   100  defer apply simp
   101 apply(subgoal_tac "n \<le> size p1")
   102  apply simp
   103 apply(rule ccontr)
   104 apply(drule_tac f = length in arg_cong)
   105 apply simp
   106 done
   107 
   108 lemma reduce_exec1:
   109  "\<langle>i # p1 @ p2,q1 @ q2,s\<rangle> -1\<rightarrow> \<langle>p1' @ p2,q1' @ q2,s'\<rangle> \<Longrightarrow>
   110   \<langle>i # p1,q1,s\<rangle> -1\<rightarrow> \<langle>p1',q1',s'\<rangle>"
   111 by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm)
   112 
   113 
   114 lemma closed_exec1:
   115  "\<lbrakk> closed 0 0 (rev q1 @ instr # p1);
   116     \<langle>instr # p1 @ p2, q1 @ q2,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle> \<rbrakk> \<Longrightarrow>
   117   \<exists>p1' q1'. p' = p1'@p2 \<and> q' = q1'@q2 \<and> rev q1' @ p1' = rev q1 @ instr # p1"
   118 apply(clarsimp simp add:forws_def backws_def
   119                split:instr.split_asm split_if_asm)
   120 done
   121 
   122 theorem closed_execn_decomp: "\<And>C1 C2 r.
   123  \<lbrakk> closed 0 0 (rev C1 @ C2);
   124    \<langle>C2 @ p1 @ p2, C1 @ q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<rbrakk>
   125  \<Longrightarrow> \<exists>s n1 n2. \<langle>C2,C1,r\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle> \<and>
   126      \<langle>p1@p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
   127          n = n1+n2"
   128 (is "\<And>C1 C2 r. \<lbrakk>?CL C1 C2; ?H C1 C2 r n\<rbrakk> \<Longrightarrow> ?P C1 C2 r n")
   129 proof(induct n)
   130   fix C1 C2 r
   131   assume "?H C1 C2 r 0"
   132   thus "?P C1 C2 r 0" by simp
   133 next
   134   fix C1 C2 r n
   135   assume IH: "\<And>C1 C2 r. ?CL C1 C2 \<Longrightarrow> ?H C1 C2 r n \<Longrightarrow> ?P C1 C2 r n"
   136   assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)"
   137   show "?P C1 C2 r (Suc n)"
   138   proof (cases C2)
   139     assume "C2 = []" with H show ?thesis by simp
   140   next
   141     fix instr tlC2
   142     assume C2: "C2 = instr # tlC2"
   143     from H C2 obtain p' q' r'
   144       where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
   145       and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
   146       by(fastsimp simp add:rel_pow_commute)
   147     from CL closed_exec1[OF _ 1] C2
   148     obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
   149       and same: "rev C1' @ C2' = rev C1 @ C2"
   150       by fastsimp
   151     have rev_same: "rev C2' @ C1' = rev C2 @ C1"
   152     proof -
   153       have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp
   154       also have "\<dots> = rev(rev C1 @ C2)" by(simp only:same)
   155       also have "\<dots> =  rev C2 @ C1" by simp
   156       finally show ?thesis .
   157     qed
   158     hence rev_same': "\<And>p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp
   159     from n have n': "\<langle>C2' @ p1 @ p2,C1' @ q,r'\<rangle> -n\<rightarrow>
   160                      \<langle>p2,rev p1 @ rev C2' @ C1' @ q,t\<rangle>"
   161       by(simp add:pq' rev_same')
   162     from IH[OF _ n'] CL
   163     obtain s n1 n2 where n1: "\<langle>C2',C1',r'\<rangle> -n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>" and
   164       "\<langle>p1 @ p2,rev C2 @ C1 @ q,s\<rangle> -n2\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle> \<and>
   165        n = n1 + n2"
   166       by(fastsimp simp add: same rev_same rev_same')
   167     moreover
   168     from 1 n1 pq' C2 have "\<langle>C2,C1,r\<rangle> -Suc n1\<rightarrow> \<langle>[],rev C2 @ C1,s\<rangle>"
   169       by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1)
   170     ultimately show ?thesis by (fastsimp simp del:relpow.simps)
   171   qed
   172 qed
   173 
   174 lemma execn_decomp:
   175 "\<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
   176  \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
   177      \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
   178          n = n1+n2"
   179 using closed_execn_decomp[of "[]",simplified] by simp
   180 
   181 lemma exec_star_decomp:
   182 "\<langle>compile c @ p1 @ p2,q,r\<rangle> -*\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
   183  \<Longrightarrow> \<exists>s. \<langle>compile c,[],r\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
   184      \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -*\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle>"
   185 by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp)
   186 
   187 
   188 (* Alternative:
   189 lemma exec_comp_n:
   190 "\<And>p1 p2 q r t n.
   191  \<langle>compile c @ p1 @ p2,q,r\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev(compile c) @ q,t\<rangle>
   192  \<Longrightarrow> \<exists>s n1 n2. \<langle>compile c,[],r\<rangle> -n1\<rightarrow> \<langle>[],rev(compile c),s\<rangle> \<and>
   193      \<langle>p1@p2,rev(compile c) @ q,s\<rangle> -n2\<rightarrow> \<langle>p2, rev p1 @ rev(compile c) @ q,t\<rangle> \<and>
   194          n = n1+n2"
   195  (is "\<And>p1 p2 q r t n. ?H c p1 p2 q r t n \<Longrightarrow> ?P c p1 p2 q r t n")
   196 proof (induct c)
   197 *)
   198 
   199 text{*Warning: 
   200 @{prop"\<langle>compile c @ p,q,s\<rangle> -*\<rightarrow> \<langle>p,rev(compile c)@q,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"}
   201 is not true! *}
   202 
   203 theorem "\<And>s t.
   204  \<langle>compile c,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile c),t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   205 proof (induct c)
   206   fix s t
   207   assume "\<langle>compile SKIP,[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile SKIP),t\<rangle>"
   208   thus "\<langle>SKIP,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
   209 next
   210   fix s t v f
   211   assume "\<langle>compile(v :== f),[],s\<rangle> -*\<rightarrow> \<langle>[],rev(compile(v :== f)),t\<rangle>"
   212   thus "\<langle>v :== f,s\<rangle> \<longrightarrow>\<^sub>c t" by simp
   213 next
   214   fix s1 s3 c1 c2
   215   let ?C1 = "compile c1" let ?C2 = "compile c2"
   216   assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
   217      and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
   218   assume "\<langle>compile(c1;c2),[],s1\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
   219   then obtain s2 where exec1: "\<langle>?C1,[],s1\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,s2\<rangle>" and
   220              exec2: "\<langle>?C2,rev ?C1,s2\<rangle> -*\<rightarrow> \<langle>[],rev(compile(c1;c2)),s3\<rangle>"
   221     by(fastsimp dest:exec_star_decomp[of _ _ "[]" "[]",simplified])
   222   from exec2 have exec2': "\<langle>?C2,[],s2\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,s3\<rangle>"
   223     using exec_star_decomp[of _ "[]" "[]"] by fastsimp
   224   have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>c s2" using IH1 exec1 by simp
   225   moreover have "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>c s3" using IH2 exec2' by fastsimp
   226   ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>c s3" ..
   227 next
   228   fix s t b c1 c2
   229   let ?if = "IF b THEN c1 ELSE c2" let ?C = "compile ?if"
   230   let ?C1 = "compile c1" let ?C2 = "compile c2"
   231   assume IH1: "\<And>s t. \<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle> \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t"
   232      and IH2: "\<And>s t. \<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle> \<Longrightarrow> \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t"
   233      and H: "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle>"
   234   show "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>c t"
   235   proof cases
   236     assume b: "b s"
   237     with H have "\<langle>?C1,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C1,t\<rangle>"
   238       by (fastsimp dest:exec_star_decomp
   239             [of _ "[JMPF (\<lambda>x. False) (size ?C2)]@?C2" "[]",simplified])
   240     hence "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH1)
   241     with b show ?thesis ..
   242   next
   243     assume b: "\<not> b s"
   244     with H have "\<langle>?C2,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C2,t\<rangle>"
   245       using exec_star_decomp[of _ "[]" "[]"] by simp
   246     hence "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c t" by(rule IH2)
   247     with b show ?thesis ..
   248   qed
   249 next
   250   fix b c s t
   251   let ?w = "WHILE b DO c" let ?W = "compile ?w" let ?C = "compile c"
   252   let ?j1 = "JMPF b (size ?C + 1)" let ?j2 = "JMPB (size ?C + 1)"
   253   assume IHc: "\<And>s t. \<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   254      and H: "\<langle>?W,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
   255   from H obtain k where ob:"\<langle>?W,[],s\<rangle> -k\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
   256     by(simp add:rtrancl_is_UN_rel_pow) blast
   257   { fix n have "\<And>s. \<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle> \<Longrightarrow> \<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
   258     proof (induct n rule: less_induct)
   259       fix n
   260       assume IHm: "\<And>m s. \<lbrakk>m < n; \<langle>?W,[],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle> \<rbrakk> \<Longrightarrow> \<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
   261       fix s
   262       assume H: "\<langle>?W,[],s\<rangle> -n\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
   263       show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t"
   264       proof cases
   265 	assume b: "b s"
   266 	then obtain m where m: "n = Suc m"
   267           and "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
   268 	  using H by fastsimp
   269 	then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
   270           and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
   271           and n12: "m = n1+n2"
   272 	  using execn_decomp[of _ "[?j2]"]
   273 	  by(simp del: execn_simp) fast
   274 	have n2n: "n2 - 1 < n" using m n12 by arith
   275 	note b
   276 	moreover
   277 	{ from n1 have "\<langle>?C,[],s\<rangle> -*\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
   278 	    by (simp add:rtrancl_is_UN_rel_pow) fast
   279 	  hence "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c r" by(rule IHc)
   280 	}
   281 	moreover
   282 	{ have "n2 - 1 < n" using m n12 by arith
   283 	  moreover from n2 have "\<langle>?W,[],r\<rangle> -n2- 1\<rightarrow> \<langle>[],rev ?W,t\<rangle>" by fastsimp
   284 	  ultimately have "\<langle>?w,r\<rangle> \<longrightarrow>\<^sub>c t" by(rule IHm)
   285 	}
   286 	ultimately show ?thesis ..
   287       next
   288 	assume b: "\<not> b s"
   289 	hence "t = s" using H by simp
   290 	with b show ?thesis by simp
   291       qed
   292     qed
   293   }
   294   with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
   295 qed
   296 
   297 (* TODO: connect with Machine 0 using M_equiv *)
   298 
   299 end