# HG changeset patch
# User nipkow
# Date 1006532354 -3600
# Node ID aa2b7b475a9444ee48b3db88ebfdf808137faf0f
# Parent  2582d16acd3df2d8f1e30836cd8bf8c4db39fd73
Isar conversion

diff -r 2582d16acd3d -r aa2b7b475a94 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Nov 22 23:46:33 2001 +0100
+++ b/src/HOL/IMP/Compiler.thy	Fri Nov 23 17:19:14 2001 +0100
@@ -14,24 +14,24 @@
 
 syntax
         "@stepa1" :: "[instr list,state,nat,state,nat] => bool"
-                     ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
+                     ("_ \<turnstile> <_,_>/ -1\<rightarrow> <_,_>" [50,0,0,0,0] 50)
         "@stepa" :: "[instr list,state,nat,state,nat] => bool"
-                     ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
+                     ("_ \<turnstile>/ <_,_>/ -*\<rightarrow> <_,_>" [50,0,0,0,0] 50)
 
-translations  "P |- <s,m> -1-> <t,n>" == "((s,m),t,n) : stepa1 P"
-              "P |- <s,m> -*-> <t,n>" == "((s,m),t,n) : ((stepa1 P)^*)"
+translations  "P \<turnstile> <s,m> -1\<rightarrow> <t,n>" == "((s,m),t,n) : stepa1 P"
+              "P \<turnstile> <s,m> -*\<rightarrow> <t,n>" == "((s,m),t,n) : ((stepa1 P)^*)"
 
 
 inductive "stepa1 P"
 intros
-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>"
+ASIN[simp]:
+       "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s[x::= a s],Suc n>"
+JMPFT[simp,intro]:
+       "\<lbrakk> n<size P; P!n = JMPF b i;  b s \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s,Suc n>"
+JMPFF[simp,intro]:
+       "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s,m>"
+JMPB[simp]:
+      "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> <s,n> -1\<rightarrow> <s,j>"
 
 consts compile :: "com => instr list"
 primrec
@@ -50,96 +50,150 @@
    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      
-      
+  "is1 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2> \<Longrightarrow> is1 @ is2 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2>"
+  (is "?P \<Longrightarrow> _")
+proof -
+ assume ?P
+ then show ?thesis
+ by induct force+
+qed
+
 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
+  "is2 \<turnstile> <s1,i1> -1\<rightarrow> <s2,i2> \<Longrightarrow>
+   is1 @ is2 \<turnstile> <s1,size is1+i1> -1\<rightarrow> <s2,size is1+i2>"
+  (is "?P \<Longrightarrow> _")
+proof -
+ assume ?P
+ then show ?thesis
+ by induct force+
+qed
+
+declare rtrancl_induct2 [induct set: rtrancl]
 
 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
+  "is1 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow> is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2>"
+  (is "?P \<Longrightarrow> _")
+proof -
+ assume ?P
+ then show ?thesis
+ proof induct
+   show "is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s1,i1>" by simp
+ next
+   fix s1' i1' s2 i2
+   assume "is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s1',i1'>"
+          "is1 \<turnstile> <s1',i1'> -1\<rightarrow> <s2,i2>"
+   thus "is1 @ is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2>"
+     by(blast intro:app_right_1 rtrancl_trans)
+ qed
+qed
 
 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
+  "is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow>
+   is1 @ is2 \<turnstile> <s1,size is1+i1> -*\<rightarrow> <s2,size is1+i2>"
+  (is "?P \<Longrightarrow> _")
+proof -
+ assume ?P
+ then show ?thesis
+ proof induct
+   show "is1 @ is2 \<turnstile> <s1,length is1 + i1> -*\<rightarrow> <s1,length is1 + i1>" by simp
+ next
+   fix s1' i1' s2 i2
+   assume "is1 @ is2 \<turnstile> <s1,length is1 + i1> -*\<rightarrow> <s1',length is1 + i1'>"
+          "is2 \<turnstile> <s1',i1'> -1\<rightarrow> <s2,i2>"
+   thus "is1 @ is2 \<turnstile> <s1,length is1 + i1> -*\<rightarrow> <s2,length is1 + i2>"
+     by(blast intro:app_left_1 rtrancl_trans)
+ qed
+qed
 
 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>"
+  "\<lbrakk> is2 \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
+   is1 @ is2 \<turnstile> <s1,j1> -*\<rightarrow> <s2,j2>"
 by (simp add:app_left)
 
 lemma app1_left:
-  "is |- <s1,i1> -*-> <s2,i2> \<Longrightarrow>
-   instr # is |- <s1,Suc i1> -*-> <s2,Suc i2>"
+  "is \<turnstile> <s1,i1> -*\<rightarrow> <s2,i2> \<Longrightarrow>
+   instr # is \<turnstile> <s1,Suc i1> -*\<rightarrow> <s2,Suc i2>"
 by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
 
-
+declare rtrancl_into_rtrancl[trans]
+        rtrancl_into_rtrancl2[trans]
+        rtrancl_trans[trans]
 (* 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
+theorem "<c,s> -c-> t \<Longrightarrow> compile c \<turnstile> <s,0> -*\<rightarrow> <t,length(compile c)>"
+        (is "?P \<Longrightarrow> ?Q c s t")
+proof -
+  assume ?P
+  then show ?thesis
+  proof induct
+    show "\<And>s. ?Q SKIP s s" by simp
+  next
+    show "\<And>a s x. ?Q (x :== a) s (s[x::= a s])" by force
+  next
+    fix c0 c1 s0 s1 s2
+    assume "?Q c0 s0 s1"
+    hence "compile c0 @ compile c1 \<turnstile> <s0,0> -*\<rightarrow> <s1,length(compile c0)>"
+      by(rule app_right)
+    moreover assume "?Q c1 s1 s2"
+    hence "compile c0 @ compile c1 \<turnstile> <s1,length(compile c0)> -*\<rightarrow>
+           <s2,length(compile c0)+length(compile c1)>"
+    proof -
+      note app_left[of _ 0]
+      thus
+	"\<And>is1 is2 s1 s2 i2.
+	is2 \<turnstile> <s1,0> -*\<rightarrow> <s2,i2> \<Longrightarrow>
+	is1 @ is2 \<turnstile> <s1,size is1> -*\<rightarrow> <s2,size is1+i2>"
+	by simp
+    qed
+    ultimately have "compile c0 @ compile c1 \<turnstile> <s0,0> -*\<rightarrow>
+                       <s2,length(compile c0)+length(compile c1)>"
+      by (rule rtrancl_trans)
+    thus "?Q (c0; c1) s0 s2" by simp
+  next
+    fix b c0 c1 s0 s1
+    let ?comp = "compile(IF b THEN c0 ELSE c1)"
+    assume "b s0" and IH: "?Q c0 s0 s1"
+    hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,1>" by auto
+    also from IH
+    have "?comp \<turnstile> <s0,1> -*\<rightarrow> <s1,length(compile c0)+1>"
+      by(auto intro:app1_left app_right)
+    also have "?comp \<turnstile> <s1,length(compile c0)+1> -1\<rightarrow> <s1,length ?comp>"
+      by(auto)
+    finally show "?Q (IF b THEN c0 ELSE c1) s0 s1" .
+  next
+    fix b c0 c1 s0 s1
+    let ?comp = "compile(IF b THEN c0 ELSE c1)"
+    assume "\<not>b s0" and IH: "?Q c1 s0 s1"
+    hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,length(compile c0) + 2>" by auto
+    also from IH
+    have "?comp \<turnstile> <s0,length(compile c0)+2> -*\<rightarrow> <s1,length ?comp>"
+      by(force intro!:app_left2 app1_left)
+    finally show "?Q (IF b THEN c0 ELSE c1) s0 s1" .
+  next
+    fix b c and s::state
+    assume "\<not>b s"
+    thus "?Q (WHILE b DO c) s s" by force
+  next
+    fix b c and s0::state and s1 s2
+    let ?comp = "compile(WHILE b DO c)"
+    assume "b s0" and
+      IHc: "?Q c s0 s1" and IHw: "?Q (WHILE b DO c) s1 s2"
+    hence "?comp \<turnstile> <s0,0> -1\<rightarrow> <s0,1>" by auto
+    also from IHc
+    have "?comp \<turnstile> <s0,1> -*\<rightarrow> <s1,length(compile c)+1>"
+      by(auto intro:app1_left app_right)
+    also have "?comp \<turnstile> <s1,length(compile c)+1> -1\<rightarrow> <s1,0>" by simp
+    also note IHw
+    finally show "?Q (WHILE b DO c) s0 s2".
+  qed
+qed
 
 (* 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)>";
+ !a z. a@compile c@z \<turnstile> <s,length a> -*\<rightarrow> <t,length a + length(compile c)>";
 apply(erule evalc.induct);
       apply simp;
      apply(force intro!: ASIN);