# HG changeset patch
# User nipkow
# Date 972564761 -7200
# Node ID b124d59f7b61fc553d029ece40dbcd10c332bd86
# Parent  6eb91805a012c4a8bb6a839ba0f39ffd4eec7c2c
*** empty log message ***

diff -r 6eb91805a012 -r b124d59f7b61 src/HOL/IMP/Compiler.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Compiler.thy	Thu Oct 26 14:52:41 2000 +0200
@@ -0,0 +1,107 @@
+theory Compiler = Natural:
+
+datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
+
+consts  stepa1 :: "instr list => ((state*nat) * (state*nat))set"
+
+syntax
+        "@stepa1" :: "[instr list,state,nat,state,nat] => bool"
+                     ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
+        "@stepa" :: "[instr list,state,nat,state,nat] => bool"
+                     ("_ |-/ <_,_>/ -*-> <_,_>" [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)^*)"
+
+
+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 = JMB i |] ==> P |- <s,n> -1-> <s,n-i>"
+
+consts compile :: "com => instr list"
+primrec
+"compile SKIP = []"
+"compile (x:==a) = [ASIN x a]"
+"compile (c1;c2) = compile c1 @ compile c2"
+"compile (IF b THEN c1 ELSE c2) =
+ [JMPF b (length(compile c1)+2)] @ compile c1 @
+ [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
+"compile (WHILE b DO c) = [JMPF b (length(compile c)+2)] @ compile c @
+ [JMPB (length(compile c)+1)]"
+
+declare nth_append[simp];
+
+lemma nth_tl[simp]: "tl(xs @ y # ys) ! (length xs + z) = ys!z";
+apply(induct_tac xs);
+by(auto);
+
+theorem "<c,s> -c-> t ==> 
+ !a z. a@compile c@z |- <s,length a> -*-> <t,length a + length(compile c)>";
+apply(erule evalc.induct);
+      apply simp;
+     apply(force intro!: ASIN);
+    apply(intro strip);
+    apply(erule_tac x = a in allE);
+    apply(erule_tac x = "a@compile c0" in allE);
+    apply(erule_tac x = "compile c1@z" in allE);
+    apply(erule_tac x = z in allE);
+    apply(simp add:add_assoc[THEN sym]);
+    apply(blast intro:rtrancl_trans);
+(* IF b THEN c0 ELSE c1; case b is true *)
+   apply(intro strip);
+   (* instantiate assumption sufficiently for later: *)
+   apply(erule_tac x = "a@[?I]" in allE);
+   apply(simp);
+   (* execute JMPF: *)
+   apply(rule rtrancl_into_rtrancl2);
+    apply(rule JMPFT);
+     apply(simp);
+     apply(blast);
+    apply assumption;
+   (* 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);
+(* 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(blast);
+ apply(force intro: JMPFF);
+apply(intro strip);
+apply(erule_tac x = "a@[?I]" in allE);
+apply(erule_tac x = a in allE);
+apply(simp);
+apply(rule rtrancl_into_rtrancl2);
+ apply(rule JMPFT);
+  apply(simp);
+  apply(blast);
+ apply assumption;
+apply(rule rtrancl_trans);
+ apply(erule allE);
+ apply assumption;
+apply(rule rtrancl_into_rtrancl2);
+ apply(rule JMPB);
+ apply(simp);
+apply(simp);
+done
+
+(* Missing: the other direction! *)
+
+end
diff -r 6eb91805a012 -r b124d59f7b61 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Thu Oct 26 11:27:48 2000 +0200
+++ b/src/HOL/IMP/ROOT.ML	Thu Oct 26 14:52:41 2000 +0200
@@ -10,3 +10,4 @@
 time_use_thy "Transition";
 time_use_thy "VC";
 time_use_thy "Examples";
+time_use_thy "Compiler";