1.1 --- a/src/HOL/IMP/Compiler.thy	Wed Jun 25 21:25:51 2008 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Wed Jun 25 22:01:34 2008 +0200
     1.3 @@ -8,16 +8,16 @@
     1.4  
     1.5  subsection "The compiler"
     1.6  
     1.7 -consts compile :: "com \<Rightarrow> instr list"
     1.8 -primrec
     1.9 -"compile \<SKIP> = []"
    1.10 -"compile (x:==a) = [SET x a]"
    1.11 -"compile (c1;c2) = compile c1 @ compile c2"
    1.12 -"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
    1.13 - [JMPF b (length(compile c1) + 1)] @ compile c1 @
    1.14 - [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
    1.15 -"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
    1.16 - [JMPB (length(compile c)+1)]"
    1.17 +primrec compile :: "com \<Rightarrow> instr list"
    1.18 +where
    1.19 +  "compile \<SKIP> = []"
    1.20 +| "compile (x:==a) = [SET x a]"
    1.21 +| "compile (c1;c2) = compile c1 @ compile c2"
    1.22 +| "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
    1.23 +    [JMPF b (length(compile c1) + 1)] @ compile c1 @
    1.24 +    [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
    1.25 +| "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
    1.26 +    [JMPB (length(compile c)+1)]"
    1.27  
    1.28  subsection "Compiler correctness"
    1.29  
    1.30 @@ -65,31 +65,33 @@
    1.31  lemma [simp]: "(\<langle>[],q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>) = (p' = [] \<and> q' = q \<and> t = s)"
    1.32  by(simp add: rtrancl_is_UN_rel_pow)
    1.33  
    1.34 -constdefs
    1.35 - forws :: "instr \<Rightarrow> nat set"
    1.36 -"forws instr == case instr of
    1.37 - SET x a \<Rightarrow> {0} |
    1.38 - JMPF b n \<Rightarrow> {0,n} |
    1.39 - JMPB n \<Rightarrow> {}"
    1.40 - backws :: "instr \<Rightarrow> nat set"
    1.41 -"backws instr == case instr of
    1.42 - SET x a \<Rightarrow> {} |
    1.43 - JMPF b n \<Rightarrow> {} |
    1.44 - JMPB n \<Rightarrow> {n}"
    1.45 +definition
    1.46 +  forws :: "instr \<Rightarrow> nat set" where
    1.47 +  "forws instr = (case instr of
    1.48 +     SET x a \<Rightarrow> {0} |
    1.49 +     JMPF b n \<Rightarrow> {0,n} |
    1.50 +     JMPB n \<Rightarrow> {})"
    1.51  
    1.52 -consts closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
    1.53 -primrec
    1.54 -"closed m n [] = True"
    1.55 -"closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
    1.56 -                        (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
    1.57 +definition
    1.58 +  backws :: "instr \<Rightarrow> nat set" where
    1.59 +  "backws instr = (case instr of
    1.60 +     SET x a \<Rightarrow> {} |
    1.61 +     JMPF b n \<Rightarrow> {} |
    1.62 +     JMPB n \<Rightarrow> {n})"
    1.63 +
    1.64 +primrec closed :: "nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
    1.65 +where
    1.66 +  "closed m n [] = True"
    1.67 +| "closed m n (instr#is) = ((\<forall>j \<in> forws instr. j \<le> size is+n) \<and>
    1.68 +                          (\<forall>j \<in> backws instr. j \<le> m) \<and> closed (Suc m) n is)"
    1.69  
    1.70  lemma [simp]:
    1.71   "\<And>m n. closed m n (C1@C2) =
    1.72           (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
    1.73 -by(induct C1, simp, simp add:add_ac)
    1.74 +by(induct C1) (simp, simp add:add_ac)
    1.75  
    1.76  theorem [simp]: "\<And>m n. closed m n (compile c)"
    1.77 -by(induct c, simp_all add:backws_def forws_def)
    1.78 +by(induct c) (simp_all add:backws_def forws_def)
    1.79  
    1.80  lemma drop_lem: "n \<le> size(p1@p2)
    1.81   \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) =