1.1 --- a/src/HOL/IMP/Compiler.thy Mon Apr 30 13:54:33 2001 +0200
1.2 +++ b/src/HOL/IMP/Compiler.thy Mon Apr 30 19:26:04 2001 +0200
1.3 @@ -24,10 +24,14 @@
1.4
1.5 inductive "stepa1 P"
1.6 intros
1.7 -ASIN: "P!n = ASIN x a ==> P |- <s,n> -1-> <s[x::= a s],Suc n>"
1.8 -JMPFT: "[| P!n = JMPF b i; b s |] ==> P |- <s,n> -1-> <s,Suc n>"
1.9 -JMPFF: "[| P!n = JMPF b i; ~b s; m=n+i |] ==> P |- <s,n> -1-> <s,m>"
1.10 -JMPB: "[| P!n = JMPB i |] ==> P |- <s,n> -1-> <s,n-i>"
1.11 +ASIN:
1.12 + "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s[x::= a s],Suc n>"
1.13 +JMPFT:
1.14 + "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,Suc n>"
1.15 +JMPFF:
1.16 + "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,m>"
1.17 +JMPB:
1.18 + "\<lbrakk> n<size P; P!n = JMPB i; i <= n \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,n-i>"
1.19
1.20 consts compile :: "com => instr list"
1.21 primrec
1.22 @@ -42,10 +46,98 @@
1.23
1.24 declare nth_append[simp];
1.25
1.26 -lemma nth_tl[simp]: "tl(xs @ y # ys) ! (length xs + z) = ys!z";
1.27 -apply(induct_tac xs);
1.28 -by(auto);
1.29 +(* Lemmas for lifting an execution into a prefix and suffix
1.30 + of instructions; only needed for the first proof *)
1.31
1.32 +lemma app_right_1:
1.33 + "is1 |- <s1,i1> -1-> <s2,i2> \<Longrightarrow> is1 @ is2 |- <s1,i1> -1-> <s2,i2>"
1.34 +apply(erule stepa1.induct);
1.35 + apply (simp add:ASIN)
1.36 + apply (force intro!:JMPFT)
1.37 + apply (force intro!:JMPFF)
1.38 +apply (simp add: JMPB)
1.39 +done
1.40 +
1.41 +lemma app_left_1:
1.42 + "is2 |- <s1,i1> -1-> <s2,i2> \<Longrightarrow>
1.43 + is1 @ is2 |- <s1,size is1+i1> -1-> <s2,size is1+i2>"
1.44 +apply(erule stepa1.induct);
1.45 + apply (simp add:ASIN)
1.46 + apply (fastsimp intro!:JMPFT)
1.47 + apply (fastsimp intro!:JMPFF)
1.48 +apply (simp add: JMPB)
1.49 +done
1.50 +
1.51 +lemma app_right:
1.52 + "is1 |- <s1,i1> -*-> <s2,i2> \<Longrightarrow> is1 @ is2 |- <s1,i1> -*-> <s2,i2>"
1.53 +apply(erule rtrancl_induct2);
1.54 + apply simp
1.55 +apply(blast intro:app_right_1 rtrancl_trans)
1.56 +done
1.57 +
1.58 +lemma app_left:
1.59 + "is2 |- <s1,i1> -*-> <s2,i2> \<Longrightarrow>
1.60 + is1 @ is2 |- <s1,size is1+i1> -*-> <s2,size is1+i2>"
1.61 +apply(erule rtrancl_induct2);
1.62 + apply simp
1.63 +apply(blast intro:app_left_1 rtrancl_trans)
1.64 +done
1.65 +
1.66 +lemma app_left2:
1.67 + "\<lbrakk> is2 |- <s1,i1> -*-> <s2,i2>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
1.68 + is1 @ is2 |- <s1,j1> -*-> <s2,j2>"
1.69 +by (simp add:app_left)
1.70 +
1.71 +lemma app1_left:
1.72 + "is |- <s1,i1> -*-> <s2,i2> \<Longrightarrow>
1.73 + instr # is |- <s1,Suc i1> -*-> <s2,Suc i2>"
1.74 +by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
1.75 +
1.76 +
1.77 +(* The first proof; statement very intuitive,
1.78 + but application of induction hypothesis requires the above lifting lemmas
1.79 +*)
1.80 +theorem "<c,s> -c-> t ==> compile c |- <s,0> -*-> <t,length(compile c)>"
1.81 +apply(erule evalc.induct);
1.82 + apply simp;
1.83 + apply(force intro!: ASIN);
1.84 + apply simp
1.85 + apply(rule rtrancl_trans)
1.86 + apply(erule app_right)
1.87 + apply(erule app_left[of _ 0,simplified])
1.88 +(* IF b THEN c0 ELSE c1; case b is true *)
1.89 + apply(simp);
1.90 + (* execute JMPF: *)
1.91 + apply (rule rtrancl_into_rtrancl2)
1.92 + apply(force intro!: JMPFT);
1.93 + (* execute compile c0: *)
1.94 + apply(rule app1_left)
1.95 + apply(rule rtrancl_into_rtrancl);
1.96 + apply(erule app_right)
1.97 + (* execute JMPF: *)
1.98 + apply(force intro!: JMPFF);
1.99 +(* end of case b is true *)
1.100 + apply simp
1.101 + apply (rule rtrancl_into_rtrancl2)
1.102 + apply(force intro!: JMPFF)
1.103 + apply(force intro!: app_left2 app1_left)
1.104 +(* WHILE False *)
1.105 + apply(force intro: JMPFF);
1.106 +(* WHILE True *)
1.107 +apply(simp)
1.108 +apply(rule rtrancl_into_rtrancl2);
1.109 + apply(force intro!: JMPFT);
1.110 +apply(rule rtrancl_trans);
1.111 + apply(rule app1_left)
1.112 + apply(erule app_right)
1.113 +apply(rule rtrancl_into_rtrancl2);
1.114 + apply(force intro!: JMPB)
1.115 +apply(simp)
1.116 +done
1.117 +
1.118 +(* Second proof; statement is generalized to cater for prefixes and suffixes;
1.119 + needs none of the lifting lemmas, but instantiations of pre/suffix.
1.120 +*)
1.121 theorem "<c,s> -c-> t ==>
1.122 !a z. a@compile c@z |- <s,length a> -*-> <t,length a + length(compile c)>";
1.123 apply(erule evalc.induct);
1.124 @@ -65,31 +157,20 @@
1.125 apply(simp);
1.126 (* execute JMPF: *)
1.127 apply(rule rtrancl_into_rtrancl2);
1.128 - apply(rule JMPFT);
1.129 - apply(simp);
1.130 - apply(blast);
1.131 - apply assumption;
1.132 + apply(force intro!: JMPFT);
1.133 (* execute compile c0: *)
1.134 apply(rule rtrancl_trans);
1.135 apply(erule allE);
1.136 apply assumption;
1.137 (* execute JMPF: *)
1.138 apply(rule r_into_rtrancl);
1.139 - apply(rule JMPFF);
1.140 - apply(simp);
1.141 - apply(blast);
1.142 - apply(blast);
1.143 - apply(simp);
1.144 + apply(force intro!: JMPFF);
1.145 (* end of case b is true *)
1.146 apply(intro strip);
1.147 apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE);
1.148 apply(simp add:add_assoc);
1.149 apply(rule rtrancl_into_rtrancl2);
1.150 - apply(rule JMPFF);
1.151 - apply(simp);
1.152 - apply(blast);
1.153 - apply assumption;
1.154 - apply(simp);
1.155 + apply(force intro!: JMPFF);
1.156 apply(blast);
1.157 apply(force intro: JMPFF);
1.158 apply(intro strip);
1.159 @@ -97,16 +178,12 @@
1.160 apply(erule_tac x = a in allE);
1.161 apply(simp);
1.162 apply(rule rtrancl_into_rtrancl2);
1.163 - apply(rule JMPFT);
1.164 - apply(simp);
1.165 - apply(blast);
1.166 - apply assumption;
1.167 + apply(force intro!: JMPFT);
1.168 apply(rule rtrancl_trans);
1.169 apply(erule allE);
1.170 apply assumption;
1.171 apply(rule rtrancl_into_rtrancl2);
1.172 - apply(rule JMPB);
1.173 - apply(simp);
1.174 + apply(force intro!: JMPB);
1.175 apply(simp);
1.176 done
1.177