1.1 --- a/src/HOL/IMP/Compiler.thy Thu Nov 22 23:46:33 2001 +0100
1.2 +++ b/src/HOL/IMP/Compiler.thy Fri Nov 23 17:19:14 2001 +0100
1.3 @@ -14,24 +14,24 @@
1.4
1.5 syntax
1.6 "@stepa1" :: "[instr list,state,nat,state,nat] => bool"
1.7 - ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
1.8 + ("_ \<turnstile> <_,_>/ -1\<rightarrow> <_,_>" [50,0,0,0,0] 50)
1.9 "@stepa" :: "[instr list,state,nat,state,nat] => bool"
1.10 - ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
1.11 + ("_ \<turnstile>/ <_,_>/ -*\<rightarrow> <_,_>" [50,0,0,0,0] 50)
1.12
1.13 -translations "P |- <s,m> -1-> <t,n>" == "((s,m),t,n) : stepa1 P"
1.14 - "P |- <s,m> -*-> <t,n>" == "((s,m),t,n) : ((stepa1 P)^*)"
1.15 +translations "P \<turnstile> <s,m> -1\<rightarrow> <t,n>" == "((s,m),t,n) : stepa1 P"
1.16 + "P \<turnstile> <s,m> -*\<rightarrow> <t,n>" == "((s,m),t,n) : ((stepa1 P)^*)"
1.17
1.18
1.19 inductive "stepa1 P"
1.20 intros
1.21 -ASIN:
1.22 - "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s[x::= a s],Suc n>"
1.23 -JMPFT:
1.24 - "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,Suc n>"
1.25 -JMPFF:
1.26 - "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,m>"
1.27 -JMPB:
1.28 - "\<lbrakk> n<size P; P!n = JMPB i; i <= n \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,n-i>"
1.29 +ASIN[simp]:
1.30 + "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s[x::= a s],Suc n>"
1.31 +JMPFT[simp,intro]:
1.32 + "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s,Suc n>"
1.33 +JMPFF[simp,intro]:
1.34 + "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s,m>"
1.35 +JMPB[simp]:
1.36 + "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s,j>"
1.37
1.38 consts compile :: "com => instr list"
1.39 primrec
1.40 @@ -50,96 +50,150 @@
1.41 of instructions; only needed for the first proof *)
1.42
1.43 lemma app_right_1:
1.44 - "is1 |- <s1,i1> -1-> <s2,i2> \<Longrightarrow> is1 @ is2 |- <s1,i1> -1-> <s2,i2>"
1.45 -apply(erule stepa1.induct);
1.46 - apply (simp add:ASIN)
1.47 - apply (force intro!:JMPFT)
1.48 - apply (force intro!:JMPFF)
1.49 -apply (simp add: JMPB)
1.50 -done
1.51 -
1.52 + "is1 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2> \<Longrightarrow> is1 @ is2 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2>"
1.53 + (is "?P \<Longrightarrow> _")
1.54 +proof -
1.55 + assume ?P
1.56 + then show ?thesis
1.57 + by induct force+
1.58 +qed
1.59 +
1.60 lemma app_left_1:
1.61 - "is2 |- <s1,i1> -1-> <s2,i2> \<Longrightarrow>
1.62 - is1 @ is2 |- <s1,size is1+i1> -1-> <s2,size is1+i2>"
1.63 -apply(erule stepa1.induct);
1.64 - apply (simp add:ASIN)
1.65 - apply (fastsimp intro!:JMPFT)
1.66 - apply (fastsimp intro!:JMPFF)
1.67 -apply (simp add: JMPB)
1.68 -done
1.69 + "is2 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2> \<Longrightarrow>
1.70 + is1 @ is2 \<turnstile> <s1,size is1+i1> -1\<rightarrow> <s2,size is1+i2>"
1.71 + (is "?P \<Longrightarrow> _")
1.72 +proof -
1.73 + assume ?P
1.74 + then show ?thesis
1.75 + by induct force+
1.76 +qed
1.77 +
1.78 +declare rtrancl_induct2 [induct set: rtrancl]
1.79
1.80 lemma app_right:
1.81 - "is1 |- <s1,i1> -*-> <s2,i2> \<Longrightarrow> is1 @ is2 |- <s1,i1> -*-> <s2,i2>"
1.82 -apply(erule rtrancl_induct2);
1.83 - apply simp
1.84 -apply(blast intro:app_right_1 rtrancl_trans)
1.85 -done
1.86 + "is1 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow> is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2>"
1.87 + (is "?P \<Longrightarrow> _")
1.88 +proof -
1.89 + assume ?P
1.90 + then show ?thesis
1.91 + proof induct
1.92 + show "is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s1,i1>" by simp
1.93 + next
1.94 + fix s1' i1' s2 i2
1.95 + assume "is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s1',i1'>"
1.96 + "is1 \<turnstile> <s1',i1'> -1\<rightarrow> <s2,i2>"
1.97 + thus "is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2>"
1.98 + by(blast intro:app_right_1 rtrancl_trans)
1.99 + qed
1.100 +qed
1.101
1.102 lemma app_left:
1.103 - "is2 |- <s1,i1> -*-> <s2,i2> \<Longrightarrow>
1.104 - is1 @ is2 |- <s1,size is1+i1> -*-> <s2,size is1+i2>"
1.105 -apply(erule rtrancl_induct2);
1.106 - apply simp
1.107 -apply(blast intro:app_left_1 rtrancl_trans)
1.108 -done
1.109 + "is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow>
1.110 + is1 @ is2 \<turnstile> <s1,size is1+i1> -*\<rightarrow> <s2,size is1+i2>"
1.111 + (is "?P \<Longrightarrow> _")
1.112 +proof -
1.113 + assume ?P
1.114 + then show ?thesis
1.115 + proof induct
1.116 + show "is1 @ is2 \<turnstile> <s1,length is1 + i1> -*\<rightarrow> <s1,length is1 + i1>" by simp
1.117 + next
1.118 + fix s1' i1' s2 i2
1.119 + assume "is1 @ is2 \<turnstile> <s1,length is1 + i1> -*\<rightarrow> <s1',length is1 + i1'>"
1.120 + "is2 \<turnstile> <s1',i1'> -1\<rightarrow> <s2,i2>"
1.121 + thus "is1 @ is2 \<turnstile> <s1,length is1 + i1> -*\<rightarrow> <s2,length is1 + i2>"
1.122 + by(blast intro:app_left_1 rtrancl_trans)
1.123 + qed
1.124 +qed
1.125
1.126 lemma app_left2:
1.127 - "\<lbrakk> is2 |- <s1,i1> -*-> <s2,i2>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
1.128 - is1 @ is2 |- <s1,j1> -*-> <s2,j2>"
1.129 + "\<lbrakk> is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
1.130 + is1 @ is2 \<turnstile> <s1,j1> -*\<rightarrow> <s2,j2>"
1.131 by (simp add:app_left)
1.132
1.133 lemma app1_left:
1.134 - "is |- <s1,i1> -*-> <s2,i2> \<Longrightarrow>
1.135 - instr # is |- <s1,Suc i1> -*-> <s2,Suc i2>"
1.136 + "is \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow>
1.137 + instr # is \<turnstile> <s1,Suc i1> -*\<rightarrow> <s2,Suc i2>"
1.138 by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
1.139
1.140 -
1.141 +declare rtrancl_into_rtrancl[trans]
1.142 + rtrancl_into_rtrancl2[trans]
1.143 + rtrancl_trans[trans]
1.144 (* The first proof; statement very intuitive,
1.145 but application of induction hypothesis requires the above lifting lemmas
1.146 *)
1.147 -theorem "<c,s> -c-> t ==> compile c |- <s,0> -*-> <t,length(compile c)>"
1.148 -apply(erule evalc.induct);
1.149 - apply simp;
1.150 - apply(force intro!: ASIN);
1.151 - apply simp
1.152 - apply(rule rtrancl_trans)
1.153 - apply(erule app_right)
1.154 - apply(erule app_left[of _ 0,simplified])
1.155 -(* IF b THEN c0 ELSE c1; case b is true *)
1.156 - apply(simp);
1.157 - (* execute JMPF: *)
1.158 - apply (rule rtrancl_into_rtrancl2)
1.159 - apply(force intro!: JMPFT);
1.160 - (* execute compile c0: *)
1.161 - apply(rule app1_left)
1.162 - apply(rule rtrancl_into_rtrancl);
1.163 - apply(erule app_right)
1.164 - (* execute JMPF: *)
1.165 - apply(force intro!: JMPFF);
1.166 -(* end of case b is true *)
1.167 - apply simp
1.168 - apply (rule rtrancl_into_rtrancl2)
1.169 - apply(force intro!: JMPFF)
1.170 - apply(force intro!: app_left2 app1_left)
1.171 -(* WHILE False *)
1.172 - apply(force intro: JMPFF);
1.173 -(* WHILE True *)
1.174 -apply(simp)
1.175 -apply(rule rtrancl_into_rtrancl2);
1.176 - apply(force intro!: JMPFT);
1.177 -apply(rule rtrancl_trans);
1.178 - apply(rule app1_left)
1.179 - apply(erule app_right)
1.180 -apply(rule rtrancl_into_rtrancl2);
1.181 - apply(force intro!: JMPB)
1.182 -apply(simp)
1.183 -done
1.184 +theorem "<c,s> -c-> t \<Longrightarrow> compile c \<turnstile> <s,0> -*\<rightarrow> <t,length(compile c)>"
1.185 + (is "?P \<Longrightarrow> ?Q c s t")
1.186 +proof -
1.187 + assume ?P
1.188 + then show ?thesis
1.189 + proof induct
1.190 + show "\<And>s. ?Q SKIP s s" by simp
1.191 + next
1.192 + show "\<And>a s x. ?Q (x :== a) s (s[x::= a s])" by force
1.193 + next
1.194 + fix c0 c1 s0 s1 s2
1.195 + assume "?Q c0 s0 s1"
1.196 + hence "compile c0 @ compile c1 \<turnstile> <s0,0> -*\<rightarrow> <s1,length(compile c0)>"
1.197 + by(rule app_right)
1.198 + moreover assume "?Q c1 s1 s2"
1.199 + hence "compile c0 @ compile c1 \<turnstile> <s1,length(compile c0)> -*\<rightarrow>
1.200 + <s2,length(compile c0)+length(compile c1)>"
1.201 + proof -
1.202 + note app_left[of _ 0]
1.203 + thus
1.204 + "\<And>is1 is2 s1 s2 i2.
1.205 + is2 \<turnstile> <s1,0> -*\<rightarrow> <s2,i2> \<Longrightarrow>
1.206 + is1 @ is2 \<turnstile> <s1,size is1> -*\<rightarrow> <s2,size is1+i2>"
1.207 + by simp
1.208 + qed
1.209 + ultimately have "compile c0 @ compile c1 \<turnstile> <s0,0> -*\<rightarrow>
1.210 + <s2,length(compile c0)+length(compile c1)>"
1.211 + by (rule rtrancl_trans)
1.212 + thus "?Q (c0; c1) s0 s2" by simp
1.213 + next
1.214 + fix b c0 c1 s0 s1
1.215 + let ?comp = "compile(IF b THEN c0 ELSE c1)"
1.216 + assume "b s0" and IH: "?Q c0 s0 s1"
1.217 + hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,1>" by auto
1.218 + also from IH
1.219 + have "?comp \<turnstile> <s0,1> -*\<rightarrow> <s1,length(compile c0)+1>"
1.220 + by(auto intro:app1_left app_right)
1.221 + also have "?comp \<turnstile> <s1,length(compile c0)+1> -1\<rightarrow> <s1,length ?comp>"
1.222 + by(auto)
1.223 + finally show "?Q (IF b THEN c0 ELSE c1) s0 s1" .
1.224 + next
1.225 + fix b c0 c1 s0 s1
1.226 + let ?comp = "compile(IF b THEN c0 ELSE c1)"
1.227 + assume "\<not>b s0" and IH: "?Q c1 s0 s1"
1.228 + hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,length(compile c0) + 2>" by auto
1.229 + also from IH
1.230 + have "?comp \<turnstile> <s0,length(compile c0)+2> -*\<rightarrow> <s1,length ?comp>"
1.231 + by(force intro!:app_left2 app1_left)
1.232 + finally show "?Q (IF b THEN c0 ELSE c1) s0 s1" .
1.233 + next
1.234 + fix b c and s::state
1.235 + assume "\<not>b s"
1.236 + thus "?Q (WHILE b DO c) s s" by force
1.237 + next
1.238 + fix b c and s0::state and s1 s2
1.239 + let ?comp = "compile(WHILE b DO c)"
1.240 + assume "b s0" and
1.241 + IHc: "?Q c s0 s1" and IHw: "?Q (WHILE b DO c) s1 s2"
1.242 + hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,1>" by auto
1.243 + also from IHc
1.244 + have "?comp \<turnstile> <s0,1> -*\<rightarrow> <s1,length(compile c)+1>"
1.245 + by(auto intro:app1_left app_right)
1.246 + also have "?comp \<turnstile> <s1,length(compile c)+1> -1\<rightarrow> <s1,0>" by simp
1.247 + also note IHw
1.248 + finally show "?Q (WHILE b DO c) s0 s2".
1.249 + qed
1.250 +qed
1.251
1.252 (* Second proof; statement is generalized to cater for prefixes and suffixes;
1.253 needs none of the lifting lemmas, but instantiations of pre/suffix.
1.254 *)
1.255 theorem "<c,s> -c-> t ==>
1.256 - !a z. a@compile c@z |- <s,length a> -*-> <t,length a + length(compile c)>";
1.257 + !a z. a@compile c@z \<turnstile> <s,length a> -*\<rightarrow> <t,length a + length(compile c)>";
1.258 apply(erule evalc.induct);
1.259 apply simp;
1.260 apply(force intro!: ASIN);