diff --git a/thys/Dominance_CHK/Listn.thy b/thys/Dominance_CHK/Listn.thy
deleted file mode 100755
--- a/thys/Dominance_CHK/Listn.thy
+++ /dev/null
@@ -1,145 +0,0 @@
-(*  Title:      HOL/MicroJava/BV/Listn.thy
-    Author:     Tobias Nipkow
-    Copyright   2000 TUM
-
-Lists of a fixed length. 
-*)
-
-text \<open>Most definitions and lemmas in this theory are extracted from Jinja \cite{Listn-AFP}. 
-      Two lemmas "acc\_le\_listI" and "Cons\_less\_Conss" in the original Listn.thy are proved in the 'Dom\_kildall\_Property.thy'.\<close>
-
-section \<open>Fixed Length Lists\<close>
-
-theory Listn
-imports Semilat
-begin
-
-definition list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"
-where
-  "list n A = {xs. size xs = n \<and> set xs \<subseteq> A}"
-
-definition le :: "'a ord \<Rightarrow> ('a list)ord"
-where
-  "le r = list_all2 (\<lambda>x y. x \<sqsubseteq>\<^sub>r y)"
-
-abbreviation
-  lesublist :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"  ("(_ /[\<sqsubseteq>\<^bsub>_\<^esub>] _)" [50, 0, 51] 50) where
-  "x [\<sqsubseteq>\<^bsub>r\<^esub>] y == x <=_(Listn.le r) y"
-
-abbreviation
-  lesssublist :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"  ("(_ /[\<sqsubset>\<^bsub>_\<^esub>] _)" [50, 0, 51] 50) where
-  "x [\<sqsubset>\<^bsub>r\<^esub>] y == x <_(Listn.le r) y"
-
-(*<*)
-notation (ASCII)
-  lesublist  ("(_ /[<=_] _)" [50, 0, 51] 50) and
-  lesssublist  ("(_ /[<_] _)" [50, 0, 51] 50)
-
-abbreviation (input)
-  lesublist2 :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"  ("(_ /[\<sqsubseteq>\<^sub>_] _)" [50, 0, 51] 50) where
-  "x [\<sqsubseteq>\<^sub>r] y == x [\<sqsubseteq>\<^bsub>r\<^esub>] y"
-
-abbreviation (input)
-  lesssublist2 :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"  ("(_ /[\<sqsubset>\<^sub>_] _)" [50, 0, 51] 50) where
-  "x [\<sqsubset>\<^sub>r] y == x [\<sqsubset>\<^bsub>r\<^esub>] y"
-(*>*)
-
-abbreviation
-  plussublist :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
-    ("(_ /[\<squnion>\<^bsub>_\<^esub>] _)" [65, 0, 66] 65) where
-  "x [\<squnion>\<^bsub>f\<^esub>] y == x \<squnion>\<^bsub>map2 f\<^esub> y"
-
-(*<*)
-notation (ASCII)
-  plussublist  ("(_ /[+_] _)" [65, 0, 66] 65)
-
-abbreviation (input)
-  plussublist2 :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
-    ("(_ /[\<squnion>\<^sub>_] _)" [65, 0, 66] 65) where
-  "x [\<squnion>\<^sub>f] y == x [\<squnion>\<^bsub>f\<^esub>] y"
-(*>*)
-
-definition sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl"
-where
-  "sl n = (\<lambda>(A,r,f). (list n A, le r, map2 f))"
-
-lemmas [simp] = set_update_subsetI
-
-lemma unfold_lesub_list: "xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys = Listn.le r xs ys"
-(*<*) by (simp add: lesub_def) (*>*)
-
-lemma le_listD: "\<lbrakk> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys; p < size xs \<rbrakk> \<Longrightarrow> xs!p \<sqsubseteq>\<^sub>r ys!p"
-(*<*)
-by (simp add: Listn.le_def lesub_def list_all2_nthD)
-(*>*)
-
-lemma lesub_list_impl_same_size [simp]: "xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<Longrightarrow> size ys = size xs"
-(*<*)
-apply (unfold Listn.le_def lesub_def)
-apply (simp add: list_all2_lengthD)
-done
-(*>*)
-
-lemma lesssub_lengthD: "xs [\<sqsubset>\<^sub>r] ys \<Longrightarrow> size ys = size xs"  
-(*<*)
-apply (unfold lesssub_def)
-apply auto  \<comment> \<open>use lemma: lesub_list_impl_same_size \<close>
-done
-
-lemma listI: "\<lbrakk> size xs = n; set xs \<subseteq> A \<rbrakk> \<Longrightarrow> xs \<in> list n A"
-(*<*)
-apply (unfold list_def)
-apply blast
-done
-(*>*)
-
-(* FIXME: remove simp *)
-lemma listE_length [simp]: "xs \<in> list n A \<Longrightarrow> size xs = n"
-(*<*)
-apply (unfold list_def)
-apply blast
-done
-(*>*)
-
-
-lemma listE_set [simp]: "xs \<in> list n A \<Longrightarrow> set xs \<subseteq> A"
-(*<*)
-apply (unfold list_def)
-apply blast
-done
-(*>*)
-
-
-lemma in_list_Suc_iff:
-  "(xs \<in> list (Suc n) A) = (\<exists>y\<in>A. \<exists>ys \<in> list n A. xs = y#ys)"
-(*<*)
-apply (unfold list_def)
-apply (case_tac "xs")
-apply auto
-done
-
-lemma nth_in [rule_format, simp]:
-  "\<forall>i n. size xs = n \<longrightarrow> set xs \<subseteq> A \<longrightarrow> i < n \<longrightarrow> (xs!i) \<in> A"
-(*<*)
-apply (induct "xs")
- apply simp
-apply (simp add: nth_Cons split: nat.split)
-done
-
-
-lemma listt_update_in_list [simp, intro!]:
-  "\<lbrakk> xs \<in> list n A; x\<in>A \<rbrakk> \<Longrightarrow> xs[i := x] \<in> list n A" 
-(*<*)
-apply (unfold list_def)
-apply simp
-done
-(*>*)
-
-
-lemma Cons_le_Cons [iff]: "x#xs [\<sqsubseteq>\<^bsub>r\<^esub>] y#ys = (x \<sqsubseteq>\<^sub>r y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys)"
-(*<*)
-  by (simp add: lesub_def Listn.le_def)
-
-
-
-end
diff --git a/thys/Dominance_CHK/Semilat.thy b/thys/Dominance_CHK/Semilat.thy
deleted file mode 100755
--- a/thys/Dominance_CHK/Semilat.thy
+++ /dev/null
@@ -1,164 +0,0 @@
-
-(*  Title:      HOL/MicroJava/BV/Semilat.thy
-    Author:     Tobias Nipkow
-    Copyright   2000 TUM
-
-Semilattices.
-*)
-
-section \<open>Semilattices\<close>
-
-theory Semilat
-imports Main 
-begin
-
-text \<open>Most definitions are lemmas in this theory are extracted from Jinja \cite{Semilat-AFP}, 
-      'order r' is redefined to 'order r A', so related lemmas are also modified. \<close>
-
-type_synonym 'a ord    = "'a \<Rightarrow> 'a \<Rightarrow> bool"
-type_synonym 'a binop  = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-type_synonym 'a sl     = "'a set \<times> 'a ord \<times> 'a binop"
-
-definition lesub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
-  where "lesub x r y \<longleftrightarrow> r x y"
-
-definition lesssub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
-  where "lesssub x r y \<longleftrightarrow> lesub x r y \<and> x \<noteq> y"
-
-definition plussub :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c"
-  where "plussub x f y = f x y"
-                                       
-notation (ASCII)
-  "lesub"  ("(_ /<='__ _)" [50, 1000, 51] 50) and
-  "lesssub"  ("(_ /<'__ _)" [50, 1000, 51] 50) and
-  "plussub"  ("(_ /+'__ _)" [65, 1000, 66] 65)
-
-notation
-  "lesub"  ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
-  "lesssub"  ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
-  "plussub"  ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
-
-
-(* allow \<sub> instead of \<bsub>..\<esub> *)
-abbreviation (input)
-  lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
-  where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
-
-abbreviation (input)
-  lesssub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
-  where "x \<sqsubset>\<^sub>r y == x \<sqsubset>\<^bsub>r\<^esub> y"
-
-abbreviation (input)
-  plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
-  where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
-
-definition ord :: "('a \<times> 'a) set \<Rightarrow> 'a ord"
-where
-  "ord r = (\<lambda>x y. (x,y) \<in> r)"
-
-definition order :: "'a ord \<Rightarrow> 'a set \<Rightarrow> bool"
-where
-  "order r A \<longleftrightarrow> (\<forall>x\<in>A. x \<sqsubseteq>\<^sub>r x) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^sub>r y \<and> y \<sqsubseteq>\<^sub>r x \<longrightarrow> x=y) \<and> (\<forall>x\<in>A.  \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^sub>r y \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<sqsubseteq>\<^sub>r z)"
-
-definition top :: "'a ord \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow>  bool"
-where
-  "top r T A \<longleftrightarrow> (\<forall>x\<in>A. x \<sqsubseteq>\<^sub>r T)"
-  
-definition acc :: "'a ord \<Rightarrow>  bool"
-where
-  "acc r \<longleftrightarrow> wf {(y,x). x \<sqsubset>\<^sub>r y }"
-
-definition closed :: "'a set \<Rightarrow> 'a binop \<Rightarrow> bool"
-where
-  "closed A f \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x \<squnion>\<^sub>f y \<in> A)"
-
-definition semilat :: "'a sl \<Rightarrow> bool"
-where
-  "semilat = (\<lambda>(A,r,f). order r A \<and> closed A f \<and> 
-                       (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and>
-                       (\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and>
-                       (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z))"
-
-definition is_ub :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  "is_ub r x y u \<longleftrightarrow> (x,u)\<in>r \<and> (y,u)\<in>r"
-
-definition is_lub :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  "is_lub r x y u \<longleftrightarrow> is_ub r x y u \<and> (\<forall>z. is_ub r x y z \<longrightarrow> (u,z)\<in>r)"
-
-definition some_lub :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
-where
-  "some_lub r x y = (SOME z. is_lub r x y z)"
-
-lemma closedD: "\<lbrakk> closed A f; x\<in>A; y\<in>A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<in> A"
-  (*<*) by (unfold closed_def) blast (*>*)
-
-
-lemma order_trans: "\<lbrakk> order r A;  x \<sqsubseteq>\<^sub>r y;  y \<sqsubseteq>\<^sub>r z \<rbrakk> \<Longrightarrow>  x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> x \<sqsubseteq>\<^sub>r z"
-  (*<*) by (unfold order_def) blast (*>*)
-
-lemma order_antisym: "\<lbrakk> order r A; x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r x \<rbrakk> \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>  x = y"
-  (*<*) by (unfold order_def) ( simp (no_asm_simp)) (*>*)
-
-lemma order_refl [simp, intro]: "order r A \<Longrightarrow> x \<in> A \<Longrightarrow>  x \<sqsubseteq>\<^sub>r x"
-  (*<*) by (unfold order_def) (simp (no_asm_simp)) (*>*)
-
-locale Semilat =
-  fixes A :: "'a set"
-  fixes r :: "'a ord"
-  fixes f :: "'a binop"
-  assumes semilat: "semilat (A, r, f)"
-
-lemma semilat_Def:
-"semilat(A,r,f) \<longleftrightarrow> order r A \<and> closed A f \<and> 
-                 (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and> 
-                 (\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and> 
-                 (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z)"
-  (*<*) by (unfold semilat_def) clarsimp (*>*)
-
-lemma (in Semilat) orderI [simp, intro]: "order r A"
-  (*<*) using semilat by (simp add: semilat_Def) (*>*)
-
-lemma (in Semilat) refl_r [intro, simp]: "x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^sub>r x" by auto
-
-lemma (in Semilat) antisym_r [intro?]: "\<lbrakk> x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r x \<rbrakk> \<Longrightarrow> x\<in>A \<Longrightarrow>y\<in>A \<Longrightarrow>x = y"
-  (*<*) by (rule order_antisym) auto (*>*)
-
-lemma (in Semilat) lub [simp, intro?]:
-  "\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z"
-  (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
-
-lemma (in Semilat) ub2 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y"
-  (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
-
-lemma (in Semilat) closedI [simp, intro]: "closed A f"
-  (*<*) using semilat by (simp add: semilat_Def) (*>*)
-
-lemma (in Semilat) closed_f [simp, intro]: "\<lbrakk>x \<in> A; y \<in> A\<rbrakk>  \<Longrightarrow> x \<squnion>\<^sub>f y \<in> A"
-  (*<*) by (simp add: closedD [OF closedI]) (*>*)  
-  
-lemma (in Semilat) ub1 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y"
-  (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
-
-lemma (in Semilat) le_iff_plus_unchanged:
-  assumes "x \<in> A" and "y \<in> A"
-  shows "x \<sqsubseteq>\<^sub>r y \<longleftrightarrow> x \<squnion>\<^sub>f y = y" (is "?P \<longleftrightarrow> ?Q")
-(*<*)
-proof
-  assume ?P
-  with assms show ?Q by (blast intro: antisym_r lub ub2)
-next
-  assume ?Q
-  then have "y = x \<squnion>\<^bsub>f\<^esub> y" by simp
-  moreover from assms have "x \<sqsubseteq>\<^bsub>r\<^esub> x \<squnion>\<^bsub>f\<^esub> y" by simp
-  ultimately show ?P by simp
-qed
-
-lemma (in Semilat) plus_le_conv :
-  "\<lbrakk> x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> (x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z) = (x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z)"
-  (*<*) by (blast intro: ub1 ub2 lub order_trans) (*>*)
-
-
-end
-
diff --git a/thys/Jinja/DFA/Kildall.thy b/thys/Jinja/DFA/Kildall.thy
deleted file mode 100644
--- a/thys/Jinja/DFA/Kildall.thy
+++ /dev/null
@@ -1,513 +0,0 @@
-(*  Title:      HOL/MicroJava/BV/Kildall.thy
-    Author:     Tobias Nipkow, Gerwin Klein
-    Copyright   2000 TUM
-
-Kildall's algorithm.
-*)
-
-section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>
-
-theory Kildall
-imports SemilatAlg
-begin
-
-
-
-primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set"
-where
-  "propa f []      \<tau>s w = (\<tau>s,w)"
-| "propa f (q'#qs) \<tau>s w = (let (q,\<tau>) = q';
-                             u = \<tau> \<squnion>\<^bsub>f\<^esub> \<tau>s!q;
-                             w' = (if u = \<tau>s!q then w else insert q w)
-                         in propa f qs (\<tau>s[q := u]) w')"
-
-definition iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>
-          's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set"
-where
-  "iter f step \<tau>s w =
-   while (\<lambda>(\<tau>s,w). w \<noteq> {})
-         (\<lambda>(\<tau>s,w). let p = SOME p. p \<in> w
-                   in propa f (step p (\<tau>s!p)) \<tau>s (w-{p}))
-         (\<tau>s,w)"
-
-definition unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set"
-where
-  "unstables r step \<tau>s = {p. p < size \<tau>s \<and> \<not>stable r step \<tau>s p}"
-
-definition kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list"
-where
-  "kildall r f step \<tau>s = fst(iter f step \<tau>s (unstables r step \<tau>s))"
-
-primrec merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list"
-where
-  "merges f []      \<tau>s = \<tau>s"
-| "merges f (p'#ps) \<tau>s = (let (p,\<tau>) = p' in merges f ps (\<tau>s[p := \<tau> \<squnion>\<^bsub>f\<^esub> \<tau>s!p]))"
-
-
-lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric]
-
-
-lemma (in Semilat) nth_merges:
- "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
-  (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] \<Squnion>\<^bsub>f\<^esub> ss!p"
-  (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
-(*<*)
-proof (induct ps)
-  show "\<And>ss. ?P ss []" by simp
-
-  fix ss p' ps'
-  assume ss: "ss \<in> list n A"
-  assume l:  "p < length ss"
-  assume "?steptype (p'#ps')"
-  then obtain a b where
-    p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and ps': "?steptype ps'"
-    by (cases p') auto
-  assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
-  hence IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" using ps' by iprover
-
-  from ss ab
-  have "ss[a := b \<squnion>\<^bsub>f\<^esub> ss!a] \<in> list n A" by (simp add: closedD)
-  moreover
-  with l have "p < length (ss[a := b \<squnion>\<^bsub>f\<^esub> ss!a])" by simp
-  ultimately
-  have "?P (ss[a := b \<squnion>\<^bsub>f\<^esub> ss!a]) ps'" by (rule IH)
-  with p' l
-  show "?P ss (p'#ps')" by simp
-qed
-(*>*)
-
-
-(** merges **)
-
-lemma length_merges [simp]:
-  "\<And>ss. size(merges f ps ss) = size ss"
-(*<*) by (induct ps, auto) (*>*)
-
-lemma (in Semilat) merges_preserves_type_lemma:
-shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
-         \<longrightarrow> merges f ps xs \<in> list n A"
-(*<*)
-apply (insert closedI)
-apply (unfold closed_def)
-apply (induct ps)
- apply simp
-apply clarsimp
-done
-(*>*)
-
-lemma (in Semilat) merges_preserves_type [simp]:
- "\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
-  \<Longrightarrow> merges f ps xs \<in> list n A"
-by (simp add: merges_preserves_type_lemma)
-
-lemma (in Semilat) merges_incr_lemma:
- "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs"
-(*<*)
-apply (induct ps)
- apply simp
-apply simp
-apply clarify
-apply (rule order_trans)
-  apply simp
- apply (erule list_update_incr)
-  apply simp
- apply simp
-apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
-done
-(*>*)
-
-lemma (in Semilat) merges_incr:
- "\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> 
-  \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs"
-  by (simp add: merges_incr_lemma)
-
-
-lemma (in Semilat) merges_same_conv [rule_format]:
- "(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> 
-     (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x \<sqsubseteq>\<^bsub>r\<^esub> xs!p))"
-(*<*)
-  apply (induct_tac ps)
-   apply simp
-  apply clarsimp
-  apply (rename_tac p x ps xs)
-  apply (rule iffI)
-   apply (rule context_conjI)
-    apply (subgoal_tac "xs[p := x \<squnion>\<^bsub>f\<^esub> xs!p] [\<sqsubseteq>\<^bsub>r\<^esub>] xs")
-     apply (force dest!: le_listD simp add: nth_list_update)
-    apply (erule subst, rule merges_incr)
-       apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
-      apply clarify
-      apply (rule conjI)
-       apply simp
-       apply (blast dest: boundedD)
-      apply blast
-   apply clarify
-   apply (erule allE)
-   apply (erule impE)
-    apply assumption
-   apply (drule bspec)
-    apply assumption
-   apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
-   apply blast
-  apply clarify 
-  apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
-  done
-(*>*)
-
-
-lemma (in Semilat) list_update_le_listI [rule_format]:
-  "set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<longrightarrow> p < size xs \<longrightarrow>  
-   x \<sqsubseteq>\<^bsub>r\<^esub> ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x \<squnion>\<^bsub>f\<^esub> xs!p] [\<sqsubseteq>\<^bsub>r\<^esub>] ys"
-(*<*)
-  apply (insert semilat)
-  apply (simp only: Listn.le_def lesub_def semilat_def)
-  apply (simp add: list_all2_conv_all_nth nth_list_update)
-  done
-(*>*)
-
-lemma (in Semilat) merges_pres_le_ub:
-  assumes "set ts \<subseteq> A"  "set ss \<subseteq> A"
-    "\<forall>(p,t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts!p \<and> t \<in> A \<and> p < size ts"  "ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts"
-  shows "merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts"
-(*<*)
-proof -
-  { fix t ts ps
-    have
-    "\<And>qs. \<lbrakk>set ts \<subseteq> A; \<forall>(p,t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts!p \<and> t \<in> A \<and> p< size ts \<rbrakk> \<Longrightarrow>
-    set qs \<subseteq> set ps  \<longrightarrow> 
-    (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f qs ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)"
-    apply (induct_tac qs)
-     apply simp
-    apply (simp (no_asm_simp))
-    apply clarify
-    apply simp
-    apply (erule allE, erule impE, erule_tac [2] mp)
-     apply (drule bspec, assumption)
-     apply (simp add: closedD)
-    apply (drule bspec, assumption)
-    apply (simp add: list_update_le_listI)
-    done 
-  } note this [dest]  
-  from assms show ?thesis by blast
-qed
-(*>*)
-
-
-(** propa **)
-
-lemma decomp_propa:
-  "\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> 
-   propa f qs ss w = 
-   (merges f qs ss, {q. \<exists>t.(q,t)\<in>set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss!q \<noteq> ss!q} \<union> w)"
-(*<*)
-  apply (induct qs)
-   apply simp   
-  apply (simp (no_asm))
-  apply clarify  
-  apply simp
-  apply (rule conjI) 
-   apply blast
-  apply (simp add: nth_list_update)
-  apply blast
-  done 
-(*>*)
-
-(** iter **)
-
-lemma (in Semilat) stable_pres_lemma:
-shows "\<lbrakk>pres_type step n A; bounded step n; 
-     ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; 
-     \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; 
-     \<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' \<squnion>\<^bsub>f\<^esub> ss!q = ss!q; 
-     q \<notin> w \<or> q = p \<rbrakk> 
-  \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q"
-(*<*)
-  apply (unfold stable_def)
-  apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")
-   prefer 2
-   apply clarify
-   apply (erule pres_typeD)
-    prefer 3 apply assumption
-    apply (rule listE_nth_in)
-     apply assumption
-    apply simp
-   apply simp
-  apply simp
-  apply clarify
-  apply (subst nth_merges)
-       apply simp
-       apply (blast dest: boundedD)
-      apply assumption
-     apply clarify
-     apply (rule conjI)
-      apply (blast dest: boundedD)
-     apply (erule pres_typeD)
-       prefer 3 apply assumption
-      apply simp
-     apply simp
-apply(subgoal_tac "q < length ss")
-prefer 2 apply simp
-  apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
-apply assumption
-  apply clarify
-  apply (rule conjI)
-   apply (blast dest: boundedD)
-  apply (erule pres_typeD)
-     prefer 3 apply assumption
-    apply simp
-   apply simp
-  apply (drule_tac P = "\<lambda>x. (a, b) \<in> set (step q x)" in subst)
-   apply assumption
-
- apply (simp add: plusplus_empty)
- apply (cases "q \<in> w")
-  apply simp
-  apply (rule ub1')
-     apply (rule Semilat.intro)
-     apply (rule semilat)
-    apply clarify
-    apply (rule pres_typeD)
-       apply assumption
-      prefer 3 apply assumption
-     apply (blast intro: listE_nth_in dest: boundedD)
-    apply (blast intro: pres_typeD dest: boundedD)
-   apply (blast intro: listE_nth_in dest: boundedD)
-  apply assumption
-
- apply simp
- apply (erule allE, erule impE, assumption, erule impE, assumption)
- apply (rule order_trans)
-   apply simp
-  defer
- apply (rule pp_ub2)(*
-    apply assumption*)
-   apply simp
-   apply clarify
-   apply simp
-   apply (rule pres_typeD)
-      apply assumption
-     prefer 3 apply assumption
-    apply (blast intro: listE_nth_in dest: boundedD)
-   apply (blast intro: pres_typeD dest: boundedD)
-  apply (blast intro: listE_nth_in dest: boundedD)
- apply blast
- done
-(*>*)
-
-
-lemma (in Semilat) merges_bounded_lemma:
- "\<lbrakk> mono r step n A; bounded step n; 
-    \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
-    ss [\<sqsubseteq>\<^sub>r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
-  \<Longrightarrow> merges f (step p (ss!p)) ss [\<sqsubseteq>\<^sub>r] ts" 
-(*<*)
-  apply (unfold stable_def)
-  apply (rule merges_pres_le_ub)
-     apply simp
-    apply simp
-   prefer 2 apply assumption
-
-  apply clarsimp
-  apply (drule boundedD, assumption+)
-  apply (erule allE, erule impE, assumption)
-  apply (drule bspec, assumption)
-  apply simp
-
-  apply (drule monoD [of _ _ _ _ p "ss!p"  "ts!p"])
-     apply assumption
-    apply simp
-   apply (simp add: le_listD)
-  
-  apply (drule lesub_step_typeD, assumption) 
-  apply clarify
-  apply (drule bspec, assumption)
-  apply simp
-  apply (blast intro: order_trans)
-  done
-(*>*)
-
-lemma termination_lemma: assumes "Semilat A r f"
-shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
-      ss [\<sqsubset>\<^sub>r] merges f qs ss \<or> 
-  merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss!q \<noteq> ss!q} \<union> (w-{p}) \<subset> w"
-(*<*) (is "PROP ?P")
-proof -
-  interpret Semilat A r f by fact
-  show "PROP ?P"
-  apply(insert semilat)
-    apply (unfold lesssub_def)
-    apply (simp (no_asm_simp) add: merges_incr)
-    apply (rule impI)
-    apply (rule merges_same_conv [THEN iffD1, elim_format]) 
-    apply assumption+
-      defer
-      apply (rule sym, assumption)
-     defer apply simp
-     apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)")
-     apply (blast intro!: psubsetI elim: equalityE)
-     apply clarsimp
-     apply (drule bspec, assumption) 
-     apply (drule bspec, assumption)
-     apply clarsimp
-    done 
-qed
-(*>*)
-
-lemma iter_properties[rule_format]: assumes "Semilat A r f"
-shows "\<lbrakk> acc r; pres_type step n A; mono r step n A;
-     bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
-     \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
-   iter f step ss0 w0 = (ss',w')
-   \<longrightarrow>
-   ss' \<in> list n A \<and> stables r step ss' \<and> ss0 [\<sqsubseteq>\<^sub>r] ss' \<and>
-   (\<forall>ts\<in>list n A. ss0 [\<sqsubseteq>\<^sub>r] ts \<and> stables r step ts \<longrightarrow> ss' [\<sqsubseteq>\<^sub>r] ts)"
-(*<*) (is "PROP ?P")
-proof -
-  interpret Semilat A r f by fact
-  show "PROP ?P"
-  apply(insert semilat)
-  apply (unfold iter_def stables_def)
-  apply (rule_tac P = "\<lambda>(ss,w).
-   ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 [\<sqsubseteq>\<^sub>r] ss \<and>
-   (\<forall>ts\<in>list n A. ss0 [\<sqsubseteq>\<^sub>r] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^sub>r] ts) \<and>
-   (\<forall>p\<in>w. p < n)" and
-   r = "{(ss',ss) . ss [\<sqsubset>\<^sub>r] ss'} <*lex*> finite_psubset"
-         in while_rule)
-
-  \<comment> \<open>Invariant holds initially:\<close>
-  apply (simp add:stables_def)
-
-  \<comment> \<open>Invariant is preserved:\<close>
-  apply(simp add: stables_def split_paired_all)
-  apply(rename_tac ss w)
-  apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
-   prefer 2 apply (fast intro: someI)
-  apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
-   prefer 2
-   apply clarify
-   apply (rule conjI)
-    apply(clarsimp, blast dest!: boundedD)
-   apply (erule pres_typeD)
-    prefer 3
-    apply assumption
-    apply (erule listE_nth_in)
-    apply blast
-   apply blast
-  apply (subst decomp_propa)
-   apply blast
-  apply simp
-  apply (rule conjI)
-   apply (rule merges_preserves_type)
-   apply blast
-   apply clarify
-   apply (rule conjI)
-    apply(clarsimp, blast dest!: boundedD)
-   apply (erule pres_typeD)
-    prefer 3
-    apply assumption
-    apply (erule listE_nth_in)
-    apply blast
-   apply blast
-  apply (rule conjI)
-   apply clarify
-   apply (blast intro!: stable_pres_lemma)
-  apply (rule conjI)
-   apply (blast intro!: merges_incr intro: le_list_trans)
-  apply (rule conjI)
-   apply clarsimp
-   apply (blast intro!: merges_bounded_lemma)
-  apply (blast dest!: boundedD)
-
-
-  \<comment> \<open>Postcondition holds upon termination:\<close>
-  apply(clarsimp simp add: stables_def split_paired_all)
-
-  \<comment> \<open>Well-foundedness of the termination relation:\<close>
-  apply (rule wf_lex_prod)
-   apply (insert orderI [THEN acc_le_listI])
-   apply (simp only: acc_def lesssub_def)
-  apply (rule wf_finite_psubset) 
-
-  \<comment> \<open>Loop decreases along termination relation:\<close>
-  apply(simp add: stables_def split_paired_all)
-  apply(rename_tac ss w)
-  apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
-   prefer 2 apply (fast intro: someI)
-  apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
-   prefer 2
-   apply clarify
-   apply (rule conjI)
-    apply(clarsimp, blast dest!: boundedD)
-   apply (erule pres_typeD)
-    prefer 3
-    apply assumption
-    apply (erule listE_nth_in)
-    apply blast
-   apply blast
-  apply (subst decomp_propa)
-   apply blast
-  apply clarify
-  apply (simp del: listE_length
-      add: lex_prod_def finite_psubset_def 
-           bounded_nat_set_is_finite)
-  apply (rule termination_lemma)
-  apply (rule assms)
-  apply assumption+
-  defer
-  apply assumption
-  apply clarsimp
-  done
-qed
-(*>*)
-
-
-lemma kildall_properties: assumes "Semilat A r f"
-shows "\<lbrakk> acc r; pres_type step n A; mono r step n A;
-     bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
-  kildall r f step ss0 \<in> list n A \<and>
-  stables r step (kildall r f step ss0) \<and>
-  ss0 [\<sqsubseteq>\<^sub>r] kildall r f step ss0 \<and>
-  (\<forall>ts\<in>list n A. ss0 [\<sqsubseteq>\<^sub>r] ts \<and> stables r step ts \<longrightarrow>
-                 kildall r f step ss0 [\<sqsubseteq>\<^sub>r] ts)"
-(*<*) (is "PROP ?P")
-proof -
-  interpret Semilat A r f by fact
-  show "PROP ?P"
-  apply (unfold kildall_def)
-  apply(case_tac "iter f step ss0 (unstables r step ss0)")
-  apply(simp)
-  apply (rule iter_properties)
-  apply (simp_all add: unstables_def stable_def)
-  apply (rule Semilat.intro)
-  apply (rule semilat)
-  done
-qed
-
-
-lemma is_bcv_kildall: assumes "Semilat A r f"
-shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk>
-  \<Longrightarrow> is_bcv r T step n A (kildall r f step)" (is "PROP ?P")
-proof -
-  interpret Semilat A r f by fact
-  show "PROP ?P"
-  apply(unfold is_bcv_def wt_step_def)
-  apply(insert \<open>Semilat A r f\<close> semilat kildall_properties[of A])
-  apply(simp add:stables_def)
-  apply clarify
-  apply(subgoal_tac "kildall r f step \<tau>s\<^sub>0 \<in> list n A")
-   prefer 2 apply (simp(no_asm_simp))
-  apply (rule iffI)
-   apply (rule_tac x = "kildall r f step \<tau>s\<^sub>0" in bexI) 
-    apply (rule conjI)
-     apply (blast)
-    apply (simp  (no_asm_simp))
-   apply(assumption)
-  apply clarify
-  apply(subgoal_tac "kildall r f step \<tau>s\<^sub>0!p <=_r \<tau>s!p")
-   apply simp
-  apply (blast intro!: le_listD less_lengthI)
-  done
-qed
-(*>*)
-
-end
diff --git a/thys/Jinja/DFA/Kildall_1.thy b/thys/Jinja/DFA/Kildall_1.thy
new file mode 100644
--- /dev/null
+++ b/thys/Jinja/DFA/Kildall_1.thy
@@ -0,0 +1,143 @@
+(*  Title:      HOL/MicroJava/BV/Kildall.thy
+    Author:     Tobias Nipkow, Gerwin Klein
+    Copyright   2000 TUM
+
+Kildall's algorithm.
+*)
+
+section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>
+
+theory Kildall_1
+imports SemilatAlg
+begin
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+primrec merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list"
+where
+  "merges f []      \<tau>s = \<tau>s"
+| "merges f (p'#ps) \<tau>s = (let (p,\<tau>) = p' in merges f ps (\<tau>s[p := \<tau> \<squnion>\<^bsub>f\<^esub> \<tau>s!p]))"
+
+
+lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric]
+
+
+lemma (in Semilat) nth_merges:
+ "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
+  (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] \<Squnion>\<^bsub>f\<^esub> ss!p"
+  (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
+(*<*)
+proof (induct ps)
+  show "\<And>ss. ?P ss []" by simp
+
+  fix ss p' ps'
+  assume ss: "ss \<in> list n A"
+  assume l:  "p < length ss"
+  assume "?steptype (p'#ps')"
+  then obtain a b where
+    p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and ps': "?steptype ps'"
+    by (cases p') auto
+  assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
+  hence IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" using ps' by iprover
+
+  from ss ab
+  have "ss[a := b \<squnion>\<^bsub>f\<^esub> ss!a] \<in> list n A" by (simp add: closedD)
+  moreover
+  with l have "p < length (ss[a := b \<squnion>\<^bsub>f\<^esub> ss!a])" by simp
+  ultimately
+  have "?P (ss[a := b \<squnion>\<^bsub>f\<^esub> ss!a]) ps'" by (rule IH)
+  with p' l
+  show "?P ss (p'#ps')" by simp
+qed
+(*>*)
+
+
+(** merges **)
+
+lemma length_merges [simp]:
+  "\<And>ss. size(merges f ps ss) = size ss"
+(*<*) by (induct ps, auto) (*>*)
+
+lemma (in Semilat) merges_preserves_type_lemma:
+shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
+         \<longrightarrow> merges f ps xs \<in> list n A"
+(*<*)
+apply (insert closedI)
+apply (unfold closed_def)
+apply (induct ps)
+ apply simp
+apply clarsimp
+done
+(*>*)
+
+lemma (in Semilat) merges_preserves_type [simp]:
+ "\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
+  \<Longrightarrow> merges f ps xs \<in> list n A"
+by (simp add: merges_preserves_type_lemma)
+
+lemma (in Semilat) list_update_le_listI [rule_format]:
+  "set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<longrightarrow> p < size xs \<longrightarrow>  
+   x \<sqsubseteq>\<^bsub>r\<^esub> ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x \<squnion>\<^bsub>f\<^esub> xs!p] [\<sqsubseteq>\<^bsub>r\<^esub>] ys"
+(*<*)
+  apply (insert semilat)
+  apply (simp only: Listn.le_def lesub_def semilat_def)
+  apply (simp add: list_all2_conv_all_nth nth_list_update)
+  done
+(*>*)
+
+lemma (in Semilat) merges_pres_le_ub:
+  assumes "set ts \<subseteq> A"  "set ss \<subseteq> A"
+    "\<forall>(p,t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts!p \<and> t \<in> A \<and> p < size ts"  "ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts"
+  shows "merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts"
+(*<*)
+proof -
+  { fix t ts ps
+    have
+    "\<And>qs. \<lbrakk>set ts \<subseteq> A; \<forall>(p,t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts!p \<and> t \<in> A \<and> p< size ts \<rbrakk> \<Longrightarrow>
+    set qs \<subseteq> set ps  \<longrightarrow> 
+    (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f qs ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)"
+    apply (induct_tac qs)
+     apply simp
+    apply (simp (no_asm_simp))
+    apply clarify
+    apply simp
+    apply (erule allE, erule impE, erule_tac [2] mp)
+     apply (drule bspec, assumption)
+     apply (simp add: closedD)
+    apply (drule bspec, assumption)
+    apply (simp add: list_update_le_listI)
+    done 
+  } note this [dest]  
+  from assms show ?thesis by blast
+qed
+(*>*)
+
+
+
+
+end
diff --git a/thys/Jinja/DFA/Kildall_2.thy b/thys/Jinja/DFA/Kildall_2.thy
new file mode 100644
--- /dev/null
+++ b/thys/Jinja/DFA/Kildall_2.thy
@@ -0,0 +1,288 @@
+(*  Title:      HOL/MicroJava/BV/Kildall.thy
+    Author:     Tobias Nipkow, Gerwin Klein
+    Copyright   2000 TUM
+
+Kildall's algorithm.
+*)
+
+section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>
+
+theory Kildall_2
+imports SemilatAlg Kildall_1
+begin
+
+
+
+primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set"
+where
+  "propa f []      \<tau>s w = (\<tau>s,w)"
+| "propa f (q'#qs) \<tau>s w = (let (q,\<tau>) = q';
+                             u = \<tau> \<squnion>\<^bsub>f\<^esub> \<tau>s!q;
+                             w' = (if u = \<tau>s!q then w else insert q w)
+                         in propa f qs (\<tau>s[q := u]) w')"
+
+definition iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>
+          's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set"
+where
+  "iter f step \<tau>s w =
+   while (\<lambda>(\<tau>s,w). w \<noteq> {})
+         (\<lambda>(\<tau>s,w). let p = SOME p. p \<in> w
+                   in propa f (step p (\<tau>s!p)) \<tau>s (w-{p}))
+         (\<tau>s,w)"
+
+definition unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set"
+where
+  "unstables r step \<tau>s = {p. p < size \<tau>s \<and> \<not>stable r step \<tau>s p}"
+
+definition kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list"
+where
+  "kildall r f step \<tau>s = fst(iter f step \<tau>s (unstables r step \<tau>s))"
+
+
+(** propa **)
+lemma (in Semilat) merges_incr_lemma:
+ "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs"
+  apply (induct ps)
+   apply simp
+   apply(insert orderI)
+   apply (fastforce intro:le_list_refl')  
+  apply simp
+  apply clarify
+  apply (rule order_trans)
+       defer
+       apply (erule list_update_incr)
+        apply simp+     
+  done       
+
+(*>*)
+
+lemma (in Semilat) merges_incr:
+ "\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> 
+  \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] merges f ps xs"
+  by (simp add: merges_incr_lemma)
+
+
+lemma (in Semilat) merges_same_conv [rule_format]:
+ "(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> 
+     (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x \<sqsubseteq>\<^bsub>r\<^esub> xs!p))"
+(*<*)
+  apply (induct_tac ps)
+   apply simp
+  apply clarsimp
+  apply (rename_tac p x ps xs)
+  apply (rule iffI)
+   apply (rule context_conjI)
+    apply (subgoal_tac "xs[p := x \<squnion>\<^bsub>f\<^esub> xs!p] [\<sqsubseteq>\<^bsub>r\<^esub>] xs")
+     apply (fastforce dest!: le_listD)  \<comment>\<open>apply (force dest!: le_listD simp add: nth_list_update) \<close>
+    apply (erule subst, rule merges_incr)
+       apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
+      apply clarify
+      apply (rule conjI)
+       apply simp
+       apply (blast dest: boundedD)
+      apply blast
+   apply clarify
+   apply (erule allE)
+   apply (erule impE)
+    apply assumption
+   apply (drule bspec)
+    apply assumption
+   apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
+   apply blast
+  apply clarify 
+  apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
+  done
+(*>*)
+
+lemma decomp_propa:
+  "\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> 
+   propa f qs ss w = 
+   (merges f qs ss, {q. \<exists>t.(q,t)\<in>set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss!q \<noteq> ss!q} \<union> w)"
+(*<*)
+  apply (induct qs)
+   apply simp   
+  apply (simp (no_asm))
+  apply clarify  
+  apply simp
+  apply (rule conjI) 
+   apply blast
+  apply (simp add: nth_list_update)
+  apply blast
+  done 
+(*>*)
+
+lemma (in Semilat) stable_pres_lemma:
+shows "\<lbrakk>pres_type step n A; bounded step n; 
+     ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; 
+     \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; 
+     \<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' \<squnion>\<^bsub>f\<^esub> ss!q = ss!q; 
+     q \<notin> w \<or> q = p \<rbrakk> 
+  \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q"
+(*<*)
+  apply (unfold stable_def)
+  apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")
+   prefer 2
+   apply clarify
+   apply (erule pres_typeD)
+    prefer 3 apply assumption
+    apply (rule listE_nth_in)
+     apply assumption
+    apply simp
+   apply simp
+  apply simp
+  apply clarify
+  apply (subst nth_merges)
+       apply simp
+       apply (blast dest: boundedD)
+      apply assumption
+     apply clarify
+     apply (rule conjI)
+      apply (blast dest: boundedD)
+     apply (erule pres_typeD)
+       prefer 3 apply assumption
+      apply simp
+     apply simp
+apply(subgoal_tac "q < length ss")
+prefer 2 apply simp
+  apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
+apply assumption
+  apply clarify
+  apply (rule conjI)
+   apply (blast dest: boundedD)
+  apply (erule pres_typeD)
+     prefer 3 apply assumption
+    apply simp
+   apply simp
+  apply (drule_tac P = "\<lambda>x. (a, b) \<in> set (step q x)" in subst)
+   apply assumption
+
+ apply (simp add: plusplus_empty)
+ apply (cases "q \<in> w")
+  apply simp
+  apply (rule ub1')
+     apply (rule Semilat.intro)
+     apply (rule semilat)
+    apply clarify
+    apply (rule pres_typeD)
+       apply assumption
+      prefer 3 apply assumption
+     apply (blast intro: listE_nth_in dest: boundedD)
+    apply (blast intro: pres_typeD dest: boundedD)
+   apply (blast intro: listE_nth_in dest: boundedD)
+  apply assumption
+
+ apply simp
+  apply (erule allE, erule impE, assumption, erule impE, assumption) 
+  apply (rule order_trans)    
+  apply fastforce
+       defer     
+       apply (rule pp_ub2)
+        apply simp        
+        apply clarify
+        apply simp
+        apply (rule pres_typeD)
+           apply assumption
+          prefer 3 
+          apply assumption
+         apply (blast intro: listE_nth_in)
+        apply (blast)
+       apply (blast intro: listE_nth_in dest: boundedD)
+     prefer 4
+  apply fastforce     
+    apply (blast intro: listE_nth_in dest: pres_typeD)
+   apply (blast intro: listE_nth_in dest: boundedD)
+  apply(subgoal_tac "\<forall>(q,t) \<in> set (step p (ss!p)). q < n \<and> t \<in> A")
+
+   apply (subgoal_tac "merges f (step p (ss!p)) ss \<in> list n A")
+  defer
+    apply (blast dest:merges_preserves_type)
+   defer
+   apply (subgoal_tac "a < n")
+  defer
+    apply (blast intro: listE_nth_in  boundedD )
+   defer
+  apply (subgoal_tac "merges f (step p (ss ! p)) ss ! a = 
+      map snd (filter (\<lambda>(p', t'). p' = a) (step p (ss ! p))) \<Squnion>\<^bsub>f\<^esub> ss ! a")
+    apply (fastforce  dest: listE_nth_in ) (* slow *)
+  apply (subgoal_tac "a < length ss")
+    apply (fastforce dest:nth_merges)
+   apply simp
+  apply (intro strip)
+  apply auto
+  defer
+   apply (auto intro:boundedD)
+  apply (fastforce intro: listE_nth_in dest:pres_typeD)
+  done
+(*>*)
+
+
+lemma (in Semilat) merges_bounded_lemma:
+ "\<lbrakk> mono r step n A; bounded step n; pres_type step n A; 
+    \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
+    ss [\<sqsubseteq>\<^sub>r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
+  \<Longrightarrow> merges f (step p (ss!p)) ss [\<sqsubseteq>\<^sub>r] ts" 
+(*<*)
+  apply (unfold stable_def)
+  apply (rule merges_pres_le_ub)
+     apply simp
+    apply simp
+   prefer 2 apply assumption
+
+  apply clarsimp
+  apply (drule boundedD, assumption+)
+  apply (erule allE, erule impE, assumption)
+  apply (drule bspec, assumption)
+  apply simp
+
+  apply (drule monoD [of _ _ _ _ p "ss!p"  "ts!p"])
+     apply assumption
+    apply simp
+   apply (simp add: le_listD)
+  
+  apply (drule lesub_step_typeD, assumption) 
+  apply clarify
+  apply (drule bspec, assumption)
+  apply simp
+
+  apply (rule order_trans)
+       apply fastforce
+      apply simp
+     apply simp
+    apply simp
+   apply (auto intro:boundedD)
+
+  apply (blast intro: listE_nth_in dest:pres_typeD)
+  done
+(*>*)
+
+
+
+(** iter **)
+lemma termination_lemma: assumes "Semilat A r f"
+shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
+      ss [\<sqsubset>\<^sub>r] merges f qs ss \<or> 
+  merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss!q \<noteq> ss!q} \<union> (w-{p}) \<subset> w"
+(*<*) (is "PROP ?P")
+proof -
+  interpret Semilat A r f by fact
+  show "PROP ?P"
+  apply(insert semilat)
+    apply (unfold lesssub_def)
+    apply (simp (no_asm_simp) add: merges_incr)
+    apply (rule impI)
+    apply (rule merges_same_conv [THEN iffD1, elim_format]) 
+    apply assumption+
+      defer
+      apply (rule sym, assumption)
+     defer apply simp
+     apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t \<squnion>\<^bsub>f\<^esub> ss ! q \<noteq> ss ! q)")
+     apply (blast intro!: psubsetI elim: equalityE)
+     apply clarsimp
+     apply (drule bspec, assumption) 
+     apply (drule bspec, assumption)
+     apply clarsimp
+    done 
+qed
+(*>*)
+
+end
diff --git a/thys/Jinja/DFA/Typing_Framework.thy b/thys/Jinja/DFA/Typing_Framework.thy
deleted file mode 100644
--- a/thys/Jinja/DFA/Typing_Framework.thy
+++ /dev/null
@@ -1,33 +0,0 @@
-(*  Title:      HOL/MicroJava/BV/Typing_Framework.thy
-    Author:     Tobias Nipkow
-    Copyright   2000 TUM
-*)
-
-section \<open>Typing and Dataflow Analysis Framework\<close>
-
-theory Typing_Framework imports Semilattices begin
-
-text \<open>
-  The relationship between dataflow analysis and a welltyped-instruction predicate. 
-\<close>
-type_synonym
-  's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
-
-definition stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
-where
-  "stable r step \<tau>s p \<longleftrightarrow> (\<forall>(q,\<tau>) \<in> set (step p (\<tau>s!p)). \<tau> \<sqsubseteq>\<^sub>r \<tau>s!q)"
-
-definition stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
-where
-  "stables r step \<tau>s \<longleftrightarrow> (\<forall>p < size \<tau>s. stable r step \<tau>s p)"
-
-definition wt_step :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
-where
-  "wt_step r T step \<tau>s \<longleftrightarrow> (\<forall>p<size \<tau>s. \<tau>s!p \<noteq> T \<and> stable r step \<tau>s p)"
-
-definition is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool"
-where
-  "is_bcv r T step n A bcv \<longleftrightarrow> (\<forall>\<tau>s\<^sub>0 \<in> list n A.
-  (\<forall>p<n. (bcv \<tau>s\<^sub>0)!p \<noteq> T) = (\<exists>\<tau>s \<in> list n A. \<tau>s\<^sub>0 [\<sqsubseteq>\<^sub>r] \<tau>s \<and> wt_step r T step \<tau>s))"
-
-end
diff --git a/thys/Jinja/DFA/Typing_Framework_1.thy b/thys/Jinja/DFA/Typing_Framework_1.thy
new file mode 100644
--- /dev/null
+++ b/thys/Jinja/DFA/Typing_Framework_1.thy
@@ -0,0 +1,28 @@
+(*  Title:      HOL/MicroJava/BV/Typing_Framework.thy
+    Author:     Tobias Nipkow
+    Copyright   2000 TUM
+*)
+
+section \<open>Typing and Dataflow Analysis Framework\<close>
+
+theory Typing_Framework_1 imports Semilattices begin
+
+text \<open>
+  The relationship between dataflow analysis and a welltyped-instruction predicate. 
+\<close>
+type_synonym
+  's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
+
+definition stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
+where
+  "stable r step \<tau>s p \<longleftrightarrow> (\<forall>(q,\<tau>) \<in> set (step p (\<tau>s!p)). \<tau> \<sqsubseteq>\<^sub>r \<tau>s!q)"
+
+definition stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
+where
+  "stables r step \<tau>s \<longleftrightarrow> (\<forall>p < size \<tau>s. stable r step \<tau>s p)"
+
+definition wt_step :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
+where
+  "wt_step r T step \<tau>s \<longleftrightarrow> (\<forall>p<size \<tau>s. \<tau>s!p \<noteq> T \<and> stable r step \<tau>s p)"
+
+end
diff --git a/thys/Jinja/DFA/Typing_Framework_2.thy b/thys/Jinja/DFA/Typing_Framework_2.thy
new file mode 100644
--- /dev/null
+++ b/thys/Jinja/DFA/Typing_Framework_2.thy
@@ -0,0 +1,19 @@
+(*  Title:      HOL/MicroJava/BV/Typing_Framework.thy
+    Author:     Tobias Nipkow
+    Copyright   2000 TUM
+*)
+
+section \<open>Typing and Dataflow Analysis Framework\<close>
+
+theory Typing_Framework_2 imports Typing_Framework_1 begin
+
+text \<open>
+  The relationship between dataflow analysis and a welltyped-instruction predicate. 
+\<close>
+
+definition is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool"
+where
+  "is_bcv r T step n A bcv \<longleftrightarrow> (\<forall>\<tau>s\<^sub>0 \<in> list n A.
+  (\<forall>p<n. (bcv \<tau>s\<^sub>0)!p \<noteq> T) = (\<exists>\<tau>s \<in> list n A. \<tau>s\<^sub>0 [\<sqsubseteq>\<^sub>r] \<tau>s \<and> wt_step r T step \<tau>s))"
+
+end