# HG changeset patch
# User kleing
# Date 976626506 -3600
# Node ID 114999ff8d1986906a399365d3033ec4bced9d8d
# Parent  fb27b5547765dd520235720986f6c2906d546fd6
added direction dynamic ==> static

diff -r fb27b5547765 -r 114999ff8d19 src/HOL/MicroJava/BV/DFA_err.thy
--- a/src/HOL/MicroJava/BV/DFA_err.thy	Tue Dec 12 14:07:11 2000 +0100
+++ b/src/HOL/MicroJava/BV/DFA_err.thy	Tue Dec 12 14:08:26 2000 +0100
@@ -40,7 +40,6 @@
     by auto
 qed
 
-text_raw {* \newpage *}
 lemma dynamic_imp_static:
   "[| bounded succs (size ts); non_empty succs;
       dynamic_wt r (err_step app step) succs ts |] 
@@ -115,4 +114,33 @@
   qed
 qed
 
-end
+
+lemma static_imp_dynamic:
+  "[| static_wt r app step succs ts; bounded succs (size ts) |] 
+  ==> dynamic_wt r (err_step app step) succs (map OK ts)"
+proof (unfold dynamic_wt_def welltyping_def, intro strip, rule conjI)
+  assume bounded: "bounded succs (size ts)"
+  assume static:  "static_wt r app step succs ts"
+  fix p assume "p < length (map OK ts)" 
+  hence p: "p < length ts" by simp
+  thus "map OK ts ! p \<noteq> Err" by simp
+  { fix q
+    assume q: "q : set (succs p)"
+    with p static obtain 
+      "app p (ts ! p)" "step p (ts ! p) <=_r ts ! q"
+      by (unfold static_wt_def) blast
+    moreover
+    from q p bounded
+    have "q < size ts" by (unfold bounded_def) blast
+    hence "map OK ts ! q = OK (ts!q)" by simp
+    moreover
+    have "p < size ts" by (rule p)
+    ultimately     
+    have "err_step app step p (map OK ts ! p) <=_(Err.le r) map OK ts ! q"
+      by (simp add: err_step_def lift_def)
+  }
+  thus "stable (Err.le r) (err_step app step) succs (map OK ts) p"
+    by (unfold stable_def) blast
+qed
+
+end
\ No newline at end of file