# HG changeset patch
# User nipkow
# Date 985779606 -7200
# Node ID f417841385b79b2f7845c89d8205a12028984c13
# Parent  5516e806dc09339d85ce5caefd9c2893b425c565
Got rid of is_dfa

diff -r 5516e806dc09 -r f417841385b7 src/HOL/MicroJava/BV/DFA_Framework.thy
--- 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
diff -r 5516e806dc09 -r f417841385b7 src/HOL/MicroJava/BV/DFA_err.thy
--- 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
diff -r 5516e806dc09 -r f417841385b7 src/HOL/MicroJava/BV/JVM.thy
--- 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"
diff -r 5516e806dc09 -r f417841385b7 src/HOL/MicroJava/BV/Kildall.thy
--- 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
diff -r 5516e806dc09 -r f417841385b7 src/HOL/MicroJava/BV/Typing_Framework.thy
--- /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
diff -r 5516e806dc09 -r f417841385b7 src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- /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