# HG changeset patch
# User nipkow
# Date 988651564 -7200
# Node ID 71498de452413523f54c1b0190c8bd1be206d695
# Parent  566a70a509562a119a545f812c5f92b96fd2eca5
new proof

diff -r 566a70a50956 -r 71498de45241 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Mon Apr 30 13:54:33 2001 +0200
+++ b/src/HOL/IMP/Compiler.thy	Mon Apr 30 19:26:04 2001 +0200
@@ -24,10 +24,14 @@
 
 inductive "stepa1 P"
 intros
-ASIN:  "P!n = ASIN x a ==> P |- <s,n> -1-> <s[x::= a s],Suc n>"
-JMPFT: "[| P!n = JMPF b i;  b s |] ==> P |- <s,n> -1-> <s,Suc n>"
-JMPFF: "[| P!n = JMPF b i; ~b s; m=n+i |] ==> P |- <s,n> -1-> <s,m>"
-JMPB:  "[| P!n = JMPB i |] ==> P |- <s,n> -1-> <s,n-i>"
+ASIN:
+       "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s[x::= a s],Suc n>"
+JMPFT:
+       "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,Suc n>"
+JMPFF:
+       "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,m>"
+JMPB:
+      "\<lbrakk> n<size P; P!n = JMPB i; i <= n \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,n-i>"
 
 consts compile :: "com => instr list"
 primrec
@@ -42,10 +46,98 @@
 
 declare nth_append[simp];
 
-lemma nth_tl[simp]: "tl(xs @ y # ys) ! (length xs + z) = ys!z";
-apply(induct_tac xs);
-by(auto);
+(* Lemmas for lifting an execution into a prefix and suffix
+   of instructions; only needed for the first proof *)
+
+lemma app_right_1:
+  "is1 |- <s1,i1> -1-> <s2,i2> \<Longrightarrow> is1 @ is2 |- <s1,i1> -1-> <s2,i2>"
+apply(erule stepa1.induct);
+   apply (simp add:ASIN)
+  apply (force intro!:JMPFT)
+ apply (force intro!:JMPFF)
+apply (simp add: JMPB)
+done      
+      
+lemma app_left_1:
+  "is2 |- <s1,i1> -1-> <s2,i2> \<Longrightarrow>
+   is1 @ is2 |- <s1,size is1+i1> -1-> <s2,size is1+i2>"
+apply(erule stepa1.induct);
+   apply (simp add:ASIN)
+  apply (fastsimp intro!:JMPFT)
+ apply (fastsimp intro!:JMPFF)
+apply (simp add: JMPB)
+done
+
+lemma app_right:
+  "is1 |- <s1,i1> -*-> <s2,i2> \<Longrightarrow> is1 @ is2 |- <s1,i1> -*-> <s2,i2>"
+apply(erule rtrancl_induct2);
+ apply simp
+apply(blast intro:app_right_1 rtrancl_trans)
+done
+
+lemma app_left:
+  "is2 |- <s1,i1> -*-> <s2,i2> \<Longrightarrow>
+   is1 @ is2 |- <s1,size is1+i1> -*-> <s2,size is1+i2>"
+apply(erule rtrancl_induct2);
+ apply simp
+apply(blast intro:app_left_1 rtrancl_trans)
+done
+
+lemma app_left2:
+  "\<lbrakk> is2 |- <s1,i1> -*-> <s2,i2>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
+   is1 @ is2 |- <s1,j1> -*-> <s2,j2>"
+by (simp add:app_left)
 
+lemma app1_left:
+  "is |- <s1,i1> -*-> <s2,i2> \<Longrightarrow>
+   instr # is |- <s1,Suc i1> -*-> <s2,Suc i2>"
+by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
+
+
+(* The first proof; statement very intuitive,
+   but application of induction hypothesis requires the above lifting lemmas
+*)
+theorem "<c,s> -c-> t ==> compile c |- <s,0> -*-> <t,length(compile c)>"
+apply(erule evalc.induct);
+      apply simp;
+     apply(force intro!: ASIN);
+    apply simp
+    apply(rule rtrancl_trans)
+    apply(erule app_right)
+    apply(erule app_left[of _ 0,simplified])
+(* IF b THEN c0 ELSE c1; case b is true *)
+   apply(simp);
+   (* execute JMPF: *)
+   apply (rule rtrancl_into_rtrancl2)
+    apply(force intro!: JMPFT);
+   (* execute compile c0: *)
+   apply(rule app1_left)
+   apply(rule rtrancl_into_rtrancl);
+    apply(erule app_right)
+   (* execute JMPF: *)
+   apply(force intro!: JMPFF);
+(* end of case b is true *)
+  apply simp
+  apply (rule rtrancl_into_rtrancl2)
+   apply(force intro!: JMPFF)
+  apply(force intro!: app_left2 app1_left)
+(* WHILE False *)
+ apply(force intro: JMPFF);
+(* WHILE True *)
+apply(simp)
+apply(rule rtrancl_into_rtrancl2);
+ apply(force intro!: JMPFT);
+apply(rule rtrancl_trans);
+ apply(rule app1_left)
+ apply(erule app_right)
+apply(rule rtrancl_into_rtrancl2);
+ apply(force intro!: JMPB)
+apply(simp)
+done
+
+(* Second proof; statement is generalized to cater for prefixes and suffixes;
+   needs none of the lifting lemmas, but instantiations of pre/suffix.
+*)
 theorem "<c,s> -c-> t ==> 
  !a z. a@compile c@z |- <s,length a> -*-> <t,length a + length(compile c)>";
 apply(erule evalc.induct);
@@ -65,31 +157,20 @@
    apply(simp);
    (* execute JMPF: *)
    apply(rule rtrancl_into_rtrancl2);
-    apply(rule JMPFT);
-     apply(simp);
-     apply(blast);
-    apply assumption;
+    apply(force intro!: JMPFT);
    (* execute compile c0: *)
    apply(rule rtrancl_trans);
     apply(erule allE);
     apply assumption;
    (* execute JMPF: *)
    apply(rule r_into_rtrancl);
-   apply(rule JMPFF);
-     apply(simp);
-     apply(blast);
-    apply(blast);
-   apply(simp);
+   apply(force intro!: JMPFF);
 (* end of case b is true *)
   apply(intro strip);
   apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE);
   apply(simp add:add_assoc);
   apply(rule rtrancl_into_rtrancl2);
-   apply(rule JMPFF);
-     apply(simp);
-     apply(blast);
-    apply assumption;
-   apply(simp);
+   apply(force intro!: JMPFF);
   apply(blast);
  apply(force intro: JMPFF);
 apply(intro strip);
@@ -97,16 +178,12 @@
 apply(erule_tac x = a in allE);
 apply(simp);
 apply(rule rtrancl_into_rtrancl2);
- apply(rule JMPFT);
-  apply(simp);
-  apply(blast);
- apply assumption;
+ apply(force intro!: JMPFT);
 apply(rule rtrancl_trans);
  apply(erule allE);
  apply assumption;
 apply(rule rtrancl_into_rtrancl2);
- apply(rule JMPB);
- apply(simp);
+ apply(force intro!: JMPB);
 apply(simp);
 done