diff --git a/src/Doc/Codegen/Inductive_Predicate.thy b/src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy
+++ b/src/Doc/Codegen/Inductive_Predicate.thy
@@ -1,268 +1,268 @@
 theory Inductive_Predicate
 imports Setup
 begin
 
 (*<*)
 hide_const %invisible append
 
 inductive %invisible append where
   "append [] ys ys"
 | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
 lemma %invisible append: "append xs ys zs = (xs @ ys = zs)"
   by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
 
 lemmas lexordp_def = 
   lexordp_def [unfolded lexord_def mem_Collect_eq split]
 (*>*)
 
 section \<open>Inductive Predicates \label{sec:inductive}\<close>
 
 text \<open>
   The \<open>predicate compiler\<close> is an extension of the code generator
   which turns inductive specifications into equational ones, from
   which in turn executable code can be generated.  The mechanisms of
   this compiler are described in detail in
   @{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}.
 
   Consider the simple predicate \<^const>\<open>append\<close> given by these two
   introduction rules:
 \<close>
 
 text %quote \<open>
   @{thm append.intros(1)[of ys]} \\
   @{thm append.intros(2)[of xs ys zs x]}
 \<close>
 
 text \<open>
   \noindent To invoke the compiler, simply use @{command_def "code_pred"}:
 \<close>
 
 code_pred %quote append .
 
 text \<open>
   \noindent The @{command "code_pred"} command takes the name of the
   inductive predicate and then you put a period to discharge a trivial
   correctness proof.  The compiler infers possible modes for the
   predicate and produces the derived code equations.  Modes annotate
   which (parts of the) arguments are to be taken as input, and which
   output. Modes are similar to types, but use the notation \<open>i\<close>
   for input and \<open>o\<close> for output.
  
   For \<^term>\<open>append\<close>, the compiler can infer the following modes:
   \begin{itemize}
     \item \<open>i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool\<close>
     \item \<open>i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool\<close>
     \item \<open>o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool\<close>
   \end{itemize}
   You can compute sets of predicates using @{command_def "values"}:
 \<close>
 
 values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
 
 text \<open>\noindent outputs \<open>{[1, 2, 3, 4, 5]}\<close>, and\<close>
 
 values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
 
 text \<open>\noindent outputs \<open>{([], [2, 3]), ([2], [3]), ([2, 3], [])}\<close>.\<close>
 
 text \<open>
   \noindent If you are only interested in the first elements of the
   set comprehension (with respect to a depth-first search on the
   introduction rules), you can pass an argument to @{command "values"}
   to specify the number of elements you want:
 \<close>
 
 values %quote 1 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
 values %quote 3 "{(xs, ys). append xs ys [(1::nat), 2, 3, 4]}"
 
 text \<open>
   \noindent The @{command "values"} command can only compute set
   comprehensions for which a mode has been inferred.
 
   The code equations for a predicate are made available as theorems with
   the suffix \<open>equation\<close>, and can be inspected with:
 \<close>
 
 thm %quote append.equation
 
 text \<open>
   \noindent More advanced options are described in the following subsections.
 \<close>
 
 subsection \<open>Alternative names for functions\<close>
 
 text \<open>
   By default, the functions generated from a predicate are named after
   the predicate with the mode mangled into the name (e.g., \<open>append_i_i_o\<close>).  You can specify your own names as follows:
 \<close>
 
 code_pred %quote (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as concat,
   o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as split,
   i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix) append .
 
 subsection \<open>Alternative introduction rules\<close>
 
 text \<open>
   Sometimes the introduction rules of an predicate are not executable
   because they contain non-executable constants or specific modes
   could not be inferred.  It is also possible that the introduction
   rules yield a function that loops forever due to the execution in a
   depth-first search manner.  Therefore, you can declare alternative
   introduction rules for predicates with the attribute @{attribute
   "code_pred_intro"}.  For example, the transitive closure is defined
   by:
 \<close>
 
 text %quote \<open>
   @{lemma [source] "r a b \<Longrightarrow> tranclp r a b" by (fact tranclp.intros(1))}\\
   @{lemma [source] "tranclp r a b \<Longrightarrow> r b c \<Longrightarrow> tranclp r a c" by (fact tranclp.intros(2))}
 \<close>
 
 text \<open>
   \noindent These rules do not suit well for executing the transitive
   closure with the mode \<open>(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool\<close>, as
   the second rule will cause an infinite loop in the recursive call.
   This can be avoided using the following alternative rules which are
   declared to the predicate compiler by the attribute @{attribute
   "code_pred_intro"}:
 \<close>
 
 lemma %quote [code_pred_intro]:
   "r a b \<Longrightarrow> tranclp r a b"
   "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
 by auto
 
 text \<open>
   \noindent After declaring all alternative rules for the transitive
   closure, you invoke @{command "code_pred"} as usual.  As you have
   declared alternative rules for the predicate, you are urged to prove
   that these introduction rules are complete, i.e., that you can
   derive an elimination rule for the alternative rules:
 \<close>
 
 code_pred %quote tranclp
 proof -
   case tranclp
   from this converse_tranclpE [OF tranclp.prems] show thesis by metis
 qed
 
 text \<open>
   \noindent Alternative rules can also be used for constants that have
   not been defined inductively. For example, the lexicographic order
   which is defined as:
 \<close>
 
 text %quote \<open>
   @{thm [display] lexordp_def [of r]}
 \<close>
 
 text \<open>
   \noindent To make it executable, you can derive the following two
   rules and prove the elimination rule:
 \<close>
 
 lemma %quote [code_pred_intro]:
   "append xs (a # v) ys \<Longrightarrow> lexordp r xs ys"
 (*<*)unfolding lexordp_def by (auto simp add: append)(*>*)
 
 lemma %quote [code_pred_intro]:
-  "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b
+  "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r a b \<Longrightarrow> a\<noteq>b 
   \<Longrightarrow> lexordp r xs ys"
 (*<*)unfolding lexordp_def append apply simp
 apply (rule disjI2) by auto(*>*)
 
 code_pred %quote lexordp
 (*<*)proof -
   fix r xs ys
   assume lexord: "lexordp r xs ys"
   assume 1: "\<And>r' xs' ys' a v. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
     \<Longrightarrow> append xs' (a # v) ys' \<Longrightarrow> thesis"
   assume 2: "\<And>r' xs' ys' u a v b w. r = r' \<Longrightarrow> xs = xs' \<Longrightarrow> ys = ys'
-    \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> thesis"
+    \<Longrightarrow> append u (a # v) xs' \<Longrightarrow> append u (b # w) ys' \<Longrightarrow> r' a b \<Longrightarrow> a\<noteq>b \<Longrightarrow> thesis"
   {
     assume "\<exists>a v. ys = xs @ a # v"
     from this 1 have thesis
         by (fastforce simp add: append)
   } moreover
   {
-    assume "\<exists>u a b v w. r a b \<and> xs = u @ a # v \<and> ys = u @ b # w"
+    assume "\<exists>u a b v w. r a b \<and> a\<noteq>b \<and> xs = u @ a # v \<and> ys = u @ b # w"
     from this 2 have thesis by (fastforce simp add: append)
   } moreover
   note lexord
   ultimately show thesis
     unfolding lexordp_def
     by fastforce
 qed(*>*)
 
 
 subsection \<open>Options for values\<close>
 
 text \<open>
   In the presence of higher-order predicates, multiple modes for some
   predicate could be inferred that are not disambiguated by the
   pattern of the set comprehension.  To disambiguate the modes for the
   arguments of a predicate, you can state the modes explicitly in the
   @{command "values"} command.  Consider the simple predicate \<^term>\<open>succ\<close>:
 \<close>
 
 inductive %quote succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   "succ 0 (Suc 0)"
 | "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
 
 code_pred %quote succ .
 
 text \<open>
   \noindent For this, the predicate compiler can infer modes \<open>o
   \<Rightarrow> o \<Rightarrow> bool\<close>, \<open>i \<Rightarrow> o \<Rightarrow> bool\<close>, \<open>o \<Rightarrow> i \<Rightarrow> bool\<close> and
   \<open>i \<Rightarrow> i \<Rightarrow> bool\<close>.  The invocation of @{command "values"}
   \<open>{n. tranclp succ 10 n}\<close> loops, as multiple modes for the
   predicate \<open>succ\<close> are possible and here the first mode \<open>o \<Rightarrow> o \<Rightarrow> bool\<close> is chosen. To choose another mode for the argument,
   you can declare the mode for the argument between the @{command
   "values"} and the number of elements.
 \<close>
 
 values %quote [mode: i \<Rightarrow> o \<Rightarrow> bool] 1 "{n. tranclp succ 10 n}" (*FIXME does not terminate for n\<ge>1*)
 values %quote [mode: o \<Rightarrow> i \<Rightarrow> bool] 1 "{n. tranclp succ n 10}"
 
 
 subsection \<open>Embedding into functional code within Isabelle/HOL\<close>
 
 text \<open>
   To embed the computation of an inductive predicate into functions
   that are defined in Isabelle/HOL, you have a number of options:
 
   \begin{itemize}
 
   \item You want to use the first-order predicate with the mode
     where all arguments are input. Then you can use the predicate directly, e.g.
 
     @{text [display]
 \<open>valid_suffix ys zs =
   (if append [Suc 0, 2] ys zs then Some ys else None)\<close>}
 
   \item If you know that the execution returns only one value (it is
     deterministic), then you can use the combinator \<^term>\<open>Predicate.the\<close>, e.g., a functional concatenation of lists is
     defined with
 
     @{term [display] "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
 
     Note that if the evaluation does not return a unique value, it
     raises a run-time error \<^term>\<open>not_unique\<close>.
 
   \end{itemize}
 \<close>
 
 
 subsection \<open>Further Examples\<close>
 
 text \<open>
   Further examples for compiling inductive predicates can be found in
   \<^file>\<open>~~/src/HOL/Predicate_Compile_Examples/Examples.thy\<close>.  There are
   also some examples in the Archive of Formal Proofs, notably in the
   \<open>POPLmark-deBruijn\<close> and the \<open>FeatherweightJava\<close>
   sessions.
 \<close>
 
 end
 
diff --git a/src/HOL/MicroJava/DFA/Kildall.thy b/src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy
+++ b/src/HOL/MicroJava/DFA/Kildall.thy
@@ -1,485 +1,489 @@
 (*  Title:      HOL/MicroJava/DFA/Kildall.thy
     Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
 *)
 
 section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>
 
 theory Kildall
 imports SemilatAlg "HOL-Library.While_Combinator"
 begin
 
 primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" where
   "propa f []      ss w = (ss,w)"
 | "propa f (q'#qs) ss w = (let (q,t) = q';
                                u = t +_f ss!q;
                                w' = (if u = ss!q then w else insert q w)
                            in propa f qs (ss[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 ss w == while (%(ss,w). w \<noteq> {})
        (%(ss,w). let p = SOME p. p \<in> w
                  in propa f (step p (ss!p)) ss (w-{p}))
        (ss,w)"
 
 definition unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set" where
 "unstables r step ss == {p. p < size ss \<and> \<not>stable r step ss p}"
 
 definition kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list" where
 "kildall r f step ss == fst(iter f step ss (unstables r step ss))"
 
 primrec merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list" where
   "merges f []      ss = ss"
 | "merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!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] ++_f 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'"
   from this [OF _ _ ps'] have IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" .
 
   from ss ab
   have "ss[a := b +_f ss!a] \<in> list n A" by (simp add: closedD)
   moreover
   from calculation l
   have "p < length (ss[a := b +_f ss!a])" by simp
   ultimately
   have "?P (ss[a := b +_f ss!a]) ps'" by (rule IH)
   with p' l
   show "?P ss (p'#ps')" by simp
 qed
 
 
 (** merges **)
 
 lemma length_merges [simp]: "size(merges f ps ss) = size ss"
   by (induct ps arbitrary: ss) 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_tac 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 <=[r] merges f ps xs"
 apply (induct_tac 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 <=[r] 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 <=_r 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 +_f xs!p] <=[r] xs")
      apply (drule_tac p = p in le_listD)
       apply simp
      apply simp
     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 <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>  
    x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys"
   apply(insert semilat)
   apply (unfold 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 <= A" and "set ss <= A"
     and "\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts" and "ss <=[r] ts"
   shows "merges f ps ss <=[r] ts"
 proof -
   { fix t ts ps
     have
     "\<And>qs. \<lbrakk>set ts <= A; \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p< size ts \<rbrakk> \<Longrightarrow>
     set qs <= set ps  \<longrightarrow> 
     (\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)"
     apply (induct_tac qs)
      apply simp
     apply (simp (no_asm_simp))
     apply clarify
     apply (rotate_tac -2)
     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 +_f ss!q \<noteq> ss!q} Un 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' +_f 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' \<in> 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)
     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 <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
   \<Longrightarrow> merges f (step p (ss!p)) ss <=[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: "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 <[r] merges f qs ss \<or> 
   merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w" (is "PROP ?P")
 proof -
   interpret Semilat A r f using assms by (rule Semilat.intro)
   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 +_f ss ! q \<noteq> ss ! q)")
     apply (blast elim: equalityE)
     apply clarsimp
     apply (drule bspec, assumption) 
     apply (drule bspec, assumption)
     apply clarsimp
     done
 qed
 
+(*for lex*)
+lemma ne_lesssub_iff [simp]: "y\<noteq>x \<and> x <[r] y \<longleftrightarrow> x <[r] y"
+  by (meson lesssub_def)
+
 lemma iter_properties[rule_format]:
   assumes semilat: "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 <=[r] ss' \<and>
    (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
   (is "PROP ?P")
 proof -
   interpret Semilat A r f using assms by (rule Semilat.intro)
   show "PROP ?P" apply(insert semilat)
 apply (unfold iter_def stables_def)
 apply (rule_tac P = "%(ss,w).
  ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
  (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss <=[r] ts) \<and>
  (\<forall>p\<in>w. p < n)" and
  r = "{(ss',ss) . ss <[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 simp
  apply simp
 apply (subst decomp_propa)
  apply fast
 apply simp
 apply (rule conjI)
  apply (rule merges_preserves_type)
  apply blast
  apply clarify
  apply (rule conjI)
   apply(clarsimp, fast 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 add: acc_def lesssub_def wfP_wf_eq [symmetric])
 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 assumption+
 defer
 apply assumption
 apply clarsimp
 done
 
 qed
 
 lemma kildall_properties:
 assumes semilat: "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 <=[r] kildall r f step ss0 \<and>
   (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow>
                  kildall r f step ss0 <=[r] ts)"
   (is "PROP ?P")
 proof -
   interpret Semilat A r f using assms by (rule Semilat.intro)
   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)
-done
+    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)
+    done
 qed
 
 lemma is_bcv_kildall:
 assumes semilat: "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 using assms by (rule Semilat.intro)
   show "PROP ?P"
 apply(unfold is_bcv_def wt_step_def)
 apply(insert semilat kildall_properties[of A])
 apply(simp add:stables_def)
 apply clarify
 apply(subgoal_tac "kildall r f step ss \<in> list n A")
  prefer 2 apply (simp(no_asm_simp))
 apply (rule iffI)
  apply (rule_tac x = "kildall r f step ss" in bexI) 
   apply (rule conjI)
    apply (blast)
   apply (simp  (no_asm_simp))
  apply(assumption)
 apply clarify
 apply(subgoal_tac "kildall r f step ss!p <=_r ts!p")
  apply simp
 apply (blast intro!: le_listD less_lengthI)
 done
 qed
 
 end