--- a/src/HOL/MicroJava/BV/DFA_Framework.thy Wed Mar 28 13:39:50 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: HOL/BCV/DFA_Framework.thy
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 2000 TUM
-*)
-
-header "Dataflow Analysis Framework"
-
-theory DFA_Framework = Listn:
-
-text {*
- The relationship between dataflow analysis and a welltyped-insruction predicate.
-*}
-
-constdefs
- bounded :: "(nat => nat list) => nat => bool"
-"bounded succs n == !p<n. !q:set(succs p). q<n"
-
- stable :: "'s ord =>
- (nat => 's => 's)
- => (nat => nat list) => 's list => nat => bool"
-"stable r step succs ss p == !q:set(succs p). step p (ss!p) <=_r ss!q"
-
- stables :: "'s ord => (nat => 's => 's)
- => (nat => nat list) => 's list => bool"
-"stables r step succs ss == !p<size ss. stable r step succs ss p"
-
- is_dfa :: "'s ord
- => ('s list => 's list)
- => (nat => 's => 's)
- => (nat => nat list)
- => nat => 's set => bool"
-"is_dfa r dfa step succs n A == !ss : list n A.
- dfa ss : list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss &
- (!ts: list n A. ss <=[r] ts & stables r step succs ts
- --> dfa ss <=[r] ts)"
-
- is_bcv :: "'s ord => 's => (nat => 's => 's) => (nat => nat list)
- => nat => 's set => ('s list => 's list) => bool"
-"is_bcv r T step succs n A bcv == !ss : list n A.
- (!p<n. (bcv ss)!p ~= T) =
- (? ts: list n A. ss <=[r] ts & welltyping r T step succs ts)"
-
- welltyping ::
-"'s ord => 's => (nat => 's => 's) => (nat => nat list) => 's list => bool"
-"welltyping r T step succs ts ==
- !p<size(ts). ts!p ~= T & stable r step succs ts p"
-
-
-lemma is_dfaD:
- "[| is_dfa r dfa step succs n A; ss : list n A |] ==>
- dfa ss:list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss &
- (!ts: list n A. stables r step succs ts & ss <=[r] ts
- --> dfa ss <=[r] ts)"
- by (simp add: is_dfa_def)
-
-
-lemma is_bcv_dfa:
- "[| order r; top r T; is_dfa r dfa step succs n A |]
- ==> is_bcv r T step succs n A dfa"
-apply (unfold is_bcv_def welltyping_def stables_def)
-apply clarify
-apply (drule is_dfaD)
-apply assumption
-apply clarify
-apply (rule iffI)
- apply (rule bexI)
- apply (rule conjI)
- apply assumption
- apply (simp add: stables_def)
- apply assumption
-apply clarify
-apply (simp add: imp_conjR all_conj_distrib stables_def
- cong: conj_cong)
-apply (drule_tac x = ts in bspec)
- apply assumption
-apply (force dest: le_listD)
-done
-
-end
--- a/src/HOL/MicroJava/BV/DFA_err.thy Wed Mar 28 13:39:50 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-(* Title: HOL/BCV/DFA_err.thy
- ID: $Id$
- Author: Gerwin Klein
- Copyright 2000 TUM
-
-*)
-
-header "Static and Dynamic Welltyping"
-
-theory DFA_err = DFA_Framework:
-
-constdefs
-
-dynamic_wt :: "'s ord => (nat => 's err => 's err) => (nat => nat list) =>
- 's err list => bool"
-"dynamic_wt r step succs ts == welltyping (Err.le r) Err step succs ts"
-
-static_wt :: "'s ord => (nat => 's => bool) =>
- (nat => 's => 's) => (nat => nat list) => 's list => bool"
-"static_wt r app step succs ts ==
- !p < size ts. app p (ts!p) & (!q:set(succs p). step p (ts!p) <=_r ts!q)"
-
-err_step :: "(nat => 's => bool) => (nat => 's => 's) =>
- (nat => 's err => 's err)"
-"err_step app step p == lift (%t. if app p t then OK (step p t) else Err)"
-
-non_empty :: "(nat => nat list) => bool"
-"non_empty succs == !p. succs p ~= []"
-
-
-lemma non_emptyD:
- "non_empty succs ==> ? q. q:set(succs p)"
-proof (unfold non_empty_def)
- assume "!p. succs p ~= []"
- hence "succs p ~= []" ..
- then obtain x xs where "succs p = x#xs"
- by (auto simp add: neq_Nil_conv)
- thus ?thesis
- by auto
-qed
-
-lemma dynamic_imp_static:
- "[| bounded succs (size ts); non_empty succs;
- dynamic_wt r (err_step app step) succs ts |]
- ==> static_wt r app step succs (map ok_val ts)"
-proof (unfold static_wt_def, intro strip, rule conjI)
-
- assume b: "bounded succs (size ts)"
- assume n: "non_empty succs"
- assume wt: "dynamic_wt r (err_step app step) succs ts"
-
- fix p
- assume "p < length (map ok_val ts)"
- hence lp: "p < length ts" by simp
-
- from wt lp
- have [intro?]: "!!p. p < length ts ==> ts ! p ~= Err"
- by (unfold dynamic_wt_def welltyping_def) simp
-
- show app: "app p (map ok_val ts ! p)"
- proof -
- from n
- obtain q where q: "q:set(succs p)"
- by (auto dest: non_emptyD)
-
- from wt lp q
- obtain s where
- OKp: "ts ! p = OK s" and
- less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
- by (unfold dynamic_wt_def welltyping_def stable_def)
- (auto iff: not_Err_eq)
-
- from lp b q
- have lq: "q < length ts"
- by (unfold bounded_def) blast
- hence "ts!q ~= Err" ..
- then
- obtain s' where OKq: "ts ! q = OK s'"
- by (auto iff: not_Err_eq)
-
- with OKp less
- have "app p s"
- by (simp add: err_step_def lift_def split: err.split_asm split_if_asm)
-
- with lp OKp
- show ?thesis
- by simp
- qed
-
- show "!q:set(succs p). step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
- proof (intro strip)
- fix q
- assume q: "q:set (succs p)"
-
- from wt lp q
- obtain s where
- OKp: "ts ! p = OK s" and
- less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
- by (unfold dynamic_wt_def welltyping_def stable_def)
- (auto iff: not_Err_eq)
-
- from lp b q
- have lq: "q < length ts"
- by (unfold bounded_def) blast
- hence "ts!q ~= Err" ..
- then
- obtain s' where OKq: "ts ! q = OK s'"
- by (auto iff: not_Err_eq)
-
- from lp lq OKp OKq app less
- show "step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
- by (simp add: err_step_def lift_def)
- qed
-qed
-
-
-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
--- a/src/HOL/MicroJava/BV/JVM.thy Wed Mar 28 13:39:50 2001 +0200
+++ b/src/HOL/MicroJava/BV/JVM.thy Wed Mar 28 13:40:06 2001 +0200
@@ -7,7 +7,8 @@
header "Kildall for the JVM"
-theory JVM = Kildall + JVMType + Opt + Product + DFA_err + StepMono + BVSpec:
+theory JVM = Kildall + JVMType + Opt + Product + Typing_Framework_err +
+ StepMono + BVSpec:
constdefs
exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> state"
--- a/src/HOL/MicroJava/BV/Kildall.thy Wed Mar 28 13:39:50 2001 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy Wed Mar 28 13:40:06 2001 +0200
@@ -8,7 +8,7 @@
header "Kildall's Algorithm"
-theory Kildall = DFA_Framework + While_Combinator:
+theory Kildall = Typing_Framework + While_Combinator:
constdefs
pres_type :: "(nat => 's => 's) => nat => 's set => bool"
@@ -343,25 +343,42 @@
apply(simp add:iter_def del:Let_def)
by(rule while_properties[THEN mp,OF _ _ _ _ _ _ _ _ refl])
-lemma is_dfa_kildall:
- "[| semilat(A,r,f); acc r; pres_type step n A;
- mono r step n A; bounded succs n|]
- ==> is_dfa r (kildall f step succs) step succs n A"
- apply (unfold is_dfa_def kildall_def)
- apply clarify
- apply (rule iter_properties)
- apply (simp_all add: unstables_def stable_def)
- apply (blast intro!: le_iff_plus_unchanged [THEN iffD2] listE_nth_in
- dest: boundedD pres_typeD)
- done
+lemma kildall_properties:
+ "\<lbrakk> semilat(A,r,f); acc r; pres_type step n A; mono r step n A;
+ bounded succs n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
+ kildall f step succs ss0 : list n A \<and>
+ stables r step succs (kildall f step succs ss0) \<and>
+ ss0 <=[r] kildall f step succs ss0 \<and>
+ (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow>
+ kildall f step succs ss0 <=[r] ts)";
+apply (unfold kildall_def)
+apply (rule iter_properties)
+apply (simp_all add: unstables_def stable_def)
+apply (blast intro!: le_iff_plus_unchanged [THEN iffD2] listE_nth_in
+ dest: boundedD pres_typeD)
+done
lemma is_bcv_kildall:
"[| semilat(A,r,f); acc r; top r T;
pres_type step n A; bounded succs n;
mono r step n A |]
==> is_bcv r T step succs n A (kildall f step succs)"
- apply (intro is_bcv_dfa is_dfa_kildall semilatDorderI)
- apply assumption+
- done
+apply(unfold is_bcv_def welltyping_def)
+apply(insert kildall_properties[of A])
+apply(simp add:stables_def)
+apply clarify
+apply(subgoal_tac "kildall f step succs ss : list n A")
+ prefer 2 apply (simp(no_asm_simp))
+apply (rule iffI)
+ apply (rule_tac x = "kildall f step succs ss" in bexI)
+ apply (rule conjI)
+ apply blast
+ apply (simp (no_asm_simp))
+ apply assumption
+apply clarify
+apply(subgoal_tac "kildall f step succs ss!p <=_r ts!p")
+ apply simp
+apply (blast intro!: le_listD less_lengthI)
+done
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy Wed Mar 28 13:40:06 2001 +0200
@@ -0,0 +1,39 @@
+(* Title: HOL/MicroJava/BV/Typing_Framework.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TUM
+*)
+
+header "Typing and Dataflow Analysis Framework"
+
+theory Typing_Framework = Listn:
+
+text {*
+ The relationship between dataflow analysis and a welltyped-insruction predicate.
+*}
+
+constdefs
+ bounded :: "(nat => nat list) => nat => bool"
+"bounded succs n == !p<n. !q:set(succs p). q<n"
+
+ stable :: "'s ord =>
+ (nat => 's => 's)
+ => (nat => nat list) => 's list => nat => bool"
+"stable r step succs ss p == !q:set(succs p). step p (ss!p) <=_r ss!q"
+
+ stables :: "'s ord => (nat => 's => 's)
+ => (nat => nat list) => 's list => bool"
+"stables r step succs ss == !p<size ss. stable r step succs ss p"
+
+ is_bcv :: "'s ord => 's => (nat => 's => 's) => (nat => nat list)
+ => nat => 's set => ('s list => 's list) => bool"
+"is_bcv r T step succs n A bcv == !ss : list n A.
+ (!p<n. (bcv ss)!p ~= T) =
+ (? ts: list n A. ss <=[r] ts & welltyping r T step succs ts)"
+
+ welltyping ::
+"'s ord => 's => (nat => 's => 's) => (nat => nat list) => 's list => bool"
+"welltyping r T step succs ts ==
+ !p<size(ts). ts!p ~= T & stable r step succs ts p"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Wed Mar 28 13:40:06 2001 +0200
@@ -0,0 +1,145 @@
+(* Title: HOL/MicroJava/BV/Typing_Framework_err.thy
+ ID: $Id$
+ Author: Gerwin Klein
+ Copyright 2000 TUM
+
+*)
+
+header "Static and Dynamic Welltyping"
+
+theory Typing_Framework_err = Typing_Framework:
+
+constdefs
+
+dynamic_wt :: "'s ord => (nat => 's err => 's err) => (nat => nat list) =>
+ 's err list => bool"
+"dynamic_wt r step succs ts == welltyping (Err.le r) Err step succs ts"
+
+static_wt :: "'s ord => (nat => 's => bool) =>
+ (nat => 's => 's) => (nat => nat list) => 's list => bool"
+"static_wt r app step succs ts ==
+ !p < size ts. app p (ts!p) & (!q:set(succs p). step p (ts!p) <=_r ts!q)"
+
+err_step :: "(nat => 's => bool) => (nat => 's => 's) =>
+ (nat => 's err => 's err)"
+"err_step app step p == lift (%t. if app p t then OK (step p t) else Err)"
+
+non_empty :: "(nat => nat list) => bool"
+"non_empty succs == !p. succs p ~= []"
+
+
+lemma non_emptyD:
+ "non_empty succs ==> ? q. q:set(succs p)"
+proof (unfold non_empty_def)
+ assume "!p. succs p ~= []"
+ hence "succs p ~= []" ..
+ then obtain x xs where "succs p = x#xs"
+ by (auto simp add: neq_Nil_conv)
+ thus ?thesis
+ by auto
+qed
+
+lemma dynamic_imp_static:
+ "[| bounded succs (size ts); non_empty succs;
+ dynamic_wt r (err_step app step) succs ts |]
+ ==> static_wt r app step succs (map ok_val ts)"
+proof (unfold static_wt_def, intro strip, rule conjI)
+
+ assume b: "bounded succs (size ts)"
+ assume n: "non_empty succs"
+ assume wt: "dynamic_wt r (err_step app step) succs ts"
+
+ fix p
+ assume "p < length (map ok_val ts)"
+ hence lp: "p < length ts" by simp
+
+ from wt lp
+ have [intro?]: "!!p. p < length ts ==> ts ! p ~= Err"
+ by (unfold dynamic_wt_def welltyping_def) simp
+
+ show app: "app p (map ok_val ts ! p)"
+ proof -
+ from n
+ obtain q where q: "q:set(succs p)"
+ by (auto dest: non_emptyD)
+
+ from wt lp q
+ obtain s where
+ OKp: "ts ! p = OK s" and
+ less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
+ by (unfold dynamic_wt_def welltyping_def stable_def)
+ (auto iff: not_Err_eq)
+
+ from lp b q
+ have lq: "q < length ts"
+ by (unfold bounded_def) blast
+ hence "ts!q ~= Err" ..
+ then
+ obtain s' where OKq: "ts ! q = OK s'"
+ by (auto iff: not_Err_eq)
+
+ with OKp less
+ have "app p s"
+ by (simp add: err_step_def lift_def split: err.split_asm split_if_asm)
+
+ with lp OKp
+ show ?thesis
+ by simp
+ qed
+
+ show "!q:set(succs p). step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
+ proof (intro strip)
+ fix q
+ assume q: "q:set (succs p)"
+
+ from wt lp q
+ obtain s where
+ OKp: "ts ! p = OK s" and
+ less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
+ by (unfold dynamic_wt_def welltyping_def stable_def)
+ (auto iff: not_Err_eq)
+
+ from lp b q
+ have lq: "q < length ts"
+ by (unfold bounded_def) blast
+ hence "ts!q ~= Err" ..
+ then
+ obtain s' where OKq: "ts ! q = OK s'"
+ by (auto iff: not_Err_eq)
+
+ from lp lq OKp OKq app less
+ show "step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
+ by (simp add: err_step_def lift_def)
+ qed
+qed
+
+
+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