summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | kleing |

Tue, 12 Dec 2000 14:08:26 +0100 | |

changeset 10650 | 114999ff8d19 |

parent 10649 | fb27b5547765 |

child 10651 | bb3a81a005f7 |

added direction dynamic ==> static

--- 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